Chore: Proofs not depending on leaks of opaque + brittleness reduction (#149)

MikaelMayer · web-flow · commit ae8708c091d3 · 2023-11-02T08:01:56.000-07:00
* Chore: Proofs not depending on leaks of opaque + brittleness reduction
I added reveal statements where they were previously "leaked" because of fuel encoding that are soon going away.
I also reduced the RU for ToLarge from 6.8M to 1.3M.

* Forgot to save a file

* Fixed brittleness issue for current Dafny

* Fixed two brittle proofs

* Fixed formatting

* Comment about the proof

* Update src/Collections/Sequences/LittleEndianNatConversions.dfy
diff --git a/src/Collections/Sequences/LittleEndianNatConversions.dfy b/src/Collections/Sequences/LittleEndianNatConversions.dfy
@@ -81,15 +81,39 @@ abstract module {:options "-functionSyntax:4"} LittleEndianNatConversions {
     requires |xs| % E() == 0
     ensures |ys| == |xs| / E()
   {
-    if |xs| == 0 then LemmaDivBasicsAuto(); []
+    if |xs| == 0 then
+      var ys := (LemmaDivBasicsAuto(); []);
+      assert |ys| == |xs| / E();
+      ys
+
     else
       LemmaModIsZero(|xs|, E());
       assert |xs| >= E();
-
       Small.LemmaSeqNatBound(xs[..E()]);
-      LemmaModSubMultiplesVanishAuto();
       LemmaDivMinusOne(|xs|, E());
-      [Small.ToNatRight(xs[..E()]) as Large.uint] + ToLarge(xs[E()..])
+      assert |xs[E()..]| % E() == 0 by {
+        LemmaModSubMultiplesVanishAuto();
+      }
+      var ys := ([Small.ToNatRight(xs[..E()]) as Large.uint] + ToLarge(xs[E()..]));
+      assert |ToLarge(xs[E()..])| == |xs[E()..]| / E();
+      assert |ys| == |xs| / E() by {
+        // To obtain a proof like this, first write a detailed proof
+        // as much as you can, not assuming anything about non-linear arithmetic (use only lemmas for that)
+        // Then remove intermediate computation steps and lemma calls if doing so decrease the resource count
+        // until arriving at at a minimum
+        calc {
+          |ys|;
+          1 + |xs[E()..]| / E();
+          1 + (|xs| - E()) / E();
+          { DivMod.ModINL.LemmaFundamentalDivMod(|xs|, E()); }
+          1 + (E() * (|xs| / E()) + |xs| % E() - E()) / E();
+          1 + (E() * (|xs| / E()) - E()) / E();
+          1 + (E() * (|xs| / E()) + E() * -1) / E();
+          { Mul.LemmaMulIsDistributiveAdd(E(), |xs| / E(), -1); }
+          1 + (E() * (|xs| / E() + -1)) / E();
+        }
+      }
+      ys
   }
 
   /* Sequence conversion from Large.BASE() to Small.BASE() does not
diff --git a/src/NonlinearArithmetic/DivMod.dfy b/src/NonlinearArithmetic/DivMod.dfy
@@ -35,13 +35,15 @@ module {:options "-functionSyntax:4"} 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
@@ -136,6 +138,7 @@ module {:options "-functionSyntax:4"} 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)}
diff --git a/src/NonlinearArithmetic/Logarithm.dfy b/src/NonlinearArithmetic/Logarithm.dfy
@@ -85,6 +85,7 @@ module {:options "-functionSyntax:4"} Logarithm {
         Log(base, base * Pow(base, n - 1));
         { LemmaPowPositive(base, n - 1);
           LemmaMulIncreases(Pow(base, n - 1), base);
+          LemmaMulIsCommutative(Pow(base, n - 1), base);
           LemmaLogS(base, base * Pow(base, n - 1)); }
         1 + Log(base, (base * Pow(base, n - 1)) / base);
         { LemmaDivMultiplesVanish(Pow(base, n - 1), base); }
diff --git a/src/NonlinearArithmetic/Power.dfy b/src/NonlinearArithmetic/Power.dfy
@@ -372,23 +372,34 @@ module {:options "-functionSyntax:4"} Power {
     requires e1 < e2
     ensures Pow(b, e1) < Pow(b, e2)
   {
+    reveal Pow();
     LemmaPowAuto();
     var f := e => 0 < e ==> Pow(b, e1) < Pow(b, e1 + e);
     forall i {:trigger IsLe(0, i)} | IsLe(0, i) && f(i)
       ensures f(i + 1)
     {
+      assert 0 < i ==> Pow(b, e1) < Pow(b, e1 + i);
       calc {
-        Pow(b, e1 + i);
+         Pow(b, e1 + i);
       <= { LemmaPowPositive(b, e1 + i);
            LemmaMulLeftInequality(Pow(b, e1 + i), 1, b); }
-        Pow(b, e1 + i) * b;
+         Pow(b, e1 + i) * b;
       == { LemmaPow1(b); }
-        Pow(b, e1 + i) * Pow(b, 1);
+         Pow(b, e1 + i) * Pow(b, 1);
       == { LemmaPowAdds(b, e1 + i, 1); }
-        Pow(b, e1 + i + 1);
+         Pow(b, e1 + i + 1);
+      == calc {
+           e1 + i + 1;
+           e1 + (i + 1);
+         }
+         Pow(b, e1 + (i + 1));
       }
+      assert f(i+1);
     }
     LemmaMulInductionAuto(e2 - e1, f);
+    assert Pow(b, e1) < Pow(b, e1 + (e2 - e1)) == Pow(b, e2) by {
+      assert 0 < e2 - e1;
+    }
   }
 
   lemma LemmaPowStrictlyIncreasesAuto()
@@ -410,6 +421,7 @@ module {:options "-functionSyntax:4"} Power {
     requires e1 <= e2
     ensures Pow(b, e1) <= Pow(b, e2)
   {
+    reveal Pow();
     LemmaPowAuto();
     var f := e => 0 <= e ==> Pow(b, e1) <= Pow(b, e1 + e);
     forall i {:trigger IsLe(0, i)} | IsLe(0, i) && f(i)
@@ -427,6 +439,9 @@ module {:options "-functionSyntax:4"} Power {
       }
     }
     LemmaMulInductionAuto(e2 - e1, f);
+    assert Pow(b, e1) <= Pow(b, e1 + (e2 - e1)) by {
+      assert 0 <= e2 - e1;
+    }
   }
 
   lemma LemmaPowIncreasesAuto()
diff --git a/src/NonlinearArithmetic/Power2.dfy b/src/NonlinearArithmetic/Power2.dfy
@@ -60,6 +60,7 @@ module {:options "-functionSyntax:4"} Power2 {
     requires 0 < e
     ensures (Pow2(e) - 1) / 2 == Pow2(e - 1) - 1
   {
+    LemmaPow2Auto();
     LemmaPowAuto();
     var f := e => 0 < e ==> (Pow2(e) - 1) / 2 == Pow2(e - 1) - 1;
     assert forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + 1);
@@ -116,6 +117,7 @@ module {:options "-functionSyntax:4"} Power2 {
     ensures Pow2(64) == 0x10000000000000000
   {
     reveal Pow2();
+    reveal Pow();
   }
 
 }
diff --git a/src/dafny/NonlinearArithmetic/DivMod.dfy b/src/dafny/NonlinearArithmetic/DivMod.dfy
@@ -36,6 +36,7 @@ module {:options "-functionSyntax:4"} Dafny.DivMod {
     requires 0 < d
     ensures DivRecursive(x, d) == x / d
   {
+    reveal DivPos();
     reveal DivRecursive();
     LemmaDivInductionAuto(d, x, u => DivRecursive(u, d) == u / d);
   }
@@ -121,6 +122,7 @@ module {:options "-functionSyntax:4"} Dafny.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)}
diff --git a/src/dafny/NonlinearArithmetic/Power.dfy b/src/dafny/NonlinearArithmetic/Power.dfy
@@ -143,6 +143,7 @@ module {:options "-functionSyntax:4"} Dafny.Power {
     ensures 0 < Pow(b, e)
   {
     LemmaMulIncreasesAuto();
+    reveal Pow();
     LemmaMulInductionAuto(e, u => 0 <= u ==> 0 < Pow(b, u));
   }
 
@@ -372,23 +373,34 @@ module {:options "-functionSyntax:4"} Dafny.Power {
     requires e1 < e2
     ensures Pow(b, e1) < Pow(b, e2)
   {
+    reveal Pow();
     LemmaPowAuto();
     var f := e => 0 < e ==> Pow(b, e1) < Pow(b, e1 + e);
     forall i {:trigger IsLe(0, i)} | IsLe(0, i) && f(i)
       ensures f(i + 1)
     {
+      assert 0 < i ==> Pow(b, e1) < Pow(b, e1 + i);
       calc {
-        Pow(b, e1 + i);
+         Pow(b, e1 + i);
       <= { LemmaPowPositive(b, e1 + i);
            LemmaMulLeftInequality(Pow(b, e1 + i), 1, b); }
-        Pow(b, e1 + i) * b;
+         Pow(b, e1 + i) * b;
       == { LemmaPow1(b); }
-        Pow(b, e1 + i) * Pow(b, 1);
+         Pow(b, e1 + i) * Pow(b, 1);
       == { LemmaPowAdds(b, e1 + i, 1); }
-        Pow(b, e1 + i + 1);
+         Pow(b, e1 + i + 1);
+      == calc {
+           e1 + i + 1;
+           e1 + (i + 1);
+         }
+         Pow(b, e1 + (i + 1));
       }
+      assert f(i+1);
     }
     LemmaMulInductionAuto(e2 - e1, f);
+    assert Pow(b, e1) < Pow(b, e1 + (e2 - e1)) == Pow(b, e2) by {
+      assert 0 < e2 - e1;
+    }
   }
 
   lemma LemmaPowStrictlyIncreasesAuto()
@@ -410,6 +422,7 @@ module {:options "-functionSyntax:4"} Dafny.Power {
     requires e1 <= e2
     ensures Pow(b, e1) <= Pow(b, e2)
   {
+    reveal Pow();
     LemmaPowAuto();
     var f := e => 0 <= e ==> Pow(b, e1) <= Pow(b, e1 + e);
     forall i {:trigger IsLe(0, i)} | IsLe(0, i) && f(i)
@@ -427,6 +440,9 @@ module {:options "-functionSyntax:4"} Dafny.Power {
       }
     }
     LemmaMulInductionAuto(e2 - e1, f);
+    assert Pow(b, e1) <= Pow(b, e1 + (e2 - e1)) by {
+      assert 0 <= e2 - e1;
+    }
   }
 
   lemma LemmaPowIncreasesAuto()
diff --git a/src/dafny/NonlinearArithmetic/Power2.dfy b/src/dafny/NonlinearArithmetic/Power2.dfy
@@ -60,6 +60,7 @@ module {:options "-functionSyntax:4"} Dafny.Power2 {
     requires 0 < e
     ensures (Pow2(e) - 1) / 2 == Pow2(e - 1) - 1
   {
+    LemmaPow2Auto();
     LemmaPowAuto();
     var f := e => 0 < e ==> (Pow2(e) - 1) / 2 == Pow2(e - 1) - 1;
     assert forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + 1);
@@ -115,6 +116,7 @@ module {:options "-functionSyntax:4"} Dafny.Power2 {
     ensures Pow2(32) == 0x100000000
     ensures Pow2(64) == 0x10000000000000000
   {
+    reveal Pow();
     reveal Pow2();
   }
 

Original file line number	Diff line number	Diff line change
`@@ -35,13 +35,15 @@ module {:options "-functionSyntax:4"} DivMod {`
`35`	`35`	`requires 0 < d`
`36`	`36`	`ensures DivRecursive(x, d) == x / d`
`37`	`37`	`{`
	`38`	`+ reveal DivPos();`
`38`	`39`	`reveal DivRecursive();`
`39`	`40`	`LemmaDivInductionAuto(d, x, u => DivRecursive(u, d) == u / d);`
`40`	`41`	`}`
`41`	`42`
`42`	`43`	`lemma LemmaDivIsDivRecursiveAuto()`
`43`	`44`	`ensures forall x: int, d: int {:trigger x / d} :: d > 0 ==> DivRecursive(x, d) == x / d`
`44`	`45`	`{`
	`46`	`+ reveal DivPos();`
`45`	`47`	`reveal DivRecursive();`
`46`	`48`	`forall x: int, d: int \| d > 0`
`47`	`49`	`ensures DivRecursive(x, d) == x / d`
`@@ -136,6 +138,7 @@ module {:options "-functionSyntax:4"} DivMod {`
`136`	`138`	`ensures x / y >= x / z`
`137`	`139`	`decreases x`
`138`	`140`	`{`
	`141`	`+ reveal DivPos();`
`139`	`142`	`reveal DivRecursive();`
`140`	`143`	`LemmaDivIsDivRecursiveAuto();`
`141`	`144`	`assert forall u: int, d: int {:trigger u / d} {:trigger DivRecursive(u, d)}`
Original file line number	Diff line number	Diff line change
`@@ -60,6 +60,7 @@ module {:options "-functionSyntax:4"} Power2 {`
`60`	`60`	`requires 0 < e`
`61`	`61`	`ensures (Pow2(e) - 1) / 2 == Pow2(e - 1) - 1`
`62`	`62`	`{`
	`63`	`+ LemmaPow2Auto();`
`63`	`64`	`LemmaPowAuto();`
`64`	`65`	`var f := e => 0 < e ==> (Pow2(e) - 1) / 2 == Pow2(e - 1) - 1;`
`65`	`66`	`assert forall i {:trigger IsLe(0, i)} :: IsLe(0, i) && f(i) ==> f(i + 1);`
`@@ -116,6 +117,7 @@ module {:options "-functionSyntax:4"} Power2 {`
`116`	`117`	`ensures Pow2(64) == 0x10000000000000000`
`117`	`118`	`{`
`118`	`119`	`reveal Pow2();`
	`120`	`+ reveal Pow();`
`119`	`121`	`}`
`120`	`122`
`121`	`123`	`}`
Original file line number	Diff line number	Diff line change
`@@ -36,6 +36,7 @@ module {:options "-functionSyntax:4"} Dafny.DivMod {`
`36`	`36`	`requires 0 < d`
`37`	`37`	`ensures DivRecursive(x, d) == x / d`
`38`	`38`	`{`
	`39`	`+ reveal DivPos();`
`39`	`40`	`reveal DivRecursive();`
`40`	`41`	`LemmaDivInductionAuto(d, x, u => DivRecursive(u, d) == u / d);`
`41`	`42`	`}`
`@@ -121,6 +122,7 @@ module {:options "-functionSyntax:4"} Dafny.DivMod {`
`121`	`122`	`ensures x / y >= x / z`
`122`	`123`	`decreases x`
`123`	`124`	`{`
	`125`	`+ reveal DivPos();`
`124`	`126`	`reveal DivRecursive();`
`125`	`127`	`LemmaDivIsDivRecursiveAuto();`
`126`	`128`	`assert forall u: int, d: int {:trigger u / d} {:trigger DivRecursive(u, d)}`
Original file line number	Diff line number	Diff line change
`@@ -143,6 +143,7 @@ module {:options "-functionSyntax:4"} Dafny.Power {`
`143`	`143`	`ensures 0 < Pow(b, e)`
`144`	`144`	`{`
`145`	`145`	`LemmaMulIncreasesAuto();`
	`146`	`+ reveal Pow();`
`146`	`147`	`LemmaMulInductionAuto(e, u => 0 <= u ==> 0 < Pow(b, u));`
`147`	`148`	`}`
`148`	`149`
`@@ -372,23 +373,34 @@ module {:options "-functionSyntax:4"} Dafny.Power {`
`372`	`373`	`requires e1 < e2`
`373`	`374`	`ensures Pow(b, e1) < Pow(b, e2)`
`374`	`375`	`{`
	`376`	`+ reveal Pow();`
`375`	`377`	`LemmaPowAuto();`
`376`	`378`	`var f := e => 0 < e ==> Pow(b, e1) < Pow(b, e1 + e);`
`377`	`379`	`forall i {:trigger IsLe(0, i)} \| IsLe(0, i) && f(i)`
`378`	`380`	`ensures f(i + 1)`
`379`	`381`	`{`
	`382`	`+ assert 0 < i ==> Pow(b, e1) < Pow(b, e1 + i);`
`380`	`383`	`calc {`
`381`		`- Pow(b, e1 + i);`
	`384`	`+ Pow(b, e1 + i);`
`382`	`385`	`<= { LemmaPowPositive(b, e1 + i);`
`383`	`386`	`LemmaMulLeftInequality(Pow(b, e1 + i), 1, b); }`
`384`		`- Pow(b, e1 + i) * b;`
	`387`	`+ Pow(b, e1 + i) * b;`
`385`	`388`	`== { LemmaPow1(b); }`
`386`		`- Pow(b, e1 + i) * Pow(b, 1);`
	`389`	`+ Pow(b, e1 + i) * Pow(b, 1);`
`387`	`390`	`== { LemmaPowAdds(b, e1 + i, 1); }`
`388`		`- Pow(b, e1 + i + 1);`
	`391`	`+ Pow(b, e1 + i + 1);`
	`392`	`+ == calc {`
	`393`	`+ e1 + i + 1;`
	`394`	`+ e1 + (i + 1);`
	`395`	`+ }`
	`396`	`+ Pow(b, e1 + (i + 1));`
`389`	`397`	`}`
	`398`	`+ assert f(i+1);`
`390`	`399`	`}`
`391`	`400`	`LemmaMulInductionAuto(e2 - e1, f);`
	`401`	`+ assert Pow(b, e1) < Pow(b, e1 + (e2 - e1)) == Pow(b, e2) by {`
	`402`	`+ assert 0 < e2 - e1;`
	`403`	`+ }`
`392`	`404`	`}`
`393`	`405`
`394`	`406`	`lemma LemmaPowStrictlyIncreasesAuto()`
`@@ -410,6 +422,7 @@ module {:options "-functionSyntax:4"} Dafny.Power {`
`410`	`422`	`requires e1 <= e2`
`411`	`423`	`ensures Pow(b, e1) <= Pow(b, e2)`
`412`	`424`	`{`
	`425`	`+ reveal Pow();`
`413`	`426`	`LemmaPowAuto();`
`414`	`427`	`var f := e => 0 <= e ==> Pow(b, e1) <= Pow(b, e1 + e);`
`415`	`428`	`forall i {:trigger IsLe(0, i)} \| IsLe(0, i) && f(i)`
`@@ -427,6 +440,9 @@ module {:options "-functionSyntax:4"} Dafny.Power {`
`427`	`440`	`}`
`428`	`441`	`}`
`429`	`442`	`LemmaMulInductionAuto(e2 - e1, f);`
	`443`	`+ assert Pow(b, e1) <= Pow(b, e1 + (e2 - e1)) by {`
	`444`	`+ assert 0 <= e2 - e1;`
	`445`	`+ }`
`430`	`446`	`}`
`431`	`447`
`432`	`448`	`lemma LemmaPowIncreasesAuto()`