diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-05-09 20:18:02 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-05-09 20:18:02 -0400 |
| commit | ee74b50cb4ccf6c0e4f6b7573a3a5c099ec621e1 (patch) | |
| tree | c96cdba7354218ef8231603e390c925c75597a40 /src/Specific/GF25519.v | |
| parent | 728b2f95dc83329c58aef7624283cb945c77b919 (diff) | |
Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid unsigned integer underflow. Also changed rep in Specific proofs so that it is PseudoMersenneBaseRep.rep rather than ModularBaseSystem.rep; these are equivalent but the first is the abstraction level we want.
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 1f6be80cc..b01e6280e 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.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 params25519 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 10%nat 255. Defined. +Definition mul2modulus := Eval compute in (construct_mul2modulus params25519). + +Instance subCoeff : SubtractionCoefficient modulus params25519. + apply Build_SubtractionCoefficient with (coeff := mul2modulus); cbv; auto. +Defined. + (* END PseudoMersenneBaseParams instance construction. *) (* Precompute k and c *) @@ -61,4 +68,17 @@ Proof. intros f g 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 |