prophecy variables

[tjhance]

I recently mentioned prophecy variables in this discussion here but glossed over their implementation. There are some subtleties involved, and I also want to get some thoughts down about prophecy variables as a feature in their own right, outside the context of mutable references.

This is not even close to a complete proposal, and there are a bunch of open questions towards the end, both technical and design-wise.

As usual, iris has a bunch of prior work here to form a foundation for our approach.

• "The Future is Ours" paper paper implements prophecy variables in separation logic. This has a fairly clean formalism, with "ghost code" that creates and resolves prophecy variables, and propositions that express ownership of the ability to resolve a prophecy variable (this prevents the user from resolving a variable more than once). The paper is mostly focused on applications. Notably, it covers future-dependent linearization points, which is something we care about.
• RustHornBelt introduces a different prophecy mechanism in order to prove correctness of the mutable-variable-prophecy-encoding. They had to introduce a new mechanism, rather than using the first one, for some technical reasons. This paper is mostly focused on the proof-of-soundness of a higher-level encoding.

Motivations and examples

A prophecy variable API

To support prophecy variables, we can consider a trusted ghost "prophecy object" that
provides some prophecied value, and provides the user a way to "resolve" the prophecy.

tracked struct Prophecy<T> { ... }

impl<T> Prophecy<T> {
    spec fn value() -> T;

    proof fn new() -> (tracked s: Self)
        ensures !s.has_resolved()

    proof fn resolve(tracked self, value: T)
        requires !self.has_resolved(),
        ensures self.has_resolved(), self.value() == value,
}

When the user "resolves" the prophecy, they can set the value to whatever they want. They can only do this once: after they resolve it, the prophecy object is set to has_resolved() == true. However, the user has access to self.value() even before they call resolve(). This is what makes it a prophecy.

Motivating example: the "lazy coin toss" API

This is an example from the Future is Ours paper that I'm going to translate into Verus. Suppose you want to implement the following coin toss API.

struct Coin { ... }
enum CoinFace { Heads, Tails }

impl Coin {
    spec fn result() -> CoinFace;

    fn new() -> Self;
    fn get_value(&mut self) -> (res: CoinFace)
        ensures res == self.result(),
            self.result() == old(self).result()
}

The idea is that, for each constructed Coin object, the "coin" is flipped once, and get_value should return the result of the coin toss (so if you call it more than once, it returns the same coin toss value - for the same Coin object, it always looks at a single toss). The simplest implementation is "eager": have new call an RNG and get the coin toss, store it internally, and just have get_value return the stored value.

However, in the "lazy coin toss" problem, we want to defer the coin toss until the first get_value() call, so the implementation looks like this:

struct Coin { res: Option<CoinFace> }

impl Coin {
    fn new() -> Self {
        Coin { res: None }
    }

    fn get_value(&mut self) {
        // Lazily evaluate the coin flip if it hasn't been evaluated yet
        if self.res.is_none() {
            self.res = Some(rng_coin_flip());
        }
        self.res.unwrap()
    }
}

From the client's perspective, this implementation is the same as the eager-evaluation that calls rng_coin_flip() during new(). After all, the client simply observes that get_value() gives a consistent result each time.

But with this implementation, we face an obvious problem: how would we implement the spec fn result() -> CoinFace? Until the first time get_value is called, there is no way to determine what the value of the rng will be.

To solve this, we can use the prophecy API:

struct Coin {
    res: Option<CoinFace>
    tracked proph: Prophecy<CoinFace>
}

impl Coin {
    fn new() -> Self {
        Coin {
            res: None,
            proph: Prophecy::<CoinFace>::new(),
        }
    }

    spec fn well_formed(&self) {
        match self.res {
            None => { !self.proph.has_resolved() },
            Some(x) => { self.proph.value() == x },
        }
    }

    spec fn result() -> CoinFace {
        self.proph.value()
    }

    fn get_value(&mut self) {
        // Lazily evaluate the coin flip if it hasn't been evaluated yet
        if self.res.is_none() {
            self.res = Some(rng_coin_flip());
            self.proph.resolve(self.res.unwrap());
        }
        self.res.unwrap()
    }
}

Motivating example: spawn

If you look at how thread spawning works, it's a little complicated: It returns a JoinHandle object is specified via a predicate of all possible values it can return.

Prophecies could potentially make this kind of thing simpler, as the JoinHandle could simply have a prophecy in it that says what value it is ultimately going to return.

Motivating example: future-dependent linearization points

One of the hairy things in the NR development was the future-dependent linearization points. We ended up proving a refinement theorem based on execution traces so that the proof could "look into the future" to see which step to take in the abstract state machine.

There are 2 angles we can take, here:

• Can prophecy variables make the above proof easier? E.g., can we add prophecy variables to the program (or to one of the state machines) to remove the need for a trace-based refinement?
• Can prophecy variables help us soundly instantiate the trace-based refinement theorem in Verus code so that we can verify client programs of NR?

From a practical perspective, I'm most interested in the second right now, since right now it's the biggest obstacle towards verifying clients of NR.

With prophecies, we could declare NR like this:

struct NR {
    tracked trace: Prophecy<NRTrace>,
    // ...
}

If we just have a prophecy of the entire execution trace, then we can know when the linearization points are when we hit them.

Okay, technically this doesn't work because we need to resolve the prophecy one entry at a time, so really we'd have:

struct NR {
    tracked trace: Map<nat, Prophecy<NRTraceEntry>>,
    // ...
}

