integrate bitwise operations

4 files changed, 71 insertions, 42 deletions

diff --git a/src/EdDSARepChange.v b/src/EdDSARepChange.v
index 2e745ffea..5bbea7f48 100644
--- a/src/EdDSARepChange.v
+++ b/src/EdDSARepChange.v
@@ -5,7 +5,7 @@ Require Import Crypto.Algebra. Import Group ScalarMult.
 Require Import Crypto.Util.Decidable Crypto.Util.Option Crypto.Util.Tactics.
 Require Import Coq.omega.Omega.
 Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil Util.LetIn.
+Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil Util.LetIn Util.NatUtil.
 Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems.
 
 Import Notations.
@@ -204,29 +204,21 @@ Section EdDSA.
             {Proper_SRepMul:Proper (SRepEq==>SRepEq==>SRepEq) SRepMul}.
     Context {ErepB:Erep} {ErepB_correct:ErepEq ErepB (EToRep B)}.
 
-    Context {wbRepKeepLow wbRepClearLow wbRepClearBit wbRepSetBit:nat->word b->word b}.
-    Context {wbRepSetBit_correct : forall n x, wordToNat (wbRepSetBit n x) = setbit (wordToNat x) n}.
-    Context {wbRepClearLow_correct : forall c x, wordToNat (wbRepClearLow c x) = wordToNat x - wordToNat x mod 2 ^ c}.
-    Context {wbRepKeepLow_correct : forall n x, wordToNat (wbRepKeepLow n x) = (wordToNat x) mod (2^n)}.
-    Context {SRepDecModLShort} {SRepDecModLShort_correct: forall (w:word b), SRepEq (S2Rep (F.of_nat _ (wordToNat w))) (SRepDecModLShort w)}.
+    Context {SRepDecModLShort} {SRepDecModLShort_correct: forall (w:word (n+1)), SRepEq (S2Rep (F.of_nat _ (wordToNat w))) (SRepDecModLShort w)}.
 
     (* We would ideally derive the optimized implementations from
     specifications using `setoid_rewrite`, but doing this without
     inlining let-bound subexpressions turned out to be quite messy in
     the current state of Coq: <https://github.com/mit-plv/fiat-crypto/issues/64> *)
 
+    Let n_le_bpb : (n <= b+b)%nat. destruct prm. omega. Qed.
+
     Definition splitSecretPrngCurve (sk:word b) : SRep * word b :=
       dlet hsk := H _ sk in
-      dlet curveKey := SRepDecModLShort (wbRepSetBit n (wbRepClearLow c (wbRepKeepLow n (split1 b b hsk)))) in
+      dlet curveKey := SRepDecModLShort (clearlow c (@wfirstn n _ hsk n_le_bpb) ++ wones 1) in
       dlet prngKey := split2 b b hsk in
       (curveKey, prngKey).
 
-    (* TODO: prove these, somewhere *)
-    Axiom wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) mod (2^a).
-    Axiom wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordToNat w) mod (2^a).
-    Axiom nat_mod_smaller_power_of_two : forall n b:nat,
-      (n <= b -> forall x:nat, (x mod 2 ^ b) mod 2 ^ n = (x mod 2^n))%nat.
-
     Lemma splitSecretPrngCurve_correct sk :
       let (s, r) := splitSecretPrngCurve sk in
       SRepEq s (S2Rep (F.of_nat l (curveKey sk))) /\ r = prngKey (H:=H) sk.
@@ -235,12 +227,16 @@ Section EdDSA.
         repeat (
             reflexivity
             || rewrite <-SRepDecModLShort_correct
-            || rewrite wbRepSetBit_correct
-            || rewrite wbRepClearLow_correct
-            || rewrite wbRepKeepLow_correct
             || rewrite wordToNat_split1
             || rewrite wordToNat_wfirstn
-            || rewrite nat_mod_smaller_power_of_two by (destruct prm; omega)
+            || rewrite wordToNat_combine
+            || rewrite wordToNat_clearlow
+            || rewrite (eq_refl:wordToNat (wones 1) = 1)
+            || rewrite mult_1_r
+            || rewrite setbit_high by
+              ( pose proof (Nat.pow_nonzero 2 n); specialize_by discriminate;
+                set (x := wordToNat (H b sk));
+                assert (x mod 2 ^ n < 2^n)%nat by (apply Nat.mod_bound_pos; omega); omega)
           ).
     Qed.
 
diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index 8b75b4502..dd6a9bed2 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -70,7 +70,7 @@ Proof.
     reflexivity.
 Defined.
 
-Fail Definition extended_to_coord (P : Erep) : (GF25519.fe25519 * GF25519.fe25519) :=
+Definition extended_to_coord (P : Erep) : (GF25519.fe25519 * GF25519.fe25519) :=
   CompleteEdwardsCurve.E.coordinates (ExtendedCoordinates.Extended.to_twisted P).
 
 Lemma encode_eq_iff :  forall x y : ModularArithmetic.F.F GF25519.modulus,
@@ -107,7 +107,7 @@ Definition feEnc (x : GF25519.fe25519) : Word.word 255 :=
             (Word.combine (ZNWord 32 x5)
               (Word.combine (ZNWord 32 x6) (ZNWord 31 x7))))))).
 
-Fail Let ERepEnc :=
+Let ERepEnc :=
   (PointEncoding.Kencode_point
          (Ksign := feSign)
          (Kenc := feEnc)
@@ -126,7 +126,7 @@ Let S2Rep := fun (x : ModularArithmetic.F.F l) =>
 
 
 
-Fail Check @sign_correct
+Check @sign_correct
       (* E := *) E
       (* Eeq := *) CompleteEdwardsCurveTheorems.E.eq
       (* Eadd := *) CompleteEdwardsCurve.E.add
@@ -172,15 +172,8 @@ Fail Check @sign_correct
       (* Proper_SRepMul := *) _
       (* ErepB := *) _
       (* ErepB_correct := *) _
-      (* wbRepKeepLow := *) _
-      (* wbRepClearLow := *) _
-      (* wbRepSetBit := *) _
-      (* wbRepSetBit_correct := *) _
-      (* wbRepClearLow_correct := *) _
-      (* wbRepKeepLow_correct := *) _
       (* SRepDecModLShort := *) _
       (* SRepDecModLShort_correct := *) _
       .
 
-
 Check verify_correct.
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 21002dad5..ea9a5653e 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -305,3 +305,6 @@ Hint Rewrite min_idempotent_S_l : natsimplify.
 Lemma min_idempotent_S_r x : min x (S x) = x.
 Proof. omega *. Qed.
 Hint Rewrite min_idempotent_S_r : natsimplify.
+
+Lemma setbit_high : forall x i, (x < 2^i -> setbit x i = x + 2^i)%nat.
+Admitted.
\ No newline at end of file
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index a7eec6fb4..a89d02364 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -5,6 +5,8 @@ Require Import Crypto.Util.Tactics.
 Require Import Bedrock.Word.
 Require Import Coq.Classes.RelationClasses.
 Require Import Coq.Program.Program.
+Require Import Coq.Numbers.Natural.Peano.NPeano Util.NatUtil.
+Require Import Coq.micromega.Psatz.
 
 Local Open Scope nat_scope.
 
@@ -68,7 +70,7 @@ Lemma combine_eq_iff {a b} (A:word a) (B:word b) C :
 Proof. intuition; subst; auto using split1_combine, split2_combine, combine_split. Qed.
 
 Class wordsize_eq (x y : nat) := wordsize_eq_to_eq : x = y.
-Ltac wordsize_eq_tac := cbv beta delta [wordsize_eq] in *; omega.
+Ltac wordsize_eq_tac := cbv beta delta [wordsize_eq] in *; omega*.
 Ltac gt84_abstract t := t. (* TODO: when we drop Coq 8.4, use [abstract] here *)
 Hint Extern 100 (wordsize_eq _ _) => gt84_abstract wordsize_eq_tac : typeclass_instances.
 
@@ -80,27 +82,62 @@ Program Fixpoint cast_word {n m} : forall {pf:wordsize_eq n m}, word n -> word m
   end.
 Global Arguments cast_word {_ _ _} _. (* 8.4 does not pick up the forall braces *)
 
+Lemma cast_word_refl {n} pf (w:word n) : @cast_word n n pf w = w.
+Proof. induction w; simpl; auto using f_equal. Qed.
+
+Lemma wordToNat_cast_word {n} (w:word n) m pf :
+  wordToNat (@cast_word n m pf w) = wordToNat w.
+Proof. destruct pf; rewrite cast_word_refl; trivial. Qed.
+
+Lemma wordToN_cast_word {n} (w:word n) m pf :
+  wordToN (@cast_word n m pf w) = wordToN w.
+Proof. destruct pf; rewrite cast_word_refl; trivial. Qed.
+
+Import NPeano Nat.
 Local Infix "++" := combine.
 
-Definition keeplow n {b} {H:n <= b} (w:word b) : word b :=
-  wand (cast_word( wones n ++ wzero (b-n) )) w.
+Definition zext_ge n {m} {pf:m <= n} (w:word m) : word n :=
+  cast_word (w ++ wzero (n - m)).
 
-Definition clearlow n {b} {H:n <= b} (w:word b) : word b :=
-  wand (cast_word( wzero n ++ wones (b-n) )) w.
+Definition keeplow {b} n (w:word b) : word b :=
+  wand (cast_word( wones (min b n) ++ wzero (b-n) )) w.
 
-Definition setbit n {b} {H:n < b} (w:word b) : word b :=
+Definition clearlow {b} n (w:word b) : word b :=
+  wand (cast_word( wzero (min b n) ++ wones (b-n) )) w.
+
+Definition setbit {b} n {H:n < b} (w:word b) : word b :=
   wor (cast_word( wzero n ++ wones 1 ++ wzero (b-n-1) )) w.
 
-Definition clearbit n {b} {H:n < b} (w:word b) : word b :=
+Definition clearbit {b} n {H:n < b} (w:word b) : word b :=
   wand (cast_word( wones n ++ wzero 1 ++ wones (b-n-1) )) w.
 
-Lemma cast_word_refl {n} pf (w:word n) : @cast_word n n pf w = w.
-Proof. induction w; simpl; auto using f_equal. Qed.
+Lemma wordToNat_wzero {n} : wordToNat (wzero n) = 0.
+Proof.
+  unfold wzero; induction n; simpl; try rewrite_hyp!*; omega.
+Qed.
 
-Lemma wordToNnat_cast_word {n} (w:word n) m pf :
-  wordToN (@cast_word n m pf w) = wordToN w.
-Proof. destruct pf; rewrite cast_word_refl; trivial. Qed.
+Lemma wordToNat_combine : forall {a} (wa:word a) {b} (wb:word b),
+  wordToNat (wa ++ wb) = wordToNat wa + 2^a * wordToNat wb.
+Proof.
+  induction wa; intros; simpl; rewrite ?IHwa; break_match; nia.
+Qed.
 
-Lemma wordToN_cast_word {n} (w:word n) m pf :
-  wordToN (@cast_word n m pf w) = wordToN w.
-Proof. destruct pf; rewrite cast_word_refl; trivial. Qed.
+Lemma wordToNat_zext_ge {n m pf} (w:word m) : wordToNat (@zext_ge n m pf w) = wordToNat w.
+Proof.
+  unfold zext_ge.
+  rewrite wordToNat_cast_word, wordToNat_combine, wordToNat_wzero; nia.
+Qed.
+
+Lemma wordToNat_clearlow {b} (c : nat) (x : Word.word b) :
+  wordToNat (clearlow c x) = wordToNat x - (wordToNat x) mod (2^c).
+Admitted.
+
+Lemma wordToNat_keeplow {b} (c : nat) (x : Word.word b) :
+  wordToNat (keeplow c x) = (wordToNat x) mod (2^c).
+Admitted.
+
+Lemma wordToNat_split1 : forall a b w, wordToNat (split1 a b w) = (wordToNat w) mod (2^a).
+Admitted.
+
+Lemma wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordToNat w) mod (2^a).
+Admitted.
\ No newline at end of file