[Iris-Club] Using Iris

[Ralf Jung]

Hi,

>     Yes, if we have a triple for the continuation, we can just use that same
>     postcondition.  We could likely have done the same thing in lambdaRust, but that
>     would be one more parameter to carry around.  I think that would amount to
>     making `cont_postcondition` a parameter here [1] and here [2].
> 
> This makes sense, simplicity is a fine motivation for using True. I would be
> willing to bet that if you globally replaced True with False, everything would
> still work out (parametricity by sed!).

I know for a fact that this is true because we started with `False`.
Well, true with one exception: The final soundness proof that "closes" the type
system uses `\ x. ()` as the final continuation, and has to prove it satisfies a
triple with the `cont_postcondition`.  That's the one place where we need `True`.

>     On our case, that is exactly the problem. If halt halts the machine, it cannot
>     have post-condition false. I guess we could define the operational semantics of
>     halt to be "infinite loop", and then indeed postcondition false would work, but
>     that didn't seem like a nice choice to us. So instead "halt" is just "()" [3] --
>     unit, a term that is immediately done computing, and we use postcondition true.
> 
> I think this is because usually "the machine is off" is not a state of the
> system. If you wanted to add a true "off" state to the system, then (I think)
> things would work out pretty easily. Simply interpret your predicates as "state
> = on -> P". Since "state = off" has no transitions (or the identity transition,
> however is more convenient to define it) the invariant is trivially preserved by
> its steps.

Ah, that is an interesting approach.  In our case we re-used the same definition
of WP and Hoare triples as "normal" (non-CPS) languages, so we likely wouldn't
want to derive all the WP laws for this tweaked WP that incorporates an "off" state.

I could imagine a slightly different take on this though (that also feels more
"Irisy" to me): Say we add that state, and we also add a new separation logic
assertion you can make about the state saying that it is off. (This would be
duplicable because once off, it is off forever.) Then we could make the
postcondition of the `halt` continuation say "the machine is off", and also use
that as the universal postcondition everywhere. This would only require very
local changes to LambdaRust.
I should probably write this down in case we want to change our story there.^^
It seems slightly annoying to have to say in every reduction step that also the
global "has the machine halted" flag is not set yet, but that's a one-time pain
so it's probably not too bad.  (This would likely be easier with a different
setup, but the shared Iris definition of WP assumes that there is a pool of
threads which all carry some per-thread state [for us, that's the expression,
the code still to be run there -- because we are using substitution, there are
no environments] and then some global state [the heap, usually].  Halting is a
clearly a cross-thread concern, but we only define a per-thread reduction which
is the automatically lifted to a thread pool.  So we would add a flag in the
global state to reflect whether the machine has halted, and not allow any
further per-thread reductions after that happened.  We could of course also
decide not to use the shared WP, define our own, and still benefit from most of
the Iris machinery [the proof mode and invariants and all that would still just
work], but we usually try to avoid that.)

> There are three reasons that I like False, though they are matters of taste:
> 
> 1. The reason that False makes sense to me is that callers of a function with a
> False post-condition do not need to specify what happens after the function
> returns, because they know that False it provable if the function returns so
> they can simply eliminate that proof. Consider `WP (if (x == 0) { halt(); } else
> { return 0; }) { \ ret => ret = 0 }`. This program will never fail to execute,
> so one could argue that the weakest pre-condition should be True, but if halt
> has post-condition True, then the weakest precondition is actually `x <> 0`.

That still looks like a somewhat different setup than ours -- the postcondition
is *always* `True` for us, and `return` would actually be a continuation (a
lambda term, because we are just encoding this in lambda calculus) that you call
and that has *precondition* "input is 0".  So if you translate your example to
our setting, you do get the uniformity you are looking for.

> 2. Another argument for this could be that the globalized program invariant
> implies some safety condition trivially. Suppose, for example, I have a program
> such as: { x <> 0 } diverge(); { True }
> If I expand this out into a "whole system" invariant, I would get something like
> "(pc = 0 -> x <> 0) /\ (pc = 1 -> True)" (assuming appropriate pc variables).
> Simply looking at this assertion, I don't know that `x <> 0`. In order to prove
> that `x <> 0` is an invariant of my system, then I need to know that `pc = 1 ->
> False` which I haven't proven.

Hm, I have a hard time translating this to Iris where we usually handle
invariants differently.

> 3. `forall x, WP x False |-- WP x True` but not vice versa. If both are
> provable, then why not prove something stronger? :-)

I got nothing to add to that. ;)

>     I agree that makes a lot of sense. I am just wondering, how do you model this
>     "halt" instruction in your operational semantics?
> 
> See above. If you wanted to do this at the OS level, then your False would be
> scoped over the program's memory and things would work similarly. If this
> program is running, then the invariant holds, if the program is not running, you
> can't start running it (without re-initializing it). 

I am slightly puzzled by your use of the term "invariant" here (and in some
places above).  We were talking about "halt" and postconditions, not about
anything I would call "invariant", so I suspect our terminology is not entirely
aligned.  We have a specific mechanism in Iris for sharing ownership across
threads, by establishing an invariant on a piece of state and then sharing
knowledge of that invariant with anyone else.  That's not what you refer to, I
think, but then I don't know which is "the invariant" that holds.

Kind regards,
Ralf