[Iris-Club] Using Iris

[Ralf Jung]

Hi Gregory,

> 1. I am interested in using Iris to build a safety case around concurrent
> software. To do this, I need a solid (semi non-technical) explanation for what
> Iris means and what it ensures. This motivated my desire to talk about the
> overall system invariant which I believe is quite easy to present and explain.
> Ideally, I could say that using Iris is just a particular way to state (and
> prove) that a property is an inductive invariant of a system.

So far, we have mostly been using Iris to prove that a particular system is
"safe" from a set of initial states -- meaning that during execution, no thread
will ever be stuck, and if the main thread terminates, it satisfies some
(Coq-level) postcondition.  That is the main adequacy theorem [1].
However, notice that this is just a property of WP, defined *inside* Iris!  Our
WP likely has further properties that one could show, and you can define your
own WP if there is something that our WP is not flexible enough for.
And indeed there is another adequacy theorem [2] that is closer to inductive
properties: If you have a view shift from the state interpretation (used by WP
to tie the real state to some ghost state) to a "pure" (Coq-level) statement
about the state, then you get that that property holds for the state all the
time during execution.  I have not used this adequacy theorem yet myself though.

[1]:
https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/program_logic/adequacy.v#L202
[2]:
https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/program_logic/adequacy.v#L236

> 2. The second thing that I'm wondering about is how I can take properties proven
> in Iris and glue them to properties not proved in Iris. For example, can I use
> Iris to prove that a piece of C code is "equivalent" to some functional
> specification, separately prove something about the functional specification and
> then combine the two into an end-to-end theorem that says that the C code has
> the high-level property? Ideally, this end-to-end theorem would only mention the
> operational semantics of C and the high-level property, but not "leak" the fact
> that the proof was performed using Iris.

You can use Iris to establish a contextual refinement, and then use the usual
laws of contextual refinement to go on "outside" Iris: At that point, Iris is
just a proof technique to obtain a contextual refinement, and indeed does not
"leak" further.  (Just like in "normal" use, Iris is in some sense just a proof
technique to establish safety. In particular, Iris is not in the TCB.)

Two papers that use Iris to establish relational properties are:
https://iris-project.org/pdfs/2017-popl-effects-final.pdf
https://iris-project.org/pdfs/2018-lics-reloc-final.pdf

I hope this helps!
Kind regards,
Ralf