Dual-mode (spec exec) functions

[jaybosamiya-ms]

Originally written as comments on #851. Copied relevant parts here to separate it out.

@jaybosamiya-ms wrote:

[...]

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.

[...], 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 [..here..], 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 wrote:

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 wrote:

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 wrote:

@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 wrote:

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