add support for prophecy variables

[zeldovich]

This design of prophecy variables follows the "Future is ours" paper: both allocation and resolution of a prophecy variable are exec-mode, and the prophecy value is an executable type.

[tjhance]

Unfortunately the mode-restriction doesn't have the intended effect because ghost code can be embedded in exec code:

    fn main()
    {   
        let p = Prophecy::<Ghost<bool>>::alloc();
        p.resolve(Ghost(!p.view().view()));

        assert(false);
    }  

However, we have a not-documented feature that lets you mark spec functions as 'prophetic':

        #[verifier::prophetic]
        pub closed spec fn view(self) -> T { self.v@ }

This adds some additional restrictions that prevent time travel paradoxes. Nobody's actually used the feature until now -- I originally implemented it in preparation for mutable reference support, which is still in-progress. However, it should be usable for standard prophecy variables as well, so I'd be happy to accept the PR if you add #[verifier::prophetic] to the view function.

There's also a discussion page for the feature here, though it's a little dated: #559

[zeldovich]

That's a nice counter-example -- thanks!

I saw the prophetic attribute support, but it seems pretty infectious. In the specific use case of prophecy variables that I wanted to achieve, this would cause every aspect of the specification to become prophetic, and as a result, hard to use higher up in the stack. The Iris-style prophecy variables don't require tracking prophecy propagation in spec/proof, which is more ergonomic in some use cases (including mine).

Is there some type constraint that can require the type T for Prophecy to be purely-exec? As a strawman proposal, how about requiring the type T to be marshallable into bytes and back (with a requires/ensures spec that says it has to be idempotent)?

[zeldovich]

Or even simpler, how about only allowing prophecies for byte slices?

[Chris-Hawblitzel]

We could try T: Structural, using builtin::Structural ( #178, #1255 ) , which guarantees exec equality matches spec equality.

[tjhance]

Interesting idea. I think this should work.

[Chris-Hawblitzel]

We should probably add Travis's counterexample as a test to make sure it fails to verify.

[jaybosamiya-ms]

Minor: when erased, resolve has the same signature as drop; basically, it consumes the value being resolved. It is quite possible that people might just use this primarily with things which are freely Copy, so maybe this is not a major concern, but nonetheless, it might be worth considering:

    pub exec fn resolve(self, v: T) -> (r: T)
        ensures
            self@ == v,
            r == v,
    {
        v
    }

This is just so that the value v remains usable later on if you want to use it for something else.

I will note that this is a mostly backwards-compatible change to the signature (unless someone is depending on it returning a (), users won't notice if a new return is added), so we can punt this until there is someone who really wants to use these prophecy variables with non-Copy types, at which point we can easily add these in.

[jaybosamiya-ms]

Another minor comment: perhaps new is a more Rust-y idiomatic name than alloc?

[Chris-Hawblitzel]

Another minor point: since these are exec no-ops, you might want to mark them with Rust's #[inline(always)] for efficiency.

[zeldovich]

Thanks for the suggestions!

Re: returning value to avoid being like drop(), it seems that Structural means it could be Copy, but I agree it might be a bit annoying, so how about requiring a non-mut ref for resolve()? As in:

    pub exec fn resolve(self, v: &T)
        ensures self@ == v;

[jaybosamiya-ms]

I don't know if Structural always implies Copy. At least this example seems to indicate it doesn't?

verus/source/rust_verify/example/adts.rs

Lines 14 to 18 in 1a2fb58

	#[derive(Structural, PartialEq, Eq)]
	enum Vehicle {
	Car(Car<u64>),
	Train(bool),
	}

I don't have a strong preference on the non-mut-ref vs take-and-return-value approaches; the take-and-return-value has the niceness of not needing & at the callers in the common case, while the non-mut-ref is likely more idiomatic to see in the callee.

Not for this PR, but potential future improvement, we don't currently have a support for std::borrow::Borrow, but that might be a way in the future to have the convenience of not needing the & at the caller (for Copy types), while also having the semantics of the borrow. In that case, going with the non-mut-ref approach is the one that will smoothly switch over.

I'm likely over-thinking this :)

[zeldovich]

In that ADT example, adding Clone, Copy to the #[derive(...)] gives Copy for Vehicle. The base types that are Structural (https://github.com/verus-lang/verus/blob/main/source/builtin/src/lib.rs#L677) are all types that are also Copy. The extra & is slightly odd to me, but I don't have a good internal sense of what's Rust-idiomatic here.