[Iris-Club] Two Monoid Questions

[Ralf Jung]

Hi Gregory,

> I thought that I had an intuition about the authoritative monoid construction
> and someone recently pointed out that I am using a slightly different definition
> and I'm wondering if they are roughly equivalent.
> 
> My fuzzy intuition was that I the type of the authoritative state could be
> different than the type of the RA in the view and the compatibility relation
> (which is equality in the paper) could be a generic "models" relation a.la
> the usual separation logic soundness definition. Semi-formally:
> 
> Auth(A, R, |=) :=
>   { v : option A * R | match fst v with
>                                    | Some a => exists f, a |= snd v * f (* using
> * to mean join *)
>                                    | None => True
>                                   end }.
> 
> This seems like it could be encoded via an extra invariant tying my A to an R
> and placing the |= relation inside that invariant.

I love this view!  This basically says that "auth" *is* the "Views Framework",
embedded as an RA into Iris.  This means we went full circle, because in some
sense one can see Iris as being a generalization of Views.

I think this is my new favorite way to explain auth. ;)  Good that I did not
write that part of my PhD thesis yet. :D

So, yes, basically what we have in Iris and ship with the Coq library is the
special case of your definition where the relation between the composition of
all the "local views" and the "global view" (the relation you wrote "|=") is
equality.

We have a long-standing [open
PR](https://gitlab.mpi-sws.org/iris/iris/merge_requests/91) about adding a
specific other instance of the auth pattern, and one reason that did not make
progress is that it seemed awfully ad-hoc.  A more general auth like you
suggested would handle this use-case and many more.  It also helps with the
friction we sometimes experience where we want to have a fraction on the "R"
side of things, but then we also get fractions on the "A" side which is annoying
because they are all 1 always anyway.

The only annoying part for engineering this will be that Coq is very bad at
inferring things like "the relation between these two types that you have been
using". But other than that, I think I want to update our auth in Iris to be
like this. ;)

> A second, slightly related, question. What is best to read to understand why
> join (in CMRA) is a function and not a deterministic relation? Is it necessary
> to the construction? Or is it for convenience?

Even just writing down things like associativity becomes so annoying with a
relation (when you do everything fully formal like we have to in Coq) that we
went with the functional version.   There's probably a translation from the
relational to the functional one at least if you assume enough classical axioms.

Being able to say things like

  own (a . b) <-> own a * own b

is just extremely useful, and with a relation that all becomes much more
annoying to state and even more annoying to actually use those lemmas.

Kind regards,
Ralf

-- 
Website: https://people.mpi-sws.org/~jung/