fix: Cross-modular override check

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

@@ -213,7 +213,8 @@ private void AddAllocationAxiom(Boogie.Declaration fieldDeclaration, Field f, To
         AddWellformednessCheck(cf);
         if (InVerificationScope(cf)) {
           var etran = new ExpressionTranslator(this, predef, f.tok);
-          heightAntecedent = Bpl.Expr.Lt(Bpl.Expr.Literal(cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf) * 2 + 1), etran.FunctionContextHeight());
+          var visibilityLevel = cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf);
+          heightAntecedent = Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight());
         }
       }
 
@@ -877,7 +878,7 @@ private void AddFunctionOverrideCheckImpl(Function f) {
       }
       // the procedure itself
       var req = new List<Boogie.Requires>();
-      // free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
+      // free requires fh == FunctionContextHeight;
       req.Add(Requires(f.tok, true, etran.HeightContext(f.OverriddenFunction, true), null, null));
       if (f is TwoStateFunction) {
         // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap)
@@ -945,7 +946,6 @@ private void AddFunctionOverrideCheckImpl(Function f) {
       AddFunctionOverrideSubsetChk(f, builder, etran, localVariables, substMap, typeMap);
 
       //adding assume Q;
-      //adding assume J.F(ins) == C.F(ins);
       //assert Post’;
       AddFunctionOverrideEnsChk(f, builder, etran, substMap, typeMap, implInParams, implOutParams.Count == 0 ? null : implOutParams[0]);
 

Source/DafnyCore/Verifier/Translator.ExpressionTranslator.cs

@@ -261,9 +261,8 @@ public Boogie.IdentifierExpr FunctionContextHeight() {
       public Boogie.Expr HeightContext(ICallable m, bool reducedScope = false) {
         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) * 2 + (reducedScope ? 0 : 1)), FunctionContextHeight());
+        var visibilityLevel = m.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(m);
+        Boogie.Expr context = Boogie.Expr.Eq(MkFunctionHeight(visibilityLevel, reducedScope), FunctionContextHeight());
         return context;
       }
 

Source/DafnyCore/Verifier/Translator.cs

@@ -2053,7 +2053,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
       //   (mh == ModuleContextHeight && fh <= FunctionContextHeight)
       //
       // USE_VIA_CONTEXT
-      //   (mh != ModuleContextHeight || fh != FunctionContextHeight) &&
+      //   fh < FunctionContextHeight &&
       //   GOOD_PARAMETERS
       // where GOOD_PARAMETERS means:
       //   $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
@@ -2157,8 +2157,8 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
         pre = BplAnd(pre, etran.TrExpr(Substitute(req.E, null, substMap)));
       }
       // useViaContext: fh < FunctionContextHeight
-      var lowerBound = (f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f) + 1) * 2;
-      Expr useViaContext = !InVerificationScope(f) ? Bpl.Expr.True : Expr.Le(Expr.Literal(lowerBound), etran.FunctionContextHeight());
+      var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f);
+      Expr useViaContext = !InVerificationScope(f) ? Bpl.Expr.True : Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight());
       // useViaCanCall: f#canCall(args)
       Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName + "#canCall", Bpl.Type.Bool);
       Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), Concat(tyargs, args));
@@ -2253,15 +2253,14 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
       return (olderParameterCount, olderCondition);
     }
 
-    Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran, bool hidden = false) {
+    Bpl.Expr AxiomActivation(Function f, ExpressionTranslator etran, bool requiresFullScope = false) {
       Contract.Requires(f != null);
       Contract.Requires(etran != null);
       Contract.Requires(VisibleInScope(f));
-      var module = f.EnclosingClass.EnclosingModuleDefinition;
 
       if (InVerificationScope(f)) {
-        var lowerBound = module.CallGraph.GetSCCRepresentativePredecessorCount(f) * 2 + (hidden ? 1 : 0);
-        return Expr.Le(Expr.Literal(lowerBound), etran.FunctionContextHeight());
+        var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f);
+        return Expr.Le(MkFunctionHeight(visibilityLevel, !requiresFullScope), etran.FunctionContextHeight());
       } else {
         return Bpl.Expr.True;
       }
@@ -2301,7 +2300,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
       // for visibility==ForeignModuleOnly, means:
       //   GOOD_PARAMETERS
       // for visibility==IntraModuleOnly, means:
-      //   fh != FunctionContextHeight &&
+      //   fh < FunctionContextHeight &&
       //   GOOD_PARAMETERS
       // where GOOD_PARAMETERS means:
       //   $IsGoodHeap($Heap) && this != null && formals-have-the-expected-types &&
@@ -2506,12 +2505,11 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
         return null;
       }
 
