From 19b850574a479ccd7984b584d89e67513d719a01 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 21 Jul 2016 11:23:18 -0400 Subject: re-introduced extra field isomorphism layer for 8.4 compatibility and better organization of reasoning. --- src/ModularArithmetic/ModularBaseSystemField.v | 71 +++++++++++++++++++++++++ src/ModularArithmetic/ModularBaseSystemOpt.v | 7 +++ src/ModularArithmetic/Pow2Base.v | 1 - src/Specific/GF1305.v | 72 ++++++++++---------------- src/Specific/GF25519.v | 70 +++++++++---------------- 5 files changed, 130 insertions(+), 91 deletions(-) create mode 100644 src/ModularArithmetic/ModularBaseSystemField.v (limited to 'src') diff --git a/src/ModularArithmetic/ModularBaseSystemField.v b/src/ModularArithmetic/ModularBaseSystemField.v new file mode 100644 index 000000000..f5bedd644 --- /dev/null +++ b/src/ModularArithmetic/ModularBaseSystemField.v @@ -0,0 +1,71 @@ +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Algebra. Import Field. +Require Import Crypto.Util.Tuple Crypto.Util.Notations. +Local Open Scope Z_scope. + +Section ModularBaseSystemField. + Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient modulus prm} + (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_). + Local Notation base := (Pow2Base.base_from_limb_widths limb_widths). + Local Notation digits := (tuple Z (length limb_widths)). + + Lemma add_decode : forall a b : digits, + decode (add_opt a b) = (decode a + decode b)%F. + Proof. + intros; rewrite add_opt_correct by assumption. + apply add_rep; apply decode_rep. + Qed. + + Lemma sub_decode : forall a b : digits, + decode (sub_opt a b) = (decode a - decode b)%F. + Proof. + intros; rewrite sub_opt_correct by assumption. + apply sub_rep; auto using coeff_mod, decode_rep. + Qed. + + Lemma mul_decode : forall a b : digits, + decode (carry_mul_opt k_ c_ a b) = (decode a * decode b)%F. + Proof. + intros; rewrite carry_mul_opt_correct by assumption. + apply carry_mul_rep; apply decode_rep. + Qed. + + Lemma zero_neq_one : eq zero one -> False. + Proof. + cbv [eq zero one]. erewrite !encode_rep. intro A. + eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). + congruence. + Qed. + + Lemma modular_base_system_field : + @field digits eq zero one opp add_opt sub_opt (carry_mul_opt k_ c_) inv div. + Proof. + eapply (Field.isomorphism_to_subfield_field (phi := decode) (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))). + Grab Existential Variables. + + intros; eapply encode_rep. + + intros; eapply encode_rep. + + intros; eapply encode_rep. + + intros; eapply encode_rep. + + intros; eapply mul_decode. + + intros; eapply sub_decode. + + intros; eapply add_decode. + + intros; eapply encode_rep. + + cbv [eq zero one]. erewrite !encode_rep. intro A. + eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). + congruence. + + trivial. + + repeat intro. cbv [div]. congruence. + + repeat intro. cbv [inv]. congruence. + + repeat intro. cbv [eq]. erewrite !mul_decode. congruence. + + repeat intro. cbv [eq]. erewrite !sub_decode. congruence. + + repeat intro. cbv [eq]. erewrite !add_decode. congruence. + + repeat intro. cbv [opp]. congruence. + + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec. + Qed. + +End ModularBaseSystemField. \ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index d1a6f6228..4543ff67d 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -528,6 +528,13 @@ Section Multiplication. Definition carry_mul_opt_cps_correct {T} (f:digits -> T) (us vs : digits) : carry_mul_opt_cps f us vs = f (carry_mul us vs) := proj2_sig (carry_mul_opt_sig f us vs). + + Definition carry_mul_opt := carry_mul_opt_cps id. + + Definition carry_mul_opt_correct (us vs : digits) + : carry_mul_opt us vs = carry_mul us vs := + carry_mul_opt_cps_correct id us vs. + End Multiplication. Section with_base. diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v index acc96ad73..c23cf8f40 100644 --- a/src/ModularArithmetic/Pow2Base.v +++ b/src/ModularArithmetic/Pow2Base.v @@ -39,7 +39,6 @@ Section Pow2Base. encode' z i' ++ (Z.shiftr (Z.land z (Z.ones (lw i))) (lw i')) :: nil end. - (* max must be greater than input; this is used to truncate last digit *) Definition encodeZ x:= encode' x (length limb_widths). (** ** Carrying *) diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index 9e9b69dbd..c30485f5e 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -1,10 +1,11 @@ Require Import Crypto.BaseSystem. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. 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.Tactics.VerdiTactics. Require Import Crypto.Util.ZUtil. @@ -80,25 +81,25 @@ Proof. Qed. Definition add_sig (f g : fe1305) : - { fg : fe1305 | fg = ModularBaseSystem.add f g}. + { fg : fe1305 | fg = add_opt f g}. Proof. eexists. - rewrite <-appify2_correct. (* Coq 8.4 : 6s *) + rewrite <-appify2_correct. cbv. reflexivity. -Defined. (* Coq 8.4 : 7s *) +Defined. Definition add (f g : fe1305) : fe1305 := Eval cbv beta iota delta [proj1_sig add_sig] in proj1_sig (add_sig f g). Definition add_correct (f g : fe1305) - : add f g = ModularBaseSystem.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). (* Coq 8.4 : 10s *) + proj2_sig (add_sig f g). Definition sub_sig (f g : fe1305) : - { fg : fe1305 | fg = ModularBaseSystem.sub mul2modulus f g}. + { fg : fe1305 | fg = sub_opt f g}. Proof. eexists. rewrite <-appify2_correct. @@ -111,19 +112,18 @@ Definition sub (f g : fe1305) : fe1305 := proj1_sig (sub_sig f g). Definition sub_correct (f g : fe1305) - : sub f g = ModularBaseSystem.sub mul2modulus 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). (* Coq 8.4 : 10s *) + 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 : fe1305) : - { fg : fe1305 | fg = ModularBaseSystem.mul f g}. + { fg : fe1305 | fg = carry_mul_opt k_ c_ f g}. Proof. cbv [fe1305] in *. repeat match goal with p : (_ * Z)%type |- _ => destruct p end. eexists. - rewrite <-mul_opt_correct with (k_ := k_) (c_ := c_) by auto. cbv. autorewrite with zsimplify. reflexivity. @@ -134,64 +134,46 @@ Definition mul_simpl (f g : fe1305) : fe1305 := proj1_sig (mul_simpl_sig f g). Definition mul_simpl_correct (f g : fe1305) - : mul_simpl f g = ModularBaseSystem.mul 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 : fe1305) : - { fg : fe1305 | fg = ModularBaseSystem.mul f g}. + { fg : fe1305 | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. rewrite <-mul_simpl_correct. rewrite <-appify2_correct. cbv. reflexivity. -Defined. (* Coq 8.4 : 14s *) +Defined. Definition mul (f g : fe1305) : fe1305 := Eval cbv beta iota delta [proj1_sig mul_sig] in proj1_sig (mul_sig f g). +Print mul. + Definition mul_correct (f g : fe1305) - : mul f g = ModularBaseSystem.mul f g := + : 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). (* Coq 8.4 : 5s *) - -Definition decode := Eval compute in ModularBaseSystem.decode. + proj2_sig (mul_sig f g). Import Morphisms. Lemma field1305 : @field fe1305 eq zero one opp add sub mul inv div. Proof. pose proof (Equivalence_Reflexive : Reflexive eq). - eapply (Field.isomorphism_to_subfield_field (phi := decode) - (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))). + eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_ c_ k_subst c_subst)). Grab Existential Variables. - + intros; change decode with ModularBaseSystem.decode; apply encode_rep. - + intros; change decode with ModularBaseSystem.decode; apply encode_rep. - + intros; change decode with ModularBaseSystem.decode; apply encode_rep. - + intros; change decode with ModularBaseSystem.decode; apply encode_rep. - + intros; change decode with ModularBaseSystem.decode. - rewrite mul_correct; apply mul_rep; reflexivity. - + intros; change decode with ModularBaseSystem.decode. - rewrite sub_correct; apply sub_rep; try reflexivity. - rewrite <- coeff_mod. reflexivity. - + intros; change decode with ModularBaseSystem.decode. - rewrite add_correct; apply add_rep; reflexivity. - + intros; change decode with ModularBaseSystem.decode; apply encode_rep. - + cbv [eq zero one]. change decode with ModularBaseSystem.decode. - rewrite !encode_rep. intro A. - eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). congruence. - + trivial. - + repeat intro. cbv [div]. congruence. - + repeat intro. cbv [inv]. congruence. - + repeat intro. cbv [eq] in *. rewrite !mul_correct, !mul_rep by reflexivity; congruence. - + repeat intro. cbv [eq] in *. rewrite !sub_correct. rewrite !sub_rep by - (rewrite <-?coeff_mod; reflexivity); congruence. - + repeat intro. cbv [eq] in *. rewrite !add_correct, !add_rep by reflexivity; congruence. - + repeat intro. cbv [opp]. congruence. - + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec. - + apply (eq_Equivalence (prm := params1305)). + + reflexivity. + + reflexivity. + + reflexivity. + + intros; rewrite mul_correct. reflexivity. + + intros; rewrite sub_correct; reflexivity. + + intros; rewrite add_correct; reflexivity. + + reflexivity. + + reflexivity. Qed. (* diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 2f1da1846..7ece3a5da 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -1,10 +1,11 @@ Require Import Crypto.BaseSystem. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. 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.Tactics.VerdiTactics. Require Import Crypto.Util.ZUtil. @@ -27,7 +28,7 @@ Defined. Definition fe25519 := Eval compute in (tuple Z (length limb_widths)). -Definition mul2modulus := +Definition mul2modulus : fe25519 := Eval compute in (from_list_default 0%Z (length limb_widths) (construct_mul2modulus params25519)). Instance subCoeff : SubtractionCoefficient modulus params25519. @@ -51,7 +52,7 @@ Definition c_subst : c = c_ := eq_refl c_. 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). @@ -60,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 *. @@ -69,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 = ModularBaseSystem.add f g}. + { fg : fe25519 | fg = add_opt f g}. Proof. eexists. rewrite <-appify2_correct. @@ -91,12 +92,12 @@ Definition add (f g : fe25519) : fe25519 := proj1_sig (add_sig f g). Definition add_correct (f g : fe25519) - : add f g = ModularBaseSystem.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). (* Coq 8.4 : 10s *) + proj2_sig (add_sig f g). Definition sub_sig (f g : fe25519) : - { fg : fe25519 | fg = ModularBaseSystem.sub mul2modulus f g}. + { fg : fe25519 | fg = sub_opt f g}. Proof. eexists. rewrite <-appify2_correct. @@ -109,19 +110,18 @@ Definition sub (f g : fe25519) : fe25519 := proj1_sig (sub_sig f g). Definition sub_correct (f g : fe25519) - : sub f g = ModularBaseSystem.sub mul2modulus 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 = ModularBaseSystem.mul 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. eexists. - rewrite <-mul_opt_correct with (k_ := k_) (c_ := c_) by auto. cbv. autorewrite with zsimplify. reflexivity. @@ -132,12 +132,12 @@ 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 = ModularBaseSystem.mul 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 = ModularBaseSystem.mul f g}. + { fg : fe25519 | fg = carry_mul_opt k_ c_ f g}. Proof. eexists. rewrite <-mul_simpl_correct. @@ -151,45 +151,25 @@ Definition mul (f g : fe25519) : fe25519 := proj1_sig (mul_sig f g). Definition mul_correct (f g : fe25519) - : mul f g = ModularBaseSystem.mul f g := + : 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). -Definition decode := Eval compute in ModularBaseSystem.decode. - Import Morphisms. Lemma field25519 : @field fe25519 eq zero one opp add sub mul inv div. Proof. pose proof (Equivalence_Reflexive : Reflexive eq). - eapply (Field.isomorphism_to_subfield_field (phi := decode) - (fieldR := PrimeFieldTheorems.field_modulo (prime_q := prime_modulus))). + eapply (Field.equivalent_operations_field (fieldR := modular_base_system_field k_ c_ k_subst c_subst)). Grab Existential Variables. - + intros; change decode with ModularBaseSystem.decode; apply encode_rep. - + intros; change decode with ModularBaseSystem.decode; apply encode_rep. - + intros; change decode with ModularBaseSystem.decode; apply encode_rep. - + intros; change decode with ModularBaseSystem.decode; apply encode_rep. - + intros; change decode with ModularBaseSystem.decode. - rewrite mul_correct; apply mul_rep; reflexivity. - + intros; change decode with ModularBaseSystem.decode. - rewrite sub_correct; apply sub_rep; try reflexivity. - rewrite <- coeff_mod. reflexivity. - + intros; change decode with ModularBaseSystem.decode. - rewrite add_correct; apply add_rep; reflexivity. - + intros; change decode with ModularBaseSystem.decode; apply encode_rep. - + cbv [eq zero one]. change decode with ModularBaseSystem.decode. - rewrite !encode_rep. intro A. - eapply (PrimeFieldTheorems.Fq_1_neq_0 (prime_q := prime_modulus)). congruence. - + trivial. - + repeat intro. cbv [div]. congruence. - + repeat intro. cbv [inv]. congruence. - + repeat intro. cbv [eq] in *. rewrite !mul_correct, !mul_rep by reflexivity; congruence. - + repeat intro. cbv [eq] in *. rewrite !sub_correct. rewrite !sub_rep by - (rewrite <-?coeff_mod; reflexivity); congruence. - + repeat intro. cbv [eq] in *. rewrite !add_correct, !add_rep by reflexivity; congruence. - + repeat intro. cbv [opp]. congruence. - + cbv [eq]. auto using ModularArithmeticTheorems.F_eq_dec. - + apply (eq_Equivalence (prm := params25519)). + + reflexivity. + + reflexivity. + + reflexivity. + + intros; rewrite mul_correct. reflexivity. + + intros; rewrite sub_correct; reflexivity. + + intros; rewrite add_correct; reflexivity. + + reflexivity. + + reflexivity. Qed. -- cgit v1.2.3