fix: Fix antecedent in induction hypothesis

Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs

@@ -170,6 +170,7 @@ void TrForallStmtCall(IOrigin tok, List<BoundVar> boundVars, List<BoundedPool> b
       Contract.Assert(s0.Method.Ins.Count == s0.Args.Count);
       var callEtran = new ExpressionTranslator(this, Predef, etran.HeapExpr, initHeap, etran.scope);
       Bpl.Expr anteCanCalls, ante;
+      Bpl.Expr typeAndAdditionalAntecedents;
       Bpl.Expr post = Bpl.Expr.True;
       Bpl.Trigger tr;
       if (forallExpressions != null) {
@@ -179,29 +180,29 @@ void TrForallStmtCall(IOrigin tok, List<BoundVar> boundVars, List<BoundedPool> b
           expr = quantifierExpr;
         }
         boundVars = expr.BoundVars;
-        ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap);
+        typeAndAdditionalAntecedents = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap);
+        if (additionalRange != null) {
+          typeAndAdditionalAntecedents = BplAnd(typeAndAdditionalAntecedents, additionalRange(substMap, initEtran));
+        }
         tr = TrTrigger(callEtran, expr.Attributes, expr.Origin, bvars, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());
 
         var p = Substitute(expr.Range, null, substMap);
         anteCanCalls = initEtran.CanCallAssumption(p);
-        ante = BplAnd(ante, initEtran.TrExpr(p));
-        if (additionalRange != null) {
-          ante = BplAnd(ante, additionalRange(substMap, initEtran));
-        }
+        ante = initEtran.TrExpr(p);
         p = Substitute(expr.Term, null, substMap);
         post = BplAnd(post, callEtran.CanCallAssumption(p));
         post = BplAnd(post, callEtran.TrExpr(p));
       } else {
-        ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap);
-
-        var p = Substitute(range, null, substMap);
-        anteCanCalls = initEtran.CanCallAssumption(p);
-        ante = BplAnd(ante, initEtran.TrExpr(p));
+        typeAndAdditionalAntecedents = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap);
         if (additionalRange != null) {
           // additionalRange produces something of the form canCallAssumptions ==> TrExpr
-          ante = BplAnd(ante, additionalRange(substMap, initEtran));
+          typeAndAdditionalAntecedents = BplAnd(typeAndAdditionalAntecedents, additionalRange(substMap, initEtran));
         }
 
+        var p = Substitute(range, null, substMap);
+        anteCanCalls = initEtran.CanCallAssumption(p);
+        ante = initEtran.TrExpr(p);
+
         var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents())), s0.Receiver.Type);
         for (int i = 0; i < s0.Method.Ins.Count; i++) {
           var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutionsWithParents());  // substitute the renamed bound variables for the declared ones
@@ -235,6 +236,7 @@ void TrForallStmtCall(IOrigin tok, List<BoundVar> boundVars, List<BoundedPool> b
       if (includeCanCalls) {
         body = BplAnd(anteCanCalls, body);
       }
+      body = BplImp(typeAndAdditionalAntecedents, body);
       var qq = new Bpl.ForallExpr(tok, bvars, tr, body);
       exporter.Add(TrAssumeCmd(tok, qq));
     }

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy

@@ -1,4 +1,4 @@
-// RUN: %verify --manual-triggers "%s" > "%t"
+// RUN: %verify "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Rustan Leino
@@ -146,6 +146,11 @@ function merge(xs: List<G>, ys: List<G>): List<G>
       if Below(a, b) then Cons(a, merge(xs', ys)) else Cons(b, merge(xs, ys'))
 }
 
+lemma MultisetOfMerge(xs: List<G>, ys: List<G>)
+  ensures multiset_of(merge(xs, ys)) <= multiset_of(xs) + multiset_of(ys)
+{
+}
+
 // the specification
 
 ghost predicate sorted(xs: List<G>)
