Proof closures

[Chris-Hawblitzel]

Verus already supports exec-mode closures (Fn, FnMut, FnOnce) and spec-mode closures (spec_fn), so it makes sense to also support proof-mode closures. Since Verus treats proof-mode functions very similarly to exec-mode functions, I would expect that proof-mode closures would be very similar to exec-mode closures.

As far as I know, this feature is currently missing simply because nobody has gotten around to implementing it yet. Currently, the workaround is to use a trait instead.

[tjhance]

This would be useful implementing a verified Rc with T as covariant instead of invariant.

[Chris-Hawblitzel]

I think I have some time to work on this now. Here's a sketch of a design and implementation.

Design

Mostly, the design borrows from what's already in place for spec mode:

• type spec_fn(t1, ..., tn) -> t0
• ghost-code closure expression |x1: t1, ..., xn: tn| [-> t0] body
• ghost-code call (expr_fun)(expr_1, ..., expr_n)

and what's already in place for exec mode:

• trait Fn(t1, ..., tn) -> t0
• trait FnMut(t1, ..., tn) -> t0
• trait FnOnce(t1, ..., tn) -> t0
• exec-code closure expression |x1: t1, ..., xn: tn| [-> t0] body
• exec-code call (expr_fun)(expr_1, ..., expr_n)

I propose the following user interface design for proof closures:

• type proof_fn([tracked_1] t1, ..., [tracked_n] tn) -> [tracked_0] t0
• type proof_fn_mut([tracked_1] t1, ..., [tracked_n] tn) -> [tracked_0] t0
• type proof_fn_once([tracked_1] t1, ..., [tracked_n] tn) -> [tracked_0] t0
• proof-code closure expressions:
  • proof_fn|[tracked_1] x1: t1, ..., [tracked_n] xn: tn| [-> [tracked_0] t0] body
  • proof_fn_mut|[tracked_1] x1: t1, ..., [tracked_n] xn: tn| [-> [tracked_0] t0] body
  • proof_fn_once|[tracked_1] x1: t1, ..., [tracked_n] xn: tn| [-> [tracked_0] t0] body
• ghost-code call (expr_fun)(expr_1, ..., expr_n)

For example:

let tracked f = proof_fn|i: int, tracked s: S| { g(i, s) }
let tracked g: proof_fn(int, tracked S) -> int = f;
let result = g(10, s);

I think types like proof_fn will convenient, particularly for the type-theory-inspired scenarios that motivate supporting proof closures in the first place. An alternative would be to use traits (e.g. a ProofFn trait), similar to how exec closures work via traits, and to use dyn to convert the traits into types. However, dyn brings implementation-related baggage related to vtables and object safety (Clone, for example, is not object safe / dyn-compatible).

Implementation

Mostly, the implementation borrows from what's already implemented for spec mode and exec mode:

In the implementation, there's currently a struct FnSpec<Args, Output> for the spec_fn type. Corresponding to this, I propose adding a struct FnProof<Usage, Modes, Mode, Args, Output>. Here, Usage is a type argument that represents Once, Mut, or many for fn_proof_once, fn_proof_mut, or fn_proof. The Modes type argument is a tuple, with the same arity as Args, that records which arguments are marked tracked and which are default ghost (spec) arguments. Similarly, Mode records the return value mode.

Currently, there are Fn, FnMut, and FnOnce impls for FnSpec. Likewise, there would be a Fn, FnMut, and FnOnce impls for FnProof, depending on the Usage argument. This would allow Rust to type-check and ownership-check the calls to the various proof functions.

Currently, there is a closure_to_fn_spec<Args, F> function that is automatically inserted by the syntax macro for constructing ghost-mode spec_fn closures. Likewise, there would be a closure_to_fn_proof<Usage, Modes, Mode, Args, F> function automatically inserted for the proof closure expressions listed above. The syntax macro would automatically instantiate the Usage, Modes, and Mode arguments based on the syntax of the parameter and return type declarations.

Currently, there is a private vstd fn exec_nonstatic_call<Args, Output, F>(f: F, args: Args) -> Output function used in VIR to represent calls to exec closures and the corresponding requires and ensures that must be checked. I think this function can be used as-is for calls to proof closures as well. The mode checking (modes.rs) will need to be extended to check calls to proof mode closures, based on which arguments are tracked.

Currently, there is an AST expression ExprX::ExecClosure for VIR exec closures. I think this can be generalized for proof-mode closures as well. Again, modes.rs will need to be extended to check these.

