Don't consume fuel when unfolding some functions in a nested group of recursive functions

I post this issue following conversations with @RustanLeino and @cpitclaudel, and as a basis for future discussions.

When we have a group of recursive functions, unfolding any function from that group requires Z3 to consume fuel. This is not always necessary, and can make proofs get stuck. For instance, below, we need to introduce a call to F1 in our proofs so that Z3 can unfold the functions one step further (the default fuel is 2):

predicate F0(n: nat) {
  if n == 0 then true else F1(n - 1)
}

predicate F1(n: nat) {
  if n == 0 then false else F2(n - 1)
}

predicate F2(n: nat) {
  if n == 0 then false else F0(n - 1)
}

// Fails
lemma L1(n: nat)
  ensures F0(n + 3) == F0(n)
{}

// Succeeds
lemma L2(n: nat)
  ensures F0(n + 3) == F0(n)
{
  // By introducing `F1(n + 2)`, we allow the recursive unfoldings to go
  // one step further.
  assert F0(n + 3) == F1(n + 2);
}

In that specific case, it would be enough for one of the functions (say F0) to consume fuel for the unfoldings to not loop, and that would allow the first proof to go through automatically. Our suggestion is to add a keywork to tag the functions whose unfolding should consume fuel (or on the contrary, to tag the functions whose unfolding should not consume fuel), together with a sanity check that this would not lead to infinite unfoldings.

To provide more motivation as to why this would be useful: this problem was identified when working on compiler-bootstrap. We define an AST and an interpreter for the Dafny language, like what is sketched below. When first writing the interpreter, we introduced several auxiliary functions to isolate the different cases. Those auxiliary functions are however mutually recursive with InterpExpr, and their unfolding consumes fuel leading to problems in the proofs. As a consequence, we ended up inlining those auxiliary functions, making InterpExpr big and not convenient to work with (see Interp.dfy).

datatype Expr =
  | Var(name: string)
  | If(cond: Expr, thn: Expr, els: Expr)
  | ...

function method InterpExpr(e: Expr, ctx: Context): Result<(int, Context)>
{
  match e
    case If(cond, thn, els) =>
      // We want to use an auxiliary `InterpIf` function, but it is then mutually recursive with `InterpExpr`
      // and unfolding it consumes fuel, leading to issues in the proofs. Our temporary solution is to
      // inline the body of `InterpIf` in `InterpExpr`.
      InterpIf(...)

    case ... =>
      ...
}

dafny-lang / dafny

Don't consume fuel when unfolding some functions in a nested group of recursive functions #2638