We generalize the prophecy variable mechanism so that prophecy variables can be resolved several times. A prophecy variable is hence associated to a list of values. This means that several "observations" can be made for a given prophecy variables, but the overall intuition remains the same. The main difference is in the specification of the resolve
operation:
Lemma wp_resolve_proph (p : proph_id) (vs : list val) (v : val) :
{{{ proph p vs }}}
ResolveProph (Val $ LitV $ LitProphecy p) (Val v)
{{{ vs', RET (LitV LitUnit); ⌜vs = v::vs'⌝ ∗ proph p vs' }}}.
Note that resolving p
consumes only the first of the list vs
, and the ownership of proph p vs'
(where vs'
is the tail of vs
) is asserted in the postcondition.
In any case, everything remains very simple, and even simpler than before. The main difference being that we replace an option
by a list
.
@jung do you have anything to add?