diff options
| -rw-r--r-- | _CoqProject | 2 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemInterface.v | 30 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 52 |
3 files changed, 63 insertions, 21 deletions
diff --git a/_CoqProject b/_CoqProject index 904d716b8..49fad12e0 100644 --- a/_CoqProject +++ b/_CoqProject @@ -35,13 +35,13 @@ src/Experiments/SpecEd25519.v src/ModularArithmetic/ExtendedBaseVector.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v +src/ModularArithmetic/ModularBaseSystemInterface.v src/ModularArithmetic/ModularBaseSystemOpt.v src/ModularArithmetic/ModularBaseSystemProofs.v src/ModularArithmetic/Pre.v src/ModularArithmetic/PrimeFieldTheorems.v src/ModularArithmetic/PseudoMersenneBaseParamProofs.v src/ModularArithmetic/PseudoMersenneBaseParams.v -src/ModularArithmetic/PseudoMersenneBaseRep.v src/ModularArithmetic/Tutorial.v src/Spec/CompleteEdwardsCurve.v src/Spec/EdDSA.v diff --git a/src/ModularArithmetic/ModularBaseSystemInterface.v b/src/ModularArithmetic/ModularBaseSystemInterface.v new file mode 100644 index 000000000..b0cfffe8b --- /dev/null +++ b/src/ModularArithmetic/ModularBaseSystemInterface.v @@ -0,0 +1,30 @@ +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystem. +Require Import Crypto.ModularArithmetic.ModularBaseSystemOpt. +Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. +Require Import Crypto.BaseSystemProofs. +Require Import Crypto.Util.Tuple Crypto.Util.CaseUtil. +Require Import ZArith. +Import PseudoMersenneBaseParams PseudoMersenneBaseParamProofs. + +Generalizable All Variables. +Section s. + Context `{prm:PseudoMersenneBaseParams m} {sc : SubtractionCoefficient m prm}. + + Definition frep := tuple Z (length PseudoMersenneBaseParamProofs.base). + + Definition mul : frep -> frep -> frep. + refine (on_tuple2 (mul_opt k c) _). + abstract (intros; rewrite mul_opt_correct; auto using length_mul). + Defined. + + Definition add : frep -> frep -> frep. + refine (on_tuple2 add_opt _). + abstract (intros; rewrite add_opt_correct, add_length_exact; case_max; omega). + Defined. + + Definition sub : frep -> frep -> frep. + refine (on_tuple2 sub_opt _). + abstract (intros; rewrite sub_opt_correct; apply length_sub; rewrite ?coeff_length; auto). + Defined. +End S.
\ No newline at end of file diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 6f82a8950..eaa1fc19e 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -56,20 +56,27 @@ Section PseudoMersenneProofs. subst; auto. Qed. + Lemma length_sub : forall c x u v, + length c = length base + -> length u = length base + -> length v = length base + -> length (ModularBaseSystem.sub c x u v) = length base. + Proof. + autounfold; unfold ModularBaseSystem.sub; intuition idtac. + rewrite sub_length, add_length_exact. + case_max; try rewrite Max.max_r; omega. + Qed. + Lemma sub_rep : forall c c_0modq, (length c = length base)%nat -> forall u v x y, u ~= x -> v ~= y -> ModularBaseSystem.sub c c_0modq u v ~= (x-y)%F. Proof. - autounfold; unfold ModularBaseSystem.sub; intuition. { - rewrite sub_length. - case_max; try rewrite Max.max_r; try omega. - auto using add_same_length. - } - unfold decode in *; unfold BaseSystem.decode in *. - rewrite BaseSystemProofs.sub_rep, BaseSystemProofs.add_rep. - rewrite ZToField_sub, ZToField_add, ZToField_mod. - rewrite c_0modq, F_add_0_l. - subst; auto. + split; autounfold in *. + { apply length_sub; intuition (auto; omega). } + { unfold decode, ModularBaseSystem.sub, BaseSystem.decode in *; intuition idtac. + rewrite BaseSystemProofs.sub_rep, BaseSystemProofs.add_rep. + rewrite ZToField_sub, ZToField_add, ZToField_mod. + rewrite c_0modq, F_add_0_l. congruence. } Qed. Lemma decode_short : forall (us : BaseSystem.digits), @@ -155,23 +162,28 @@ Section PseudoMersenneProofs. apply Max.max_l; omega. Qed. - Lemma mul_rep : forall u v x y, u ~= x -> v ~= y -> u .* v ~= (x*y)%F. + Lemma length_mul : forall u v, + length u = length base + -> length v = length base + -> length (u .* v) = length base. Proof. - autounfold; unfold ModularBaseSystem.mul; intuition. - { + autounfold in *; unfold ModularBaseSystem.mul in *; intuition eauto. apply reduce_length. rewrite mul_length_exact, extended_base_length; try omega. destruct u; try congruence. rewrite @nil_length0 in *. pose proof base_length_nonzero; omega. - } { + Qed. + + Lemma mul_rep : forall u v x y, u ~= x -> v ~= y -> u .* v ~= (x*y)%F. + Proof. + split; autounfold in *; unfold ModularBaseSystem.mul in *. + { apply length_mul; intuition auto. } + { intuition idtac; subst. rewrite ZToField_mod, reduce_rep, <-ZToField_mod. - rewrite mul_rep by - (apply ExtBaseVector || rewrite extended_base_length; omega). - subst. - do 2 rewrite decode_short by omega. - apply ZToField_mul. - } + rewrite mul_rep by (apply ExtBaseVector || rewrite extended_base_length; omega). + rewrite 2decode_short by omega. + apply ZToField_mul. } Qed. Lemma set_nth_sum : forall n x us, (n < length us)%nat -> |