1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55

#![allow(unused_variables)]

use super::prelude::*;

verus! {

/// 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_](https://plv.mpi-sws.org/prophecies/paper.pdf).
/// 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.
pub struct Prophecy<T> {
    v: Ghost<T>,
}

impl<T> Prophecy<T> where T: Structural {
    /// The prophecized value.
    pub closed spec fn view(self) -> T {
        self.v@
    }

    /// Allocate a new prophecy variable.
    #[inline(always)]
    pub exec fn new() -> (result: Self) {
        Prophecy::<T> { v: Ghost(arbitrary()) }
    }

    /// Resolve the prophecy variable to a concrete value.
    /// This consumes `self`, so it can only be called once.
    #[inline(always)]
    #[verifier::external_body]
    pub exec fn resolve(self, v: &T)
        ensures
            self@ == v,
    {
    }
}

} // verus!