diff options
-rw-r--r-- | src/Experiments/Ed25519.v | 75 | ||||
-rw-r--r-- | src/Util/WordUtil.v | 126 |
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. |