Most of the admits in Ed25519.v

2 files changed, 195 insertions, 6 deletions

diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index d3b9c4af6..90cac35e2 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -1072,33 +1072,96 @@ Admitted.
 
 Lemma WordNZ_split1 : forall {n m} w,
     Z.of_N (Word.wordToN (Word.split1 n m w)) = ZUtil.Z.pow2_mod (Z.of_N (Word.wordToN w)) n.
-Admitted.
+Proof.
+  intros; unfold ZUtil.Z.pow2_mod.
+  rewrite WordUtil.wordToN_split1.
+  apply Z.bits_inj_iff'; intros k Hpos.
+  rewrite Z.land_spec.
+  repeat (rewrite Z2N.inj_testbit; [|assumption]).
+  rewrite N.land_spec; f_equal.
+  rewrite WordUtil.wordToN_wones.
+
+  destruct (WordUtil.Nge_dec (Z.to_N k) (N.of_nat n)).
+
+  - rewrite Z.ones_spec_high, N.ones_spec_high;
+      [reflexivity|apply N.ge_le; assumption|split; [omega|]].
+    apply Z2N.inj_le; [apply Nat2Z.is_nonneg|assumption|].
+    etransitivity; [|apply N.ge_le; eassumption].
+    apply N.eq_le_incl.
+    induction n; cbn; reflexivity.
+
+  - rewrite Z.ones_spec_low, N.ones_spec_low;
+      [reflexivity|assumption|split; [omega|]].
+    apply Z2N.inj_lt; [assumption|apply Nat2Z.is_nonneg|].
+    eapply N.lt_le_trans; [eassumption|].
+    apply N.eq_le_incl.
+    induction n; cbn; reflexivity.
+Qed.
 
 Lemma WordNZ_split2 : forall {n m} w,
     Z.of_N (Word.wordToN (Word.split2 n m w)) = Z.shiftr (Z.of_N (Word.wordToN w)) n.
-Admitted.
+Proof.
+  intros; unfold ZUtil.Z.pow2_mod.
+  rewrite WordUtil.wordToN_split2.
+  apply Z.bits_inj_iff'; intros k Hpos.
+  rewrite Z2N.inj_testbit; [|assumption].
+  rewrite Z.shiftr_spec, N.shiftr_spec; [|apply N2Z.inj_le; rewrite Z2N.id|]; try assumption.
+  rewrite Z2N.inj_testbit; [f_equal|omega].
+  rewrite Z2N.inj_add; [f_equal|assumption|apply Nat2Z.is_nonneg].
+  induction n; cbn; reflexivity.
+Qed.
 
 Lemma WordNZ_range : forall {n} B w,
   (2 ^ Z.of_nat n <= B)%Z ->
   (0 <= Z.of_N (@Word.wordToN n w) < B)%Z.
-Admitted.
+Proof.
+  intros n B w H.
+  split; [apply N2Z.is_nonneg|].
+  eapply Z.lt_le_trans; [apply N2Z.inj_lt; apply WordUtil.word_size_bound|].
+  rewrite WordUtil.Npow2_N, N2Z.inj_pow, nat_N_Z.
+  assumption.
+Qed.
 
 Lemma WordNZ_range_mono : forall {n} m w,
   (Z.of_nat n <= m)%Z ->
   (0 <= Z.of_N (@Word.wordToN n w) < 2 ^ m)%Z.
-Admitted.
+Proof.
+  intros n m w H.
+  split; [apply N2Z.is_nonneg|].
+  eapply Z.lt_le_trans; [apply N2Z.inj_lt; apply WordUtil.word_size_bound|].
+  rewrite WordUtil.Npow2_N, N2Z.inj_pow, nat_N_Z.
+  apply Z.pow_le_mono; [|assumption].
+  split; cbn; omega.
+Qed.
 
 (* TODO : move to ZUtil *)
 Lemma pow2_mod_range : forall a n m,
+  (0 <= n)%Z ->
   (n <= m)%Z ->
   (0 <= ZUtil.Z.pow2_mod a n < 2 ^ m)%Z.
-Admitted.
+Proof.
+  intros; unfold ZUtil.Z.pow2_mod.
+  rewrite Z.land_ones; [|assumption].
+  split; [apply Z.mod_pos_bound, WordUtil.Z_pow2_gt_0; assumption|].
+  eapply Z.lt_le_trans; [apply Z.mod_pos_bound, WordUtil.Z_pow2_gt_0; assumption|].
+  apply Z.pow_le_mono; [|assumption].
+  split; cbn; omega.
+Qed.
 
 (* TODO : move to ZUtil *)
 Lemma shiftr_range : forall a n m,
+  (0 <= n)%Z ->
+  (0 <= m)%Z ->
   (0 <= a < 2 ^ (n + m))%Z ->
   (0 <= Z.shiftr a n < 2 ^ m)%Z.
-Admitted.
+Proof.
+  intros a n m H0 H1 H2; destruct H2.
+  split; [apply Z.shiftr_nonneg; assumption|].
+  rewrite Z.shiftr_div_pow2; [|assumption].
+  apply Z.div_lt_upper_bound; [apply WordUtil.Z_pow2_gt_0; assumption|].
+  eapply Z.lt_le_trans; [eassumption|apply Z.eq_le_incl].
+  apply Z.pow_add_r; omega.
+Qed.
 
 Lemma feDec_correct : forall w : Word.word (pred b),
         option_eq GF25519BoundedCommon.eq
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 97d40db6b..58917dff5 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -5,6 +5,7 @@ Require Import Coq.Classes.RelationClasses.
 Require Import Coq.Program.Program.
 Require Import Coq.Numbers.Natural.Peano.NPeano Util.NatUtil.
 Require Import Coq.micromega.Psatz.
