[Iris-Club] Using Iris
Ralf Jung
jung at mpi-sws.org
Tue Oct 30 18:14:38 CET 2018
Hi Greg,
> These are interesting points. I'm wondering how much this is an artifact of
> heap_lang/lambdaRust rather than the Iris logic. If I were to encode C, a la
> CompCert, then I'd have commands that return in one of 4 ways, normal
> termination, return, break, and continue, would the current formulation of WP be
> good for that? You can always use the continuation pointer encoding (discussed
> below), but in that case it doesn't even need the value in the post-condition,
> though you still need it for doing expressions. Perhaps we could just say that
> commands always return unit?
I think there are many ways you could do this, and I haven't done the work to be
familiar with the trade-offs. I am looking forward to reading Robbert's paper
on that. :D
> Thanks, this is helpful in understanding things, I didn't realize this. I'll
> need to look more at the code to better understand how to connect Iris to
> languages (especially wrt my exploration connecting Iris to C/C++). I did some
> digging into the Language abstractions inside the Iris code base, but didn't get
> a clear enough picture of things.
>
> Is this a matter of saying that we have a predicate over ghost states (P) and a
> relation between ghost states and physical states (R), so we can morally
> construct a predicate over physical states by saying: PP s := exists gs, P gs /\
> R s gs. There's obviously a little bit more going on here from an evolution of
> the system perspective (protocols and the like) but that /might/ just be a
> matter of exposing the existentially quantified ghost state (which you almost
> certainly need to do in the proof).
The iris base logic comes with a notion of "resources" -- "state" if you want to
call it that way. Being a separation logic, these resourced are treated
implicitly, i.e. every assertion "P" is just a predicate over resources,
"P /\ Q" lifts the predicate point-wise, and "P * Q" does what you would expect
from a separation logic.
If we were to compare this with the more traditional terminology you are using,
then these resources are the ghost state: Every Iris assertion says what has to
hold of the ghost state for it to be true. (Though "truth" is really the wrong
notion here, it's about ownership.) But since we build our program logic
*inside* the base logic, we don't think of these assertions as predicates over
some state; we think of them as propositions that can implicitly claim
ownership. In particular, even the adequacy proof of WP does not ever talk
about "ghost state", it is entirely performed inside the Iris base logic (so
resources are implicit), and ultimately defers to the soundness theorem of the
base logic itself.
The definition of WP involves a "state interpretation", which is a predicate
over physical state -- but it is a predicate *in Iris* (PState -> iProp), so
really it is a relation between physical and ghost state because iProp is itself
a predicate (if you choose to unfold the Iris model, which I do not think is the
best way to think about this). The state interpretation is used to connect the
ghost state to the physical state -- one way to think about this is to let the
state interpretation say "that part of the ghost state is owned by us, and it is
equal to the physical state". But it could be anything. The key point is that
because our ghost state is flexible enough to encode all sorts of sharing, we
can entirely define \mapsto and friends in ghost state, and use the state
interpretation to make all of that "mean anything". It's a bit like in
"Fictional Separation Logic" (Jensen, Birkedal), except that *all* separation is
fiction in Iris (and so none is, you could say ;).
I suggest reading the Iris 3 paper
<https://iris-project.org/pdfs/2017-esop-iris3-final.pdf>, it develops a
definition of WP and \mapsto inside the base logic step-by-step; that should
help explain how we set these things up. If you want, I'd also be happy to chat
about this and interactively answer the questions that will likely come up. :)
Kind regards,
Ralf
More information about the Iris-Club
mailing list