Fix roundup proofs

src/nonlin/arith.dfy

@@ -51,6 +51,12 @@ module Arith {
     ensures x1 <= x1 * x2
   {}
 
+  lemma mul_increasing(x1: nat, x2: nat, k: nat)
+    requires 0 <= k
+    requires x1 <= x2
+    ensures x1 * k <= x2 * k
+  {}
+
   lemma mul_positive(x: nat, y: nat)
     ensures 0 <= x*y
   {}

src/nonlin/roundup.dfy

@@ -100,6 +100,13 @@ module Round {
     if x % k == 0 then x else x/k*k + k
   }
 
+  lemma roundup_spec(x: nat, k: nat)
+    requires k >= 1
+    ensures roundup(x, k) == ((x + (k-1)) / k) * k
+  {
+    div_roundup_spec(x, k);
+  }
+
   function roundup64(x: uint64, k: uint64): (r:uint64)
     requires k >= 1
     requires x as nat < 0x1_0000_0000_0000_0000-k as nat
@@ -114,14 +121,18 @@ module Round {
     ensures roundup(x1, k) <= roundup(x2, k)
   {
     div_increasing(x1+(k-1), x2+(k-1), k);
-    div_roundup_spec(x1, k);
-    div_roundup_spec(x2, k);
+    assert (x1+(k-1))/k <= (x2+(k-1))/k;
+    mul_increasing((x1+(k-1))/k, (x2+(k-1))/k, k);
+    roundup_spec(x1, k);
+    roundup_spec(x2, k);
   }
 
   lemma div_roundup_bound(x: nat, k: nat)
     requires k >= 1
     ensures div_roundup(x, k) >= x/k
-  {}
+  {
+    div_roundup_spec(x, k);
+  }
 
   lemma roundup_bound(x: nat, k: nat)
     requires k >= 1