diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs index 79fd638b7eb..d1d8b8125cb 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs @@ -170,6 +170,7 @@ void TrForallStmtCall(IOrigin tok, List boundVars, List 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 boundVars, List 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 boundVars, List 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)); } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect index 5000230e330..68f4e91ebc9 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/CoinductiveProofs.dfy.expect @@ -31,5 +31,5 @@ CoinductiveProofs.dfy(208,21): Related location: this is the postcondition that CoinductiveProofs.dfy(4,23): Related location: this proposition could not be proved Dafny program verifier finished with 23 verified, 12 errors -Total resources used is 748715 +Total resources used is 752683 Max resources used by VC is 59297 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy index 4463e4a41a6..7ce3da204c8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy +++ b/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, ys: List): List if Below(a, b) then Cons(a, merge(xs', ys)) else Cons(b, merge(xs, ys')) } +lemma MultisetOfMerge(xs: List, ys: List) + ensures multiset_of(merge(xs, ys)) <= multiset_of(xs) + multiset_of(ys) +{ +} + // the specification ghost predicate sorted(xs: List) @@ -447,6 +452,29 @@ lemma sorted_merge(xs: List, ys: List) 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, ys: List) { } +lemma filter_append_notInXs(g: G, b: G, xs: List, ys: List) + 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, ys: List) + 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, ys: List) 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) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy.expect index 3d4178cf545..3b71b05bfb8 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/GHC-MergeSort.dfy.expect +++ b/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 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6366.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6366.dfy new file mode 100644 index 00000000000..7dd6850f3d0 --- /dev/null +++ b/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) { + predicate LessThan(n: nat) + decreases seqn + { + if seqn == [] then true else seqn[0].n < n && Seq(seqn[1..]).LessThan(n) + } +} + +predicate LessThan(ss: seq, n: nat) { + if ss == [] then true else + ss[0].LessThan(n) && LessThan(ss[1..], n) +} + +lemma Foo(ss: seq, 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; +} diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6366.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-6366.dfy.expect new file mode 100644 index 00000000000..a5e5fd5640a --- /dev/null +++ b/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 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg b/Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg index 2eea6855460..c2be6af01e0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/lit.site.cfg +++ b/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) diff --git a/docs/dev/news/6367.fix b/docs/dev/news/6367.fix new file mode 100644 index 00000000000..3e0ba164e44 --- /dev/null +++ b/docs/dev/news/6367.fix @@ -0,0 +1 @@ +Fix the generated induction hypothesis for auto-induction