Automatic Specification of 'small' closures

[rsofaer]

Idiomatic Rust includes significant use of higher order functions. One very simple example might be as follows:

enum Errors {
      A,
      B
  }
  pub fn use_ok_or_else(opt: Option<i64>) -> bool
   {
      let res: Result<i64, Errors> = None.ok_or_else(|| 
      {
         Errors::A
      });
      matches!(res, Err(Errors::A))
  }

Verus example: https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=071d0a0ce566bf4100a681caea2bfa35

Another example would be the vec map with closure page in the Verus docs: https://verus-lang.github.io/verus/guide/exec_closures.html

From the perspective of someone integrating Verus into an existing codebase, annotating very simple closures with spec definitions is making code quality and readability worse, and we would prefer for this kind of code to go unmodified.

@dschoepe mentioned that @Chris-Hawblitzel was considering an approach to this. Maybe the dual exec/spec work could be extended to closures? Maybe a triggering annotation #[autospec]|x,y|{..} would be best at least at first to avoid excessive symbolic execution?

[Chris-Hawblitzel]

Yes, I was thinking about inferring requires by running weakest precondition on the closure body and ensures by running strongest postcondition on the closure body, perhaps automatically (for small closures) if the programmer doesn't supply their own requires and ensures. The hope is that this could infer simple requires and ensures as in the https://verus-lang.github.io/verus/guide/exec_closures.html example:

|x: u8| -> (res: u8)
        requires 0 <= x < 128
        ensures res == 2 * x
    {
        2 * x
    }

For example, the inferred requires might look like 0 <= 2 * x < 256.

[tjhance]

I'll second that this would be extremely useful.