@@ -447,6 +452,29 @@ lemma sorted_merge(xs: List<G>, ys: List<G>)
   requires sorted(xs) && sorted(ys)
   ensures sorted(merge(xs, ys))
 {
+  match xs
+  case Nil =>
+    assert merge(xs, ys) == ys;
+  case Cons(a, xs') =>
+    assert (forall z :: z in multiset_of(xs') ==> Below(a, z));
+    match ys
+    case Nil =>
+      assert merge(xs, ys) == xs;
+    case Cons(b, ys') =>
+      assert (forall z :: z in multiset_of(ys') ==> Below(b, z));
+      if Below(a, b) {
+        assert merge(xs, ys) == Cons(a, merge(xs', ys));
+        var rest := merge(xs', ys);
+        MultisetOfMerge(xs', ys);
+        assert (forall z :: z in multiset_of(rest) ==> Below(a, z));
+        sorted_merge(xs', ys);
+      } else {
+        assert merge(xs, ys) == Cons(b, merge(xs, ys'));
+        var rest := merge(xs, ys');
+        MultisetOfMerge(xs, ys');
+        assert (forall z :: z in multiset_of(rest) ==> Below(b, z));
+        sorted_merge(xs, ys');
+      }
 }
 
 // -- stability lemmas
@@ -667,11 +695,34 @@ lemma filter_append(g: G, xs: List<G>, ys: List<G>)
 {
 }
 
+lemma filter_append_notInXs(g: G, b: G, xs: List<G>, ys: List<G>)
+  requires forall z <- multiset_of(xs) :: key(g) != key(z)
+  ensures filter(g, Cons(b, append(xs, ys))) == filter(g, append(xs, Cons(b, ys)))
+{
+}
+
+lemma filter_append_notSame(g: G, b: G, xs: List<G>, ys: List<G>)
+  requires key(g) != key(b)
+  ensures filter(g, append(xs, ys)) == filter(g, append(xs, Cons(b, ys)))
+{
+}
+
 lemma filter_append_notBelow(g: G, b: G, xs: List<G>, ys: List<G>)
   requires sorted(xs)
   requires xs.Cons? ==> !Below(xs.head, b)
   ensures filter(g, Cons(b, append(xs, ys))) == filter(g, append(xs, Cons(b, ys)))
 {
+  if key(g) == key(b) {
+    filter_append_notInXs(g, b, xs, ys);
+  } else {
+    calc {
+      filter(g, Cons(b, append(xs, ys)));
+      // def. filter
+      filter(g, append(xs, ys));
+      { filter_append_notSame(g, b, xs, ys); }
+      filter(g, append(xs, Cons(b, ys)));
+    }
+  }
 }
 
 lemma filter_Cons_notBelow(g: G, b: G, a: G, ys: List<G>)

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy.expect

@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 52 verified, 0 errors
+Dafny program verifier finished with 55 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6366.dfy

@@ -0,0 +1,56 @@
+// RUN: %exits-with 4 %verify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Nat = Nat(n: nat)
+
+datatype SeqNat = Seq(seqn: seq<Nat>) {
+  predicate LessThan(n: nat) 
+  decreases seqn
+  {
+    if seqn == [] then true else seqn[0].n < n && Seq(seqn[1..]).LessThan(n)
+  }
+}
+
+predicate LessThan(ss: seq<SeqNat>, n: nat) {
+  if ss == [] then true else
+    ss[0].LessThan(n) && LessThan(ss[1..], n)
+}
+
+lemma Foo(ss: seq<SeqNat>, l: nat)
+  requires l < |ss|
+  requires LessThan(ss, 30)
+  requires LessThan(ss, 239)
+  ensures ss[l].LessThan(1) // error: (but this was once provable, due to a bug)
+{
+  if ss != [] {
+    if l != 0 {
+      Foo(ss[1..], l - 1);
+      assert ss[1..][l - 1] == ss[l];
+      assert ss[1..][l - 1..] == ss[l..];
+    }
+  }
+}
+
+method Main() {
+  var sn: SeqNat := Seq([Nat(28)]);
+  assert sn.LessThan(30);
+  assert sn.LessThan(239);
+
+  var ss := [sn];
+  var l := 0;
+  Foo(ss, l);
+
+  // by the postcondition of Foo:
+  assert ss[l].LessThan(1);
+  assert ss[l] == sn;
+  assert sn.LessThan(1);
+  assert sn.seqn[0].n < 1;
+
+  // yet:
+  assert sn.seqn[0] == Nat(28);
+  assert sn.seqn[0].n == 28;
+  assert 28 < 1;
+  assert false;
+
+  print 10 / 0;
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6366.dfy.expect

@@ -0,0 +1,8 @@
+git-issue-6366.dfy(26,4): Error: a postcondition could not be proved on this return path
+git-issue-6366.dfy(23,24): Related location: this is the postcondition that could not be proved
+git-issue-6366.dfy(10,43): Related location: this proposition could not be proved
+git-issue-6366.dfy(26,4): Error: a postcondition could not be proved on this return path
+git-issue-6366.dfy(23,24): Related location: this is the postcondition that could not be proved
+git-issue-6366.dfy(10,73): Related location: this proposition could not be proved
+
+Dafny program verifier finished with 4 verified, 2 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg

@@ -164,7 +164,7 @@ def buildCmd(cmd, args):
         argStr = ' /'.join(args)
         return f'{cmd} /{argStr}'
     else:
-        return args
+        return cmd
 
 dafny = addParams(buildCmd(dafnyExecutable, dafnyArgs))
 boogie = buildCmd(boogieExecutable, boogieArgs)

docs/dev/news/6367.fix

@@ -0,0 +1 @@
+Fix the generated induction hypothesis for auto-induction