fix: Use reveal_ constant as function argument in override axiom

Source/DafnyCore/AST/Grammar/Printer/Printer.cs

@@ -980,7 +980,7 @@ private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes,
       if (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhost) {
         bool verify = true;
         if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify) { return true; }
-        if (name.Contains("INTERNAL") || name.StartsWith("reveal_")) { return true; }
+        if (name.Contains("INTERNAL") || name.StartsWith(RevealStmt.RevealLemmaPrefix)) { return true; }
       }
       return false;
     }

Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs

@@ -235,7 +235,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
 
     DesugarElephantStatement(expectExtract, lhsExtract, firstType, resolver, (Method)resolutionContext.CodeContext);
     ResolvedStatements.ForEach(a => resolver.ResolveStatement(a, resolutionContext));
-    resolver.EnsureSupportsErrorHandling(Tok, firstType, expectExtract, KeywordToken != null);
+    resolver.EnsureSupportsErrorHandling(Tok, firstType, expectExtract, KeywordToken?.Token.val);
   }
 
   public void ResolveKeywordToken(INewOrOldResolver resolver, ResolutionContext resolutionContext) {

Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs

@@ -5,6 +5,8 @@
 namespace Microsoft.Dafny;
 
 public class RevealStmt : Statement, ICloneable<RevealStmt>, ICanFormat {
+  public const string RevealLemmaPrefix = "reveal_";
+
   public readonly List<Expression> Exprs;
   [FilledInDuringResolution] public readonly List<AssertLabel> LabeledAsserts = new List<AssertLabel>();  // to indicate that "Expr" denotes a labeled assertion
   [FilledInDuringResolution] public readonly List<Statement> ResolvedStatements = new List<Statement>();

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -2295,6 +2295,9 @@ void InheritedTraitMembers(TopLevelDeclWithMembers cl) {
         } else if (member.IsGhost != traitMember.IsGhost) {
           reporter.Error(MessageSource.Resolver, member.tok, "overridden {0} '{1}' in '{2}' has different ghost/compiled status than in trait '{3}'",
             traitMember.WhatKind, traitMember.Name, cl.Name, trait.Name);
+        } else if (!member.IsOpaque && traitMember.IsOpaque) {
+          reporter.Error(MessageSource.Resolver, member.tok, "overridden {0} '{1}' in '{2}' must be 'opaque' since the member is 'opaque' in trait '{3}'",
+            traitMember.WhatKind, traitMember.Name, cl.Name, trait.Name);
         } else {
           // Copy trait member's extern attribute onto class member if class does not provide one
           if (!Attributes.Contains(member.Attributes, "extern") && Attributes.Contains(traitMember.Attributes, "extern")) {
@@ -2949,7 +2952,7 @@ public Expression makeTemp(String prefix, AssignOrReturnStmt s, ResolutionContex
       return id;
     }
 
-    public void EnsureSupportsErrorHandling(IToken tok, Type tp, bool expectExtract, bool hasKeywordToken) {
+    public void EnsureSupportsErrorHandling(IToken tok, Type tp, bool expectExtract, [CanBeNull] string keyword) {
       // The "method not found" errors which will be generated here were already reported while
       // resolving the statement, so we don't want them to reappear and redirect them into a sink.
       var origReporter = reporter;
@@ -2959,23 +2962,22 @@ public void EnsureSupportsErrorHandling(IToken tok, Type tp, bool expectExtract,
       var propagateFailure = ResolveMember(tok, tp, "PropagateFailure", out _);
       var extract = ResolveMember(tok, tp, "Extract", out _);
 
-      if (hasKeywordToken) {
+      if (keyword != null) {
         if (isFailure == null || (extract != null) != expectExtract) {
           // more details regarding which methods are missing have already been reported by regular resolution
+          var requiredMembers = expectExtract
+            ? "functions 'IsFailure()' and 'Extract()'"
+            : "function 'IsFailure()', but not 'Extract()'";
           origReporter.Error(MessageSource.Resolver, tok,
-            "The right-hand side of ':-', which is of type '{0}', with a keyword token must have function{1}", tp,
-            expectExtract
-              ? "s 'IsFailure()' and 'Extract()'"
-              : " 'IsFailure()', but not 'Extract()'");
+            $"The right-hand side of ':- {keyword}', which is of type '{tp}', with a keyword token must have {requiredMembers}");
         }
       } else {
         if (isFailure == null || propagateFailure == null || (extract != null) != expectExtract) {
           // more details regarding which methods are missing have already been reported by regular resolution
-          origReporter.Error(MessageSource.Resolver, tok,
-            "The right-hand side of ':-', which is of type '{0}', must have function{1}", tp,
-            expectExtract
-              ? "s 'IsFailure()', 'PropagateFailure()', and 'Extract()'"
-              : "s 'IsFailure()' and 'PropagateFailure()', but not 'Extract()'");
+          var requiredMembers = expectExtract
+            ? "functions 'IsFailure()', 'PropagateFailure()', and 'Extract()'"
+            : "functions 'IsFailure()' and 'PropagateFailure()', but not 'Extract()'";
+          origReporter.Error(MessageSource.Resolver, tok, $"The right-hand side of ':-', which is of type '{tp}', must have {requiredMembers}");
         }
       }
 
@@ -2995,7 +2997,7 @@ void CheckIsFunction([CanBeNull] MemberDecl memberDecl, bool allowMethod) {
       }
 
       CheckIsFunction(isFailure, false);
-      if (!hasKeywordToken) {
+      if (keyword == null) {
         CheckIsFunction(propagateFailure, true);
       }
       if (expectExtract) {
@@ -3145,7 +3147,7 @@ public void ResolveLetOrFailExpr(LetOrFailExpr expr, ResolutionContext resolutio
       ResolveExpression(expr.ResolvedExpression, resolutionContext);
       expr.Type = expr.ResolvedExpression.Type;
       bool expectExtract = (expr.Lhs != null);
-      EnsureSupportsErrorHandling(expr.tok, PartiallyResolveTypeForMemberSelection(expr.tok, tempType), expectExtract, false);
+      EnsureSupportsErrorHandling(expr.tok, PartiallyResolveTypeForMemberSelection(expr.tok, tempType), expectExtract, null);
     }
 
     public static Type SelectAppropriateArrowTypeForFunction(Function function, Dictionary<TypeParameter, Type> subst, SystemModuleManager systemModuleManager) {

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs

@@ -189,7 +189,7 @@ protected override void PostVisitOneExpression(Expression expr, TypeInferenceChe
           ? e.Function.EnclosingClass.TypeArgs[i]
           : e.Function.TypeArgs[i - e.TypeApplication_AtEnclosingClass.Count];
         if (!IsDetermined(p.Normalize())) {
-          var hint = e.Name.StartsWith("reveal_")
+          var hint = e.Name.StartsWith(RevealStmt.RevealLemmaPrefix)
             ? ". If you are making an opaque function, make sure that the function can be called."
             : "";
           resolver.ReportError(ResolutionErrors.ErrorId.r_function_type_parameter_undetermined, e.tok,

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -3535,7 +3535,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
               var e = (ApplySuffix)expr;
               var methodCallInfo = ResolveApplySuffix(e, revealResolutionContext, true);
               if (methodCallInfo == null) {
-                reporter.Error(MessageSource.Resolver, expr.tok, "expression has no reveal lemma");
+                // error has already been reported
               } else if (methodCallInfo.Callee.Member is TwoStateLemma && !revealResolutionContext.IsTwoState) {
                 reporter.Error(MessageSource.Resolver, methodCallInfo.Tok, "a two-state function can only be revealed in a two-state context");
               } else if (methodCallInfo.Callee.AtLabel != null) {
@@ -4550,7 +4550,7 @@ public MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName
           if (memberName == "_ctor") {
             reporter.Error(MessageSource.Resolver, tok, "{0} {1} does not have an anonymous constructor", cd.WhatKind, cd.Name);
           } else {
-            reporter.Error(MessageSource.Resolver, tok, "member '{0}' does not exist in {2} '{1}'", memberName, cd.Name, cd.WhatKind);
+            ReportMemberNotFoundError(tok, memberName, cd);
           }
         } else if (!VisibleInScope(member)) {
           reporter.Error(MessageSource.Resolver, tok, "member '{0}' has not been imported in this scope and cannot be accessed here", memberName);
@@ -4567,6 +4567,31 @@ public MemberDecl ResolveMember(IToken tok, Type receiverType, string memberName
       return null;
     }
 
+    private void ReportMemberNotFoundError(IToken tok, string memberName, TopLevelDecl receiverDecl) {
+      if (memberName.StartsWith(RevealStmt.RevealLemmaPrefix)) {
+        var nameToBeRevealed = memberName[RevealStmt.RevealLemmaPrefix.Length..];
+        var members = receiverDecl is TopLevelDeclWithMembers topLevelDeclWithMembers ? GetClassMembers(topLevelDeclWithMembers) : null;
+        if (members == null) {
+          reporter.Error(MessageSource.Resolver, tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'");
+        } else if (!members.TryGetValue(nameToBeRevealed, out var member)) {
+          reporter.Error(MessageSource.Resolver, tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'");
+        } else if (member is not (ConstantField or Function)) {
+          Contract.Assert(!member.IsOpaque);
+          reporter.Error(MessageSource.Resolver, tok,
+            $"a {member.WhatKind} ('{nameToBeRevealed}') cannot be revealed; only opaque constants and functions can be revealed");
+        } else if (!member.IsOpaque) {
+          reporter.Error(MessageSource.Resolver, tok, $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it is not opaque");
+        } else if (member is Function { Body: null }) {
+          reporter.Error(MessageSource.Resolver, tok,
+            $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it has no body in {receiverDecl.WhatKind} '{receiverDecl.Name}'");
+        } else {
+          reporter.Error(MessageSource.Resolver, tok, $"cannot reveal '{nameToBeRevealed}'");
+        }
+      } else {
+        reporter.Error(MessageSource.Resolver, tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'");
+      }
+    }
+
     /// <summary>
     /// Roughly speaking, tries to figure out the head of the type of "t", making as few inference decisions as possible.
     /// More precisely, returns a type that contains all the members of "t"; or if "memberName" is non-null, a type
@@ -5301,7 +5326,7 @@ Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<Act
       // For 2 and 5:
       // For 3:
 
-      var name = resolutionContext.InReveal ? "reveal_" + expr.Name : expr.Name;
+      var name = resolutionContext.InReveal ? RevealStmt.RevealLemmaPrefix + expr.Name : expr.Name;
       v = scope.Find(name);
       if (v != null) {
         // ----- 0. local variable, parameter, or bound variable
@@ -5397,11 +5422,7 @@ Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<Act
       } else {
         // ----- None of the above
         if (complain) {
-          if (resolutionContext.InReveal) {
-            reporter.Error(MessageSource.Resolver, expr.tok, "cannot reveal '{0}' because no constant, assert label, or requires label in the current scope is named '{0}'", expr.Name);
-          } else {
-            reporter.Error(MessageSource.Resolver, expr.tok, "unresolved identifier: {0}", name);
-          }
+          ReportUnresolvedIdentifierError(expr.tok, expr.Name, resolutionContext);
         } else {
           expr.ResolvedExpression = null;
           return null;
@@ -5420,6 +5441,17 @@ Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<Act
       return rWithArgs;
     }
 
+    private void ReportUnresolvedIdentifierError(IToken tok, string name, ResolutionContext resolutionContext) {
+      if (resolutionContext.InReveal) {
+        var nameToReport = name.StartsWith(RevealStmt.RevealLemmaPrefix) ? name[RevealStmt.RevealLemmaPrefix.Length..] : name;
+        reporter.Error(MessageSource.Resolver, tok,
+          "cannot reveal '{0}' because no revealable constant, function, assert label, or requires label in the current scope is named '{0}'",
+          nameToReport);
+      } else {
+        reporter.Error(MessageSource.Resolver, tok, "unresolved identifier: {0}", name);
+      }
+    }
+
     public static Expression GetReceiver(TopLevelDeclWithMembers container, MemberDecl member, IToken token) {
       Expression receiver;
       token = new AutoGeneratedToken(token);
@@ -5631,7 +5663,7 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List<Actua
       Expression rWithArgs = null;  // the resolved expression after incorporating "args"
       MemberDecl member = null;
 
-      var name = resolutionContext.InReveal ? "reveal_" + expr.SuffixName : expr.SuffixName;
+      var name = resolutionContext.InReveal ? RevealStmt.RevealLemmaPrefix + expr.SuffixName : expr.SuffixName;
       if (!expr.Lhs.WasResolved()) {
         return null;
       }
@@ -5693,7 +5725,7 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List<Actua
             r = ResolveExprDotCall(expr.tok, receiver, null, member, args, expr.OptTypeArguments, resolutionContext, allowMethodCall);
           }
         } else {
-          reporter.Error(MessageSource.Resolver, expr.tok, "unresolved identifier: {0}", name);
+          ReportUnresolvedIdentifierError(expr.tok, name, resolutionContext);
         }
 
       } else if (lhs != null && lhs.Type is Resolver_IdentifierExpr.ResolverType_Type) {
@@ -5735,7 +5767,7 @@ Expression ResolveDotSuffix(ExprDotName expr, bool isLastNameSegment, List<Actua
           }
         }
         if (r == null) {
-          reporter.Error(MessageSource.Resolver, expr.tok, "member '{0}' does not exist in {2} '{1}'", name, ri.Decl.Name, ri.Decl.WhatKind);
+          ReportMemberNotFoundError(expr.tok, name, ri.Decl);
         }
       } else if (lhs != null) {
         // ----- 4. Look up name in the type of the Lhs