Function alloc soundness fix

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -2160,7 +2160,12 @@ public Expr CanCallAssumption(Expression expr, CanCallOptions cco = null) {
               r = BplAnd(r, correctConstructor);
             }
           } else if (e.Member is ConstantField { Rhs: { } rhs } && BoogieGenerator.RevealedInScope(e.Member)) {
-            r = CanCallAssumption(Substitute(rhs, e.Obj, new Dictionary<IVariable, Expression>(), null));
+            // JATIN_TODO: Why do we need this can call?
+            // r = CanCallAssumption(Substitute(rhs, e.Obj, new Dictionary<IVariable, Expression>(), null));
+          }
+          if (e.Type.IsArrowType && this.HeapExpr != null) {
+            var alloced = BoogieGenerator.MkIsAlloc(TrExpr(e), e.Type, this.HeapExpr);
+            r = BplAnd(r,  alloced);
           }
           return r;
         } else if (expr is SeqSelectExpr) {
@@ -2357,7 +2362,6 @@ [new BoogieWrapper(index, Type.Int)],
 
         } else if (expr is LambdaExpr) {
           var e = (LambdaExpr)expr;
-
           var bvarsAndAntecedents = new List<Tuple<Boogie.Variable, Boogie.Expr>>();
           var varNameGen = BoogieGenerator.CurrentIdGenerator.NestedFreshIdGenerator("$l#");
 
@@ -2388,7 +2392,13 @@ [new BoogieWrapper(index, Type.Int)],
           //TRIG (forall $l#0#heap#0: Heap, $l#0#x#0: int :: true)
           //TRIG (forall $l#0#heap#0: Heap, $l#0#t#0: DatatypeType :: _module.__default.TMap#canCall(_module._default.TMap$A, _module._default.TMap$B, $l#0#heap#0, $l#0#t#0, f#0))
           //TRIG (forall $l#4#heap#0: Heap, $l#4#x#0: Box :: _0_Monad.__default.Bind#canCall(Monad._default.Associativity$B, Monad._default.Associativity$C, $l#4#heap#0, Apply1(Monad._default.Associativity$A, #$M$B, f#0, $l#4#heap#0, $l#4#x#0), g#0))
-          return BplForallTrim(bvarsAndAntecedents, null, canCall); // L_TRIGGER
+          if (this.HeapExpr != null) {
+            var alloced = BoogieGenerator.MkIsAlloc(TrExpr(e), e.Type, this.HeapExpr);
+            return BplAnd(BplForallTrim(bvarsAndAntecedents, null, canCall), alloced); // L_TRIGGER
+          } else {
+            return BplForallTrim(bvarsAndAntecedents, null, canCall); // L_TRIGGER
+          }
+
 
         } else if (expr is ComprehensionExpr) {
           var e = (ComprehensionExpr)expr;

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs

@@ -1239,6 +1239,12 @@ void CheckOperand(Expression operand) {
                   }
 
                   void AddResultCommands(BoogieStmtListBuilder returnBuilder, Expression result) {
+                    if (etran.UsesOldHeap) {
+                      // JATIN_TODO: what is the label here?
+                      var desc = new IsAllocated("function's output", "in the state in which the function is defined", result);
+                      var earg = MkIsAlloc(etran.TrExpr(result), result.Type, etran.HeapExpr);
+                      returnBuilder.Add(Assert(GetToken(result), earg, desc, builder.Context));
+                    }
                     if (rangeType != null) {
                       CheckSubsetType(etran, result, resultIe, rangeType, returnBuilder, "lambda expression");
                     }

Source/DafnyCore/Verifier/BoogieGenerator.Types.cs

@@ -378,24 +378,24 @@ even fields of *unallocated* objects o are unchanged from h0 to h1
         sink.AddTopLevelDeclaration(new Axiom(tok,
           BplForall(bvarsOuter, new Bpl.Trigger(tok, true, new[] { IsT, IsU }), body)));
       }
-      /*  This is the definition of $IsAlloc function the arrow type:
-        axiom (forall f: HandleType, t0: Ty, t1: Ty, h: Heap ::
-          { $IsAlloc(f, Tclass._System.___hFunc1(t0, t1), h) }
-          $IsGoodHeap(h)
-          ==>
-          (
-            $IsAlloc(f, Tclass._System.___hFunc1(t0, t1), h)
-              <==>
-              (forall bx0: Box ::
-                { Apply1(t0, t1, f, h, bx0) } { Reads1(t0, t1, f, h, bx0) }
-                $IsBox(bx0, t0) && $IsAllocBox(bx0, t0, h)
-                && precondition of f(bx0) holds in h
-                ==>
-                  (everything in reads set of f(bx0) is allocated in h)
-          ));
-        However, for /allocated:0 and /allocated:1, IsAlloc for arrow types is trivially true
-        and implies nothing about the reads set.
-      */
+      // /*  This is the definition of $IsAlloc function the arrow type:
+      //   axiom (forall f: HandleType, t0: Ty, t1: Ty, h: Heap ::
+      //     { $IsAlloc(f, Tclass._System.___hFunc1(t0, t1), h) }
+      //     $IsGoodHeap(h)
+      //     ==>
+      //     (
+      //       $IsAlloc(f, Tclass._System.___hFunc1(t0, t1), h)
+      //         ==>
+      //         (forall bx0: Box ::
+      //           { Apply1(t0, t1, f, h, bx0) } { Reads1(t0, t1, f, h, bx0) }
+      //           $IsBox(bx0, t0) && $IsAllocBox(bx0, t0, h)
+      //           && precondition of f(bx0) holds in h
+      //           ==>
+      //             (everything in reads set of f(bx0) is allocated in h)
+      //     ));
+      //   However, for /allocated:0 and /allocated:1, IsAlloc for arrow types is trivially true
+      //   and implies nothing about the reads set.
+      // */
       {
         var bvarsOuter = new List<Bpl.Variable>();
         var f = BplBoundVar("f", Predef.HandleType, bvarsOuter);
@@ -423,11 +423,12 @@ and implies nothing about the reads set.
         sink.AddTopLevelDeclaration(new Axiom(tok,
           BplForall(bvarsOuter, BplTrigger(isAlloc),
             BplImp(goodHeap,
-              BplIff(isAlloc,
+              BplImp(isAlloc,
                 BplForall(bvarsInner,
                   new Bpl.Trigger(tok, true, new List<Bpl.Expr> { applied }, BplTrigger(reads)),
                   BplImp(BplAnd(isAllocBoxes, pre), isAllocReads)))))));
       }
+
       /*  This is the allocatedness consequence axiom of arrow types:
         axiom (forall f: HandleType, t0: Ty, t1: Ty, h: Heap ::
           { $IsAlloc(f, Tclass._System.___hFunc1(t0, t1), h) }
@@ -958,7 +959,7 @@ void AddTypeDecl(SubsetTypeDecl dd) {
   /// <summary>
   /// Generate $Is (if "!generateIsAlloc") or $IsAlloc (if "generateIsAlloc") axioms for the newtype/subset-type "dd",
   /// whose printable name is "fullName".
-  /// 
+  ///
   /// Given that the type "dd" is
   ///
   ///     (new)type dd<X> = x: Base<Y> | constraint

Source/IntegrationTests/TestFiles/LitTests/LitTest/HigherOrderIntrinsicSpecification/ReadPreconditionBypass3.dfy.expect

@@ -1,4 +1,3 @@
 ReadPreconditionBypass3.dfy(26,2): Error: assertion might not hold
-ReadPreconditionBypass3.dfy(31,2): Error: assertion might not hold
 
-Dafny program verifier finished with 1 verified, 2 errors
+Dafny program verifier finished with 1 verified, 1 error

Source/IntegrationTests/TestFiles/LitTests/LitTest/blogposts/TestGenerationWithInliningQuantifiedDefinitions.dfy

@@ -8,7 +8,7 @@
 // the verifier chooses to do first. Thus, if something changes in the verifier, then the CHECK lines below
 // may need to be permuted.
 // RUN: %OutputCheck --file-to-check "%t" "%s"
-// CHECK: .*Dafny program verifier finished with 4 verified, 0 errors*
+// CHECK: .*Dafny program verifier finished with 5 verified, 0 errors*
 // CHECK: .*Evaluating the position: checked=yes, checkmate=yes, pawn is attacking*
 // CHECK: .*Evaluating the position: checked=yes, checkmate=no, pawn is attacking*
 // CHECK: .*Evaluating the position: checked=no, checkmate=no*

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect

@@ -91,5 +91,5 @@ SubsetTypes.dfy(459,6): Error: assertion might not hold
 SubsetTypes.dfy(464,4): Error: assertion might not hold
 
 Dafny program verifier finished with 13 verified, 91 errors
-Total resources used is 738600
-Max resources used by VC is 76700
+Total resources used is 753600
+Max resources used by VC is 88100

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

@@ -3,4 +3,4 @@ git-issue-1163.dfy(21,42): Error: receiver argument could not be proved to be al
 git-issue-1163.dfy(23,44): Error: argument could not be proved to be allocated in the state in which the function is invoked
 git-issue-1163.dfy(27,40): Error: receiver argument could not be proved to be allocated in the state in which the function is invoked
 
-Dafny program verifier finished with 2 verified, 3 errors
+Dafny program verifier finished with 3 verified, 3 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/Apply.dfy.expect

@@ -1,7 +1,8 @@
 Apply.dfy(95,4): Error: assertion might not hold
 Apply.dfy(46,23): Error: function could not be proved to be allocated in the state in which the function is invoked
+Apply.dfy(57,29): Error: function could not be proved to be allocated in the state in which the function is invoked
 Apply.dfy(57,31): Error: argument could not be proved to be allocated in the state in which the function is invoked
+Apply.dfy(58,29): Error: function could not be proved to be allocated in the state in which the function is invoked
 Apply.dfy(58,31): Error: argument could not be proved to be allocated in the state in which the function is invoked
-Apply.dfy(61,31): Error: argument could not be proved to be allocated in the state in which the function is invoked
 
-Dafny program verifier finished with 7 verified, 5 errors
+Dafny program verifier finished with 7 verified, 6 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/SumSum.dfy

@@ -38,26 +38,10 @@ lemma Distribute(n: nat, f: int -> int, g: int -> int)
 {
 }
 
-lemma PrettyBasicBetaReduction(n: nat, g: (int,int) -> int, i: int)
+lemma {:induction false} PrettyBasicBetaReduction(n: nat, g: (int,int) -> int, i: int)
   ensures (x => Sum(n, y => g(x,y)))(i) == Sum(n, y => g(i,y))
 {
-  // NOTE: This proof is by induction on n
-  if n == 0 {
-    calc {
-      (x => Sum(n, y => g(x,y)))(i);
-      0;
-      Sum(n, y => g(i,y));
-    }
-  } else {
-    calc {
-      (x => Sum(n, y => g(x,y)))(i);
-      g(i,n-1) + (x => Sum(n-1, y => g(x,y)))(i);
-      { PrettyBasicBetaReduction(n-1, g, i); }
-      g(i,n-1) + Sum(n-1, y => g(i,y));
-      (y => g(i,y))(n-1) + Sum(n-1, y => g(i,y));
-      Sum(n, y => g(i,y));
-    }
-  }
+
 }
 
 lemma BetaReduction0(n: nat, g: (int,int) -> int, i: int)