+Require Import Coq.Bool.Bool.
 
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Tactics.
@@ -386,6 +387,131 @@ Section WordToN.
           reflexivity.
   Qed.
 
+  Lemma wordToN_split1: forall {n m} x,
+    wordToN (@split1 n m x) = N.land (wordToN x) (wordToN (wones n)).
+  Proof.
+    intros.
+
+    pose proof (Word.combine_split _ _ x) as C; revert C.
+    generalize (split1 n m x) as a, (split2 n m x) as b.
+    intros a b C; rewrite <- C; clear C x.
+
+    apply N.bits_inj_iff; unfold N.eqf; intro x.
+    rewrite N.land_spec.
+    repeat rewrite wordToN_testbit.
+    revert x a b.
+
+    induction n, m; intros;
+      shatter a; shatter b;
+      induction (N.to_nat x) as [|n0];
+      try rewrite <- (Nat2N.id n0);
+      try rewrite andb_false_r;
+      try rewrite andb_true_r;
+      simpl; intuition.
+  Qed.
+
+  Lemma wordToN_split2: forall {n m} x,
+    wordToN (@split2 n m x) = N.shiftr (wordToN x) (N.of_nat n).
+  Proof.
+    intros.
+
+    pose proof (Word.combine_split _ _ x) as C; revert C.
+    generalize (split1 n m x) as a, (split2 n m x) as b.
+    intros a b C.
+    rewrite <- C; clear C x.
+
+    apply N.bits_inj_iff; unfold N.eqf; intro x;
+      rewrite N.shiftr_spec;
+      repeat rewrite wordToN_testbit;
+      try apply N_ge_0.
+
+    revert x a b.
+    induction n, m; intros;
+      shatter a;
+      try apply N_ge_0.
+
+    - simpl; intuition.
+
+    - replace (x + N.of_nat 0)%N with x by nomega.
+      simpl; intuition.
+
+    - rewrite (IHn x (wtl a) b).
+      rewrite <- (N2Nat.id x).
+      repeat rewrite <- Nat2N.inj_add.
+      repeat rewrite Nat2N.id; simpl.
+      replace (N.to_nat x + S n) with (S (N.to_nat x + n)) by omega.
+      reflexivity.
+
+    - rewrite (IHn x (wtl a) b).
+      rewrite <- (N2Nat.id x).
+      repeat rewrite <- Nat2N.inj_add.
+      repeat rewrite Nat2N.id; simpl.
+      replace (N.to_nat x + S n) with (S (N.to_nat x + n)) by omega.
+      reflexivity.
+  Qed.
+
+  Lemma wordToN_wones: forall x, wordToN (wones x) = N.ones (N.of_nat x).
+  Proof.
+    induction x.
+
+    - simpl; intuition.
+
+    - rewrite Nat2N.inj_succ.
+      replace (wordToN (wones (S x))) with (2 * wordToN (wones x) + N.b2n true)%N
+        by (simpl; rewrite ?N.succ_double_spec; simpl; nomega).
+      replace (N.ones (N.succ _))
+         with (2 * N.ones (N.of_nat x) + N.b2n true)%N.
+
+      + rewrite IHx; nomega.
+
+      + replace (N.succ (N.of_nat x)) with (1 + (N.of_nat x))%N by (
+          rewrite N.add_comm; nomega).
+        rewrite N.ones_add.
+        replace (N.ones 1) with 1%N by (
+          unfold N.ones; simpl; intuition).
+        simpl.
+        reflexivity.
+  Qed.
+
+  Local Tactic Notation "replaceAt1" constr(x) "with" constr(y) "by" tactic(tac) :=
+    let tmp := fresh in
+    set (tmp := x) at 1;
+    replace tmp with y by (unfold tmp; tac);
+    clear tmp.
+
+  Lemma wordToN_combine: forall {n m} a b,
+    wordToN (@Word.combine n a m b)
+      = N.lxor (N.shiftl (wordToN b) (N.of_nat n)) (wordToN a).
+  Proof.
+    intros; symmetry.
+
+    replaceAt1 a with (Word.split1 _ _ (Word.combine a b))
+      by (apply Word.split1_combine).
+
+    replaceAt1 b with (Word.split2 _ _ (Word.combine a b))
+      by (apply Word.split2_combine).
+
+    generalize (Word.combine a b); intro x; clear a b.
+
+    rewrite wordToN_split1, wordToN_split2, wordToN_wones.
+    generalize (wordToN x); clear x; intro x.
+    apply N.bits_inj_iff; unfold N.eqf; intro k.
+    rewrite N.lxor_spec.
+
+    destruct (Nge_dec k (N.of_nat n)).
+
+    - rewrite N.shiftl_spec_high; try apply N_ge_0;
+        [|apply N.ge_le; assumption].
+      rewrite N.shiftr_spec; try apply N_ge_0.
+      replace (k - N.of_nat n + N.of_nat n)%N with k by nomega.
+      rewrite N.land_spec, N.ones_spec_high; [|apply N.ge_le; assumption].
+      induction (N.testbit x k); cbv; reflexivity.
+
+    - rewrite N.shiftl_spec_low; try assumption; try apply N_ge_0.
+      rewrite N.land_spec, N.ones_spec_low; [|nomega].
+      induction (N.testbit x k); cbv; reflexivity.
+  Qed.
+
   Lemma NToWord_equal: forall n (x y: word n),
       wordToN x = wordToN y -> x = y.
   Proof.