Do not use the `Result` type for functions which syntactically never fail

[sonmarcho]

For now we always use the Result type in the output type of the functions we generate. This can make it cumbersome to prove theorems about simple functions. For instance, the Option::is_some function below:

fn is_some<T>(x : &Option<T>) -> bool {
  match x {
    Some(_) => true,
    None => false,
  }
}

gets extracted to:

def is_some (T : Type) (x : Option T) : Result Bool :=
  match x with
  | Some _ => ok true
  | None => ok false

while it would be more natural to extract it to:

def is_some (T : Type) (x : Option T) : Bool :=
  match x with
  | Some _ => true
  | None => false

Following feedback from some users I suggest updating the way the code is generated to not always use the Result type. As a side note, several functions of the standard library already have a special treatment (hardcoded for now) so as not to use the Result type; the list is here: https://github.com/AeneasVerif/aeneas/blob/5da597289c1723aa59bf87ad5075675820c18f73/compiler/ExtractBuiltin.ml#L534

There are several points about which we need to be careful when doing so.

The first reason why we always use the Result type is that it makes the compilation completely modular: we never need to look at the body of a function when translating a function call. This is very useful when translating traits: if I have a trait with a method fn f(&self) -> bool, we know the model of the trait is a structure containing a field f : Self -> Result Bool, and that any implementation of this method will have exactly this type. If we simplify the Result type it is not the case anymore.

Backward functions also make this difficult. As of today, backward functions can not fail (though they always use the Result type). But once we handle enumerations with borrows, it is not the case anymore. For instance, if we write a function which optionally returns a borrow to the ith element of a list:

fn get<T>(ls : &List<T>, i : usize) -> Option<&T> {
  match ls {
    Nil => None,
    Cons(hd, tl) => {
      if i = 0 { Some(hd) } else { get(tl, i - 1) }
    }
}

The translation (which is work in progress) will give something along the lines of:

def get (T : Type) (ls : List T) (i : Usize) : Result (Option T & (Option T -> Result (List T))) :=
  match ls with
  | Nil =>
    ok (none, fun _ => ok Nil)
  | Cons hd tl =>
    if i = 0 then
      let back := fun x =>
        match x with -- Deconstruct the given back option
        | none => fail
        | some x => ok (Cons x tl) -- Update the current element
      ok (hd, back)
    else ... -- Omitted

Determining whether a backward function might fail or not just by looking at the rust signature will be hard, if not impossible.

I suggest proceeding in an incremental manner, by first simplifying a small subset of functions first, then eventually allowing the simplification of more functions. For now, I suggest to not use the Result type only if: 1. the function can not fail (syntactically), and 2. it does not have non-degenerate backward functions. By non-degenerate backward functions I mean backward functions which do consume a value (for instance, fn incr(x : &mut u32) has a backward function, but it is degenerate, as it gets extracted to a model of type U32 -> Result U32). We will have to update the way we generate trait instances to make this work. Methods in trait declarations will always use the Result type, and when extracting a trait instance we will have to wrap the result of some methods into an ok.

Finally, there are two ways of proceeding with the implementation:

• either we analyze the Rust code before doing the translation, so that we know which functions can fail or not at the moment of generating the pure code (in SymbolicToPure.ml)
• or we first generate a pure model, and simplify it during the micro-passes

I'm actually leaning towards the second solution, because I'm not sure how to make the first one work if we want to simplify the backward functions at some point.

In the future, we will have to think about compiling projects which span several verified crates. To make this work I see two possibilities. Either we generate interface files, for instance with Aeneas, which would be consumed by the children projects. Or we could directly annotate the Rust functions with attributes, to indicate their "effect" (for now, whether they can fail or not): when translating a function which has an attribute stating that it can't fail, we would check that the translated code indeed can't fail; when translating a function call we would trust that the function doesn't fail.

[sonmarcho]

@msprotz @R1kM I'm interested in your feedback.

[sonmarcho]

@zhassan-aws you might be interested in this

[msprotz]

I will read in more detail later but for now my feedback is that this needs to remain a modular, type-based analysis, so an attribute on the function seems like a nice way for the user to indicate that a more direct translation is in order, and will allow generating correct code from the caller's perspective without having to inspect the body of the callee.

For traits, this might require an attribute on the trait definition itself.

Thoughts?

[sonmarcho]

Using attributes to indicate the effect is indeed a general, modular way of directing the translation. And I agree with the idea of annotating trait definitions, or rather trait methods.

For now I'm really hesitating between triggering the simplification with attributes only, or giving the possibility (for instance with a CLI option) of always simplifying when possible.

[zhassan-aws]

triggering the simplification with attributes only

One difficulty here would be for functions in external dependencies, which would not be possible/easy to annotate.

[msprotz]

What happens if the simplification criterion gets improved and starts detecting more functions? Would this break proofs that depended on the previous behavior?

[R1kM]

I like the idea of using attributes, as this also paves the way towards more expressive "effects". Regarding your idea of simplifying through micro-passes in the pure model, wouldn't you need a whole-program analysis to do this? In this case, considering for now the single-crate case, could a first part of the analysis be performed during the SymbolicToPure translation (i.e., annotating functions with the can/cannot_fail attribute), to later be simplified in a modular fashion?

[sonmarcho]

triggering the simplification with attributes only

One difficulty here would be for functions in external dependencies, which would not be possible/easy to annotate.

Yes, that's an issue. But I was thinking that we could provide a file which describes the effects of the external dependencies, a bit like what we're doing today (though the behavior is hardcoded in ExtractBuiltin.ml at this point).

[sonmarcho]

I like the idea of using attributes, as this also paves the way towards more expressive "effects". Regarding your idea of simplifying through micro-passes in the pure model, wouldn't you need a whole-program analysis to do this? In this case, considering for now the single-crate case, could a first part of the analysis be performed during the SymbolicToPure translation (i.e., annotating functions with the can/cannot_fail attribute), to later be simplified in a modular fashion?

This is likely what would happen if we're using attributes. But I'd rather not do too many analyses in SymbolicToPure because this file became a lot more complex than what I had expected, and is not really modular. There are actually severao simplifications which happen there that I would like to move to the micro-passes for this reason.

[sonmarcho]

What happens if the simplification criterion gets improved and starts detecting more functions? Would this break proofs that depended on the previous behavior?

Yes, it will likely break proofs. But how badly would it break the proofs, I'm not sure. On the other hand, if we (allow the user to) control the simplification with attributes, I think it's ok.