The point is: now, when we can tell whenever we hit a linearization point, so we can advance the abstract NR state and provide a usable specification for the client.

Soundly implementing prophecy variables

The fundamental difficulty

If you think about prophecy variables for 30 seconds, you'll quickly see there's a problem:

proof fn grandfather_paradox() {
    let tracked proph = Prophecy::<bool>::new();

    let luigi = proph.value();    // (1)
    let waluigi = !luigi;

    proph.resolve(waluigi);       // (2)

    assert(luigi == proph.value());     // By line (1)
    assert(waluigi == proph.value());   // By line (2)
    assert(false);
}

Basically, if we ever use the result of a prophecy to make a decision regarding the resolution of that prophecy, we can easily create a paradox.

The prior work

• In The Future is Ours paper, there is a distinction between "ghost instructions" (ghost instructions in the programming language), and "ghost state" (propositions in the separation logic which are manipulated with the update-modality). Thus, there are multiple levels of "ghostness". The prophecy variables are initialized and resolved in the ghost instructions; thus, they can't be influenced by "ghost state".

  • (This might be confusing if you've only seen the Verus way of ghost state. In Verus, we write everything as ghost code, so everything looks like "ghost instructions" - but we use this ghost state to do things that in Iris you'd do in the separation logic. So keep this in mind when thinking about how to relate separation logic to Verus)

• In the RustHornBelt paper, they define parametric prophecies, where they "parameterize over all possible futures." They represent every prophecy-dependent value as a function ProphAsn -> T, i.e., a function over all possible prophecy assignments. To resolve a value, they just restrict the set of all possible futures, as long as there remains one consistent future. This allows them to resolve prophecy values to value dependent on other (unresolved) prophecy variables. This allows substantially more fine-grained dependency analysis than the above method.

Verus???

Verus has "multiple levels of ghostness" (ghost vs. tracked) but they don't really correspond to the distinction that needs to be made here: the evolution of tracked variables can depend on ghost variables.

Okay, well, on the other hand, tracked and ghost code absolutely can't affect exec code. (It almost seems like they can - the exec value from a PPtr::write operation is given by the ghost PointsTo value. That's true, but the PointsTo value can't be set arbitrarily, it can't be changed without an actual exec operation and it it always has to match the exec value off the heap. So it's really the PointsTo object whose value is determined by the exec code.)

Anyway, it seems to me that we need is another "dimension" to our mode-checking, say prophetic versus not_prophetic.

tracked struct Prophecy<T> { ... }

impl<T> Prophecy<T> {
    spec fn value() -> T;

    proof fn new() -> (#[prophetic] tracked s: Self)
        ensures !s.has_resolved()

    proof fn resolve(tracked self, #[not_prophetic] value: T)
        requires !self.has_resolved(),
        ensures self.has_resolved(), self.value() == value,
}

Now if we tried to do the grandfather paradox:

proof fn grandfather_paradox() {
    #[prophetic] let tracked proph = Prophecy::<bool>::new();

    #[prophetic] let luigi = proph.value();
    #[prophetic] let waluigi = !luigi;

    proph.resolve(waluigi);     // ERROR: `resolve` expects not_prophetic argument, got prophetic

    assert(luigi == proph.value());
    assert(waluigi == proph.value());
    assert(false);
}

This doesn't sound too bad, and we can probably use inference to infer the 'prophetic' labels in most cases. Is it enough, though?

Prophecy-dependencies

The one-dimensional prophetic/not_prophetic label would never allow us to resolve one prophecy variable to a value dependent on another (unresolved) value. RustHornBelt illustrated that this capability is necessary to prove the mut-ref encoding. Is it useful for "user" applications? I expect it might be, if we keep pushing in this direction, but I don't have a super-compelling example right now.

The NR example, though, looks kind of complicated. Recall the idea to use a prophetic trace:

struct NR {
    tracked trace: Map<nat, Prophecy<NRTraceEntry>>,
    // ...
}

Since trace is prophetic, the value of the trace has to be determined purely by non-prophetic values. This might be fine? The trace is determined mostly by inputs to the NR data structure, which are probably based on exec-values, which won't be prophetic. But what would happen if the user wanted to use say, CoinToss (from the above example) as a command? That sounds really contrived, but it's just an example.

In the case of NR, it might not matter. The actual future-dependent part only depends on the exact order that threads access the log entries / head / tail pointers. So you could restructure the proof so that this is the only part that gets prophecies ... this breaks the generality of the current "just prove a refinement theorem however you want" approach, but maybe the desired outcome is fundamentally at odds with an arbitrary trace-refinement. (It would be useful to see if we can work out a concrete paradoxical example.)

Here's another thing: trace is prophecy-dependent, and it is also involved in the evolution of the ghost state corresponding to the abstract NR state. Therefore, the output-ghost-state would also be prophecy-dependent (if computed as the result of a naive analysis similar to mode-checking). However, even though the linearization point is future dependent, the output ghost state might not actually depend on when the linearization point happens. So in principle, it could be marked not_prophetic, but might require a really complicated encoding to prove it (e.g., similar to parametric prophecies?)

This part seems really muddy right now, but based on this analysis, it seems like if we "default" to things being prophecy-dependent & carve out small prophecy-independent parts when we need to resolve a prophecy, then it should all work out, at least with NR, though it would require us to restructure the proof slightly to limit the data that actually gets prophesied.