From 471465f4bfce4a68078b924bf2099d0281313a00 Mon Sep 17 00:00:00 2001
From: jadep <jade.philipoom@gmail.com>
Date: Tue, 14 Feb 2017 09:57:43 -0500
Subject: move lemmas from Ed25519 to WordUtil

---
 src/Experiments/Ed25519.v | 68 -----------------------------------------------
 1 file changed, 68 deletions(-)

(limited to 'src/Experiments')

diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v
index 1e3611399..db28ffe34 100644
--- a/src/Experiments/Ed25519.v
+++ b/src/Experiments/Ed25519.v
@@ -980,74 +980,6 @@ Proof.
   reflexivity.
 Qed.
 
-(* MOVE : WordUtil *) (* TODO : automate *)
-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.
-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; simpl; 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; simpl; reflexivity.
-Qed.
-
-(* MOVE : WordUtil *) (* TODO : automate *)
-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.
-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; simpl; reflexivity.
-Qed.
-
-(* MOVE : WordUtil *)
-Lemma WordNZ_range : forall {n} B w,
-  (2 ^ Z.of_nat n <= B)%Z ->
-  (0 <= Z.of_N (@Word.wordToN n w) < B)%Z.
-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.
-
-(* MOVE : WordUtil *)
-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.
-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; simpl; omega.
-Qed.
-
 (* MOVE : same place as feDec *) (* TODO : automate *)
 Lemma feDec_correct : forall w : Word.word (pred b),
         option_eq GF25519BoundedCommon.eq
-- 
cgit v1.2.3