Asserted precondition might not hold in mutual inductive Dafny lemmas

Question

I am trying to prove something about the semantics of programs with side-effects in Dafny using trees that record the interaction, following the free monad approach. Thus, what the semantics will produce are trees of the following shape (simplified to only one instruction for reading an input).

datatype Prog<A>
  = Return (pure : A)
  | Get(input : string -> Prog<A>)

The main issue is that these are infinitely branching trees and it requires some trickery to work with such trees in Dafny because they have no bound on the depth, although every leaf is reachable via a finite path.

What I would like to do now is to define big-step semantics as inductive relation, see the article "Well-founded Functions and Extreme Predicates in Dafny: A Tutorial". Here is a small part of the language, just with one command for reading and one for sequential composition of commands. The relation big_step_bind sequentially composes two interaction trees (bind is the usual terminology for the map that composes monadic computations), while big_step is the big-step semantics relation. These relations are inductively and mutually defined.

datatype Com =  GetC | SeqC(Com, Com)

type Store = map<int, string>

least predicate big_step_bind(c : Com, p : Prog<Store>, q : Prog<Store>) {
  match p {
    case Return(s) => big_step(c, s, q)
    case Get(f)    => exists g :: q == Get(g) && forall i :: big_step_bind(c, f(i), g(i))
  }
}

least predicate big_step(c : Com, s : Store, p : Prog<Store>) {
  match c {
    case GetC =>
      p == Get(i => Return(s[0 := i]))
    case SeqC(c1, c2) =>
      exists p1 :: big_step(c1, s, p1) && big_step_bind(c2, p1, p)
  }
}

So far, everything works reasonably well. But to run any functions on the resulting interaction trees, I need to know that the big-step semantics only gives well-founded trees because Dafny will not allow definitions by recursion over Prog and complain about non-termination. Thus, I define a predicate wfTree that singles out all well-founded trees of the type Prog, which should in fact be all of them.

least predicate wfTree<A> (p : Prog<A>){
  match p {
    case Return(b) => true
    case Get(g)    => forall x :: wfTree(g(x))
  }
}

Problem

Now I would like to prove that all trees "produced" by the big-step semantics are well-founded:

least lemma big_step_bind_wf(c : Com, p : Prog<Store>, q : Prog<Store>)
  requires wfTree(p)                                      // (1)
  requires big_step_bind(c, p, q)
  ensures wfTree(q)
{
  match p {
    case Return(s) => big_step_wf(c, s, q);
    case Get(f) =>
      var i ;
      var q' :| big_step_bind(c, f(i), q');
      big_step_bind_wf(c, f(i), q');
  }
}

least lemma big_step_wf(c : Com, s : Store, p : Prog<Store>)
  requires big_step(c, s, p)
  ensures wfTree(p)
{
  match c {
    case GetC => return;
    case SeqC(c1, c2) =>
      var p1 :| big_step(c1, s, p1) && big_step_bind(c2, p1, p);
      big_step_wf(c1, s, p1);                             // (2)
      assert wfTree(p1);                                  // (3)
      big_step_bind_wf(c2, p1, p);                        // (4)
  }
}

Again, these lemmas are mutually proven by induction. However, the last step (4) of the proof cannot be verified. Dafny says

Error: A precondition for this call might not hold.

and refers to (1), which is the precondition of big_step_bind_wf that requires wfTree(p1) to hold. However, (2) has as postcondition exactly that and the assert at (3) shows this.

My question is now: Why can Dafny not be sure that the precondition holds? Am I missing something or is this an issue with the implementation? Thank you very much!

Answer 1

I am able to verify by moving well founded program precondition to postcondition in least lemma for bind.

datatype Program<T> = Result(T) | Get(input: string -> Program<T>)
    
datatype Command = GetInput | Sequence(Command, Command)
    
    
least predicate big_step_bind
   (c: Command,
    p1: Program<string>,
    p2: Program<string>)
{
    match p1 {
      case Result(x) => big_step(c, p2)
      case Get(pr) =>
         exists qr :: p2 == Get(qr)
            && forall i :: big_step_bind(c, pr(i), qr(i))
    }
}
    
least predicate big_step(c: Command, p: Program<string>){
    match c  {
      case GetInput => p == Get(input => Result(input))
      case Sequence(c1, c2) =>
       exists p1 ::  big_step(c1, p1) && big_step_bind(c2, p1, p)
    }
}
    
least predicate wellFoundedProgram(p: Program<string>)
{
   match p {
     case Result(x) => true
     case Get(px) => forall i ::  wellFoundedProgram(px(i))
   }
}
    
    
least lemma wellFoundedGenerationBind(c: Command, p1: Program<string>, p: Program<string>)
   requires big_step_bind(c, p1, p)
   ensures wellFoundedProgram(p1)
   ensures wellFoundedProgram(p)
{
   match p1 {
     case Result(x) => { wellFoundedGeneration(c, p) ;}
     case Get(px) => {
     }
   }
}
    
least lemma wellFoundedGeneration(c: Command, p: Program<string>)
  requires big_step(c, p)
  ensures wellFoundedProgram(p)
{
   match c {
     case GetInput => {}
     case Sequence(c1, c2) => {
        var p1 :| big_step(c1, p1) && big_step_bind(c2, p1, p);
        wellFoundedGenerationBind(c2, p1, p);
     }
   }
}