diff options
author | Andres Erbsen <andreser@mit.edu> | 2015-11-06 14:52:00 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2015-11-06 14:52:00 -0500 |
commit | 06575718a966e87903a883b736b3623d580800fd (patch) | |
tree | 88c68efdf524c60ddfa8f9c38b894ce146c38d0b /src/Specific | |
parent | d7fda87eb069080ffd29421eff048aeffb52fac5 (diff) |
instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19)
Diffstat (limited to 'src/Specific')
-rw-r--r-- | src/Specific/GF25519.v | 59 |
1 files changed, 55 insertions, 4 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. |