Making sub bounds actually tight

5 files changed, 111 insertions, 180 deletions

diff --git a/src/Assembly/Compile.v b/src/Assembly/Compile.v
index d73ed8a07..53612cfbb 100644
--- a/src/Assembly/Compile.v
+++ b/src/Assembly/Compile.v
@@ -245,7 +245,7 @@ Module CompileLL.
 
                   omap (exprF (S (S nextRegName)) (eC var)) (fun out =>
                     omap (argToTT var) (fun var' =>
-                      update (reg w (S nextRegName)) var' op' x' y' out))))))
+                      update (reg w nextRegName) var' op' x' y' out))))))
         | Return _ a => get _ a
         end.
     End ExprF.
diff --git a/src/Assembly/Conversions.v b/src/Assembly/Conversions.v
index bb2f1e6fa..705a49a5b 100644
--- a/src/Assembly/Conversions.v
+++ b/src/Assembly/Conversions.v
@@ -340,7 +340,6 @@ Module LLConversions.
 
         admit.
 
-        admit.
 
       - simpl; unfold getUpperBoundOpt.
         repeat rewrite convertArg_interp in H.
diff --git a/src/Assembly/Evaluables.v b/src/Assembly/Evaluables.v
index 7b6e4a264..30d1029a3 100644
--- a/src/Assembly/Evaluables.v
+++ b/src/Assembly/Evaluables.v
@@ -104,7 +104,7 @@ Section RangeUpdate.
         induction (Npow2 n0); simpl; reflexivity.
     Qed.
 
-    Lemma bWSub_lem0: forall (x0 x1: word n) (low0 high1: N),
+    Lemma bWSub_lem: forall (x0 x1: word n) (low0 high1: N),
       (low0 <= wordToN x0)%N -> (wordToN x1 <= high1)%N -> 
       (low0 - high1 <= & (x0 ^- x1))%N.
     Proof.
@@ -177,138 +177,7 @@ Section RangeUpdate.
         transitivity low0; try assumption.
         apply N.le_sub_le_add_r.
         apply N.le_add_r.
