proof variables, soundness & theory

[tjhance]

Writing this after a slack conversation before I forget.

There are a couple of ways to think about #[proof] variables, but given how we used them in LinearDafny and the connections to iris separation logic, we can look at proof computations as effectively serving as a proof that takes place in the "update modality". If we run with this intuition, we come to an interesting conclusion. Basically, if "A update=> B" and B is a "pure predicate" (no ghost state) then we have "A => B" as well.

In Verus terms, this would mean that if we have a function:

#[proof]
#[verifier(returns(spec))]
fn foo(#[proof] a: A) -> S { ... }

then it would be sound to call foo(a) without consuming a. I'll call this the ownership-retaining rule. This is initially somewhat surprising, and it begs the following objection: if foo takes ownership of a, it could make an irrevocable decision on the ghost state; it could then return information about that irrevocable decision. If the caller still has ownership of a, it could make a different irrevocable decision, and then derive a contradiction.

However, this is not actually a contradiction because foo is declared to only return #[spec] data. This data can't encode the results of any irrevocable decision. It turns out, all foo is able to do, externally, is prove facts about the input a: A that were "already true" at the beginning of the function. And in this sense, it's safe to "roll back" the ghost state.

Why would we want to do this? Besides strengthening the theoretical connection, it could be a convenience. In LinearDafny, I frequently had to write ghost methods that would take in an A and return another A with a postcondition that they were equal. (Note also that taking &mut A and &mut B can be stronger than &A and &B - see the Burrow laws - so the latter often wasn't an option.)

Furthermore, this concept could apply in any context where we might want to input proof variables and output only "pure" logical expressions (like a forall block).

Do we have to give up anything to support these rules?
As I said before, the ownership-retaining rule is sound because the #[spec] output with postconditions can't encode information about irrevocable decisions made. Will that always be true? We can conceive situations where it isn't true ... maybe.

Prophecy variables

Prophecy variables have been integrated into sep. logic (see The Future is Ours for example). The idea of a prophecy variable is you have a variable x which you can know the value of in advance of setting it.

One could imagine a function that looks like this:

// strawperson's method to represent prophecy variables
fn resolve(#[spec] x: int, #[proof] token: Token, #[spec] v: int)
ensures x == v

where token represents the exclusive ability to resolve prophecy variable x to a value v of one's choice. This violates our principle above - we consumed the token, and made an irrevocable decision about x, a spec variable. So would it be useful to support something like this?

Well ... no, because this is unsound, even if we ignore all the extra rules in the prior section. This is unsound because we could call resolve(x, token, x + 1) to resolve x to some value that is already known to be not equal to x.

For sound prophecy variables to work, there cannot be causation from "decisions made by the prophecy variable" to the resolution of that prophecy variable. Thus, representing prophecy variables like this is out immediately. If we want to support prophecy variables, they need to exist at a "lower ghost level", between what we currently have as #[proof] and #[exec], i.e., code which is still erased, but which would be treated more like exec code in the framework we have right now. (Again, see the Future is Ours paper, where prophecy resolution is essentially a ghost instruction in their programming language).

Conclusion

My current view is that it makes sense to establish the ownership-retaining rule mentioned at the beginning of the post, for a few reasons.

One, I currently don't see anything we'd be giving up. I suspect that any mechanism we might imagine which lets us encode irrevocable decisions into #[spec] post-conditions would suffer the same time-travel paradox as the naive prophecy variable representation. Chris mentioned an interesting technique about prophecy types, which I definitely don't understand, but I suspect a similar principle would apply.

Furthermore, if we ever do come up with a feature which is inconsistent with the ownership-retaining rule, then that feature would be inconsistent with the principle of viewing #[proof] computations as proofs within the update modality. Since that forms the theoretical basis of everything we've done with ghost linear state up to this point, I'd find that pretty surprising.

I will conclude by saying, though, that we don't need to decide on this urgently or anything, and in fact, something like this should be made slowly and deliberately - since we're doing a more restricted thing right now, which means it's easy to change our mind later (as opposed to the opposite). I am mostly writing this up before I forget it all (and to espouse a bit more about the way I think about the theoretical underpinnings of proof variables).