Extensions for marker traits

Closures may implement the following marker traits: Clone, Copy, Send, Sync. For normal Rust exec closures, functions can add these markers as bounds on function types, as in f<F>() where F: Fn(u8) -> u8, F: Copy, F: Sync. This extends partially to dyn, so that you can write dyn Fn(u8) -> u8 + Send + Sync, although dyn does not easily support + Copy or + Clone.

To support these marker traits for proof closures, I propose extending the proof_fn_* types and proof_fn_* closure syntax with an optional bracketed list of marker traits implemented by the proof closure. For example:

let tracked f = proof_fn[Clone, Sync]|i: int, tracked s: S| { g(i, s) }
let tracked g: proof_fn[Clone, Sync](int, tracked S) -> int = f;
let result = g(10, s);

In the underlying implementation, this can be encoded with more type arguments: FnProof<Usage, Cln, Cpy, Snd, Syn, Modes, Mode, Args, Output>, combined with various trait impl tricks and where clauses to pass the implemented traits from the original Rust closure to the FnProof<...> type.

[zeldovich]

I think it would be helpful to be able to specify requires / ensures clauses for a proof_fn type, or whatever type a closure expression has. This would be helpful in the logical atomicity use cases for proof closures, and more generally seems helpful whenever proof closures take arguments or return values, to state something even as simple as x.inv() for any x argument or return value; otherwise it might be difficult for a proof closure to make use of state that's passed in, or to capture whatever facts the proof closure establishes.

[Chris-Hawblitzel]

I don't think it makes sense for proof functions to implement FnOnce.

spec_fn already implements FnOnce:

#[cfg(verus_keep_ghost)]
impl<Args: core::marker::Tuple, Output> FnOnce<Args> for FnSpec<Args, Output> {
    type Output = Output;
    extern "rust-call" fn call_once(self, _: Args) -> <Self as FnOnce<Args>>::Output {
        todo!()
    }
}

#[cfg(verus_keep_ghost)]
impl<Args: core::marker::Tuple, Output> FnMut<Args> for FnSpec<Args, Output> {
    extern "rust-call" fn call_mut(&mut self, _: Args) -> <Self as FnOnce<Args>>::Output {
        todo!()
    }
}

#[cfg(verus_keep_ghost)]
impl<Args: core::marker::Tuple, Output> Fn<Args> for FnSpec<Args, Output> {
    extern "rust-call" fn call(&self, _: Args) -> <Self as FnOnce<Args>>::Output {
        todo!()
    }
}

Without implementing FnOnce/FnMut/Fn, is there a way to overload call expressions for calling proof closures?

[tjhance]

Ah I kinda forgot about that 😓

I think of that more as a hack so that it passes the type-checker, though, not something we should rely on.

[Chris-Hawblitzel]

I think I can keep the reliance on FnOnce/FnMut/Fn to just the minimum we need to overload call expressions, then. For example, instead of reusing the exec call_requires/call_ensures/FnWithRequiresEnsures, which are based directly on FnOnce, I can declare something like proof_call_requires/proof_call_ensures/FnProofWithRequiresEnsures, all based on the FnProof type instead of the FnOnce trait. The user interface would still look the same, since the new trait could declare functions named requires and ensures so users could still write .requires and .ensures.

[tjhance]

yep, that sounds good

[Chris-Hawblitzel]

proof_call_requires/proof_call_ensures/FnProofWithRequiresEnsures

(Just a note to myself: it's even simpler -- I don't think we'll actually need a FnProofWithRequiresEnsures trait anyway, since FnProof is a type (our own type) and we can just impl requires and ensures functions directly on the FnProof type, without needing a trait at all. These direct impl functions will take the place of proof_call_requires/proof_call_ensures, so there's no need to declare top-level proof_call_requires/proof_call_ensures functions either.)

[Chris-Hawblitzel]

And there's one more design detail that I forgot: a proof function will have a lifetime. So the underlying Rust type will be something with an 'a, like FnProof<'a, Usage, Cln, Cpy, Snd, Syn, Modes, Mode, Args, Output>. As a surface syntax, I propose having an optional <'lifetime> annotation on the proof_fn type:

let tracked f = proof_fn[Clone, Sync]|i: int, tracked s: S| { g(i, s) }
let tracked g: proof_fn<'static>[Clone, Sync](int, tracked S) -> int = f;
let result = g(10, s);