-    Qed.
-
-    Lemma bWSub_lem1: forall (x0 x1: word n) (low1 high0: N),
-      (low1 <= wordToN x1)%N -> (wordToN x0 <= high0)%N -> 
-      (& (x0 ^- x1) <= high0 + Npow2 n - low1)%N.
-    Proof.
-      intros; unfold wminus.
-      destruct (Nge_dec (wordToN x1) 1)%N as [e|e].
-      destruct (Nge_dec (wordToN x0) (wordToN x1)).
-
-      - assert (& x0 - & x1 < Npow2 n)%N. {
-          transitivity (wordToN x0);
-          try apply word_size_bound;
-          apply N.sub_lt.
-
-          + apply N.ge_le; assumption.
-
-          + nomega.
-        }
-
-        assert (& x0 - & x1 + & x1 < Npow2 n)%N. {
-          replace (wordToN x0 - wordToN x1 + wordToN x1)%N
-            with (wordToN x0) by nomega.
-          apply word_size_bound.
-        }
-
-        assert (x0 = NToWord n (wordToN x0 - wordToN x1) ^+ x1) as Hv. {
-          apply NToWord_equal.
-          rewrite <- wordize_plus; rewrite wordToN_NToWord;
-          try assumption.
-          nomega.
-        }
-
-        rewrite Hv.
-        rewrite <- wplus_assoc.
-        rewrite wminus_inv.
-        rewrite wplus_comm.
-        rewrite wplus_unit.
-        rewrite wordToN_NToWord.
-
-        + transitivity (wordToN x0 - low1)%N.
-
-          * apply N.sub_le_mono_l; assumption.
-
-          * apply N.sub_le_mono_r.
-            transitivity high0; [assumption|].
-            replace' high0 with (high0 + 0)%N at 1 by nomega.
-            apply N.add_le_mono_l.
-            apply N_ge_0.
-
-        + transitivity (wordToN x0); try apply word_size_bound.
-          nomega.
-
-      - rewrite <- wordize_plus.
-
-        + transitivity (high0 + (wordToN (wneg x1)))%N.
-
-          * apply N.add_le_mono_r; assumption.
-
-          * unfold wneg.
-
-            rewrite wordToN_NToWord; [|abstract (
-              apply N.sub_lt;
-              try apply N.lt_le_incl;
-              try apply word_size_bound;
-              nomega )].
-
-            rewrite N.add_sub_assoc; [|abstract (
-              try apply N.lt_le_incl;
-              try apply word_size_bound)].
-
-            apply N.sub_le_mono_l.
-            assumption.
-
-        + unfold wneg.
-
-          rewrite wordToN_NToWord; [|abstract (
-            apply N.sub_lt;
-            try apply N.lt_le_incl;
-            try apply word_size_bound;
-            nomega )].
-
-          replace (wordToN x0 + (Npow2 n - wordToN x1))%N
-            with (Npow2 n - (wordToN x1 - wordToN x0))%N.
-
-          * apply N.sub_lt; try nomega.
-            transitivity (wordToN x1); [apply N.le_sub_l|].
-            apply N.lt_le_incl.
-            apply word_size_bound.
-
-          * apply N.add_sub_eq_l.
-            rewrite <- N.add_sub_swap;
-                [|apply N.lt_le_incl; assumption].
-            rewrite (N.add_comm (wordToN x0)).
-            rewrite N.add_assoc.
-            rewrite N.add_sub_assoc;
-                [|apply N.lt_le_incl; apply word_size_bound].
-            rewrite N.add_sub.
-            rewrite N.add_comm.
-            rewrite N.add_sub.
-            reflexivity.
-
-      - assert (wordToN x1 = 0)%N as e' by nomega.
-        assert (NToWord n (wordToN x1) = NToWord n 0%N) as E by
-            (rewrite e'; reflexivity).
-        rewrite NToWord_wordToN in E.
-        simpl in E; rewrite wzero'_def in E.
-        rewrite E.
-        unfold wneg.
-        rewrite wordToN_zero.
-        rewrite N.sub_0_r.
-        rewrite <- NToWord_Npow2.
-        rewrite wplus_comm.
-        rewrite wplus_unit.
-        transitivity high0.
-
-        + assumption.
-
-        + rewrite <- N.add_sub_assoc.
-
-          * replace high0 with (high0 + 0)%N by nomega.
-            apply N.add_le_mono; [|apply N_ge_0].
-            apply N.eq_le_incl.
-            rewrite N.add_0_r.
-            reflexivity.
-
-          * transitivity (wordToN x1);
-            [ assumption
-            | apply N.lt_le_incl;
-                apply word_size_bound].
-
-    Qed.
+    Qed. 
   End BoundedSub.
 
   Section LandOnes.
@@ -391,20 +260,14 @@ Section RangeUpdate.
            then Some (range N (low0 - high1)%N
               (if (Nge_dec high0 (Npow2 n)) then N.pred (Npow2 n) else
                if (Nge_dec high1 (Npow2 n)) then N.pred (Npow2 n) else
-               if (Nge_dec (high0 + Npow2 n - low1) (Npow2 n))
-               then N.pred (Npow2 n)
-               else high0 + Npow2 n - low1)%N)
+               high0 - low1)%N)
            else None
          end)
       (@wminus n).
   Proof.
     unfold validBinaryWordOp; intros.
 
-    destruct (Nge_dec high0 (Npow2 n)),
-             (Nge_dec high1 (Npow2 n)),
-             (Nge_dec low0 high1),
-             (Nge_dec (high0 + Npow2 n - low1) (Npow2 n));
-      repeat split;
+    Ltac kill_preds := 
       repeat match goal with
       | [|- (N.pred _ < _)%N] =>
         rewrite <- (N.pred_succ (Npow2 n));
@@ -412,13 +275,31 @@ Section RangeUpdate.
           rewrite N.pred_succ;
         [ apply N.lt_succ_diag_r
         | apply N.neq_0_lt_0; apply Npow2_gt0]
-
       | [|- (wordToN _ <= N.pred _)%N] => apply N.lt_le_pred
+      end.
+
+    destruct (Nge_dec high0 (Npow2 n)),
+             (Nge_dec high1 (Npow2 n)),
+             (Nge_dec low0 high1);
+      repeat split; kill_preds;
+      repeat match goal with
       | [|- (wordToN _ < Npow2 _)%N] => apply word_size_bound
-      | [|- (_ - ?x <= wordToN _)%N] => apply bWSub_lem0
-      | [|- (wordToN _ <= ?x + _ - _)%N] => apply bWSub_lem1
+      | [|- (?x - _ < Npow2)%N] => transitivity x; [nomega|]
+      | [|- (_ - ?x <= wordToN _)%N] => apply bWSub_lem
+      | [|- (wordToN _ <= _ - _)%N] => eapply wordize_sub
       | [|- (0 <= _)%N] => apply N_ge_0
-      end; try assumption.
+      end; try eassumption.
+
+    - apply N.le_ge. 
+      transitivity high1; [assumption|].
+      transitivity low0; [|assumption].
+      apply N.ge_le; assumption.
+
+    - apply (N.le_lt_trans _ high0 _); [|assumption].
+      replace high0 with (high0 - 0)%N by nomega.
+      replace' (high0 - 0)%N with high0 at 1 by nomega.
+      apply N.sub_le_mono_l.
+      apply N.ge_le; nomega.
   Qed.
 
   Lemma range_mul_valid :
