Remove usage of opaque from standard library

Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticExamples.dfy

@@ -32,19 +32,23 @@ module ArithmeticExamples {
     }
 
     method {:test} TestToNatRight() {
+      hide *;
+      reveal BASE;
       expect ToNatRight([0]) == 0;
       expect ToNatRight([1]) == 1;
       expect ToNatRight([3]) == 3;
       expect ToNatRight([3,0,2]) == 203;
     }
 
-    method {:test} TestSeqExtend() {
+    method {:test} {:isolate_assertions} TestSeqExtend() {
       expect SeqExtend([], 3) == [0, 0, 0];
       expect SeqExtend([1], 3) == [1, 0, 0];
       expect SeqExtend([3,0,2], 4) == [3,0,2,0];
     }
 
     method {:test} 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

@@ -15,7 +15,7 @@ module ArithmeticTests {
     }
   }
 
-  method {:test} TestPowLog() {
+  method {:test} {:isolate_assertions} TestPowLog() {
     expect Pow(-4, 0) == 1;
     expect Pow(-2, 2) == 4;
     expect Pow(-2, 3) == -8;

Source/DafnyStandardLibraries/examples/CollectionsExamples.dfy

@@ -37,6 +37,8 @@ module CollectionsExamples {
     }
 
     method {:test} 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

@@ -29,16 +29,12 @@ module {:disableNonlinearArithmetic} 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
     {
@@ -132,8 +128,6 @@ module {:disableNonlinearArithmetic} 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;
@@ -954,7 +948,6 @@ module {:disableNonlinearArithmetic} 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);
@@ -989,7 +982,6 @@ module {:disableNonlinearArithmetic} 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

@@ -25,7 +25,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivInternals {
   import opened MulInternals
 
   /* Performs division recursively with positive denominator. */
-  function {:opaque} 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
   {
@@ -38,10 +38,9 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.DivInternals {
   }
 
   /* Performs division recursively. */
-  function {:opaque} 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

@@ -26,7 +26,7 @@ module {:disableNonlinearArithmetic} Std.Arithmetic.ModInternals {
   import opened DivInternalsNonlinear
 
   /* Performs modulus recursively. */
-  function {:opaque} 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

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