'returns' clause for exec functions

[tjhance]

Verus currently has when_used_as_spec which lets you use an exec function in spec contexts. This is particularly useful for functions like u64::wrapping_add or Option::unwrap or Vec::len - pure functions that have clear uses in both spec code and exec code.

Unfortunately, it can be a little cumbersome to use. It also has the unexpected behavior that the exec function doesn't have to agree with the spec function.

I propose incorporating this into the verus signature syntax. For example:

fn fibonacci_impl(x: u64) -> u64
requires x < 20
returns fibonacci(x) as u64 
{
   ...
}

In general:

• The clause returns P is equivalent to ensures return_value == P. This is checked like an ordinary ensures clause.
• An exec function with a returns clause can be used in spec position where of course it has the meaning of the expression P.

In other words, the above is roughly equivalent to:

open spec fn _spec_fibonacci(x: u64) -> u64 {
   fibonacci(x) as u64
}

#[when_used_as_spec(_spec_fibonacci)]
fn fibonacci_impl(x: u64) -> (ret: u64)
requires x < 20
ensures ret == _spec_fibonacci(x)
{
   ...
}

Even without the second bullet, I think the returns clauses is a cleaner way to write some specs.

Questions:

Should the when_used_as_spec effect be automatic, or should it require an additional annotation?

Should the 'requires' clause of the exec function become a 'recommends' clause on the spec function?

[parno]

FWIW, Dafny has a similar concept, except in the other direction. It's called a "function-by-method" and you attach the method implementation to the function (a.k.a. spec).

Should the when_used_as_spec effect be automatic, or should it require an additional annotation?

Seems reasonable to make it automatic, unless we can think of an example where the programmer would accidentally use the exec function in a spec and expect a warning/error instead of silently using the when clause. I can't immediately think of such an example, but perhaps others can.

[jaylorch]

This seems very nice. Is it possible to do away with the as u64 in your example, since it's not needed in the equivalent ensures ret == fibonacci(x)?

To answer your questions:

1. I think the when_used_as_spec effect may as well be automatic, since that's what returns would be for.
2. It should probably be a requires clause on the spec function once we have those. :-)

[parno]

If I were writing the ensures clause manually, I would tend to write it as:

fn fibonacci_impl(x: u64) -> (r: u64)
  requires x < 20
  ensures r as int == fibonacci(x) 

I think upcasting the result to int makes verification a bit simpler, since you don't have to prove that fibonacci(x) fits in a u64. You've probably already proved in the implementation that your calculation of r doesn't overflow, so it would be nice to not have to re-prove that. And keeping spec functions over int when possible simplifies life.

[jaybosamiya-ms]

Closely related proposals: dual-mode functions (spec exec functions) and returns@.

Inspiration

fn foo(x: bool, y: bool) -> Vec<bool> {
  vec![x, y]
}

For Rust functions such as the one above, there is essentially only one reasonable specification for it. As a practical example, consider combinators of Option, such as map, unwrap_or, etc.

returns@

Both the exec function and equivalent spec function need to have the same type signature (for convenient naming/usage/...), but we sometimes need to deal with exec objects like Vec. The idea of returns@ is to support this by having the spec function return an exec object whose only known thing is facts about its view. In particular, for the above foo, one would write something like returns@ seq![x, y] (modulo any bike-shedding on syntax). This essentially extends the proposed returns to support the use case that Bryan has written about above.

Dual-mode functions

Rather than writing an explicit returns@, notice that for functions like foo, the specification follows the body so closely that they might as well be identical. That's the idea for dual-mode functions (similar to function methods in Dafny). Essentially, by marking a function as spec exec (bike-sheddable again; "spec/exec, or as I've recently taken to calling it, spec+exec" etc.), you don't need to provide a requires/ensures/returns clause. Instead, the function becomes in a certain sense "transparent", being quite usable in both exec and spec contexts with its body "known". Care must be taken (thanks @Chris-Hawblitzel for noticing this) to make sure we don't become unsound just by having equal bodies, since spec functions guarantee determinism---the approach to this essentially is why returns@ is needed---we only talk about the view of any returned value in a spec exec context, making sure that we don't accidentally end up saying unsound things about (say) Vec::capacity and such.

Speaking of how this might look, one would simply have to prefix the foo above:

spec exec fn foo(x: bool, y: bool) -> Vec<bool> {
  vec![x, y]
}

and then would be able to use it in exec contexts as normal, while also suddenly being able to use it in spec contexts, such as showing (say):

assert(foo(true, false)@[0] == true);

The aim of such functions is to explicitly not have much in the way of pre/post-conditions or such; they are essentially intended to only be used for small functions where you don't have anything particularly interesting to say about the function other than the body.

Overall, with dual-mode functions, many common utility functions and library functions become trivial to write and specify, thereby reducing friction for migrating codebases from unverified to verified (where otherwise, a non-trivial collection of small utility functions need to end up explicitly specifying that their body is equal to their body, causing unnecessary duplication).

However, recognizing that spec exec functions don't cover the full range of things one might wish to specify, this gets us to the returns@ written above, which covers situations where the spec is not immediately trivial, but nonetheless having a spec+exec function with the same name would be nice.

[tjhance]

I wonder if checking needs to be done on the foo function at all. Perhaps we could just substitute the body everywhere it is used.

[y1ca1]

I second that. Dual mode spec exec is incredibly useful for small utility functions! An interesting question might be defining "smallness"? Or maybe a notion of "pure exec function"?

[utaal]

@Chris-Hawblitzel: One challenge of spec-exec functions is that exec by itself isn't immediately deterministic. We need to make sure that everything that gets return is indistinguishable from a deterministic model.

[utaal]

Interpret them as const: it should be executable code and there's a way to interpret it as spec code.

[parno]

@tjhance This was completed with #1283, right? Can we close this discussion?

[jaybosamiya-ms]

The related (but somewhat tangential) dual-mode functions proposal (#851 (comment)) was not handled by #1283. I've separated it out into a separate discussion (#1429) so it stays open when this proposal on returns is closed.

[tjhance]

The when-use-as-spec part of the feature hasn't been implemented yet.