diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 18 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 94 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 46 | ||||
-rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseRep.v | 4 | ||||
-rw-r--r-- | src/Specific/GF1305.v | 2 | ||||
-rw-r--r-- | src/Specific/GF25519.v | 2 |
6 files changed, 89 insertions, 77 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index a1258674e..9c6a58f9a 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -61,25 +61,25 @@ Section CarryBasePow2. Definition carry_sequence is us := fold_right carry us is. -End CarryBasePow2. - -Section Canonicalization. - Context `{prm :PseudoMersenneBaseParams}. - Fixpoint make_chain i := match i with | O => nil | S i' => i' :: make_chain i' end. - (* compute at compile time *) Definition full_carry_chain := make_chain (length limb_widths). + Definition carry_full := carry_sequence full_carry_chain. + + Definition carry_mul us vs := carry_full (mul us vs). + +End CarryBasePow2. + +Section Canonicalization. + Context `{prm :PseudoMersenneBaseParams}. + (* compute at compile time *) Definition max_ones := Z.ones (fold_right Z.max 0 limb_widths). - - (* compute at compile time? *) - Definition carry_full := carry_sequence full_carry_chain. Definition max_bound i := Z.ones (log_cap i). diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index b2c9ee0fa..4fd9748c5 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -28,6 +28,8 @@ Definition nth_default_opt {A} := Eval compute in @nth_default A. Definition set_nth_opt {A} := Eval compute in @set_nth A. Definition map_opt {A B} := Eval compute in @map A B. Definition base_from_limb_widths_opt := Eval compute in base_from_limb_widths. +Definition full_carry_chain_opt := Eval compute in @full_carry_chain. +Definition length_opt := Eval compute in length. Definition Let_In {A P} (x : A) (f : forall y : A, P y) := let y := x in f y. @@ -226,14 +228,35 @@ Section Carries. Lemma carry_sequence_opt_cps_rep : forall (is : list nat) (us : list Z) (x : F modulus), (forall i : nat, In i is -> i < length base)%nat -> - length us = length base -> rep us x -> rep (carry_sequence_opt_cps is us) x. Proof. intros. rewrite carry_sequence_opt_cps_correct by assumption. - apply carry_sequence_rep; assumption. + apply carry_sequence_rep; eauto using rep_length. Qed. + + Lemma full_carry_chain_bounds : forall i, In i full_carry_chain -> (i < length base)%nat. + Proof. + unfold full_carry_chain; rewrite <-base_length; intros. + apply make_chain_lt; auto. + Qed. + + Definition carry_full_opt_sig (us : digits) : { b : digits | b = carry_full us }. + Proof. + eexists. + cbv [carry_full]. + change @full_carry_chain with full_carry_chain_opt. + rewrite <-carry_sequence_opt_cps_correct by (auto; apply full_carry_chain_bounds). + reflexivity. + Defined. + + Definition carry_full_opt (us : digits) : digits + := Eval cbv [proj1_sig carry_full_opt_sig] in proj1_sig (carry_full_opt_sig us). + + Definition carry_full_opt_correct us : carry_full_opt us = carry_full us := + proj2_sig (carry_full_opt_sig us). + End Carries. Section Addition. @@ -433,33 +456,32 @@ Section Multiplication. : mul_opt us vs = mul us vs := proj2_sig (mul_opt_sig us vs). - Lemma mul_opt_rep: + Definition carry_mul_opt_sig (us vs : T) : { b : digits | b = carry_mul us vs }. + Proof. + eexists. + cbv [carry_mul]. + erewrite <-carry_full_opt_correct by eauto. + erewrite <-mul_opt_correct. + reflexivity. + Defined. + + Definition carry_mul_opt (us vs : T) : digits + := Eval cbv [proj1_sig carry_mul_opt_sig] in proj1_sig (carry_mul_opt_sig us vs). + + Definition carry_mul_opt_correct us vs + : carry_mul_opt us vs = carry_mul us vs + := proj2_sig (carry_mul_opt_sig us vs). + + Lemma carry_mul_opt_rep: forall (u v : T) (x y : F modulus), PseudoMersenneBaseRep.rep u x -> PseudoMersenneBaseRep.rep v y -> - PseudoMersenneBaseRep.rep (mul_opt u v) (x * y)%F. + PseudoMersenneBaseRep.rep (carry_mul_opt u v) (x * y)%F. Proof. intros. - rewrite mul_opt_correct. - change mul with PseudoMersenneBaseRep.mul. + rewrite carry_mul_opt_correct. + change carry_mul with PseudoMersenneBaseRep.mul. auto using PseudoMersenneBaseRep.mul_rep. Qed. - Definition carry_mul_opt - (is : list nat) - (us vs : list Z) - : list Z - := carry_sequence_opt_cps c_ is (mul_opt us vs). - - Lemma carry_mul_opt_correct - : forall (is : list nat) (us vs : list Z) (x y: F modulus), - PseudoMersenneBaseRep.rep us x -> PseudoMersenneBaseRep.rep vs y -> - (forall i : nat, In i is -> i < length base)%nat -> - length (mul_opt us vs) = length base -> - PseudoMersenneBaseRep.rep (carry_mul_opt is us vs) (x*y)%F. - Proof. - intros is us vs x y; intros. - change (carry_mul_opt _ _ _) with (carry_sequence_opt_cps c_ is (mul_opt us vs)). - apply carry_sequence_opt_cps_rep, mul_opt_rep; auto. - Qed. End Multiplication. Section Canonicalization. @@ -475,8 +497,6 @@ Section Canonicalization. Definition max_ones_opt := Eval compute in max_ones. Definition max_bound_opt := Eval compute in max_bound. - Definition full_carry_chain_opt := Eval compute in full_carry_chain. - Definition length_opt := Eval compute in length. Definition minus_opt := Eval compute in minus. Definition isFull'_opt_sig (us : T) full i : @@ -494,27 +514,6 @@ Section Canonicalization. Definition isFull'_opt_correct us full i: isFull'_opt us full i = isFull' us full i := proj2_sig (isFull'_opt_sig us full i). - Lemma full_carry_chain_bounds : forall i, In i full_carry_chain -> (i < length base)%nat. - Proof. - unfold full_carry_chain; rewrite <-base_length; intros. - apply make_chain_lt; auto. - Qed. - - Definition carry_full_opt_sig (us : T) : { b : digits | b = carry_full us }. - Proof. - eexists. - cbv [carry_full]. - change full_carry_chain with full_carry_chain_opt. - rewrite <-(carry_sequence_opt_cps_correct c_) by (auto; apply full_carry_chain_bounds). - reflexivity. - Defined. - - Definition carry_full_opt (us : T) : digits - := Eval cbv [proj1_sig carry_full_opt_sig] in proj1_sig (carry_full_opt_sig us). - - Definition carry_full_opt_correct us : carry_full_opt us = carry_full us := - proj2_sig (carry_full_opt_sig us). - Definition and_term_opt_sig (us : T) : { b : Z | b = and_term us }. Proof. eexists. @@ -536,8 +535,7 @@ Section Canonicalization. Proof. eexists. cbv beta iota delta [freeze map2]. - repeat rewrite <-carry_full_opt_correct. - change (@carry_full modulus prm) with @carry_full_opt. + repeat erewrite <-carry_full_opt_correct by eauto. change and_term with and_term_opt. change @map with @map_opt. reflexivity. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 0aa83ae6b..562c7d6d4 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -22,6 +22,11 @@ Section PseudoMersenneProofs. autounfold; intuition. Qed. + Lemma rep_length : forall us x, us ~= x -> length us = length base. + Proof. + autounfold; intuition. + Qed. + Lemma encode_rep : forall x : F modulus, encode x ~= x. Proof. intros. unfold encode, rep. @@ -385,6 +390,31 @@ Section CarryProofs. induction is; boring. Qed. + + (* TODO : move? *) + Lemma make_chain_lt : forall x i : nat, In i (make_chain x) -> (i < x)%nat. + Proof. + induction x; simpl; intuition. + Qed. + + Lemma carry_full_preserves_rep : forall us x, + rep us x -> rep (carry_full us) x. + Proof. + unfold carry_full; intros. + apply carry_sequence_rep; auto. + unfold full_carry_chain; rewrite base_length; apply make_chain_lt. + eauto using rep_length. + Qed. + + Opaque carry_full. + + Lemma carry_mul_rep : forall us vs x y, rep us x -> rep vs y -> + rep (carry_mul us vs) (x * y)%F. + Proof. + unfold carry_mul; intros; apply carry_full_preserves_rep. + auto using mul_rep. + Qed. + End CarryProofs. Section CanonicalizationProofs. @@ -1132,22 +1162,6 @@ Section CanonicalizationProofs. (* END proofs about third carry loop *) - (* TODO : move? *) - Lemma make_chain_lt : forall x i : nat, In i (make_chain x) -> (i < x)%nat. - Proof. - induction x; simpl; intuition. - Qed. - - Lemma carry_full_preserves_rep : forall us x, (length us = length base)%nat -> - rep us x -> rep (carry_full us) x. - Proof. - unfold carry_full; intros. - apply carry_sequence_rep; auto. - unfold full_carry_chain; rewrite base_length; apply make_chain_lt. - Qed. - - Opaque carry_full. - Lemma isFull'_false : forall us n, isFull' us false n = false. Proof. unfold isFull'; induction n; intros; rewrite Bool.andb_false_r; auto. diff --git a/src/ModularArithmetic/PseudoMersenneBaseRep.v b/src/ModularArithmetic/PseudoMersenneBaseRep.v index 5f3644cca..6b4d29a35 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseRep.v +++ b/src/ModularArithmetic/PseudoMersenneBaseRep.v @@ -45,6 +45,6 @@ Instance PseudoMersenneBase m (prm : PseudoMersenneBaseParams m) (sc : Subtracti sub := ModularBaseSystem.sub coeff coeff_mod; sub_rep := ModularBaseSystemProofs.sub_rep coeff coeff_mod coeff_length; - mul := ModularBaseSystem.mul; - mul_rep := ModularBaseSystemProofs.mul_rep + mul := ModularBaseSystem.carry_mul; + mul_rep := ModularBaseSystemProofs.carry_mul_rep }. diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index b004a60d1..31dee21f3 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -45,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_rep k_ c_ (eq_refl k) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg. compute_formula. Defined. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 68278ce4c..37e0c08db 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -47,7 +47,7 @@ Lemma GF25519Base25Point5_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;9;8;7;6;5;4;3;2;1;0]_ _ _ _ Hf Hg) as Hfg. + pose proof (carry_mul_opt_rep k_ c_ (eq_refl k_) (eq_refl c_) _ _ _ _ Hf Hg) as Hfg. compute_formula. Time Defined. |