Remove usage of opaque from standard library

Source/DafnyCore/AST/Substituter.cs

@@ -874,7 +874,9 @@ protected virtual Statement SubstStmt(Statement stmt) {
         r = rr;
       } else if (stmt is HideRevealStmt revealStmt) {
         // don't need to substitute s.Expr since it won't be used, only the s.ResolvedStatements are used.
-        var rr = new HideRevealStmt(revealStmt.RangeToken, revealStmt.Exprs, revealStmt.Mode);
+        var rr = revealStmt.Wildcard
+          ? new HideRevealStmt(revealStmt.RangeToken, revealStmt.Mode)
+          : new HideRevealStmt(revealStmt.RangeToken, revealStmt.Exprs, revealStmt.Mode);
         rr.LabeledAsserts.AddRange(revealStmt.LabeledAsserts);
         rr.ResolvedStatements.AddRange(revealStmt.ResolvedStatements.ConvertAll(SubstStmt));
         rr.OffsetMembers = revealStmt.OffsetMembers.ToList();

Source/DafnyCore/Verifier/BoogieGenerator.Reveal.cs

@@ -13,36 +13,70 @@ namespace Microsoft.Dafny;
 
 public partial class BoogieGenerator {
 
+  private static void TranslateRevealStmt(BoogieGenerator boogieGenerator, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran,
+    HideRevealStmt revealStmt) {
+    AddComment(builder, revealStmt, "hide/reveal statement");
+    foreach (var la in revealStmt.LabeledAsserts) {
+      Contract.Assert(la.E != null);  // this should have been filled in by now
+      builder.Add(new AssumeCmd(revealStmt.Tok, la.E));
+    }
+
+    if (builder.Context.ContainsHide) {
+      if (revealStmt.Wildcard) {
+        builder.Add(new HideRevealCmd(revealStmt.Tok, revealStmt.Mode));
+      } else {
+        foreach (var member in revealStmt.OffsetMembers) {
+          builder.Add(new HideRevealCmd(new Bpl.IdentifierExpr(revealStmt.Tok, member.FullSanitizedName), revealStmt.Mode));
+        }
+      }
+    }
+
+    boogieGenerator.TrStmtList(revealStmt.ResolvedStatements, builder, locals, etran);
+  }
+
   Expr TrStmtSideEffect(Expr e, Statement stmt, ExpressionTranslator etran) {
-    if (stmt is CallStmt) {
-      var call = (CallStmt)stmt;
-      var m = call.Method;
-      if (IsOpaqueRevealLemma(m)) {
-        List<Expression> args = Attributes.FindExpressions(m.Attributes, "fuel");
-        if (args != null) {
-          MemberSelectExpr selectExpr = args[0].Resolved as MemberSelectExpr;
-          if (selectExpr != null) {
-            Function f = selectExpr.Member as Function;
-            FuelConstant fuelConstant = this.functionFuel.Find(x => x.f == f);
-            if (fuelConstant != null) {
-              Bpl.Expr startFuel = fuelConstant.startFuel;
-              Bpl.Expr startFuelAssert = fuelConstant.startFuelAssert;
-              Bpl.Expr moreFuel_expr = fuelConstant.MoreFuel(sink, Predef, f.IdGenerator);
-              Bpl.Expr layer = etran.layerInterCluster.LayerN(1, moreFuel_expr);
-              Bpl.Expr layerAssert = etran.layerInterCluster.LayerN(2, moreFuel_expr);
-
-              e = BplAnd(e, Bpl.Expr.Eq(startFuel, layer));
-              e = BplAnd(e, Bpl.Expr.Eq(startFuelAssert, layerAssert));
-              e = BplAnd(e, Bpl.Expr.Eq(this.FunctionCall(f.tok, BuiltinFunction.AsFuelBottom, null, moreFuel_expr), moreFuel_expr));
-            }
+    switch (stmt) {
+      case CallStmt call: {
+          var m = call.Method;
+          if (!IsOpaqueRevealLemma(m)) {
+            return e;
+          }
+
+          var args = Attributes.FindExpressions(m.Attributes, "fuel");
+          if (args == null) {
+            return e;
+          }
+
+          if (args[0].Resolved is not MemberSelectExpr selectExpr) {
+            return e;
+          }
+
+          var f = selectExpr.Member as Function;
+          var fuelConstant = functionFuel.Find(x => x.f == f);
+          if (fuelConstant == null) {
+            return e;
           }
+
+          var startFuel = fuelConstant.startFuel;
+          var startFuelAssert = fuelConstant.startFuelAssert;
+          var moreFuelExpr = fuelConstant.MoreFuel(sink, Predef, f.IdGenerator);
+          var layer = etran.layerInterCluster.LayerN(1, moreFuelExpr);
+          var layerAssert = etran.layerInterCluster.LayerN(2, moreFuelExpr);
+
+          e = BplAnd(e, Expr.Eq(startFuel, layer));
+          e = BplAnd(e, Expr.Eq(startFuelAssert, layerAssert));
+          e = BplAnd(e, Expr.Eq(FunctionCall(f.tok, BuiltinFunction.AsFuelBottom, null, moreFuelExpr), moreFuelExpr));
+
+          return e;
         }
-      }
-    } else if (stmt is HideRevealStmt reveal) {
-      foreach (var s in reveal.ResolvedStatements) {
-        e = BplAnd(e, TrFunctionSideEffect(s, etran));
-      }
+      case HideRevealStmt reveal: {
+          foreach (var s in reveal.ResolvedStatements) {
+            e = BplAnd(e, TrFunctionSideEffect(s, etran));
+          }
+
+          return e;
+        }
+      default: return e;
     }
-    return e;
   }
 }

Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs

@@ -42,7 +42,7 @@ public void TrStmt(Statement stmt, BoogieStmtListBuilder builder,
       }
 
     } else if (stmt is HideRevealStmt revealStmt) {
-      TranslateRevealStmt(builder, locals, etran, revealStmt);
+      TranslateRevealStmt(this, builder, locals, etran, revealStmt);
     } else if (stmt is BreakOrContinueStmt breakStmt) {
       TrBreakStmt(builder, etran, breakStmt);
     } else if (stmt is ReturnStmt returnStmt) {
@@ -501,27 +501,6 @@ void TrVarDeclStmt(VarDeclStmt varDeclStmt, BoogieStmtListBuilder builder, Varia
     }
   }
 
-  private void TranslateRevealStmt(BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran,
-    HideRevealStmt revealStmt) {
-    AddComment(builder, revealStmt, "hide/reveal statement");
-    foreach (var la in revealStmt.LabeledAsserts) {
-      Contract.Assert(la.E != null);  // this should have been filled in by now
-      builder.Add(new Bpl.AssumeCmd(revealStmt.Tok, la.E));
-    }
-
-    if (builder.Context.ContainsHide) {
-      if (revealStmt.Wildcard) {
-        builder.Add(new HideRevealCmd(revealStmt.Tok, revealStmt.Mode));
-      } else {
-        foreach (var member in revealStmt.OffsetMembers) {
-          builder.Add(new HideRevealCmd(new Bpl.IdentifierExpr(revealStmt.Tok, member.FullSanitizedName), revealStmt.Mode));
-        }
-      }
-    }
-
-    TrStmtList(revealStmt.ResolvedStatements, builder, locals, etran);
-  }
-
   private void TrCalcStmt(CalcStmt stmt, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran) {
     Contract.Requires(stmt != null);
     Contract.Requires(builder != null);

Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticExamples.dfy

@@ -34,13 +34,16 @@ module ArithmeticExamples {
 
     @Test
     method TestToNatRight() {
+      hide *;
+      reveal BASE;
       expect ToNatRight([0]) == 0;
       expect ToNatRight([1]) == 1;
       expect ToNatRight([3]) == 3;
       expect ToNatRight([3,0,2]) == 203;
     }
 
     @Test
+    @IsolateAssertions
     method TestSeqExtend() {
       expect SeqExtend([], 3) == [0, 0, 0];
       expect SeqExtend([1], 3) == [1, 0, 0];
@@ -49,6 +52,8 @@ module ArithmeticExamples {
 
     @Test
     method TestSeqExtendMultiple() {
+      hide *;
+      reveal BASE;
       expect SeqExtendMultiple([], 3) == [0, 0, 0];
       print "length: ", |SeqExtendMultiple([1, 2, 3], 3)|;
       expect SeqExtendMultiple([1, 2], 3) == [1, 2, 0];

Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticTests.dfy

@@ -17,6 +17,7 @@ module ArithmeticTests {
   }
 
   @Test
+  @IsolateAssertions
   method TestPowLog() {
     expect Pow(-4, 0) == 1;
     expect Pow(-2, 2) == 4;

Source/DafnyStandardLibraries/examples/CollectionsExamples.dfy

@@ -39,6 +39,8 @@ module CollectionsExamples {
 
     @Test
     method TestSequenceIndexOf() {
+      hide *;
+      reveal s;
       AssertAndExpect(IndexOf(s, 5) == 4);
       expect IndexOf(s, 1) == 0;
       AssertAndExpect(IndexOfOption(s, 5) == Some(4));

Source/DafnyStandardLibraries/src/Std/Arithmetic/DivMod.dfy

@@ -30,16 +30,12 @@ module Std.Arithmetic.DivMod {
     requires 0 < d
     ensures DivRecursive(x, d) == x / d
   {
-    reveal DivPos();
-    reveal DivRecursive();
     LemmaDivInductionAuto(d, x, u => DivRecursive(u, d) == u / d);
   }
 
   lemma LemmaDivIsDivRecursiveAuto()
     ensures forall x: int, d: int {:trigger x / d} :: d > 0 ==> DivRecursive(x, d) == x / d
   {
-    reveal DivPos();
-    reveal DivRecursive();
     forall x: int, d: int | d > 0
       ensures DivRecursive(x, d) == x / d
     {
@@ -133,8 +129,6 @@ module Std.Arithmetic.DivMod {
     ensures x / y >= x / z
     decreases x
   {
-    reveal DivPos();
-    reveal DivRecursive();
     LemmaDivIsDivRecursiveAuto();
     assert forall u: int, d: int {:trigger u / d} {:trigger DivRecursive(u, d)}
         :: d > 0 ==> DivRecursive(u, d) == u / d;
@@ -956,7 +950,6 @@ module Std.Arithmetic.DivMod {
     ensures ModRecursive(x, m) == x % m
     decreases if x < 0 then -x + m else x
   {
-    reveal ModRecursive();
     if x < 0 {
       calc {
         ModRecursive(x, m);
@@ -991,7 +984,6 @@ module Std.Arithmetic.DivMod {
   lemma LemmaModIsModRecursiveAuto()
     ensures forall x: int, d: int {:trigger x % d}:: d > 0 ==> ModRecursive(x, d) == x % d
   {
-    reveal ModRecursive();
     forall x: int, d: int | d > 0
       ensures ModRecursive(x, d) == x % d
     {

Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/DivInternals.dfy

@@ -26,7 +26,7 @@ module Std.Arithmetic.DivInternals {
   import opened MulInternals
 
   /* Performs division recursively with positive denominator. */
-  opaque function DivPos(x: int, d: int): int
+  function DivPos(x: int, d: int): int
     requires d > 0
     decreases if x < 0 then (d - x) else x
   {
@@ -39,10 +39,9 @@ module Std.Arithmetic.DivInternals {
   }
 
   /* Performs division recursively. */
-  opaque function DivRecursive(x: int, d: int): int
+  function DivRecursive(x: int, d: int): int
     requires d != 0
   {
-    reveal DivPos();
     if d > 0 then
       DivPos(x, d)
     else

Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/ModInternals.dfy

@@ -27,7 +27,7 @@ module Std.Arithmetic.ModInternals {
   import opened DivInternalsNonlinear
 
   /* Performs modulus recursively. */
-  opaque function ModRecursive(x: int, d: int): int
+  function ModRecursive(x: int, d: int): int
     requires d > 0
     decreases if x < 0 then (d - x) else x
   {

Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/MulInternals.dfy

@@ -15,7 +15,7 @@ module Std.Arithmetic.MulInternals {
   import opened MulInternalsNonlinear
 
   /* performs multiplication for positive integers using recursive addition */
-  opaque function MulPos(x: int, y: int) : int
+  function MulPos(x: int, y: int) : int
     requires x >= 0
   {
     if x == 0 then 0