-      // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight)
-      ModuleDefinition mod = f.EnclosingClass.EnclosingModuleDefinition;
+      // useViaContext: fh < FunctionContextHeight
+      var visibilityLevel = f.EnclosingClass.EnclosingModuleDefinition.CallGraph.GetSCCRepresentativePredecessorCount(f);
       Bpl.Expr useViaContext = !InVerificationScope(f)
-        ? (Bpl.Expr)Bpl.Expr.True
-        : Bpl.Expr.Le(Bpl.Expr.Literal((mod.CallGraph.GetSCCRepresentativePredecessorCount(f) + 1) * 2),
-          etran.FunctionContextHeight());
+        ? Bpl.Expr.True
+        : Bpl.Expr.Lt(MkFunctionHeight(visibilityLevel), etran.FunctionContextHeight());
       // ante := (useViaContext && typeAnte && pre)
       ante = BplAnd(useViaContext, BplAnd(ante, pre));
 
@@ -3488,7 +3486,7 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder
       //generating assume C.F(ins) == out, if a result variable was given
       if (resultVariable != null) {
         var funcIdC = new FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullSanitizedName, TrType(f.ResultType)));
-        List<Expr> argsC = new List<Expr>();
+        var argsC = new List<Bpl.Expr>();
 
         // add type arguments
         argsC.AddRange(GetTypeArguments(f, null).ConvertAll(TypeToTy));
@@ -3508,9 +3506,9 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder
 
         argsC.AddRange(implInParams.Select(var => new Bpl.IdentifierExpr(f.tok, var)));
 
-        Expr funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
+        var funcExpC = new Bpl.NAryExpr(f.tok, funcIdC, argsC);
         var resultVar = new Bpl.IdentifierExpr(resultVariable.tok, resultVariable);
-        builder.Add(TrAssumeCmd(f.tok, Expr.Eq(funcExpC, resultVar)));
+        builder.Add(TrAssumeCmd(f.tok, Bpl.Expr.Eq(funcExpC, resultVar)));
       }
 
       //generating trait post-conditions with class variables
@@ -10722,6 +10720,14 @@ List<Variable> MkTyParamFormals(List<TypeParameter> args, bool includeWhereClaus
       return null;
     }
 
+    // We use the $FunctionContextHeight to restrict the applicability of certain axioms. The entity at the end of a
+    // dependency chain has the highest number. To get more granular control over the visibility, we extend every
+    // visibility level by a precursory intermediate level. This additional level is helpful for proofs that would be
+    // disturbed by axioms that are visible the the final level.
+    static Bpl.Expr MkFunctionHeight(int visibilityLevel, bool intermediateScope = false) {
+      return Expr.Literal(visibilityLevel * 2 + (intermediateScope ? 0 : 1));
+    }
+
     public static void MapM<A>(IEnumerable<A> xs, Action<A> K) {
       Contract.Requires(xs != null);
       Contract.Requires(K != null);

Test/git-issues/git-issue-2500.dfy

@@ -0,0 +1,22 @@
+// RUN: %dafny_0 /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module A {
+  trait {:termination false} Trait {
+    function TotallyNotZero() : (ret: int)
+      ensures ret != 0
+  }
+}
+
+module B {
+  import opened A
+
+  class Class extends Trait {
+    constructor() {}
+    function TotallyNotZero() : (ret: int)
+      // Missing: ensures ret != 0
+    { 
+      0 
+    }
+  }
+}

Test/git-issues/git-issue-2500.dfy.expect

@@ -0,0 +1,3 @@
+git-issue-2500.dfy(16,13): Error: the function must provide an equal or more detailed postcondition than in its parent trait
+
+Dafny program verifier finished with 1 verified, 1 error

docs/dev/news/3223.fix

@@ -0,0 +1 @@
+To ensure that a `class` correctly implements a `trait`, we perform an override check. This check was previously faulty across `module`s, but works unconditionally now.