@@ -534,9 +415,7 @@ Section RangeUpdate.
          match (range0, range1) with
          | (range low0 high0, range low1 high1) =>
            let upper := (N.pred (Npow2 (min (N.to_nat (getBits high0)) (N.to_nat (getBits high1)))))%N in
-           Some (range N 0%N (
-             if (Nge_dec upper (Npow2 n))
-             then (N.pred (Npow2 n)) else upper))
+           Some (range N 0%N (if (Nge_dec upper (Npow2 n)) then (N.pred (Npow2 n)) else upper))
           end)
       (@wand n).
   Proof.
diff --git a/src/Assembly/GF25519.v b/src/Assembly/GF25519.v
index 0ec5f508c..081ddc008 100644
--- a/src/Assembly/GF25519.v
+++ b/src/Assembly/GF25519.v
@@ -6,11 +6,23 @@ Require Import Crypto.Specific.GF25519.
 Require Import Crypto.Util.Tuple.
 
 Module GF25519.
-  Definition q : Z := (2 ^ 255 - 19)%Z.
-  Definition d : F q := (F.opp (F.of_Z q 121665%Z) / (F.of_Z q 121666%Z))%F.
+  Definition bits: nat := 32.
+  Definition width: Width bits := W32.
 
-  Definition twice_d' := Eval cbv [length params25519 ModularBaseSystemOpt.limb_widths_from_len ModularBaseSystem.encode ModularBaseSystemList.encode PseudoMersenneBaseParams.limb_widths] in ModularBaseSystem.encode(modulus:=q) (d + d)%F.
-  Definition twice_d : fe25519 := Eval vm_compute in twice_d'.
+  Fixpoint makeBoundList {n} k (b: @WordRangeOpt n) :=
+    match k with
+    | O => nil
+    | S k' => cons b (makeBoundList k' b)
+    end.
+
+  Section DefaultBounds.
+    Import ListNotations.
+    Local Notation rr exp := (makeRange 0 (2^exp + 2^exp/10)%Z).
+
+    Definition feBound: list (@WordRangeOpt bits) :=
+      [rr 26; rr 27; rr 26; rr 27; rr 26;
+       rr 27; rr 26; rr 27; rr 26; rr 27].
+  End DefaultBounds.
 
   Definition FE: type.
   Proof.
@@ -22,22 +34,15 @@ Module GF25519.
   Definition liftFE {T} (F: @interp_type Z FE -> T) :=
     fun (a b c d e f g h i j: Z) => F (a, b, c, d, e, f, g, h, i, j).
 
-  Fixpoint makeBoundList {n} k (b: @WordRangeOpt n) :=
-    match k with
-    | O => nil
-    | S k' => cons b (makeBoundList k' b)
-    end.
-
   Module AddExpr <: Expression.
-    Definition bits: nat := 64.
+    Definition bits: nat := bits.
     Definition inputs: nat := 20.
-    Definition width: Width bits := W64.
+    Definition width: Width bits := width.
     Definition ResultType := FE.
-    Definition inputUpperBounds: list (@WordRangeOpt bits) :=
-      makeBoundList 20 (makeRange 0 (Z.of_N (Npow2 28))).
+    Definition inputUpperBounds: list (@WordRangeOpt bits) := feBound ++ feBound.
 
     Definition ge25519_add_expr :=
