diff options
Diffstat (limited to 'src/Specific/GF25519.v')
| -rw-r--r-- | src/Specific/GF25519.v | 59 |
1 files changed, 32 insertions, 27 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 6298941db..7ece3a5da 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -1,16 +1,19 @@ -Require Import Crypto.ModularArithmetic.ModularBaseSystem. -Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Import Crypto.ModularArithmetic.ModularBaseSystemField. Require Import Coq.Lists.List Crypto.Util.ListUtil. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.ModularArithmetic.ModularBaseSystemInterface. Require Import Crypto.Tactics.VerdiTactics. -Require Import Crypto.BaseSystem. -Require Import Algebra. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Notations. +Require Import Crypto.Algebra. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Require Import Crypto.Util.Notations. Local Open Scope Z. (* BEGIN PseudoMersenneBaseParams instance construction. *) @@ -23,12 +26,13 @@ Instance params25519 : PseudoMersenneBaseParams modulus. construct_params prime_modulus 10%nat 255. Defined. -Definition mul2modulus := Eval compute in (construct_mul2modulus params25519). +Definition fe25519 := Eval compute in (tuple Z (length limb_widths)). + +Definition mul2modulus : fe25519 := + Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params25519)). Instance subCoeff : SubtractionCoefficient modulus params25519. apply Build_SubtractionCoefficient with (coeff := mul2modulus). - cbv; auto. - cbv [ModularBaseSystem.decode]. apply ZToField_eqmod. cbv; reflexivity. Defined. @@ -45,11 +49,10 @@ Definition k_ := Eval compute in k. Definition c_ := Eval compute in c. Definition k_subst : k = k_ := eq_refl k_. Definition c_subst : c = c_ := eq_refl c_. -Definition fe25519 : Type := Eval cbv in fe. Local Opaque Z.shiftr Z.shiftl Z.land Z.mul Z.add Z.sub Let_In. -Definition app_10 (f : fe25519) (P : fe25519 -> fe25519) : fe25519. +Definition app_5 (f : fe25519) (P : fe25519 -> fe25519) : fe25519. Proof. cbv [fe25519] in *. set (f0 := f). @@ -58,7 +61,7 @@ Proof. apply f0. Defined. -Lemma app_10_correct : forall f P, app_10 f P = P f. +Definition app_5_correct f (P : fe25519 -> fe25519) : app_5 f P = P f. Proof. intros. cbv [fe25519] in *. @@ -67,16 +70,16 @@ Proof. Qed. Definition appify2 (op : fe25519 -> fe25519 -> fe25519) (f g : fe25519):= - app_10 f (fun f0 => (app_10 g (fun g0 => op f0 g0))). + app_5 f (fun f0 => (app_5 g (fun g0 => op f0 g0))). Lemma appify2_correct : forall op f g, appify2 op f g = op f g. Proof. intros. cbv [appify2]. - etransitivity; apply app_10_correct. + etransitivity; apply app_5_correct. Qed. Definition add_sig (f g : fe25519) : - { fg : fe25519 | fg = ModularBaseSystemInterface.add f g}. + { fg : fe25519 | fg = add_opt f g}. Proof. eexists. rewrite <-appify2_correct. @@ -89,12 +92,12 @@ Definition add (f g : fe25519) : fe25519 := proj1_sig (add_sig f g). Definition add_correct (f g : fe25519) - : add f g = ModularBaseSystemInterface.add f g := + : add f g = add_opt f g := Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (add_sig f g). Definition sub_sig (f g : fe25519) : - { fg : fe25519 | fg = ModularBaseSystemInterface.sub f g}. + { fg : fe25519 | fg = sub_opt f g}. Proof. eexists. rewrite <-appify2_correct. @@ -107,12 +110,14 @@ Definition sub (f g : fe25519) : fe25519 := proj1_sig (sub_sig f g). Definition sub_correct (f g : fe25519) - : sub f g = ModularBaseSystemInterface.sub f g := + : sub f g = sub_opt f g := Eval cbv beta iota delta [proj1_sig sub_sig] in proj2_sig (sub_sig f g). +(* For multiplication, we add another layer of definition so that we can + rewrite under the [let] binders. *) Definition mul_simpl_sig (f g : fe25519) : - { fg : fe25519 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}. + { fg : fe25519 | fg = carry_mul_opt k_ c_ f g}. Proof. cbv [fe25519] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. @@ -127,15 +132,15 @@ Definition mul_simpl (f g : fe25519) : fe25519 := proj1_sig (mul_simpl_sig f g). Definition mul_simpl_correct (f g : fe25519) - : mul_simpl f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g := + : mul_simpl f g = carry_mul_opt k_ c_ f g := Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in proj2_sig (mul_simpl_sig f g). Definition mul_sig (f g : fe25519) : - { fg : fe25519 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}. + { fg : fe25519 | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. - rewrite <- mul_simpl_correct. + rewrite <-mul_simpl_correct. rewrite <-appify2_correct. cbv. reflexivity. @@ -146,8 +151,8 @@ Definition mul (f g : fe25519) : fe25519 := proj1_sig (mul_sig f g). Definition mul_correct (f g : fe25519) - : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g := - Eval cbv beta iota delta [proj1_sig mul_sig] in + : mul f g = carry_mul_opt k_ c_ f g := + Eval cbv beta iota delta [proj1_sig add_sig] in proj2_sig (mul_sig f g). Import Morphisms. @@ -155,12 +160,12 @@ Import Morphisms. Lemma field25519 : @field fe25519 eq zero one opp add sub mul inv div. Proof. pose proof (Equivalence_Reflexive : Reflexive eq). - eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_subst c_subst)). + eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_ c_ k_subst c_subst)). Grab Existential Variables. + reflexivity. + reflexivity. + reflexivity. - + intros; rewrite mul_correct; reflexivity. + + intros; rewrite mul_correct. reflexivity. + intros; rewrite sub_correct; reflexivity. + intros; rewrite add_correct; reflexivity. + reflexivity. |