fix: Invalid declaration errors with /typeEncoding:m (#4275)

Attempting verification directly from Dafny using `/typeEncoding:m`
sometimes leads to invalid declaration errors in existing integration
tests. The issue does not happen when printing to a Boogie file first,
then verifying that file directly with Boogie. This PR tries to fix
this.

By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.

Source/DafnyCore/Verifier/Translator.cs

@@ -4425,13 +4425,6 @@ void AddWellformednessCheck(Function f) {
  }
  Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);
 
- DefineFrame(f.tok, f.Reads, bodyCheckBuilder
- , new List<Variable>() /* dummy local variable list, since frame axiom variable (and its definition)
- * is already added. The only reason why we add the frame axiom definition
- * again is to make boogie gives the same trace as before the change that
- * makes reads clauses also guard the requires */
- , null);
-
  wfo = new WFOptions(null, true, true /* do delayed reads checks */);
  CheckWellformedWithResult(f.Body, wfo, funcAppl, f.ResultType, locals, bodyCheckBuilder, etran);
  if (f.Result != null) {

Test/dafny0/Fuel.dfy.expect

@@ -20,41 +20,41 @@ Fuel.dfy(324,21): Related location
 Fuel.dfy(313,41): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,93): Related location
+Fuel.dfy(314,46): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
 Fuel.dfy(312,58): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,72): Related location
+Fuel.dfy(312,43): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(314,46): Related location
+Fuel.dfy(314,72): Related location
 Fuel.dfy(335,26): Error: function precondition could not be proved
 Fuel.dfy(324,21): Related location
-Fuel.dfy(312,43): Related location
+Fuel.dfy(314,93): Related location
 Fuel.dfy(335,49): Error: destructor 't' can only be applied to datatype values constructed by 'VTuple'
 Fuel.dfy(335,50): Error: index out of range
 Fuel.dfy(336,38): Error: index out of range
 Fuel.dfy(336,42): Error: destructor 'u' can only be applied to datatype values constructed by 'VUint64'
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(312,43): Related location
+Fuel.dfy(311,43): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(312,58): Related location
+Fuel.dfy(312,43): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
 Fuel.dfy(314,93): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(314,72): Related location
+Fuel.dfy(312,58): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(311,43): Related location
+Fuel.dfy(313,41): Related location
 Fuel.dfy(336,45): Error: function precondition could not be proved
 Fuel.dfy(329,21): Related location
-Fuel.dfy(313,41): Related location
+Fuel.dfy(314,72): Related location
 Fuel.dfy(336,71): Error: index out of range
 Fuel.dfy(397,22): Error: assertion might not hold
 Fuel.dfy(398,22): Error: assertion might not hold

Test/dafny0/FunctionSpecifications.dfy