-        Eval cbv beta delta [fe25519 add mul sub Let_In twice_d] in add.
+        Eval cbv beta delta [fe25519 add mul sub Let_In] in add.
 
     Definition ge25519_add' (P Q: @interp_type Z FE) :
         { r: @HL.expr Z (@interp_type Z) FE
@@ -83,15 +88,14 @@ Module GF25519.
   End AddExpr.
 
   Module SubExpr <: Expression.
-    Definition bits: nat := 64.
+    Definition bits: nat := bits.
     Definition inputs: nat := 20.
-    Definition width: Width bits := W64.
+    Definition width: Width bits := width.
     Definition ResultType := FE.
-    Definition inputUpperBounds: list (@WordRangeOpt bits) :=
-      makeBoundList 20 (makeRange 0 (Z.of_N (Npow2 28))).
+    Definition inputUpperBounds: list (@WordRangeOpt bits) := feBound ++ feBound.
 
     Definition ge25519_sub_expr :=
-        Eval cbv beta delta [fe25519 add mul sub Let_In twice_d] in sub.
+        Eval cbv beta delta [fe25519 add mul sub Let_In] in sub.
 
     Definition ge25519_sub' (P Q: @interp_type Z FE) :
         { r: @HL.expr Z (@interp_type Z) FE
@@ -137,15 +141,14 @@ Module GF25519.
   End SubExpr.
 
   Module MulExpr <: Expression.
-    Definition bits: nat := 64.
+    Definition bits: nat := bits.
     Definition inputs: nat := 20.
-    Definition width: Width bits := W64.
+    Definition width: Width bits := width.
     Definition ResultType := FE.
-    Definition inputUpperBounds: list (@WordRangeOpt bits) :=
-      makeBoundList 20 (makeRange 0 (Z.of_N (Npow2 28))).
+    Definition inputUpperBounds: list (@WordRangeOpt bits) := feBound ++ feBound.
 
     Definition ge25519_mul_expr :=
-        Eval cbv beta delta [fe25519 add mul sub Let_In twice_d] in mul.
+        Eval cbv beta delta [fe25519 add mul sub Let_In] in mul.
 
     Definition ge25519_mul' (P Q: @interp_type Z FE) :
         { r: @HL.expr Z (@interp_type Z) FE
@@ -191,15 +194,14 @@ Module GF25519.
   End MulExpr.
 
   Module OppExpr <: Expression.
-    Definition bits: nat := 64.
+    Definition bits: nat := bits.
     Definition inputs: nat := 10.
-    Definition width: Width bits := W64.
+    Definition width: Width bits := width.
     Definition ResultType := FE.
-    Definition inputUpperBounds: list (@WordRangeOpt bits) :=
-      makeBoundList 10 (makeRange 0 (Z.of_N (Npow2 28))).
+    Definition inputUpperBounds: list (@WordRangeOpt bits) := feBound.
 
     Definition ge25519_opp_expr :=
-        Eval cbv beta delta [fe25519 add mul sub opp Let_In twice_d] in opp.
+        Eval cbv beta delta [fe25519 add mul sub opp Let_In] in opp.
 
     Definition ge25519_opp' (P: @interp_type Z FE) :
         { r: @HL.expr Z (@interp_type Z) FE
diff --git a/src/Assembly/WordizeUtil.v b/src/Assembly/WordizeUtil.v
index d0b563368..d4a9409e2 100644
--- a/src/Assembly/WordizeUtil.v
+++ b/src/Assembly/WordizeUtil.v
@@ -806,6 +806,57 @@ Section TopLevel.
       apply wordize_plus; assumption.
   Qed.
 
+  Lemma wordize_sub: forall {n} (x y: word n) low0 high0 low1 high1,
+     (low0 <= wordToN x)%N -> (wordToN x <= high0)%N
+   -> (low1 <= wordToN y)%N -> (wordToN y <= high1)%N
+   -> (&x >= &y)%N -> (& (x ^- y) <= high0 - low1)%N.
+  Proof.
+    intros.
+
+    destruct (Nge_dec 0%N (&y)). {
+      unfold wminus, wneg.
+      replace (& y) with 0%N in * by nomega.
+      replace low1 with 0%N by (symmetry; apply N.le_0_r; assumption).
+      replace (Npow2 n - 0)%N with (& (wzero n) + Npow2 n)%N
+        by (rewrite wordToN_zero; nomega).
+      rewrite <- Npow2_ignore.
+      rewrite wplus_comm.
+      rewrite wplus_unit.
+      replace (high0 - 0)%N with high0 by nomega; assumption.
+    }
+
+    assert (& x - & y < Npow2 n)%N. {
+      transitivity (wordToN x);
+        try apply word_size_bound;
+        apply N.sub_lt;
+        [apply N.ge_le|]; assumption.
+    }
+
+    assert (& x - & y + & y < Npow2 n)%N. {
+      replace (& x - & y + & y)%N
+        with (wordToN x) by nomega;
+        apply word_size_bound.
+    }
+
+    assert (x = NToWord n (wordToN x - wordToN y) ^+ y) as Hv. {
+      apply NToWord_equal.
+      rewrite <- wordize_plus; rewrite wordToN_NToWord; try assumption.
+      nomega.
+    }
+
+    rewrite Hv.
+    unfold wminus.
+    rewrite <- wplus_assoc.
+    rewrite wminus_inv.
+    rewrite wplus_comm.
+    rewrite wplus_unit.
+    rewrite wordToN_NToWord; try assumption.
+
+    transitivity (high0 - & y)%N;
+    [apply N.sub_le_mono_r | apply N.sub_le_mono_l];
+    assumption.
+  Qed.
+
   Lemma wordize_mult: forall {n} (x y: word n),
       (&x * &y < Npow2 n)%N
     -> (&x * &y)%N = &(x ^* y).