<div dir="ltr"><div dir="ltr">Thanks, Ralf! This really useful.</div><div dir="ltr"><br></div><div>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?</div><div><br></div><div><span style="font-family:courier new,monospace">Definition Auth {A V : Type} (R : A -> V -> Prop) : RA :=</span></div><div><br></div><div>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:</div><div><br></div><div><span style="font-family:courier new,monospace">Record AuthS : Type :=</span></div><div><span style="font-family:courier new,monospace">{ a_auth : Type</span></div><div><span style="font-family:courier new,monospace">; a_view : Type</span></div><div><span style="font-family:courier new,monospace">; a_models : a_auth -> a_view -> Prop }. (* subject to the appropriate constraints.</span></div><div><span style="font-family:courier new,monospace">Definition auth (A : AuthS) (m : A.(a_auth)) : Auth A := (Some m, id).<br></span></div><div><span style="font-family:courier new,monospace">Definition view (A : AuthS) (m : A.(a_view)) : Auth A := (None, m).</span><br></div><div><br></div><div>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.</div><div><br></div><div>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:</div><div><br></div><div><span style="font-family:courier new,monospace">Auth(V) :=</span></div><div><span style="font-family:courier new,monospace"> { av : option { t : Type & t * (t -> V -> Prop) } * V</span></div><div><span style="font-family:courier new,monospace"> | match fst av with</span></div><div><span style="font-family:courier new,monospace"> | None => True</span></div><div><span style="font-family:courier new,monospace"> | Some (existT _ (a, M)) => M a (snd av)</span></div><div><span style="font-family:courier new,monospace"> end }.</span></div><div><span style="font-family:courier new,monospace"><br></span></div><div><span style="font-family:courier new,monospace"><font face="arial,sans-serif">I guess this simplifies to just making the authoritative piece a predicate over the view:</font></span></div><div><span style="font-family:courier new,monospace"><font face="arial,sans-serif"><br></font></span></div><div><span style="font-family:courier new,monospace">Auth(V) :=</span></div><div><span style="font-family:courier new,monospace"> { av : option (V -> Prop) * V</span></div><div><span style="font-family:courier new,monospace"> | match fst av with</span></div><div><span style="font-family:courier new,monospace"> | None => True</span></div><div><span style="font-family:courier new,monospace"> | Some ok => ok (snd av)</span></div><div><span style="font-family:courier new,monospace"> end }.</span></div><div><font face="arial,sans-serif"><br></font></div><div><font face="arial,sans-serif">I imagine that in practice they would both be used in the same way.<br></font></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Aug 1, 2019 at 9:12 AM Ralf Jung <<a href="mailto:jung@mpi-sws.org">jung@mpi-sws.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Gregory,<br>
<br>
> I thought that I had an intuition about the authoritative monoid construction<br>
> and someone recently pointed out that I am using a slightly different definition<br>
> and I'm wondering if they are roughly equivalent.<br>
> <br>
> My fuzzy intuition was that I the type of the authoritative state could be<br>
> different than the type of the RA in the view and the compatibility relation<br>
> (which is equality in the paper) could be a generic "models" relation <a href="http://a.la" rel="noreferrer" target="_blank">a.la</a><br>
> the usual separation logic soundness definition. Semi-formally:<br>
> <br>
> Auth(A, R, |=) :=<br>
> { v : option A * R | match fst v with<br>
> | Some a => exists f, a |= snd v * f (* using<br>
> * to mean join *)<br>
> | None => True<br>
> end }.<br>
> <br>
> This seems like it could be encoded via an extra invariant tying my A to an R<br>
> and placing the |= relation inside that invariant.<br>
<br>
I love this view! This basically says that "auth" *is* the "Views Framework",<br>
embedded as an RA into Iris. This means we went full circle, because in some<br>
sense one can see Iris as being a generalization of Views.<br>
<br>
I think this is my new favorite way to explain auth. ;) Good that I did not<br>
write that part of my PhD thesis yet. :D<br>
<br>
So, yes, basically what we have in Iris and ship with the Coq library is the<br>
special case of your definition where the relation between the composition of<br>
all the "local views" and the "global view" (the relation you wrote "|=") is<br>
equality.<br>
<br>
We have a long-standing [open<br>
PR](<a href="https://gitlab.mpi-sws.org/iris/iris/merge_requests/91" rel="noreferrer" target="_blank">https://gitlab.mpi-sws.org/iris/iris/merge_requests/91</a>) about adding a<br>
specific other instance of the auth pattern, and one reason that did not make<br>
progress is that it seemed awfully ad-hoc. A more general auth like you<br>
suggested would handle this use-case and many more. It also helps with the<br>
friction we sometimes experience where we want to have a fraction on the "R"<br>
side of things, but then we also get fractions on the "A" side which is annoying<br>
because they are all 1 always anyway.<br>
<br>
The only annoying part for engineering this will be that Coq is very bad at<br>
inferring things like "the relation between these two types that you have been<br>
using". But other than that, I think I want to update our auth in Iris to be<br>
like this. ;)<br>
<br>
> A second, slightly related, question. What is best to read to understand why<br>
> join (in CMRA) is a function and not a deterministic relation? Is it necessary<br>
> to the construction? Or is it for convenience?<br>
<br>
Even just writing down things like associativity becomes so annoying with a<br>
relation (when you do everything fully formal like we have to in Coq) that we<br>
went with the functional version. There's probably a translation from the<br>
relational to the functional one at least if you assume enough classical axioms.<br>
<br>
Being able to say things like<br>
<br>
own (a . b) <-> own a * own b<br>
<br>
is just extremely useful, and with a relation that all becomes much more<br>
annoying to state and even more annoying to actually use those lemmas.<br>
<br>
Kind regards,<br>
Ralf<br>
<br>
-- <br>
Website: <a href="https://people.mpi-sws.org/~jung/" rel="noreferrer" target="_blank">https://people.mpi-sws.org/~jung/</a><br>
</blockquote></div><br clear="all"><br>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>gregory malecha</div><div><a href="mailto:gregory@bedrocksystems.com" target="_blank">gregory@bedrocksystems.com</a></div><div><span>director of formal methods</span></div></div></div></div></div></div>