@@ -1,9 +1,9 @@
-// RUN: %exits-with 4 %dafny /compile:0 /deprecation:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %exits-with 4 %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 ghost function Fib(n: int): int
- requires 0 <= n;
- ensures 0 <= Fib(n);
+ requires 0 <= n
+ ensures 0 <= Fib(n)
 {
  if n < 2 then n else
  Fib(n-2) + Fib(n-1)
@@ -12,53 +12,61 @@ ghost function Fib(n: int): int
 datatype List = Nil | Cons(int, List)
 
 ghost function Sum(a: List): int
- ensures 0 <= Sum(a);
+ ensures 0 <= Sum(a)
 {
  match a
  case Nil => 0
  case Cons(x, tail) => if x < 0 then 0 else Fib(x)
 }
 
 ghost function FibWithoutPost(n: int): int
- requires 0 <= n;
+ requires 0 <= n
 {
  if n < 2 then n else
  FibWithoutPost(n-2) + FibWithoutPost(n-1)
 }
 
 ghost function SumBad(a: List): int
- ensures 0 <= Sum(a); // this is still okay, because this is calling the good Sum
- ensures 0 <= SumBad(a); // error: cannot prove postcondition
+ ensures 0 <= Sum(a) // this is still okay, because this is calling the good Sum
+ ensures 0 <= SumBad(a) // error: cannot prove postcondition
 {
  match a
  case Nil => 0
  case Cons(x, tail) => if x < 0 then 0 else FibWithoutPost(x)
 }
 
 ghost function FibWithExtraPost(n: int): int
- ensures 2 <= n ==> 0 <= FibWithExtraPost(n-1); // This is fine, because the definition of the function is discovered via canCall
- ensures 1 <= n ==> 0 <= FibWithExtraPost(n-1); // Error: In the current implementation of Dafny, one needs to actually call the
+ ensures 2 <= n ==> 0 <= FibWithExtraPost(n-1) // This is fine, because the definition of the function is discovered via canCall
+ ensures 1 <= n ==> 0 <= FibWithExtraPost(n-1) // Error: In the current implementation of Dafny, one needs to actually call the
  // function in order to benefit from canCall. This may be improved in the future.
- ensures 0 <= FibWithExtraPost(n);
+ ensures 0 <= FibWithExtraPost(n)
 {
  if n < 0 then 0 else
  if n < 2 then n else
  FibWithExtraPost(n-2) + FibWithExtraPost(n-1)
 }
 
+ghost function GoodPost(n: int): int
+ requires 0 <= n
+ ensures 1 <= n ==> GoodPost(n-1) == GoodPost(n-1)
+ ensures GoodPost(2*n - n) == GoodPost(2*(n+5) - 10 - n) // these are legal ways to denote the result value of the function
+{
+ assert 2*n - n == 2*(n+5) - 10 - n;
+ if n < 2 then n else
+ GoodPost(n-2) + GoodPost(n-1)
+}
+
 ghost function DivergentPost(n: int): int
- requires 0 <= n;
- ensures 1 <= n ==> DivergentPost(n-1) == DivergentPost(n-1);
- ensures DivergentPost(2*n - n) == DivergentPost(2*(n+5) - 10 - n); // these are legal ways to denote the result value of the function
- ensures DivergentPost(n+1) == DivergentPost(n+1); // error: call may not terminate
+ requires 0 <= n
+ ensures DivergentPost(n+1) == DivergentPost(n+1) // error: call may not terminate
 {
  assert 2*n - n == 2*(n+5) - 10 - n;
  if n < 2 then n else
  DivergentPost(n-2) + DivergentPost(n-1)
 }
 
 ghost function HoldsAtLeastForZero(x: int): bool
- ensures x == 0 ==> HoldsAtLeastForZero(x);
+ ensures x == 0 ==> HoldsAtLeastForZero(x)
 {
  x < -2 // error: this does not hold for 0
 }
@@ -67,7 +75,7 @@ ghost function HoldsAtLeastForZero(x: int): bool
 // ----- the subrange test (which they didn't always do).
 
 ghost function IncA(x: nat): nat
- ensures x < IncA(x);
+ ensures x < IncA(x)
 {
  if x == 17 then
  18
@@ -87,7 +95,7 @@ ghost function IncB(i: nat): nat
 }
 
 ghost function IncC(i: nat): int
- ensures IncC(i)>=0;
+ ensures IncC(i)>=0
 {
  var n :| n>i; n
 }
@@ -99,9 +107,9 @@ ghost function IncC(i: nat): int
 
 // Test basic function hiding
 ghost function {:opaque} secret(x:int, y:int) : int
- requires 0 <= x < 5;
- requires 0 <= y < 5;
- ensures secret(x, y) < 10;
+ requires 0 <= x < 5
+ requires 0 <= y < 5
+ ensures secret(x, y) < 10
 { x + y }
 
 method test_secret()
@@ -115,7 +123,7 @@ method test_secret()
 // Check that opaque doesn't break recursion unrolling
 // Also checks that opaque functions that do terminate are verified as such
 ghost function {:opaque} recursive_f(x:int) : int
- requires x >= 0;
+ requires x >= 0
 {
  if x == 0 then 0
  else 1 + recursive_f(x - 1)
@@ -134,22 +142,22 @@ method test_recursive_f()
 
 // Check that opaque doesn't interfere with ensures checking
 ghost function {:opaque} bad_ensures(x:int, y:int):int
- requires x >= 0 && y >= 0;
- ensures bad_ensures(x, y) > 0;
+ requires x >= 0 && y >= 0
+ ensures bad_ensures(x, y) > 0
 {
  x + y
 }
 
 // Check that opaque doesn't interfere with termination checking
 ghost function {:opaque} f(i:int):int
- decreases i;
+ decreases i
 {
  f(i) + 1
 }
 
 // Try a sneakier (nested) version of the test above
 ghost function {:opaque} g(i:int):int
- decreases i;
+ decreases i
 {
  h(i) + 1
 }

Test/dafny0/FunctionSpecifications.dfy.expect

@@ -2,17 +2,17 @@ FunctionSpecifications.dfy(35,24): Error: a postcondition could not be proved on
 FunctionSpecifications.dfy(31,12): Related location: this is the postcondition that could not be proved
 FunctionSpecifications.dfy(45,2): Error: a postcondition could not be proved on this return path
 FunctionSpecifications.dfy(40,23): Related location: this is the postcondition that could not be proved
-FunctionSpecifications.dfy(53,10): Error: cannot prove termination; try supplying a decreases clause
-FunctionSpecifications.dfy(60,15): Error: a postcondition could not be proved on this return path
-FunctionSpecifications.dfy(61,21): Related location: this is the postcondition that could not be proved
-FunctionSpecifications.dfy(109,22): Error: assertion might not hold
-FunctionSpecifications.dfy(112,22): Error: assertion might not hold
-FunctionSpecifications.dfy(127,26): Error: assertion might not hold
-FunctionSpecifications.dfy(131,26): Error: assertion might not hold
-FunctionSpecifications.dfy(136,25): Error: a postcondition could not be proved on this return path
-FunctionSpecifications.dfy(138,28): Related location: this is the postcondition that could not be proved
-FunctionSpecifications.dfy(147,2): Error: decreases clause might not decrease
-FunctionSpecifications.dfy(154,2): Error: decreases clause might not decrease
-FunctionSpecifications.dfy(159,2): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(61,10): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(68,15): Error: a postcondition could not be proved on this return path
+FunctionSpecifications.dfy(69,21): Related location: this is the postcondition that could not be proved
+FunctionSpecifications.dfy(117,22): Error: assertion might not hold
+FunctionSpecifications.dfy(120,22): Error: assertion might not hold
+FunctionSpecifications.dfy(135,26): Error: assertion might not hold
+FunctionSpecifications.dfy(139,26): Error: assertion might not hold
+FunctionSpecifications.dfy(144,25): Error: a postcondition could not be proved on this return path
+FunctionSpecifications.dfy(146,28): Related location: this is the postcondition that could not be proved
+FunctionSpecifications.dfy(155,2): Error: decreases clause might not decrease
+FunctionSpecifications.dfy(162,2): Error: decreases clause might not decrease
+FunctionSpecifications.dfy(167,2): Error: cannot prove termination; try supplying a decreases clause
 
-Dafny program verifier finished with 9 verified, 12 errors
+Dafny program verifier finished with 10 verified, 12 errors

docs/dev/news/inconsistent-ast-monomorphic.fix

@@ -0,0 +1 @@
+Fixes invalid declaration errors when verifying directly from Dafny using /typeEncoding:m.