diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Galois/ModularBaseSystem.v | 2 | ||||
-rw-r--r-- | src/Specific/GF25519.v | 78 | ||||
-rw-r--r-- | src/Util/ListUtil.v | 9 |
3 files changed, 87 insertions, 2 deletions
diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v index 61ca58442..de5c40f1b 100644 --- a/src/Galois/ModularBaseSystem.v +++ b/src/Galois/ModularBaseSystem.v @@ -55,7 +55,7 @@ Module Type GFrep (Import M:Modulus). (* we will want a non-trivial implementation later, currently square x = mul x x *) End GFrep. -Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBaseParams BC M) <: GFrep M. +Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBaseParams BC M) (* TODO(jadep): "<: GFrep M" *). Module Import GF := GaloisTheory M. Module EC <: BaseCoefs. Definition base := BC.base ++ (map (Z.mul (2^(P.k))) BC.base). diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v new file mode 100644 index 000000000..25405b988 --- /dev/null +++ b/src/Specific/GF25519.v @@ -0,0 +1,78 @@ +Require Import Galois GaloisTheory Galois.BaseSystem. +Require Import List Util.ListUtil. +Import ListNotations. +Require Import ZArith.ZArith Zpower ZArith Znumtheory. +Require Import QArith.QArith QArith.Qround. +Require Import VerdiTactics. + +Module Base25Point5_10limbs <: BaseCoefs. + 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. + Qed. + Lemma base_good : + forall i j, (i+j < length base)%nat -> + let b := nth_default 0 base in + let r := (b i * b j) / b (i+j)%nat in + b i * b j = r * b (i+j)%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. +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 4d807c779..e8be33dac 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -128,7 +128,7 @@ 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). @@ -136,6 +136,13 @@ Proof. 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. + Lemma combine_truncate_r : forall {A} (xs ys : list A), combine xs ys = combine xs (firstn (length xs) ys). Proof. |