vstd/
proph.rs

Help
1#![allow(unused_variables)]
2
3use super::prelude::*;
4
5verus! {
6
7/// A "prophecy variable" that predicts some value of type T.
8///
9/// A prophecy can be allocated by calling [`Prophecy::<T>::new()`] in exec mode.
10/// The result is a prophecy variable whose view is an arbitrary value of type T.
11///
12/// A prophecy can be resolved by calling [`Prophecy::<T>::resolve()`] in exec mode.
13/// This call ensures that the view of the prophecy variable is equal to the value
14/// passed to `resolve()`.  This call (and in particular, its argument v) must be
15/// exec-mode to avoid circular dependency on the value of the prophecy variable.
16/// The value cannot have _any_ "ghost content" (not even via `Ghost`);
17/// hence the `T: Structural` trait bound.
18///
19/// We make an informal soundness argument based on the paper
20/// [_The Future is Ours: Prophecy Variables in Separation Logic_](https://plv.mpi-sws.org/prophecies/paper.pdf).
21/// The argument goes as follows:
22/// For any execution of the program, there is some sequence of calls to `resolve()`,
23/// whose values do not depend on spec- or proof-mode values.  Those values can be
24/// plugged into the arbitrary ghost values chosen by `new()`, for the corresponding
25/// prophecy variables, to justify the proof accompanying the program.  Since both
26/// `new()` and `resolve()` are exec-mode, there is no ambiguity about which `new()`
27/// call corresponds to a particular `resolve()` value.
28pub struct Prophecy<T> {
29    v: Ghost<T>,
30}
31
32impl<T> Prophecy<T> where T: Structural {
33    /// The prophecized value.
34    pub closed spec fn view(self) -> T {
35        self.v@
36    }
37
38    /// Allocate a new prophecy variable.
39    #[inline(always)]
40    pub exec fn new() -> (result: Self) {
41        Prophecy::<T> { v: Ghost(arbitrary()) }
42    }
43
44    /// Resolve the prophecy variable to a concrete value.
45    /// This consumes `self`, so it can only be called once.
46    #[inline(always)]
47    #[verifier::external_body]
48    pub exec fn resolve(self, v: &T)
49        ensures
50            self@ == v,
51    {
52    }
53}
54
55} // verus!
vstd/proph.rs

vstd/
proph.rs
