diff options
Diffstat (limited to 'src/Specific/GF1305.v')
| -rw-r--r-- | src/Specific/GF1305.v | 22 |
1 files changed, 21 insertions, 1 deletions
diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index 9d11cf8e1..b004a60d1 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -2,6 +2,7 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystem. Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseRep. Require Import Coq.Lists.List Crypto.Util.ListUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.Tactics.VerdiTactics. @@ -19,6 +20,12 @@ Instance params1305 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 5%nat 130. Defined. +Definition mul2modulus := Eval compute in (construct_mul2modulus params1305). + +Instance subCoeff : SubtractionCoefficient modulus params1305. + apply Build_SubtractionCoefficient with (coeff := mul2modulus); cbv; auto. +Defined. + (* END PseudoMersenneBaseParams instance construction. *) (* Precompute k and c *) @@ -38,7 +45,7 @@ Lemma GF1305Base26_mul_reduce_formula : -> rep ls (f*g)%F}. Proof. eexists; intros ? ? Hf Hg. - pose proof (carry_mul_opt_correct k_ c_ (eq_refl k_) (eq_refl c_) [0;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg. + pose proof (carry_mul_opt_correct k_ c_ (eq_refl k) (eq_refl c_) [0;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg. compute_formula. Defined. @@ -51,4 +58,17 @@ Proof. eexists; intros ? ? Hf Hg. pose proof (add_opt_rep _ _ _ _ Hf Hg) as Hfg. compute_formula. +Defined. + +Lemma GF25519Base25Point5_sub_formula : + forall f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 + g0 g1 g2 g3 g4 g5 g6 g7 g8 g9, + {ls | forall f g, rep [f0;f1;f2;f3;f4;f5;f6;f7;f8;f9] f + -> rep [g0;g1;g2;g3;g4;g5;g6;g7;g8;g9] g + -> rep ls (f - g)%F}. +Proof. + eexists. + intros f g Hf Hg. + pose proof (sub_opt_rep _ _ _ _ Hf Hg) as Hfg. + compute_formula. Defined.
\ No newline at end of file |