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

#149) * 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
dafny-lang · Nov 2, 2023 · ae8708c · ae8708c
1 parent 5d89343
commit ae8708c
Show file tree

Hide file tree

Showing 8 changed files with 77 additions and 12 deletions.
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();
   }