Remove function-context-height variable in Boogie encoding

Source/DafnyCore/DafnyPrelude.bpl

@@ -480,14 +480,6 @@ axiom (forall o: ORDINAL, m,n: int ::
     (0 <= m - n ==> ORD#Plus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Minus(o, ORD#FromNat(m-n))) &&
     (m - n <= 0 ==> ORD#Plus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Plus(o, ORD#FromNat(n-m))));
 
-// ---------------------------------------------------------------
-// -- Axiom contexts ---------------------------------------------
-// ---------------------------------------------------------------
-
-// used to make sure function axioms are not used while their consistency is being checked
-const $ModuleContextHeight: int;
-const $FunctionContextHeight: int;
-
 // ---------------------------------------------------------------
 // -- Layers of function encodings -------------------------------
 // ---------------------------------------------------------------

Source/DafnyCore/Prelude/PreludeCore.bpl

@@ -480,14 +480,6 @@ axiom (forall o: ORDINAL, m,n: int ::
     (0 <= m - n ==> ORD#Plus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Minus(o, ORD#FromNat(m-n))) &&
     (m - n <= 0 ==> ORD#Plus(ORD#Minus(o, ORD#FromNat(m)), ORD#FromNat(n)) == ORD#Plus(o, ORD#FromNat(n-m))));
 
-// ---------------------------------------------------------------
-// -- Axiom contexts ---------------------------------------------
-// ---------------------------------------------------------------
-
-// used to make sure function axioms are not used while their consistency is being checked
-const $ModuleContextHeight: int;
-const $FunctionContextHeight: int;
-
 // ---------------------------------------------------------------
 // -- Layers of function encodings -------------------------------
 // ---------------------------------------------------------------

Source/DafnyCore/Resolver/ExtremeLemmaChecks_Visitor.cs

@@ -11,26 +11,24 @@ public ExtremeLemmaChecks_Visitor(ModuleResolver resolver, ExtremeLemma context)
     this.context = context;
   }
   protected override void VisitOneStmt(Statement stmt) {
-    if (stmt is CallStmt) {
-      var s = (CallStmt)stmt;
-      if (s.Method is ExtremeLemma || s.Method is PrefixLemma) {
+    if (stmt is CallStmt callStmt) {
+      if (callStmt.Method is ExtremeLemma or PrefixLemma) {
         // all is cool
       } else {
         // the call goes from an extreme lemma context to a non-extreme-lemma callee
-        if (ModuleDefinition.InSameSCC(context, s.Method)) {
+        if (ModuleDefinition.InSameSCC(context, callStmt.Method)) {
           // we're looking at a recursive call (to a non-extreme-lemma)
-          resolver.reporter.Error(MessageSource.Resolver, s.Origin, "a recursive call from a {0} can go only to other {0}s and prefix lemmas", context.WhatKind);
+          resolver.reporter.Error(MessageSource.Resolver, callStmt.Origin, "a recursive call from a {0} can go only to other {0}s and prefix lemmas", context.WhatKind);
         }
       }
     }
   }
   protected override void VisitOneExpr(Expression expr) {
-    if (expr is FunctionCallExpr) {
-      var e = (FunctionCallExpr)expr;
+    if (expr is FunctionCallExpr callExpr) {
       // the call goes from a greatest lemma context to a non-greatest-lemma callee
-      if (ModuleDefinition.InSameSCC(context, e.Function)) {
+      if (ModuleDefinition.InSameSCC(context, callExpr.Function)) {
         // we're looking at a recursive call (to a non-greatest-lemma)
-        resolver.reporter.Error(MessageSource.Resolver, e.Origin, "a recursive call from a greatest lemma can go only to other greatest lemmas and prefix lemmas");
+        resolver.reporter.Error(MessageSource.Resolver, callExpr.Origin, "a recursive call from a greatest lemma can go only to other greatest lemmas and prefix lemmas");
       }
     }
   }

Source/DafnyCore/Resolver/FunctionEntanglementChecks_Visitor.cs

@@ -0,0 +1,37 @@
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Dafny;
+
+class FunctionEntanglementChecks_Visitor : ResolverBottomUpVisitor {
+  private readonly ICallable context;
+  public bool DoDecreasesChecks;
+  public FunctionEntanglementChecks_Visitor(ModuleResolver resolver, ICallable context)
+    : base(resolver) {
+    Contract.Requires(resolver != null);
+    Contract.Requires(context != null);
+    this.context = context;
+  }
+
+  protected override void VisitOneExpr(Expression expr) {
+    if (!DoDecreasesChecks && expr is MemberSelectExpr { Member: Function fn }) {
+      if (ModuleDefinition.InSameSCC(context, fn)) {
+        resolver.reporter.Error(MessageSource.Resolver, expr.Origin,
+          "cannot use naked function in recursive setting. Possible solution: eta expansion.");
+      }
+    }
+
+    if (DoDecreasesChecks && expr is FunctionCallExpr callExpr) {
+      if (ModuleDefinition.InSameSCC(context, callExpr.Function)) {
+        string msg;
+        if (context == callExpr.Function) {
+          msg = "a decreases clause is not allowed to call the enclosing function";
+        } else {
+          msg = $"the decreases clause of {context.WhatKind} '{context.NameRelativeToModule}' is not allowed to call '{callExpr.Function}', " +
+                "because they are mutually recursive";
+        }
+
+        resolver.reporter.Error(MessageSource.Resolver, callExpr.Origin, msg);
+      }
+    }
+  }
+}

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -1262,6 +1262,15 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
         FillInPostConditionsAndBodiesOfPrefixLemmas(declarations);
       }
 
+      // A function is not allowed to be used naked in its own SCC. Also, a function is not allowed to be used
+      // in any way inside a "decreases" clause its its own SCC.
+      foreach (var function in ModuleDefinition.AllFunctions(declarations)) {
+        var visitor = new FunctionEntanglementChecks_Visitor(this, function);
+        visitor.Visit(function);
+        visitor.DoDecreasesChecks = true;
+        visitor.Visit(function.Decreases.Expressions);
+      }
+
       // An inductive datatype is allowed to be defined as an empty type. For example, in
       //     predicate P(x: int) { false }
       //     type Subset = x: int | P(x) witness *

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -290,20 +290,6 @@ public Boogie.Expr ArbitraryValue(Type type) {
         }
       }
 
-      public Boogie.IdentifierExpr FunctionContextHeight() {
-        Contract.Ensures(Contract.Result<Boogie.IdentifierExpr>().Type != null);
-        return new Boogie.IdentifierExpr(Token.NoToken, "$FunctionContextHeight", Boogie.Type.Int);
-      }
-
-      public Boogie.Expr HeightContext(ICallable m) {
-        Contract.Requires(m != null);
-        // free requires fh == FunctionContextHeight;
-        var module = m.EnclosingModule;
-        Boogie.Expr context =
-          Boogie.Expr.Eq(Boogie.Expr.Literal(module.CallGraph.GetSCCRepresentativePredecessorCount(m)), FunctionContextHeight());
-        return context;
-      }
-
       public Expression GetSubstitutedBody(LetExpr e) {
         Contract.Requires(e != null);
         Contract.Requires(e.Exact);

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs

@@ -332,7 +332,6 @@ public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions,
           }
         case MemberSelectExpr selectExpr: {
             MemberSelectExpr e = selectExpr;
-            CheckFunctionSelectWF("naked function", builder, etran, e, " Possible solution: eta expansion.");
             CheckWellformed(e.Obj, wfOptions, locals, builder, etran);
             if (e.Obj.Type.IsRefType) {
               if (inBodyInitContext && Expression.AsThis(e.Obj) != null && !e.Member.IsInstanceIndependentConstant) {
@@ -681,8 +680,6 @@ public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions,
               CheckWellformed(e.Receiver, wfOptions, locals, builder, etran);
               if (!e.Function.IsStatic && !(e.Receiver is ThisExpr) && !e.Receiver.Type.IsArrowType) {
                 CheckNonNull(callExpr.Origin, e.Receiver, builder, etran, wfOptions.AssertKv);
-              } else if (e.Receiver.Type.IsArrowType) {
-                CheckFunctionSelectWF("function specification", builder, etran, e.Receiver, "");
               }
               if (!e.Function.IsStatic && !etran.UsesOldHeap) {
                 // the argument can't be assumed to be allocated for the old heap

Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs

@@ -37,15 +37,10 @@ public partial class BoogieGenerator {
   ///   forall args :: (QQQ k: nat :: P#[k](args)) ==> P(args)
   ///   forall args,k :: k == 0 ==> NNN P#[k](args)
   /// where "args" is "heap, formals".  In more details:
-  ///   AXIOM_ACTIVATION ==> forall args :: { P(args) } args-have-appropriate-values && P(args) ==> QQQ k { P#[k](args) } :: 0 ATMOST k HHH P#[k](args)
-  ///   AXIOM_ACTIVATION ==> forall args :: { P(args) } args-have-appropriate-values && (QQQ k :: 0 ATMOST k HHH P#[k](args)) ==> P(args)
-  ///   AXIOM_ACTIVATION ==> forall args,k :: args-have-appropriate-values && k == 0 ==> NNN P#0#[k](args)
-  ///   AXIOM_ACTIVATION ==> forall args,k,m :: args-have-appropriate-values && 0 ATMOST k LESS m ==> (P#[k](args) EEE P#[m](args))  (*)
-  /// where
-  /// AXIOM_ACTIVATION
-  /// means:
-  ///   mh LESS ModuleContextHeight ||
-  ///   (mh == ModuleContextHeight && fh ATMOST FunctionContextHeight)
+  ///   forall args :: { P(args) } args-have-appropriate-values && P(args) ==> QQQ k { P#[k](args) } :: 0 ATMOST k HHH P#[k](args)
+  ///   forall args :: { P(args) } args-have-appropriate-values && (QQQ k :: 0 ATMOST k HHH P#[k](args)) ==> P(args)
+  ///   forall args,k :: args-have-appropriate-values && k == 0 ==> NNN P#0#[k](args)
+  ///   forall args,k,m :: args-have-appropriate-values && 0 ATMOST k LESS m ==> (P#[k](args) EEE P#[m](args))  (*)
   /// There is also a specialized version of (*) for least predicates.
   /// </summary>
   void AddPrefixPredicateAxioms(PrefixPredicate pp) {
@@ -155,8 +150,6 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {
     funcID = new Bpl.IdentifierExpr(tok, pp.FullSanitizedName, TrType(pp.ResultType));
     var prefixAppl = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgs);
 
-    var activation = AxiomActivation(pp, etran);
-
     // forall args :: { P(args) } args-have-appropriate-values && P(args) ==> QQQ k { P#[k](args) } :: 0 ATMOST k HHH P#[k](args)
     var tr = BplTrigger(prefixAppl);
     var qqqK = pp.ExtremePred is GreatestPredicate
@@ -166,13 +159,11 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {
         kWhere == null ? prefixAppl : BplAnd(kWhere, prefixAppl));
     tr = BplTriggerHeap(this, tok, coAppl, pp.ReadsHeap ? null : h);
     var allS = new Bpl.ForallExpr(tok, bvs, tr, BplImp(BplAnd(ante, coAppl), qqqK));
-    sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, BplImp(activation, allS),
-      "1st prefix predicate axiom for " + pp.FullSanitizedName));
+    sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, allS, "1st prefix predicate axiom for " + pp.FullSanitizedName));
 
     // forall args :: { P(args) } args-have-appropriate-values && (QQQ k :: 0 ATMOST k HHH P#[k](args)) ==> P(args)
     allS = new Bpl.ForallExpr(tok, bvs, tr, BplImp(BplAnd(ante, qqqK), coAppl));
-    sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, BplImp(activation, allS),
-      "2nd prefix predicate axiom"));
+    sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, allS, "2nd prefix predicate axiom"));
 
     // forall args,k :: args-have-appropriate-values && k == 0 ==> NNN P#0#[k](args)
     var moreBvs = new List<Variable>();
@@ -188,8 +179,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {
 
     var trigger = BplTriggerHeap(this, prefixLimitedBody.tok, prefixLimitedBody, pp.ReadsHeap ? null : h);
     var trueAtZero = new Bpl.ForallExpr(tok, moreBvs, trigger, BplImp(BplAnd(ante, z), prefixLimited));
-    sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, BplImp(activation, trueAtZero),
-      "3rd prefix predicate axiom"));
+    sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, trueAtZero, "3rd prefix predicate axiom"));
 
 #if WILLING_TO_TAKE_THE_PERFORMANCE_HIT
       // forall args,k,m :: args-have-appropriate-values && 0 <= k <= m ==> (P#[k](args) EEE P#[m](args))
@@ -211,8 +201,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {
 
       var trigger2 = new Bpl.Trigger(tok, true, new List<Bpl.Expr> { prefixPred_K, prefixPred_M });
       var monotonicity = new Bpl.ForallExpr(tok, moreBvs, trigger2, BplImp(smaller, direction));
-      AddRootAxiom(new Bpl.Axiom(tok, BplImp(activation, monotonicity),
-        "prefix predicate monotonicity axiom"));
+      AddRootAxiom(new Bpl.Axiom(tok, monotonicity, "prefix predicate monotonicity axiom"));
 #endif
     // A more targeted monotonicity axiom used to increase the power of automation for proving the limit case for
     // least predicates that have more than one focal-predicate term.
@@ -237,8 +226,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) {
 
       var trigger3 = new Bpl.Trigger(tok, true, new List<Bpl.Expr> { prefixPred_K, kLessLimit, mLessLimit });
       var monotonicity = new Bpl.ForallExpr(tok, moreBvs, trigger3, BplImp(kLessM, direction));
-      sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, BplImp(activation, monotonicity),
-        "targeted prefix predicate monotonicity axiom"));
+      sink.AddTopLevelDeclaration(new Bpl.Axiom(tok, monotonicity, "targeted prefix predicate monotonicity axiom"));
     }
   }
 

Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs

@@ -188,8 +188,6 @@ void AddWellformednessCheck(ConstantField decl) {
 
       // the procedure itself
       var req = new List<Bpl.Requires>();
-      // free requires mh == ModuleContextHeight && fh == TypeContextHeight;
-      req.Add(FreeRequires(decl.Origin, etran.HeightContext(decl), null));
       foreach (var typeBoundAxiom in TypeBoundAxioms(decl.Origin, decl.EnclosingClass.TypeArgs)) {
         req.Add(FreeRequires(decl.Origin, typeBoundAxiom, null));
       }

Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs

@@ -372,13 +372,9 @@ private List<Variable> GetWellformednessProcedureOutParameters(Function f, Expre
 
     private List<Bpl.Requires> GetWellformednessProcedureRequires(Function f, ExpressionTranslator etran) {
       var requires = new List<Bpl.Requires>();
-      // free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
-      requires.Add(generator.FreeRequires(f.Origin, etran.HeightContext(f), null));
-
       foreach (var typeBoundAxiom in generator.TypeBoundAxioms(f.Origin, Concat(f.EnclosingClass.TypeArgs, f.TypeArgs))) {
         requires.Add(generator.Requires(f.Origin, true, null, typeBoundAxiom, null, null, null));
       }
-
       return requires;
     }
 

Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs

@@ -87,29 +87,16 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
     // return type and postconditions
     //
     // axiom  // consequence axiom
-    //   AXIOM_ACTIVATION
-    //   ==>
     //   (forall s, $Heap, formals ::                  // let args := $Heap,formals
     //       { f(s, args) }
-    //       f#canCall(args) || USE_VIA_CONTEXT
+    //       f#canCall(args)
     //       ==>
     //       ens &&
     //       OlderCondition &&
     //       f(s, args)-has-the-expected type);
     //
     // where:
     //
-    // AXIOM_ACTIVATION
-    // means:
-    //   fh <= FunctionContextHeight
-    //
-    // USE_VIA_CONTEXT
-    //   fh < FunctionContextHeight &&
-    //   GOOD_PARAMETERS
-    // where GOOD_PARAMETERS means:
-    //   $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
-    //   Pre($Heap,formals)
-    //
     // OlderCondition is added if the function has some 'older' parameters.
     //
     // Note, an antecedent $Heap[this,alloc] is intentionally left out:  including it would only weaken
@@ -233,10 +220,6 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
     foreach (AttributedExpression req in ConjunctsOf(f.Req)) {
       pre = BplAnd(pre, etran.TrExpr(req.E));
     }
-    // useViaContext: fh < FunctionContextHeight
-    Expr useViaContext = !(InVerificationScope(f) || (f.EnclosingClass is TraitDecl))
-      ? Bpl.Expr.True
-      : Bpl.Expr.Lt(Expr.Literal(forModule.CallGraph.GetSCCRepresentativePredecessorCount(f)), etran.FunctionContextHeight());
     // useViaCanCall: f#canCall(args)
     var canCallFuncID = new Bpl.IdentifierExpr(f.Origin, f.FullSanitizedName + "#canCall", Bpl.Type.Bool);
     var useViaCanCall = new Bpl.NAryExpr(f.Origin, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs, args));
@@ -268,10 +251,8 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
 
     Bpl.Expr axBody = BplImp(ante, post);
     Bpl.Expr ax = BplForall(f.Origin, new List<Bpl.TypeVariable>(), formals, null, tr, axBody);
-    var activate = AxiomActivation(f, etran);
     if (RemoveLit(axBody) != Bpl.Expr.True) {
-      AddOtherDefinition(boogieFunction, new Bpl.Axiom(f.Origin, BplImp(activate, ax),
-        "consequence axiom for " + f.FullSanitizedName));
+      AddOtherDefinition(boogieFunction, new Bpl.Axiom(f.Origin, ax, "consequence axiom for " + f.FullSanitizedName));
     }
 
     if (f.ResultType.MayInvolveReferences) {
@@ -289,8 +270,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
         ax = BplForall(f.Origin, new List<Bpl.TypeVariable>(), formals, null, BplTrigger(whr), axBody);
 
         if (RemoveLit(axBody) != Bpl.Expr.True) {
-          var comment = "alloc consequence axiom for " + f.FullSanitizedName;
-          var allocConsequenceAxiom = new Bpl.Axiom(f.Origin, BplImp(activate, ax), comment);
+          var allocConsequenceAxiom = new Bpl.Axiom(f.Origin, ax, "alloc consequence axiom for " + f.FullSanitizedName);
           AddOtherDefinition(boogieFunction, allocConsequenceAxiom);
         }
       }
@@ -310,33 +290,13 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
     // This method generates the Definition Axiom, suitably modified according to the optional "lits".
     //
     // axiom  // definition axiom
-    //   AXIOM_ACTIVATION
-    //   ==>
     //   (forall s, $Heap, formals ::                  // let args := $Heap,formals
     //       { f(Succ(s), args) }                      // (*)
-    //       (f#canCall(args) || USE_VIA_CONTEXT)
+    //       f#canCall(args)
     //       ==>
     //       BODY-can-make-its-calls &&
     //       f(Succ(s), args) == BODY);                // (*)
     //
-    // where:
-    //
-    // AXIOM_ACTIVATION
-    // for visibility==ForeignModuleOnly, means:
-    //   true
-    // for visibility==IntraModuleOnly, means:
-    //   fh <= FunctionContextHeight
-    //
-    // USE_VIA_CONTEXT
-    // for visibility==ForeignModuleOnly, means:
-    //   GOOD_PARAMETERS
-    // for visibility==IntraModuleOnly, means:
-    //   fh < FunctionContextHeight &&
-    //   GOOD_PARAMETERS
-    // where GOOD_PARAMETERS means:
-    //   $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
-    //   Pre($Heap,formals)
-    //
     // NOTE: this is lifted out to a #requires function for intra module calls,
     //       and used in the function pseudo-handles for top level functions.
     //       For body-less functions, this is emitted when body is null.
@@ -609,7 +569,6 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
 
     Bpl.Expr ax = BplForall(f.Origin, new List<Bpl.TypeVariable>(), forallFormals, kv, tr,
       BplImp(ante, tastyVegetarianOption));
-    var activate = AxiomActivation(f, etran);
     string comment;
     comment = "definition axiom for " + f.FullSanitizedName;
     if (lits != null) {
@@ -625,7 +584,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
     } else {
       comment += " (opaque)";
     }
-    var axe = new Axiom(f.Origin, BplImp(activate, ax), comment) {
+    var axe = new Axiom(f.Origin, ax, comment) {
       CanHide = true
     };
     if (proofDependencies == null) {

Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs

@@ -79,10 +79,6 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) {
       var mod = new List<Bpl.IdentifierExpr>();
       var ens = new List<Bpl.Ensures>();
       // FREE PRECONDITIONS
-      if (kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation) {  // the other cases have no need for a free precondition
-        // free requires mh == ModuleContextHeight && fh = FunctionContextHeight;
-        req.Add(FreeRequires(iter.Origin, etran.HeightContext(iter), null));
-      }
       mod.Add(etran.HeapCastToIdentifierExpr);
 
       if (kind != MethodTranslationKind.SpecWellformedness) {