Skip to content

Prophecy variables

Ralf Jung requested to merge ralf/prophecy into master

I propose we merge this work by @amaurremi to implement prophecy variables in Iris. The basic idea is to equip languages with an observation type, such that an observation is made at every program step (the observation is optional, basically building in support for τ transitions). The state that is kept track of by WP (the data passed to the state interpretation) now consists of the machine state and the list of future observations, and when WP takes a step, that step (if it has an attached observation) must conform with the prediction. This works in adequacy because adequacy knows the entire trace from the beginning.

The key new feature this enables in heap_lang are the following two Hoare triples:

Lemma wp_new_proph :
  {{{ True }}} NewProph {{{ (p : proph), RET (LitV (LitProphecy p)); p ⥱ - }}}.

Lemma wp_resolve_proph e1 e2 p v w:
  IntoVal e1 (LitV (LitProphecy p)) →
  IntoVal e2 w →
  {{{ p ⥱ v }}} ResolveProph e1 e2 {{{ RET (LitV LitUnit); ⌜v = Some w⌝ }}}.

NewProph creates a prophecy variable that can later be resolved to a value using ResolveProph. Here, p ⥱ v (notation still up for debate :D ) asserts ownership of a prophecy variable, including the right to resolve; p ⥱ - (as usual) says that the value is existentially quantified. The Haore triples make it so that when you create the prophecy variable, you are already told the value that it will eventually resolve to, and when you resolve the prophecy variable, you get a proof that the prediction made earlier was correct. v in p ⥱ v is an option value because the prediction might be "this variable is never going to be resolved". (This will later be generalized to predicting a list, and allowing a variable to be resolved multiple times, but that still has to be implemented and I think we can land this now.)

In case you are wondering -- yes, we have actual code in our programs for creating and resolving prophecy variables. This is ghost code. As much as I dislike ghost code, I do not know of a way to do prophecy without it.

I did not manage to make prophecy variables work for total-WP in heap_lang, but at least I managed to find a definition for TWP that preserves all the existing lemmas. We are not currently interested in reasoning about termination of programs that perform prophecy.

In terms of examples, this PR includes a simple "coin flip" example that would be impossible to prove without prophecy. We also have the "atomic snapshot" from https://software.imdea.org/fcsl/papers/histories-esop15.pdf, which I propose we include in iris-examples. You can see that code at https://gitlab.mpi-sws.org/amaurremi/iris-coq/blob/marianna/prophecy/theories/heap_lang/lib/atomic_snapshot.v. We are working on more examples, which unfortunately will likely need further changes to heap_lang itself -- but I think it is worth landing this "most pure" form of prophecy now (which is already useful, as these examples show!), and then discuss the ugly changes we also need for more advanced examples later. (Basically, we need a way to perform a CAS and resolve a prophecy in the same physical step.)

Main points for debate are, as usual, notations:

  • p ⥱ v for ownership of a prophecy variable.
  • NewProph as expression to create a new prophecy variable, and resolve_proph: p to: v for resolving it.

Merge request reports