instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19)

2 files changed, 63 insertions, 5 deletions

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 3841d9b07..25405b988 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -1,13 +1,13 @@
-Require Import Galois.BaseSystem.
+Require Import Galois GaloisTheory Galois.BaseSystem.
 Require Import List Util.ListUtil.
 Import ListNotations.
-Require Import ZArith.ZArith.
+Require Import ZArith.ZArith Zpower ZArith Znumtheory.
 Require Import QArith.QArith QArith.Qround.
 Require Import VerdiTactics.
 
 Module Base25Point5_10limbs <: BaseCoefs.
-  Definition base := map (fun i => two_p (Qceiling (Z_of_nat i *255 # 10))) (seq 0 10).
   Local Open Scope Z_scope.
+  Definition base := map (fun i => two_p (Qceiling (Z_of_nat i *255 # 10))) (seq 0 10).
   Lemma base_positive : forall b, In b base -> b > 0.
   Proof.
     compute; intros; repeat break_or_hyp; intuition.
@@ -22,6 +22,57 @@ Module Base25Point5_10limbs <: BaseCoefs.
     assert (In i (seq 0 (length base))) by nth_tac.
     assert (In j (seq 0 (length base))) by nth_tac.
     subst b; subst r; simpl in *.
-    repeat break_or_hyp; try omega; auto.
+    repeat break_or_hyp; try omega; vm_compute; reflexivity.
   Qed.
 End Base25Point5_10limbs.
+
+Module Modulus25519 <: Modulus.
+  Local Open Scope Z_scope.
+  Definition two_255_19 := two_p 255 - 19.
+  Lemma two_255_19_prime : prime two_255_19. Admitted.
+  Definition prime25519 := exist _ two_255_19 two_255_19_prime.
+  Definition modulus := prime25519.
+End Modulus25519.
+
+Module GF25519Base25Point5. (*TODO(jadep): "<: PseudoMersenneBaseParams Base25Point5_10limbs Modulus25519."*)
+  Import Base25Point5_10limbs.
+  Import Modulus25519.
+  Local Open Scope Z_scope.
+  (* TODO: do we actually want B and M "up there" in the type parameters? I was
+  * imagining writing something like "Paramter Module M : Modulus". *)
+
+  Definition k := 255.
+  Definition c := 19.
+  Lemma modulus_pseudomersenne :
+    primeToZ modulus = 2^k - c.
+  Proof.
+    reflexivity.
+  Qed.
+
+  Lemma base_matches_modulus :
+    forall i j,
+    (i   <  length base)%nat ->
+    (j   <  length base)%nat ->
+    (i+j >= length base)%nat ->
+    let b := nth_default 0 base in
+    let r := (b i * b j)  /  (2^k * b (i+j-length base)%nat) in
+              b i * b j = r * 2^k * b (i+j-length base)%nat.
+  Proof.
+    intros.
+    assert (In i (seq 0 (length base))) by nth_tac.
+    assert (In j (seq 0 (length base))) by nth_tac.
+    subst b; subst r; simpl in *.
+    repeat break_or_hyp; try omega; vm_compute; reflexivity.
+  Qed.
+
+
+  Lemma b0_1 : nth_default 0 base 0 = 1.
+  Proof.
+    reflexivity.
+  Qed.
+
+  Lemma k_pos : 0 <= k.
+  Proof.
+    rewrite Zle_is_le_bool; reflexivity.
+  Qed.
+End GF25519Base25Point5.
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index d1c12dbfd..1eb9c5075 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -118,10 +118,17 @@ Lemma combine_set_nth : forall {A B} n (x:A) xs (ys:list B),
     | Some y => set_nth n (x,y) (combine xs ys)
     end.
 Proof.
-  (* TODO(andreser): this proof can totally be automated, but requires writing ltac that vets multiple hypothesis at once *)
+  (* TODO(andreser): this proof can totally be automated, but requires writing ltac that vets multiple hypotheses at once *)
   induction n, xs, ys; nth_tac; try rewrite IHn; nth_tac; 
     try (f_equal; specialize (IHn x xs ys ); rewrite H in IHn; rewrite <- IHn);
     try (specialize (nth_error_value_length _ _ _ _ H); omega).
   assert (Some b0=Some b1) as HA by (rewrite <-H, <-H0; auto).
   injection HA; intros; subst; auto.
 Qed.
+
+Lemma nth_value_index : forall {T} i xs (x:T),
+  nth_error xs i = Some x -> In i (seq 0 (length xs)).
+Proof.
+  induction i; destruct xs; nth_tac; right.
+  rewrite <- seq_shift; apply in_map; eapply IHi; eauto.
+Qed.