feat: Support for the {:opaque} attibute on const

RELEASE_NOTES.md

@@ -1,5 +1,8 @@
 # Upcoming
 
+- feat: Support for the `{:opaque}` attibute on `const`
+
+
 # 3.8.0
 
 - fix: Use the right bitvector comparison in decrease checks
@@ -22,12 +25,14 @@
 - fix: Perform well-definedness checks for ensures clauses of forall statements (https://github.com/dafny-lang/dafny/pull/2606)
 - fix: Resolution and verification of StmtExpr now pay attention to if the StmtExpr is inside an 'old' (https://github.com/dafny-lang/dafny/pull/2607)
 
+
 # 3.7.3
 
 - feat: *Less code navigation when verifying code*: In the IDE, failing postconditions and preconditions error messages now immediately display the sub-conditions that Dafny could not prove. Both on hover and in the Problems window. (https://github.com/dafny-lang/dafny/pull/2434)
 - feat: Whitespaces and comments are kept in relevant parts of the AST (https://github.com/dafny-lang/dafny/pull/1801)
 - fix: NuGet packages no longer depend on specific patch releases of the .NET frameworks.
 
+
 # 3.7.2
 
 - fix: Hovering over variables and methods inside cases of nested match statements work again. (https://github.com/dafny-lang/dafny/pull/2334)
@@ -39,11 +44,13 @@
 - fix: Correctly infer type of numeric arguments, where the type is a subset type of a newtype. (https://github.com/dafny-lang/dafny/pull/2314)
 - fix: Fix concurrency bug that sometimes led to an exception during the production of verification logs. (https://github.com/dafny-lang/dafny/pull/2398)
 
+
 # 3.7.1
 
 - fix: The Dafny runtime library for C# is now compatible with .NET Standard 2.1, as it was before 3.7.0. Its version has been updated to 1.2.0 to reflect this. (https://github.com/dafny-lang/dafny/pull/2277)
 - fix: Methods produced by the test generation code can now be compiled directly to C# XUnit tests (https://github.com/dafny-lang/dafny/pull/2269)
 
+
 # 3.7.0
 
 - feat: The Dafny CLI, Dafny as a library, and the C# runtime are now available on NuGet. You can install the CLI with `dotnet tool install --global Dafny`. The library is available as `DafnyPipeline` and the runtime is available as `DafnyRuntime`. (https://github.com/dafny-lang/dafny/pull/2051)
@@ -57,6 +64,7 @@
 - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080)
 - fix: Various improvements to language server robustness (https://github.com/dafny-lang/dafny/pull/2254)
 
+
 # 3.6.0
 
 - feat: The `synthesize` attribute on methods with no body allows synthesizing objects based on method postconditions at compile time (currently only available for C#). See Section [22.2.20](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-synthesize-attr) of the Reference Manual. (https://github.com/dafny-lang/dafny/pull/1809)

Source/Dafny/Resolver.cs

@@ -418,7 +418,7 @@ public void ResolveProgram(Program prog) {
       refinementTransformer = new RefinementTransformer(prog);
       rewriters.Add(refinementTransformer);
       rewriters.Add(new AutoContractsRewriter(reporter, builtIns));
-      rewriters.Add(new OpaqueFunctionRewriter(this.reporter));
+      rewriters.Add(new OpaqueMemberRewriter(this.reporter));
       rewriters.Add(new AutoReqFunctionRewriter(this.reporter));
       rewriters.Add(new TimeLimitRewriter(reporter));
       rewriters.Add(new ForallStmtRewriter(reporter));
@@ -11100,6 +11100,21 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
                 var call = new CallStmt(methodCallInfo.Tok, s.EndTok, new List<Expression>(), methodCallInfo.Callee, methodCallInfo.ActualParameters);
                 s.ResolvedStatements.Add(call);
               }
+            } else if (expr is NameSegment or ExprDotName) {
+              if (expr is NameSegment) {
+                ResolveNameSegment((NameSegment)expr, true, null, revealResolutionContext, true);
+              } else {
+                ResolveDotSuffix((ExprDotName)expr, true, null, revealResolutionContext, true);
+              }
+              MemberSelectExpr callee = (MemberSelectExpr)((ConcreteSyntaxExpression)expr).ResolvedExpression;
+              if (callee == null) {
+              } else if (callee.Member is Lemma or TwoStateLemma && Attributes.Contains(callee.Member.Attributes, "axiom")) {
+                //The revealed member is a function
+                reporter.Error(MessageSource.Resolver, callee.tok, "to reveal a function ({0}), append parentheses", callee.Member.ToString().Substring(7));
+              } else {
+                var call = new CallStmt(expr.tok, s.EndTok, new List<Expression>(), callee, new List<ActualBinding>());
+                s.ResolvedStatements.Add(call);
+              }
             } else {
               ResolveExpression(expr, revealResolutionContext);
             }

Source/Dafny/Rewriter.cs

@@ -4,6 +4,7 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
 
 namespace Microsoft.Dafny {
   /// <summary>
@@ -970,17 +971,16 @@ void AddHoverText(IToken tok, string format, params object[] args) {
     }
   }
 
-
   /// <summary>
   /// For any function foo() with the :opaque attribute,
   /// hide the body, so that it can only be seen within its
   /// recursive clique (if any), or if the programmer
   /// specifically asks to see it via the reveal_foo() lemma
   /// </summary>
-  public class OpaqueFunctionRewriter : IRewriter {
+  public class OpaqueMemberRewriter : IRewriter {
     protected Dictionary<Method, Function> revealOriginal; // Map reveal_* lemmas (or two-state lemmas) back to their original functions
 
-    public OpaqueFunctionRewriter(ErrorReporter reporter)
+    public OpaqueMemberRewriter(ErrorReporter reporter)
       : base(reporter) {
       Contract.Requires(reporter != null);
 
@@ -990,17 +990,17 @@ public OpaqueFunctionRewriter(ErrorReporter reporter)
     internal override void PreResolve(ModuleDefinition m) {
       foreach (var d in m.TopLevelDecls) {
         if (d is TopLevelDeclWithMembers) {
-          ProcessOpaqueClassFunctions((TopLevelDeclWithMembers)d);
+          ProcessOpaqueClassMembers((TopLevelDeclWithMembers)d);
         }
       }
     }
 
     internal override void PostResolveIntermediate(ModuleDefinition m) {
       foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
-        if (decl is Lemma || decl is TwoStateLemma) {
+        if (decl is Lemma or TwoStateLemma) {
           var lem = (Method)decl;
           if (revealOriginal.ContainsKey(lem)) {
-            Function fn = revealOriginal[lem];
+            var fn = revealOriginal[lem];
             AnnotateRevealFunction(lem, fn);
           }
         }
@@ -1043,68 +1043,83 @@ protected void AnnotateRevealFunction(Method lemma, Function f) {
 
 
     // Tells the function to use 0 fuel by default
-    protected void ProcessOpaqueClassFunctions(TopLevelDeclWithMembers c) {
+    protected void ProcessOpaqueClassMembers(TopLevelDeclWithMembers c) {
       Contract.Requires(c != null);
-      List<MemberDecl> newDecls = new List<MemberDecl>();
-      foreach (MemberDecl member in c.Members) {
-        if (member is Function function) {
-          if (!Attributes.Contains(function.Attributes, "opaque")) {
-            // Nothing to do
-          } else if (!RefinementToken.IsInherited(function.tok, c.EnclosingModuleDefinition)) {
-            RewriteOpaqueFunctionUseFuel(function, newDecls);
-          }
+      var newDecls = new List<MemberDecl>();
+      foreach (var member in c.Members.Where(member => member is Function or ConstantField)) {
+        if (!Attributes.Contains(member.Attributes, "opaque")) {
+          // Nothing to do
+        } else if (!RefinementToken.IsInherited(member.tok, c.EnclosingModuleDefinition)) {
+          GenerateRevealLemma(member, newDecls);
         }
       }
       c.Members.AddRange(newDecls);
     }
 
-    private void RewriteOpaqueFunctionUseFuel(Function f, List<MemberDecl> newDecls) {
-      // mark the opaque function with {:fuel 0, 0}
-      LiteralExpr amount = new LiteralExpr(f.tok, 0);
-      f.Attributes = new Attributes("fuel", new List<Expression>() { amount, amount }, f.Attributes);
+    private void GenerateRevealLemma(MemberDecl m, List<MemberDecl> newDecls) {
+      if (m is Function f) {
+        // mark the opaque function with {:fuel 0, 0}
+        var amount = new LiteralExpr(m.tok, 0);
+        m.Attributes = new Attributes("fuel", new List<Expression>() { amount, amount }, m.Attributes);
+
+        // That is, given:
+        //   function {:opaque} foo(x:int, y:int) : int
+        //     requires 0 <= x < 5;
+        //     requires 0 <= y < 5;
+        //     ensures foo(x, y) < 10;
+        //   { x + y }
+        // We produce:
+        //   lemma {:axiom} {:auto_generated} {:fuel foo, 1, 2 } reveal_foo()
+        //
+        // If "foo" is a two-state function, then "reveal_foo" will be declared as a two-state lemma.
+        //
+        // The translator, in AddMethod, then adds ensures clauses to bump up the fuel parameters appropriately
+
+        var cloner = new Cloner();
+
+        List<TypeParameter> typeVars = new List<TypeParameter>();
+        List<Type> optTypeArgs = new List<Type>();
+        foreach (var tp in f.TypeArgs) {
+          typeVars.Add(cloner.CloneTypeParam(tp));
+          // doesn't matter what type, just so we have it to make the resolver happy when resolving function member of
+          // the fuel attribute. This might not be needed after fixing codeplex issue #172.
+          optTypeArgs.Add(new IntType());
+        }
+      }
 
-      // That is, given:
-      //   function {:opaque} foo(x:int, y:int) : int
-      //     requires 0 <= x < 5;
-      //     requires 0 <= y < 5;
-      //     ensures foo(x, y) < 10;
-      //   { x + y }
+      // Given:
+      //   const {:opaque} foo := x
       // We produce:
-      //   lemma {:axiom} {:auto_generated} {:fuel foo, 1, 2 } reveal_foo()
-      //
-      // If "foo" is a two-state function, then "reveal_foo" will be declared as a two-state lemma.
-      //
-      // The translator, in AddMethod, then adds ensures clauses to bump up the fuel parameters appropriately
-
-      var cloner = new Cloner();
-
-      List<TypeParameter> typeVars = new List<TypeParameter>();
-      List<Type> optTypeArgs = new List<Type>();
-      foreach (TypeParameter tp in f.TypeArgs) {
-        typeVars.Add(cloner.CloneTypeParam(tp));
-        // doesn't matter what type, just so we have it to make the resolver happy when resolving function member of
-        // the fuel attribute. This might not be needed after fixing codeplex issue #172.
-        optTypeArgs.Add(new IntType());
-      }
+      //   lemma {:auto_generated} {:opaque_reveal} {:verify false} reveal_foo()
+      //     ensures foo == x
 
       // Add an axiom attribute so that the compiler won't complain about the lemma's lack of a body
-      Attributes lemma_attrs = BuiltIns.AxiomAttribute();
+      Attributes lemma_attrs = null;
+      if (m is Function) {
+        lemma_attrs = new Attributes("axiom", new List<Expression>(), lemma_attrs);
+      }
       lemma_attrs = new Attributes("auto_generated", new List<Expression>(), lemma_attrs);
       lemma_attrs = new Attributes("opaque_reveal", new List<Expression>(), lemma_attrs);
-      lemma_attrs = new Attributes("verify", new List<Expression>() { new LiteralExpr(f.tok, false) }, lemma_attrs);
+      lemma_attrs = new Attributes("verify", new List<Expression>() { new LiteralExpr(m.tok, false) }, lemma_attrs);
+      var ens = new List<AttributedExpression>();
+      if (m is ConstantField c && c.Rhs != null) {
+        ens.Add(new AttributedExpression(new BinaryExpr(c.tok, BinaryExpr.Opcode.Eq, new NameSegment(c.Tok, c.Name, null), c.Rhs)));
+      }
       Method reveal;
-      if (f is TwoStateFunction) {
-        reveal = new TwoStateLemma(f.tok, "reveal_" + f.Name, f.HasStaticKeyword, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<AttributedExpression>(),
-          new Specification<FrameExpression>(new List<FrameExpression>(), null), /* newEnsuresList*/new List<AttributedExpression>(),
+      if (m is TwoStateFunction) {
+        reveal = new TwoStateLemma(m.tok, "reveal_" + m.Name, m.HasStaticKeyword, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<AttributedExpression>(),
+          new Specification<FrameExpression>(new List<FrameExpression>(), null), ens,
           new Specification<Expression>(new List<Expression>(), null), null, lemma_attrs, null);
       } else {
-        reveal = new Lemma(f.tok, "reveal_" + f.Name, f.HasStaticKeyword, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<AttributedExpression>(),
-          new Specification<FrameExpression>(new List<FrameExpression>(), null), /* newEnsuresList*/new List<AttributedExpression>(),
+        reveal = new Lemma(m.tok, "reveal_" + m.Name, m.HasStaticKeyword, new List<TypeParameter>(), new List<Formal>(), new List<Formal>(), new List<AttributedExpression>(),
+          new Specification<FrameExpression>(new List<FrameExpression>(), null), ens,
           new Specification<Expression>(new List<Expression>(), null), null, lemma_attrs, null);
       }
       newDecls.Add(reveal);
-      revealOriginal[reveal] = f;
-      reveal.InheritVisibility(f, true);
+      reveal.InheritVisibility(m, true);
+      if (m is Function fn) {
+        revealOriginal[reveal] = fn;
+      }
     }
   }
 

Source/Dafny/Verifier/Translator.cs

@@ -1535,9 +1535,9 @@ public Bpl.Expr GetArrayIndexFieldName(IToken tok, List<Bpl.Expr> indices) {
     static bool FunctionBodyIsAvailable(Function f, ModuleDefinition context, VisibilityScope scope, bool revealProtectedBody) {
       Contract.Requires(f != null);
       Contract.Requires(context != null);
-      return f.Body != null && !IsOpaqueFunction(f) && f.IsRevealedInScope(scope);
+      return f.Body != null && !IsOpaque(f) && f.IsRevealedInScope(scope);
     }
-    static bool IsOpaqueFunction(Function f) {
+    static bool IsOpaque(MemberDecl f) {
       Contract.Requires(f != null);
       return Attributes.Contains(f.Attributes, "opaque");
     }
@@ -6575,7 +6575,9 @@ Bpl.Function GetReadonlyField(Field f) {
           var cf = (ConstantField)f;
           if (cf.Rhs != null && RevealedInScope(cf)) {
             var etran = new ExpressionTranslator(this, predef, NewOneHeapExpr(f.tok));
-            sink.AddTopLevelDeclaration(ff.CreateDefinitionAxiom(etran.TrExpr(cf.Rhs)));
+            if (!IsOpaque(cf)) {
+              sink.AddTopLevelDeclaration(ff.CreateDefinitionAxiom(etran.TrExpr(cf.Rhs)));
+            }
           }
           sink.AddTopLevelDeclaration(ff);
 

Test/allocated1/dafny0/OpaqueFunctions.dfy.expect

@@ -25,7 +25,7 @@ OpaqueFunctions.dfy(261,11): Error: assertion might not hold
 OpaqueFunctions.dfy(326,16): Error: assertion might not hold
 OpaqueFunctions.dfy(328,15): Error: assertion might not hold
 OpaqueFunctions.dfy(330,15): Error: assertion might not hold
-OpaqueFunctions.dfy(343,46): Error: result of operation might violate newtype constraint for 'Small'
+OpaqueFunctions.dfy(343,38): Error: assertion might not hold
 OpaqueFunctions.dfy(350,15): Error: assertion might not hold
 OpaqueFunctions.dfy(352,15): Error: assertion might not hold
 OpaqueFunctions.dfy(354,15): Error: assertion might not hold

Test/dafny0/OpaqueConstants.dfy

@@ -0,0 +1,102 @@
+// RUN: %dafny_0 /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module Module {
+  module M {
+    const {:opaque} Five := 5
+  }
+
+  method Test() {
+    if * {
+      assert M.Five == 5; // error: this is not known here
+    } else {
+      reveal M.Five;
+      assert M.Five == 5;
+    }
+  }
+}
+
+module Class {
+  class Class {
+    const {:opaque} Five := 5
+  }
+
+  method Test(c: Class) {
+    if * {
+      assert c.Five == 5; // error: this is not known here
+    } else {
+      reveal c.Five;
+      assert c.Five == 5;
+    }
+  }
+}
+
+module TypeMembers {
+  trait Tr {
+    const fav: bool
+    const {:opaque} IsFavorite := fav
+    static const {:opaque} Five := 5
+  }
+
+  datatype Color = Carrot | Pumpkin
+  {
+    const {:opaque} IsFavorite := this == Pumpkin
+    static const {:opaque} Five := 5
+  }
+
+  newtype Small = x | 30 <= x < 40 witness 30
+  {
+    const {:opaque} IsFavorite := this == 34
+    static const {:opaque} Five := 5
+  }
+
+  method Test(tr: Tr, c: Color, s: Small) {
+    if
+    case tr.IsFavorite =>
+      assert tr.fav;  // error: this is not known here
+    case c.IsFavorite =>
+      assert c == Pumpkin;  // error: this is not known here
+    case s.IsFavorite =>
+      assert s == 34;  // error: this is not known here
+    case tr.IsFavorite =>
+      reveal tr.IsFavorite;
+      assert tr.fav;
+    case c.IsFavorite =>
+      reveal c.IsFavorite;
+      assert c == Pumpkin;
+    case s.IsFavorite =>
+      reveal s.IsFavorite;
+      assert s == 34;
+    case true =>
+      if tr.IsFavorite && c.IsFavorite && s.IsFavorite {
+        reveal tr.IsFavorite, c.IsFavorite, s.IsFavorite;
+        assert !tr.fav || c == Carrot || s == 39;  // error: not true
+      }
+  }
+
+  function IsUneven(i: int): bool { i % 2 == 1 }
+
+  method StaticTest() {
+    if
+    case IsUneven(Tr.Five) =>
+      assert Tr.Five == 5;  // error: this is not known here
+    case IsUneven(Color.Five) =>
+      assert Color.Five == 5;  // error: this is not known here
+    case IsUneven(Small.Five) =>
+      assert Color.Five == 5;  // error: this is not known here
+    case IsUneven(Tr.Five) =>
+      reveal Tr.Five;
+      assert Tr.Five == 5;
+    case IsUneven(Color.Five) =>
+      reveal Color.Five;
+      assert Color.Five == 5;
+    case IsUneven(Small.Five) =>
+      reveal Small.Five;
+      assert Small.Five == 5;
+    case true =>
+      if IsUneven(Tr.Five) && IsUneven(Color.Five) && IsUneven(Small.Five) {
+        reveal Tr.Five, Color.Five, Small.Five;
+        assert Tr.Five != 5 || Color.Five != 5 || Small.Five != 5;  // error: not true
+      }
+  }
+}