pub struct Prophecy<T> { /* private fields */ }Expand description
A “prophecy variable” that predicts some value of type T.
A prophecy can be allocated by calling Prophecy::<T>::new() in exec mode.
The result is a prophecy variable whose view is an arbitrary value of type T.
A prophecy can be resolved by calling Prophecy::<T>::resolve() in exec mode.
This call ensures that the view of the prophecy variable is equal to the value
passed to resolve(). This call (and in particular, its argument v) must be
exec-mode to avoid circular dependency on the value of the prophecy variable.
The value cannot have any “ghost content” (not even via Ghost);
hence the T: Structural trait bound.
We make an informal soundness argument based on the paper
The Future is Ours: Prophecy Variables in Separation Logic.
The argument goes as follows:
For any execution of the program, there is some sequence of calls to resolve(),
whose values do not depend on spec- or proof-mode values. Those values can be
plugged into the arbitrary ghost values chosen by new(), for the corresponding
prophecy variables, to justify the proof accompanying the program. Since both
new() and resolve() are exec-mode, there is no ambiguity about which new()
call corresponds to a particular resolve() value.