[Iris-Club] Two Monoid Questions

[Gregory Malecha]

Thanks, Ralf! This really useful.

I'm probably showing my ignorance and naivity with the following thoughts
but....On the engineering Coq inference point, would it make sense to set
up parameters like?

Definition Auth {A V : Type} (R : A -> V -> Prop) : RA :=

This would allow you to write `Auth R` where `R` is the models relation as
the type. While the type is easy to write, this doesn't really solve the
problem with the constructors. I guess a canonical structure would address
this:

Record AuthS : Type :=
{ a_auth : Type
; a_view : Type
; a_models : a_auth -> a_view -> Prop }. (* subject to the appropriate
constraints.
Definition auth (A : AuthS) (m : A.(a_auth)) : Auth A := (Some m, id).
Definition view (A : AuthS) (m : A.(a_view)) : Auth A := (None, m).

If `m` have appropriate types, then you could probably just write `auth m`
and `view m`, but getting the right annotations might be annoying when
values arise in the middle of your proofs.

A possible alternative would be to embed the models relation into the
authoritative piece (though I don't understand the meta-theory to know if
this would be sound, I'm just using Prop below but it obviously needs to
adhere to a bunch of laws). In this case the relation gets carried around
in the logic but is only ever mentioned in one place. I guess this would
look something like:

Auth(V) :=
  { av : option { t : Type & t * (t -> V -> Prop) } * V
  | match fst av with
    | None => True
    | Some (existT _ (a, M)) => M a (snd av)
    end }.

I guess this simplifies to just making the authoritative piece a predicate
over the view:

Auth(V) :=
   { av : option (V -> Prop) * V
   | match fst av with
     | None => True
     | Some ok => ok (snd av)
     end }.

I imagine that in practice they would both be used in the same way.

On Thu, Aug 1, 2019 at 9:12 AM Ralf Jung <jung at mpi-sws.org> wrote:

> 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/
>


-- 
gregory malecha
gregory at bedrocksystems.com
director of formal methods
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20190801/364c033c/attachment.html>