Fix: Ability to cast a datatype to its trait when overriding functions

Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs

@@ -569,6 +569,8 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis
     }
   }
 
+  private int Cutoff = 0;
+
   /// <summary>
   /// The list of formals "lits" is allowed to contain an object of type ThisSurrogate, which indicates that
   /// the receiver parameter of the function should be included among the lit formals.
@@ -876,9 +878,13 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List<Formal> lits) {
       }
 
       var etranBody = layer == null ? etran : etran.LimitedFunctions(f, ly);
-      var trbody = etranBody.TrExpr(bodyWithSubst);
+      // Traits as datatypes might require boxing
+      var conclusion = etranBody.TrExpr(new BinaryExpr(f.tok, BinaryExpr.ResolvedOpcode.EqCommon,
+        new BoogieWrapper(funcAppl, f.ResultType), bodyWithSubst
+      ) { RangeToken = f.RangeToken });
+
       tastyVegetarianOption = BplAnd(etranBody.CanCallAssumption(bodyWithSubst),
-        BplAnd(TrFunctionSideEffect(bodyWithSubst, etranBody), Bpl.Expr.Eq(funcAppl, trbody)));
+        BplAnd(TrFunctionSideEffect(bodyWithSubst, etranBody), conclusion));
     }
 
     QKeyValue kv = null;

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -1094,7 +1094,7 @@ private void AddFunctionOverrideEnsChk(Function f, BoogieStmtListBuilder builder
       //generating trait post-conditions with class variables
       FunctionCallSubstituter sub = null;
       foreach (var en in f.OverriddenFunction.Ens) {
-        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (ClassLikeDecl)f.EnclosingClass);
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)f.EnclosingClass);
         foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) {
           builder.Add(Assert(f.tok, s.E, new PODesc.FunctionContractOverride(true)));
         }
@@ -1135,7 +1135,7 @@ private void AddFunctionOverrideSubsetChk(Function func, BoogieStmtListBuilder b
       List<FrameExpression> traitFrameExps = new List<FrameExpression>();
       FunctionCallSubstituter sub = null;
       foreach (var e in func.OverriddenFunction.Reads.Expressions) {
-        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)func.OverriddenFunction.EnclosingClass, (ClassLikeDecl)func.EnclosingClass);
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)func.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)func.EnclosingClass);
         var newE = sub.Substitute(e.E);
         FrameExpression fe = new FrameExpression(e.tok, newE, e.FieldName);
         traitFrameExps.Add(fe);
@@ -1182,7 +1182,7 @@ private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builde
       //generating trait pre-conditions with class variables
       FunctionCallSubstituter sub = null;
       foreach (var req in f.OverriddenFunction.Req) {
-        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (ClassLikeDecl)f.EnclosingClass);
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)f.OverriddenFunction.EnclosingClass, (TopLevelDeclWithMembers)f.EnclosingClass);
         builder.Add(TrAssumeCmdWithDependencies(etran, f.tok, sub.Substitute(req.E), "overridden function requires clause"));
       }
       //generating class pre-conditions
@@ -1425,7 +1425,7 @@ private void AddMethodOverrideEnsChk(Method m, BoogieStmtListBuilder builder, Ex
       //generating trait post-conditions with class variables
       FunctionCallSubstituter sub = null;
       foreach (var en in m.OverriddenMethod.Ens) {
-        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassLikeDecl)m.EnclosingClass);
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (TopLevelDeclWithMembers)m.EnclosingClass);
         foreach (var s in TrSplitExpr(sub.Substitute(en.E), etran, false, out _).Where(s => s.IsChecked)) {
           builder.Add(Assert(m.RangeToken, s.E, new PODesc.EnsuresStronger()));
         }
@@ -1442,7 +1442,7 @@ private void AddMethodOverrideReqsChk(Method m, BoogieStmtListBuilder builder, E
       //generating trait pre-conditions with class variables
       FunctionCallSubstituter sub = null;
       foreach (var req in m.OverriddenMethod.Req) {
-        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (ClassLikeDecl)m.EnclosingClass);
+        sub ??= new FunctionCallSubstituter(substMap, typeMap, (TraitDecl)m.OverriddenMethod.EnclosingClass, (TopLevelDeclWithMembers)m.EnclosingClass);
         builder.Add(TrAssumeCmdWithDependencies(etran, m.tok, sub.Substitute(req.E), "overridden requires clause"));
       }
       //generating class pre-conditions

Source/DafnyCore/Verifier/FunctionCallSubstituter.cs

@@ -4,13 +4,13 @@
 namespace Microsoft.Dafny {
   public class FunctionCallSubstituter : Substituter {
     public readonly TraitDecl Tr;
-    public readonly ClassLikeDecl Cl;
+    public readonly TopLevelDeclWithMembers Cl;
 
     // We replace all occurrences of the trait version of the function with the class version. This is only allowed if
     // the receiver is `this`. We underapproximate this by looking for a `ThisExpr`, which misses more complex
     // expressions that evaluate to one.
     public FunctionCallSubstituter(Dictionary<IVariable, Expression /*!*/> /*!*/ substMap, Dictionary<TypeParameter, Type> typeMap,
-      TraitDecl parentTrait, ClassLikeDecl cl)
+      TraitDecl parentTrait, TopLevelDeclWithMembers cl)
       : base(new ThisExpr(cl.tok) { Type = UserDefinedType.FromTopLevelDecl(cl.tok, cl) }, substMap, typeMap) {
       this.Tr = parentTrait;
       this.Cl = cl;

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect

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

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

@@ -0,0 +1,11 @@
+// RUN: %baredafny verify %args --type-system-refresh --general-traits=datatype "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait Test<T> {
+  function Cast(t: T): Test<T>
+}
+
+datatype Impl extends Test<Impl> = ImplConstructor()
+{
+  function Cast(t: Impl): Test<Impl> { t }
+}

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

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

docs/dev/news/4823.fix

@@ -0,0 +1 @@
+Ability to cast a datatype to its trait when overriding functions