diff options
54 files changed, 1586 insertions, 2407 deletions
diff --git a/.gitignore b/.gitignore index b2acd253d..fbde72c56 100644 --- a/.gitignore +++ b/.gitignore @@ -39,6 +39,22 @@ src/Specific/NISTP256/AMD64/measure src/Specific/NISTP256/AMD64/test/feadd_test src/Specific/NISTP256/AMD64/test/femul_test src/Specific/NISTP256/AMD64/test/p256_test +src/Specific/NISTP256/AMD128/feadd.c +src/Specific/NISTP256/AMD128/feadd.h +src/Specific/NISTP256/AMD128/femul.c +src/Specific/NISTP256/AMD128/femul.h +src/Specific/NISTP256/AMD128/fenz.c +src/Specific/NISTP256/AMD128/fenz.h +src/Specific/NISTP256/AMD128/feopp.c +src/Specific/NISTP256/AMD128/feopp.h +src/Specific/NISTP256/AMD128/fesub.c +src/Specific/NISTP256/AMD128/fesub.h +src/Specific/NISTP256/AMD128/icc/measure +src/Specific/NISTP256/AMD128/icc/p256_test +src/Specific/NISTP256/AMD128/measure +src/Specific/NISTP256/AMD128/test/feadd_test +src/Specific/NISTP256/AMD128/test/femul_test +src/Specific/NISTP256/AMD128/test/p256_test src/Specific/X25519/C64/femul.c src/Specific/X25519/C64/femul.h src/Specific/X25519/C64/fesquare.c @@ -61,7 +61,7 @@ SPECIAL_VOFILES := src/Specific/%Display.vo UNMADE_VOFILES := # add files to this list to prevent them from being built as final # targets by the "lite" target -LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo src/Specific/X2448/Karatsuba/C64/Synthesis.vo src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.vo src/Specific/X25519/C64/ladderstep.vo src/Specific/X25519/C32/%.vo +LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo src/Specific/X2448/Karatsuba/C64/Synthesis.vo src/Specific/NISTP256/AMD64/Synthesis.vo src/Specific/X25519/C64/ladderstep.vo src/Specific/X25519/C32/%.vo REGULAR_VOFILES := $(filter-out $(SPECIAL_VOFILES),$(VOFILES)) CURVES_PROOFS_PRE_VOFILES := $(filter src/Curves/%Proofs.vo,$(REGULAR_VOFILES)) NO_CURVES_PROOFS_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo diff --git a/_CoqProject b/_CoqProject index 5bcc76f6c..d36554986 100644 --- a/_CoqProject +++ b/_CoqProject @@ -228,22 +228,13 @@ src/Spec/MontgomeryCurve.v src/Spec/MxDH.v src/Spec/WeierstrassCurve.v src/Spec/Test/X25519.v -src/Specific/IntegrationTestMontgomeryP256_128.v -src/Specific/IntegrationTestMontgomeryP256_128Display.v -src/Specific/IntegrationTestMontgomeryP256_128_Add.v -src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v -src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v -src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v -src/Specific/IntegrationTestMontgomeryP256_128_Opp.v -src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v -src/Specific/IntegrationTestMontgomeryP256_128_Sub.v -src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v -src/Specific/MontgomeryP256_128.v src/Specific/Framework/CurveParameters.v src/Specific/Framework/CurveParametersPackage.v src/Specific/Framework/IntegrationTestDisplayCommon.v src/Specific/Framework/IntegrationTestDisplayCommonTactics.v src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v +src/Specific/Framework/MontgomeryReificationTypes.v +src/Specific/Framework/MontgomeryReificationTypesPackage.v src/Specific/Framework/Packages.v src/Specific/Framework/ReificationTypes.v src/Specific/Framework/ReificationTypesPackage.v @@ -259,8 +250,23 @@ src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v src/Specific/Framework/ArithmeticSynthesis/Ladderstep.v src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v +src/Specific/Framework/ArithmeticSynthesis/Montgomery.v +src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v src/Specific/Framework/ArithmeticSynthesis/SquareFromMul.v -src/Specific/NISTP256/AMD64/MontgomeryP256.v +src/Specific/NISTP256/AMD128/CurveParameters.v +src/Specific/NISTP256/AMD128/Synthesis.v +src/Specific/NISTP256/AMD128/feadd.v +src/Specific/NISTP256/AMD128/feaddDisplay.v +src/Specific/NISTP256/AMD128/femul.v +src/Specific/NISTP256/AMD128/femulDisplay.v +src/Specific/NISTP256/AMD128/fenz.v +src/Specific/NISTP256/AMD128/fenzDisplay.v +src/Specific/NISTP256/AMD128/feopp.v +src/Specific/NISTP256/AMD128/feoppDisplay.v +src/Specific/NISTP256/AMD128/fesub.v +src/Specific/NISTP256/AMD128/fesubDisplay.v +src/Specific/NISTP256/AMD64/CurveParameters.v +src/Specific/NISTP256/AMD64/Synthesis.v src/Specific/NISTP256/AMD64/feadd.v src/Specific/NISTP256/AMD64/feaddDisplay.v src/Specific/NISTP256/AMD64/femul.v diff --git a/src/Specific/Framework/ArithmeticSynthesis/Montgomery.v b/src/Specific/Framework/ArithmeticSynthesis/Montgomery.v new file mode 100644 index 000000000..1680fe792 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/Montgomery.v @@ -0,0 +1,491 @@ +Require Import Coq.micromega.Lia. +Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. +Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Proofs. +Require Import Crypto.Arithmetic.Core. Import B. +Require Crypto.Arithmetic.Saturated.MontgomeryAPI. +Require Import Crypto.Arithmetic.Saturated.UniformWeight. +Require Import Crypto.Util.Sigma.Lift. +Require Import Coq.ZArith.BinInt. +Require Import Coq.PArith.BinPos. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ZUtil.ModInv. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Arithmetic.Saturated.UniformWeightInstances. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics. +Require Import Crypto.Util.Tactics.CacheTerm. + +Local Open Scope Z_scope. +Local Infix "^" := Tuple.tuple : type_scope. + +Local Definition sig_by_eq {A P} (x : { a : A | P a }) (a : A) (H : a = proj1_sig x) + : { a : A | P a }. +Proof. + exists a; subst; exact (proj2_sig x). +Defined. + +Section with_args. + Context (wt : nat -> Z) + (r : positive) + (sz : nat) + (m : positive) + (m_enc : Z^sz) + (r' : Z) + (r'_correct : ((Z.pos r * r') mod (Z.pos m) = 1)%Z) + (m' : Z) + (m'_correct : ((Z.pos m * m') mod (Z.pos r) = (-1) mod Z.pos r)%Z) + (m_enc_correct_montgomery : Z.pos m = MontgomeryAPI.eval (n:=sz) (Z.pos r) m_enc) + (r'_pow_correct : ((r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) m_enc = 1)%Z) + (* computable *) + (r_big : Z.pos r > 1) + (m_big : 1 < Z.pos m) + (m_enc_small : small (Z.pos r) m_enc) + (map_m_enc : Tuple.map (Z.land (Z.pos r - 1)) m_enc = m_enc). + + Local Ltac t_fin := + repeat match goal with + | _ => assumption + | [ |- ?x = ?x ] => reflexivity + | [ |- and _ _ ] => split + | [ |- (0 <= MontgomeryAPI.eval (Z.pos r) _)%Z ] => apply MontgomeryAPI.eval_small + | _ => rewrite <- !m_enc_correct_montgomery + | _ => rewrite !r'_correct + | _ => rewrite !Z.mod_1_l by assumption; reflexivity + | _ => rewrite !(Z.mul_comm m' (Z.pos m)) + | _ => lia + end. + + + Local Definition mul'_gen + : { f:Z^sz -> Z^sz -> Z^sz + | forall (A B : Z^sz), + small (Z.pos r) A -> small (Z.pos r) B -> + let eval := MontgomeryAPI.eval (Z.pos r) in + (small (Z.pos r) (f A B) + /\ (eval B < eval m_enc -> 0 <= eval (f A B) < eval m_enc) + /\ (eval (f A B) mod Z.pos m + = (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z + }. + Proof. + exists (fun A B => redc (r:=r)(R_numlimbs:=sz) m_enc A B m'). + abstract ( + intros; + split; [ | split ]; + [ apply small_redc with (ri:=r') | apply redc_bound_N with (ri:=r') | rewrite !m_enc_correct_montgomery; apply redc_mod_N ]; + t_fin + ). + Defined. + + Import ModularArithmetic. + + Definition montgomery_to_F_gen (v : Z) : F m + := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F. + + Local Definition mul_ext_gen + : { f:Z^sz -> Z^sz -> Z^sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + montgomery_to_F_gen (eval (f A B)) + = (montgomery_to_F_gen (eval A) * montgomery_to_F_gen (eval B))%F) + /\ (forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval B < eval m_enc -> 0 <= eval (f A B) < eval m_enc)%Z) }. + Proof. + exists (proj1_sig mul'_gen). + abstract ( + split; intros A Asm B Bsm; + pose proof (proj2_sig mul'_gen A B Asm Bsm) as H; + cbv zeta in *; + try solve [ destruct_head'_and; assumption ]; + rewrite ModularArithmeticTheorems.F.eq_of_Z_iff in H; + unfold montgomery_to_F_gen; + destruct H as [H1 [H2 H3]]; + rewrite H3; + rewrite <- !ModularArithmeticTheorems.F.of_Z_mul; + f_equal; nia + ). + Defined. + + Local Definition add_ext_gen + : { f:Z^sz -> Z^sz -> Z^sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + ((forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval A < eval m_enc + -> eval B < eval m_enc + -> montgomery_to_F_gen (eval (f A B)) + = (montgomery_to_F_gen (eval A) + montgomery_to_F_gen (eval B))%F)) + /\ (forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval A < eval m_enc + -> eval B < eval m_enc + -> 0 <= eval (f A B) < eval m_enc)))%Z }. + Proof. + exists (fun A B => add (r:=r)(R_numlimbs:=sz) m_enc A B). + abstract ( + split; intros; + unfold montgomery_to_F_gen; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?ModularArithmeticTheorems.F.of_Z_add; + rewrite <- ?Z.mul_add_distr_r; + [ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_enc_correct_montgomery; push_Zmod; rewrite eval_add_mod_N; pull_Zmod + | apply add_bound ]; + t_fin + ). + Defined. + + Local Definition sub_ext_gen + : { f:Z^sz -> Z^sz -> Z^sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + ((forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval A < eval m_enc + -> eval B < eval m_enc + -> montgomery_to_F_gen (eval (f A B)) + = (montgomery_to_F_gen (eval A) - montgomery_to_F_gen (eval B))%F)) + /\ (forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval A < eval m_enc + -> eval B < eval m_enc + -> 0 <= eval (f A B) < eval m_enc)))%Z }. + Proof. + exists (fun A B => sub (r:=r) (R_numlimbs:=sz) m_enc A B). + abstract ( + split; intros; + unfold montgomery_to_F_gen; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?ModularArithmeticTheorems.F.of_Z_sub; + rewrite <- ?Z.mul_sub_distr_r; + [ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_enc_correct_montgomery; push_Zmod; rewrite eval_sub_mod_N; pull_Zmod + | apply sub_bound ]; + t_fin + ). + Defined. + + Local Definition opp_ext_gen + : { f:Z^sz -> Z^sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + ((forall (A : Z^sz) (_ : small (Z.pos r) A), + (eval A < eval m_enc + -> montgomery_to_F_gen (eval (f A)) + = (F.opp (montgomery_to_F_gen (eval A)))%F)) + /\ (forall (A : Z^sz) (_ : small (Z.pos r) A), + (eval A < eval m_enc + -> 0 <= eval (f A) < eval m_enc)))%Z }. + Proof. + exists (fun A => opp (r:=r) (R_numlimbs:=sz) m_enc A). + abstract ( + split; intros; + unfold montgomery_to_F_gen; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?F_of_Z_opp; + rewrite <- ?Z.mul_opp_l; + [ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_enc_correct_montgomery; push_Zmod; rewrite eval_opp_mod_N; pull_Zmod + | apply opp_bound ]; + t_fin + ). + Defined. + + Local Definition nonzero_ext_gen + : { f:Z^sz -> Z + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Z^sz) (_ : small (Z.pos r) A), + (eval A < eval m_enc + -> f A = 0 <-> (montgomery_to_F_gen (eval A) = F.of_Z m 0))%Z }. + Proof. + exists (fun A => nonzero (R_numlimbs:=sz) A). + abstract ( + intros eval A H **; rewrite (@eval_nonzero r) by (eassumption || reflexivity); + subst eval; + unfold montgomery_to_F_gen, uweight in *; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul; + rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_enc_correct_montgomery; + let H := fresh in + split; intro H; + [ rewrite H; autorewrite with zsimplify_const; reflexivity + | cut ((MontgomeryAPI.eval (Z.pos r) A * (r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz)) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) m_enc = 0)%Z; + [ rewrite Z.mul_mod, r'_pow_correct; autorewrite with zsimplify_const; pull_Zmod; [ | t_fin ]; + rewrite Z.mod_small; [ trivial | split; try assumption; apply MontgomeryAPI.eval_small; try assumption; lia ] + | rewrite Z.mul_assoc, Z.mul_mod, H by t_fin; autorewrite with zsimplify_const; reflexivity ] ] + ). + Defined. +End with_args. + +Local Definition for_assumptions + := (mul_ext_gen, add_ext_gen, sub_ext_gen, opp_ext_gen, nonzero_ext_gen). + +Print Assumptions for_assumptions. + +Ltac pose_m' modinv_fuel m r m' := (* (-m)⁻¹ mod r *) + pose_modinv modinv_fuel (-Z.pos m) (Z.pos r) m'. +Ltac pose_r' modinv_fuel m r r' := (* r⁻¹ mod m *) + pose_modinv modinv_fuel (Z.pos r) (Z.pos m) r'. + +Ltac pose_m'_correct m m' r m'_correct := + pose_correct_if_Z + m' + ltac:(fun _ => constr:((Z.pos m * m') mod (Z.pos r) = (-1) mod Z.pos r)) + m'_correct. +Ltac pose_r'_correct m r r' r'_correct := + pose_correct_if_Z + r' + ltac:(fun _ => constr:((Z.pos r * r') mod (Z.pos m) = 1)) + r'_correct. + +Ltac pose_m_enc_correct_montgomery m sz r m_enc m_enc_correct_montgomery := + cache_proof_with_type_by + (Z.pos m = MontgomeryAPI.eval (n:=sz) (Z.pos r) m_enc) + ltac:(vm_compute; vm_cast_no_check (eq_refl (Z.pos m))) + m_enc_correct_montgomery. + +Ltac pose_r'_pow_correct r' sz r m_enc r'_pow_correct := + cache_proof_with_type_by + ((r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) m_enc = 1) + ltac:(vm_compute; reflexivity) + r'_pow_correct. + +Ltac pose_montgomery_to_F sz m r' montgomery_to_F := + let v := (eval cbv [montgomery_to_F_gen] in (montgomery_to_F_gen sz m r')) in + cache_term v montgomery_to_F. + +Ltac pose_r_big r r_big := + cache_proof_with_type_by + (Z.pos r > 1) + ltac:(vm_compute; reflexivity) + r_big. + +Ltac pose_m_big m m_big := + cache_proof_with_type_by + (1 < Z.pos m) + ltac:(vm_compute; reflexivity) + m_big. + +Ltac pose_m_enc_small sz r m_enc m_enc_small := + cache_proof_with_type_by + (small (n:=sz) (Z.pos r) m_enc) + ltac:(pose (small_Decidable (n:=sz) (bound:=Z.pos r)); vm_decide_no_check) + m_enc_small. + +Ltac pose_map_m_enc sz r m_enc map_m_enc := + cache_proof_with_type_by + (Tuple.map (n:=sz) (Z.land (Z.pos r - 1)) m_enc = m_enc) + ltac:(pose (@dec_eq_prod); pose dec_eq_Z; vm_decide_no_check) + map_m_enc. + +Ltac internal_pose_sig_by_eq ty sigl tac_eq id := + cache_term_with_type_by + ty + ltac:(eapply (@sig_by_eq _ _ sigl _); tac_eq ()) + id. + +Import ModularArithmetic. + +Local Ltac reduce_eq _ := + cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp runtime_lor Let_In]. + +Ltac pose_mul_ext r sz m m_enc r' r'_correct m' m'_correct m_enc_correct_montgomery r_big m_big m_enc_small montgomery_to_F mul_ext := + internal_pose_sig_by_eq + { f:Z^sz -> Z^sz -> Z^sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F) + /\ (forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval B < eval m_enc -> 0 <= eval (f A B) < eval m_enc)%Z) } + (@mul_ext_gen r sz m m_enc r' r'_correct m' m'_correct m_enc_correct_montgomery r_big m_big m_enc_small) + ltac:(fun _ => reduce_eq (); reflexivity) + mul_ext. + +Ltac pose_add_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_big m_enc_small montgomery_to_F add_ext := + internal_pose_sig_by_eq + { f:Z^sz -> Z^sz -> Z^sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + ((forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval A < eval m_enc + -> eval B < eval m_enc + -> montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)) + /\ (forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval A < eval m_enc + -> eval B < eval m_enc + -> 0 <= eval (f A B) < eval m_enc)))%Z } + (@add_ext_gen r sz m m_enc r' m_enc_correct_montgomery r_big m_big m_enc_small) + ltac:(fun _ => reduce_eq (); reflexivity) + add_ext. + +Ltac pose_sub_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map_m_enc montgomery_to_F sub_ext := + internal_pose_sig_by_eq + { f:Z^sz -> Z^sz -> Z^sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + ((forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval A < eval m_enc + -> eval B < eval m_enc + -> montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)) + /\ (forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval A < eval m_enc + -> eval B < eval m_enc + -> 0 <= eval (f A B) < eval m_enc)))%Z } + (@sub_ext_gen r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map_m_enc) + ltac:(fun _ => reduce_eq (); reflexivity) + sub_ext. + +Ltac pose_opp_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map_m_enc montgomery_to_F opp_ext := + internal_pose_sig_by_eq + { f:Z^sz -> Z^sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + ((forall (A : Z^sz) (_ : small (Z.pos r) A), + (eval A < eval m_enc + -> montgomery_to_F (eval (f A)) + = (F.opp (montgomery_to_F (eval A)))%F)) + /\ (forall (A : Z^sz) (_ : small (Z.pos r) A), + (eval A < eval m_enc + -> 0 <= eval (f A) < eval m_enc)))%Z } + (@opp_ext_gen r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map_m_enc) + ltac:(fun _ => reduce_eq (); reflexivity) + opp_ext. + +Ltac pose_nonzero_ext r sz m m_enc r' m_enc_correct_montgomery r'_pow_correct r_big m_big montgomery_to_F nonzero_ext := + internal_pose_sig_by_eq + { f:Z^sz -> Z + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Z^sz) (_ : small (Z.pos r) A), + (eval A < eval m_enc + -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z } + (@nonzero_ext_gen r sz m m_enc r' m_enc_correct_montgomery r'_pow_correct r_big m_big) + ltac:(fun _ => reduce_eq (); reflexivity) + nonzero_ext. + +Ltac pose_mul_sig r sz montgomery_to_F mul_ext mul_sig := + cache_term_with_type_by + { f:Z^sz -> Z^sz -> Z^sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F } + ltac:(idtac; + let v := (eval cbv [proj1_sig mul_ext_gen mul_ext sig_by_eq] in (proj1_sig mul_ext)) in + (exists v); + abstract apply (proj2_sig mul_ext)) + mul_sig. + +Ltac pose_mul_bounded r sz m_enc montgomery_to_F mul_ext mul_sig mul_bounded := + cache_proof_with_type_by + (let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval B < eval m_enc + -> 0 <= eval (proj1_sig mul_sig A B) < eval m_enc)%Z) + ltac:(apply (proj2_sig mul_ext)) + mul_bounded. + + +Ltac pose_add_sig r sz m_enc montgomery_to_F add_ext add_sig := + cache_term_with_type_by + { f:Z^sz -> Z^sz -> Z^sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval A < eval m_enc + -> eval B < eval m_enc + -> montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)%Z } + ltac:(idtac; + let v := (eval cbv [proj1_sig add_ext_gen add_ext sig_by_eq] in (proj1_sig add_ext)) in + (exists v); + abstract apply (proj2_sig add_ext)) + add_sig. + +Ltac pose_add_bounded r sz m_enc montgomery_to_F add_ext add_sig add_bounded := + cache_proof_with_type_by + (let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval A < eval m_enc + -> eval B < eval m_enc + -> 0 <= eval (proj1_sig add_sig A B) < eval m_enc))%Z) + ltac:(apply (proj2_sig add_ext)) + add_bounded. + + +Ltac pose_sub_sig r sz m_enc montgomery_to_F sub_ext sub_sig := + cache_term_with_type_by + { f:Z^sz -> Z^sz -> Z^sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval A < eval m_enc + -> eval B < eval m_enc + -> montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)%Z } + ltac:(idtac; + let v := (eval cbv [proj1_sig sub_ext_gen sub_ext sig_by_eq] in (proj1_sig sub_ext)) in + (exists v); + abstract apply (proj2_sig sub_ext)) + sub_sig. + +Ltac pose_sub_bounded r sz m_enc montgomery_to_F sub_ext sub_sig sub_bounded := + cache_proof_with_type_by + (let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Z^sz) (_ : small (Z.pos r) A) + (B : Z^sz) (_ : small (Z.pos r) B), + (eval A < eval m_enc + -> eval B < eval m_enc + -> 0 <= eval (proj1_sig sub_sig A B) < eval m_enc))%Z) + ltac:(apply (proj2_sig sub_ext)) + sub_bounded. + + +Ltac pose_opp_sig r sz m_enc montgomery_to_F opp_ext opp_sig := + cache_term_with_type_by + { f:Z^sz -> Z^sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Z^sz) (_ : small (Z.pos r) A), + (eval A < eval m_enc + -> montgomery_to_F (eval (f A)) + = (F.opp (montgomery_to_F (eval A)))%F)%Z } + ltac:(idtac; + let v := (eval cbv [proj1_sig opp_ext_gen opp_ext sig_by_eq] in (proj1_sig opp_ext)) in + (exists v); + abstract apply (proj2_sig opp_ext)) + opp_sig. + +Ltac pose_opp_bounded r sz m_enc montgomery_to_F opp_ext opp_sig opp_bounded := + cache_proof_with_type_by + (let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Z^sz) (_ : small (Z.pos r) A), + (eval A < eval m_enc + -> 0 <= eval (proj1_sig opp_sig A) < eval m_enc))%Z) + ltac:(apply (proj2_sig opp_ext)) + opp_bounded. + + +Ltac pose_nonzero_sig r sz m m_enc montgomery_to_F nonzero_ext nonzero_sig := + cache_term_with_type_by + { f:Z^sz -> Z + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Z^sz) (_ : small (Z.pos r) A), + (eval A < eval m_enc + -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z } + ltac:(idtac; + let v := (eval cbv [proj1_sig nonzero_ext_gen nonzero_ext sig_by_eq] in (proj1_sig nonzero_ext)) in + (exists v); + abstract apply (proj2_sig nonzero_ext)) + nonzero_sig. + +Ltac pose_ring ring := + (* FIXME: TODO *) + cache_term + I + ring. + +(* disable default unused things *) +Ltac pose_carry_sig carry_sig := + cache_term tt carry_sig. +Ltac pose_freeze_sig freeze_sig := + cache_term tt freeze_sig. +Ltac pose_Mxzladderstep_sig Mxzladderstep_sig := + cache_term tt Mxzladderstep_sig. diff --git a/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v new file mode 100644 index 000000000..4980f09b9 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v @@ -0,0 +1,458 @@ +(* This file is autogenerated from Montgomery.v by remake_packages.py *) +Require Import Crypto.Specific.Framework.CurveParametersPackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.FreezePackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.LadderstepPackage. +Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Montgomery. +Require Import Crypto.Specific.Framework.Packages. +Require Import Crypto.Util.TagList. + +Module TAG. + Inductive tags := m' | r' | m'_correct | r'_correct | m_enc_correct_montgomery | r'_pow_correct | montgomery_to_F | r_big | m_big | m_enc_small | map_m_enc | mul_ext | add_ext | sub_ext | opp_ext | nonzero_ext | mul_bounded | add_bounded | sub_bounded | opp_bounded | nonzero_sig. +End TAG. + +Ltac add_m' pkg := + if_montgomery + pkg + ltac:(fun _ => let modinv_fuel := Tag.get pkg TAG.modinv_fuel in + let m := Tag.get pkg TAG.m in + let r := Tag.get pkg TAG.r in + let m' := fresh "m'" in + let m' := pose_m' modinv_fuel m r m' in + Tag.update pkg TAG.m' m') + ltac:(fun _ => pkg) + (). +Ltac add_r' pkg := + if_montgomery + pkg + ltac:(fun _ => let modinv_fuel := Tag.get pkg TAG.modinv_fuel in + let m := Tag.get pkg TAG.m in + let r := Tag.get pkg TAG.r in + let r' := fresh "r'" in + let r' := pose_r' modinv_fuel m r r' in + Tag.update pkg TAG.r' r') + ltac:(fun _ => pkg) + (). +Ltac add_m'_correct pkg := + if_montgomery + pkg + ltac:(fun _ => let m := Tag.get pkg TAG.m in + let m' := Tag.get pkg TAG.m' in + let r := Tag.get pkg TAG.r in + let m'_correct := fresh "m'_correct" in + let m'_correct := pose_m'_correct m m' r m'_correct in + Tag.update pkg TAG.m'_correct m'_correct) + ltac:(fun _ => pkg) + (). +Ltac add_r'_correct pkg := + if_montgomery + pkg + ltac:(fun _ => let m := Tag.get pkg TAG.m in + let r := Tag.get pkg TAG.r in + let r' := Tag.get pkg TAG.r' in + let r'_correct := fresh "r'_correct" in + let r'_correct := pose_r'_correct m r r' r'_correct in + Tag.update pkg TAG.r'_correct r'_correct) + ltac:(fun _ => pkg) + (). +Ltac add_m_enc_correct_montgomery pkg := + if_montgomery + pkg + ltac:(fun _ => let m := Tag.get pkg TAG.m in + let sz := Tag.get pkg TAG.sz in + let r := Tag.get pkg TAG.r in + let m_enc := Tag.get pkg TAG.m_enc in + let m_enc_correct_montgomery := fresh "m_enc_correct_montgomery" in + let m_enc_correct_montgomery := pose_m_enc_correct_montgomery m sz r m_enc m_enc_correct_montgomery in + Tag.update pkg TAG.m_enc_correct_montgomery m_enc_correct_montgomery) + ltac:(fun _ => pkg) + (). +Ltac add_r'_pow_correct pkg := + if_montgomery + pkg + ltac:(fun _ => let r' := Tag.get pkg TAG.r' in + let sz := Tag.get pkg TAG.sz in + let r := Tag.get pkg TAG.r in + let m_enc := Tag.get pkg TAG.m_enc in + let r'_pow_correct := fresh "r'_pow_correct" in + let r'_pow_correct := pose_r'_pow_correct r' sz r m_enc r'_pow_correct in + Tag.update pkg TAG.r'_pow_correct r'_pow_correct) + ltac:(fun _ => pkg) + (). +Ltac add_montgomery_to_F pkg := + if_montgomery + pkg + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let r' := Tag.get pkg TAG.r' in + let montgomery_to_F := fresh "montgomery_to_F" in + let montgomery_to_F := pose_montgomery_to_F sz m r' montgomery_to_F in + Tag.update pkg TAG.montgomery_to_F montgomery_to_F) + ltac:(fun _ => pkg) + (). +Ltac add_r_big pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let r_big := fresh "r_big" in + let r_big := pose_r_big r r_big in + Tag.update pkg TAG.r_big r_big) + ltac:(fun _ => pkg) + (). +Ltac add_m_big pkg := + if_montgomery + pkg + ltac:(fun _ => let m := Tag.get pkg TAG.m in + let m_big := fresh "m_big" in + let m_big := pose_m_big m m_big in + Tag.update pkg TAG.m_big m_big) + ltac:(fun _ => pkg) + (). +Ltac add_m_enc_small pkg := + if_montgomery + pkg + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let r := Tag.get pkg TAG.r in + let m_enc := Tag.get pkg TAG.m_enc in + let m_enc_small := fresh "m_enc_small" in + let m_enc_small := pose_m_enc_small sz r m_enc m_enc_small in + Tag.update pkg TAG.m_enc_small m_enc_small) + ltac:(fun _ => pkg) + (). +Ltac add_map_m_enc pkg := + if_montgomery + pkg + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let r := Tag.get pkg TAG.r in + let m_enc := Tag.get pkg TAG.m_enc in + let map_m_enc := fresh "map_m_enc" in + let map_m_enc := pose_map_m_enc sz r m_enc map_m_enc in + Tag.update pkg TAG.map_m_enc map_m_enc) + ltac:(fun _ => pkg) + (). +Ltac add_mul_ext pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let m_enc := Tag.get pkg TAG.m_enc in + let r' := Tag.get pkg TAG.r' in + let r'_correct := Tag.get pkg TAG.r'_correct in + let m' := Tag.get pkg TAG.m' in + let m'_correct := Tag.get pkg TAG.m'_correct in + let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in + let r_big := Tag.get pkg TAG.r_big in + let m_big := Tag.get pkg TAG.m_big in + let m_enc_small := Tag.get pkg TAG.m_enc_small in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let mul_ext := fresh "mul_ext" in + let mul_ext := pose_mul_ext r sz m m_enc r' r'_correct m' m'_correct m_enc_correct_montgomery r_big m_big m_enc_small montgomery_to_F mul_ext in + Tag.update pkg TAG.mul_ext mul_ext) + ltac:(fun _ => pkg) + (). +Ltac add_add_ext pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let m_enc := Tag.get pkg TAG.m_enc in + let r' := Tag.get pkg TAG.r' in + let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in + let r_big := Tag.get pkg TAG.r_big in + let m_big := Tag.get pkg TAG.m_big in + let m_enc_small := Tag.get pkg TAG.m_enc_small in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let add_ext := fresh "add_ext" in + let add_ext := pose_add_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_big m_enc_small montgomery_to_F add_ext in + Tag.update pkg TAG.add_ext add_ext) + ltac:(fun _ => pkg) + (). +Ltac add_sub_ext pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let m_enc := Tag.get pkg TAG.m_enc in + let r' := Tag.get pkg TAG.r' in + let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in + let r_big := Tag.get pkg TAG.r_big in + let m_enc_small := Tag.get pkg TAG.m_enc_small in + let map_m_enc := Tag.get pkg TAG.map_m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let sub_ext := fresh "sub_ext" in + let sub_ext := pose_sub_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map_m_enc montgomery_to_F sub_ext in + Tag.update pkg TAG.sub_ext sub_ext) + ltac:(fun _ => pkg) + (). +Ltac add_opp_ext pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let m_enc := Tag.get pkg TAG.m_enc in + let r' := Tag.get pkg TAG.r' in + let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in + let r_big := Tag.get pkg TAG.r_big in + let m_enc_small := Tag.get pkg TAG.m_enc_small in + let map_m_enc := Tag.get pkg TAG.map_m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let opp_ext := fresh "opp_ext" in + let opp_ext := pose_opp_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map_m_enc montgomery_to_F opp_ext in + Tag.update pkg TAG.opp_ext opp_ext) + ltac:(fun _ => pkg) + (). +Ltac add_nonzero_ext pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let m_enc := Tag.get pkg TAG.m_enc in + let r' := Tag.get pkg TAG.r' in + let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in + let r'_pow_correct := Tag.get pkg TAG.r'_pow_correct in + let r_big := Tag.get pkg TAG.r_big in + let m_big := Tag.get pkg TAG.m_big in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let nonzero_ext := fresh "nonzero_ext" in + let nonzero_ext := pose_nonzero_ext r sz m m_enc r' m_enc_correct_montgomery r'_pow_correct r_big m_big montgomery_to_F nonzero_ext in + Tag.update pkg TAG.nonzero_ext nonzero_ext) + ltac:(fun _ => pkg) + (). +Ltac add_mul_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let mul_ext := Tag.get pkg TAG.mul_ext in + let mul_sig := fresh "mul_sig" in + let mul_sig := pose_mul_sig r sz montgomery_to_F mul_ext mul_sig in + Tag.update pkg TAG.mul_sig mul_sig) + ltac:(fun _ => pkg) + (). +Ltac add_mul_bounded pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let mul_ext := Tag.get pkg TAG.mul_ext in + let mul_sig := Tag.get pkg TAG.mul_sig in + let mul_bounded := fresh "mul_bounded" in + let mul_bounded := pose_mul_bounded r sz m_enc montgomery_to_F mul_ext mul_sig mul_bounded in + Tag.update pkg TAG.mul_bounded mul_bounded) + ltac:(fun _ => pkg) + (). +Ltac add_add_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let add_ext := Tag.get pkg TAG.add_ext in + let add_sig := fresh "add_sig" in + let add_sig := pose_add_sig r sz m_enc montgomery_to_F add_ext add_sig in + Tag.update pkg TAG.add_sig add_sig) + ltac:(fun _ => pkg) + (). +Ltac add_add_bounded pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let add_ext := Tag.get pkg TAG.add_ext in + let add_sig := Tag.get pkg TAG.add_sig in + let add_bounded := fresh "add_bounded" in + let add_bounded := pose_add_bounded r sz m_enc montgomery_to_F add_ext add_sig add_bounded in + Tag.update pkg TAG.add_bounded add_bounded) + ltac:(fun _ => pkg) + (). +Ltac add_sub_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let sub_ext := Tag.get pkg TAG.sub_ext in + let sub_sig := fresh "sub_sig" in + let sub_sig := pose_sub_sig r sz m_enc montgomery_to_F sub_ext sub_sig in + Tag.update pkg TAG.sub_sig sub_sig) + ltac:(fun _ => pkg) + (). +Ltac add_sub_bounded pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let sub_ext := Tag.get pkg TAG.sub_ext in + let sub_sig := Tag.get pkg TAG.sub_sig in + let sub_bounded := fresh "sub_bounded" in + let sub_bounded := pose_sub_bounded r sz m_enc montgomery_to_F sub_ext sub_sig sub_bounded in + Tag.update pkg TAG.sub_bounded sub_bounded) + ltac:(fun _ => pkg) + (). +Ltac add_opp_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let opp_ext := Tag.get pkg TAG.opp_ext in + let opp_sig := fresh "opp_sig" in + let opp_sig := pose_opp_sig r sz m_enc montgomery_to_F opp_ext opp_sig in + Tag.update pkg TAG.opp_sig opp_sig) + ltac:(fun _ => pkg) + (). +Ltac add_opp_bounded pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let opp_ext := Tag.get pkg TAG.opp_ext in + let opp_sig := Tag.get pkg TAG.opp_sig in + let opp_bounded := fresh "opp_bounded" in + let opp_bounded := pose_opp_bounded r sz m_enc montgomery_to_F opp_ext opp_sig opp_bounded in + Tag.update pkg TAG.opp_bounded opp_bounded) + ltac:(fun _ => pkg) + (). +Ltac add_nonzero_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let r := Tag.get pkg TAG.r in + let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let m_enc := Tag.get pkg TAG.m_enc in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let nonzero_ext := Tag.get pkg TAG.nonzero_ext in + let nonzero_sig := fresh "nonzero_sig" in + let nonzero_sig := pose_nonzero_sig r sz m m_enc montgomery_to_F nonzero_ext nonzero_sig in + Tag.update pkg TAG.nonzero_sig nonzero_sig) + ltac:(fun _ => pkg) + (). +Ltac add_ring pkg := + if_montgomery + pkg + ltac:(fun _ => let ring := fresh "ring" in + let ring := pose_ring ring in + Tag.update pkg TAG.ring ring) + ltac:(fun _ => pkg) + (). +Ltac add_carry_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let carry_sig := fresh "carry_sig" in + let carry_sig := pose_carry_sig carry_sig in + Tag.update pkg TAG.carry_sig carry_sig) + ltac:(fun _ => pkg) + (). +Ltac add_freeze_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let freeze_sig := fresh "freeze_sig" in + let freeze_sig := pose_freeze_sig freeze_sig in + Tag.update pkg TAG.freeze_sig freeze_sig) + ltac:(fun _ => pkg) + (). +Ltac add_Mxzladderstep_sig pkg := + if_montgomery + pkg + ltac:(fun _ => let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in + let Mxzladderstep_sig := pose_Mxzladderstep_sig Mxzladderstep_sig in + Tag.update pkg TAG.Mxzladderstep_sig Mxzladderstep_sig) + ltac:(fun _ => pkg) + (). +Ltac add_Montgomery_package pkg := + let pkg := add_m' pkg in + let pkg := add_r' pkg in + let pkg := add_m'_correct pkg in + let pkg := add_r'_correct pkg in + let pkg := add_m_enc_correct_montgomery pkg in + let pkg := add_r'_pow_correct pkg in + let pkg := add_montgomery_to_F pkg in + let pkg := add_r_big pkg in + let pkg := add_m_big pkg in + let pkg := add_m_enc_small pkg in + let pkg := add_map_m_enc pkg in + let pkg := add_mul_ext pkg in + let pkg := add_add_ext pkg in + let pkg := add_sub_ext pkg in + let pkg := add_opp_ext pkg in + let pkg := add_nonzero_ext pkg in + let pkg := add_mul_sig pkg in + let pkg := add_mul_bounded pkg in + let pkg := add_add_sig pkg in + let pkg := add_add_bounded pkg in + let pkg := add_sub_sig pkg in + let pkg := add_sub_bounded pkg in + let pkg := add_opp_sig pkg in + let pkg := add_opp_bounded pkg in + let pkg := add_nonzero_sig pkg in + let pkg := add_ring pkg in + let pkg := add_carry_sig pkg in + let pkg := add_freeze_sig pkg in + let pkg := add_Mxzladderstep_sig pkg in + Tag.strip_local pkg. + + +Module MakeMontgomeryPackage (PKG : PrePackage). + Module Import MakeMontgomeryPackageInternal := MakePackageBase PKG. + + Ltac get_m' _ := get TAG.m'. + Notation m' := (ltac:(let v := get_m' () in exact v)) (only parsing). + Ltac get_r' _ := get TAG.r'. + Notation r' := (ltac:(let v := get_r' () in exact v)) (only parsing). + Ltac get_m'_correct _ := get TAG.m'_correct. + Notation m'_correct := (ltac:(let v := get_m'_correct () in exact v)) (only parsing). + Ltac get_r'_correct _ := get TAG.r'_correct. + Notation r'_correct := (ltac:(let v := get_r'_correct () in exact v)) (only parsing). + Ltac get_m_enc_correct_montgomery _ := get TAG.m_enc_correct_montgomery. + Notation m_enc_correct_montgomery := (ltac:(let v := get_m_enc_correct_montgomery () in exact v)) (only parsing). + Ltac get_r'_pow_correct _ := get TAG.r'_pow_correct. + Notation r'_pow_correct := (ltac:(let v := get_r'_pow_correct () in exact v)) (only parsing). + Ltac get_montgomery_to_F _ := get TAG.montgomery_to_F. + Notation montgomery_to_F := (ltac:(let v := get_montgomery_to_F () in exact v)) (only parsing). + Ltac get_r_big _ := get TAG.r_big. + Notation r_big := (ltac:(let v := get_r_big () in exact v)) (only parsing). + Ltac get_m_big _ := get TAG.m_big. + Notation m_big := (ltac:(let v := get_m_big () in exact v)) (only parsing). + Ltac get_m_enc_small _ := get TAG.m_enc_small. + Notation m_enc_small := (ltac:(let v := get_m_enc_small () in exact v)) (only parsing). + Ltac get_map_m_enc _ := get TAG.map_m_enc. + Notation map_m_enc := (ltac:(let v := get_map_m_enc () in exact v)) (only parsing). + Ltac get_mul_ext _ := get TAG.mul_ext. + Notation mul_ext := (ltac:(let v := get_mul_ext () in exact v)) (only parsing). + Ltac get_add_ext _ := get TAG.add_ext. + Notation add_ext := (ltac:(let v := get_add_ext () in exact v)) (only parsing). + Ltac get_sub_ext _ := get TAG.sub_ext. + Notation sub_ext := (ltac:(let v := get_sub_ext () in exact v)) (only parsing). + Ltac get_opp_ext _ := get TAG.opp_ext. + Notation opp_ext := (ltac:(let v := get_opp_ext () in exact v)) (only parsing). + Ltac get_nonzero_ext _ := get TAG.nonzero_ext. + Notation nonzero_ext := (ltac:(let v := get_nonzero_ext () in exact v)) (only parsing). + Ltac get_mul_bounded _ := get TAG.mul_bounded. + Notation mul_bounded := (ltac:(let v := get_mul_bounded () in exact v)) (only parsing). + Ltac get_add_bounded _ := get TAG.add_bounded. + Notation add_bounded := (ltac:(let v := get_add_bounded () in exact v)) (only parsing). + Ltac get_sub_bounded _ := get TAG.sub_bounded. + Notation sub_bounded := (ltac:(let v := get_sub_bounded () in exact v)) (only parsing). + Ltac get_opp_bounded _ := get TAG.opp_bounded. + Notation opp_bounded := (ltac:(let v := get_opp_bounded () in exact v)) (only parsing). + Ltac get_nonzero_sig _ := get TAG.nonzero_sig. + Notation nonzero_sig := (ltac:(let v := get_nonzero_sig () in exact v)) (only parsing). +End MakeMontgomeryPackage. diff --git a/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py b/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py index 52f5e0f54..5bc6bac3e 100755 --- a/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py +++ b/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py @@ -13,9 +13,11 @@ NORMAL_PACKAGE_NAMES = [('Base.v', (CP_LIST, None)), ('../ReificationTypes.v', (CP_BASE_LIST, None)), ('Freeze.v', (CP_BASE_LIST, 'not_exists')), ('Ladderstep.v', (CP_BASE_DEFAULTS_LIST, 'not_exists')), - ('Karatsuba.v', (CP_BASE_DEFAULTS_LIST, 'goldilocks'))] + ('Karatsuba.v', (CP_BASE_DEFAULTS_LIST, 'goldilocks')), + ('Montgomery.v', (CP_BASE_DEFAULTS_FREEZE_LADDERSTEP_LIST, 'montgomery')), + ('../MontgomeryReificationTypes.v', (CP_BASE_LIST + ['MontgomeryPackage.v', '../ReificationTypesPackage.v'], 'montgomery'))] ALL_FILE_NAMES = PACKAGE_NAMES + NORMAL_PACKAGE_NAMES # PACKAGE_CP_NAMES + WITH_CURVE_BASE_NAMES + ['../ReificationTypes.v'] -CONFIGS = ('goldilocks', ) +CONFIGS = ('goldilocks', 'montgomery') EXCLUDES = ('constr:((wt_divides_chain, wt_divides_chains))', ) diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v index 7078d4bec..4aa255d11 100644 --- a/src/Specific/Framework/CurveParameters.v +++ b/src/Specific/Framework/CurveParameters.v @@ -28,6 +28,7 @@ Module Type CurveParameters. Parameter coef_div_modulus : option nat. Parameter goldilocks : bool. + Parameter montgomery : bool. Parameter mul_code : option (Z^sz -> Z^sz -> Z^sz). Parameter square_code : option (Z^sz -> Z^sz). @@ -43,7 +44,7 @@ Module Type CurveParameters. End CurveParameters. Module TAG. - Inductive tags := sz | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel. + Inductive tags := sz | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | montgomery | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel. End TAG. Module FillCurveParameters (P : CurveParameters). @@ -66,6 +67,7 @@ Module FillCurveParameters (P : CurveParameters). Definition coef_div_modulus := defaulted P.coef_div_modulus 0%nat. Definition goldilocks := P.goldilocks. + Definition montgomery := P.montgomery. Ltac default_mul := lazymatch (eval hnf in P.mul_code) with @@ -82,7 +84,9 @@ Module FillCurveParameters (P : CurveParameters). Definition upper_bound_of_exponent := defaulted P.upper_bound_of_exponent - (fun exp => (2^exp + 2^(exp-3))%Z). + (if P.montgomery + then (fun exp => (2^exp - 1)%Z) + else (fun exp => (2^exp + 2^(exp-3))%Z)). Local Notation list_8_if_not_exists ls := (if existsb (Nat.eqb 8) ls then nil @@ -91,7 +95,10 @@ Module FillCurveParameters (P : CurveParameters). Definition allowable_bit_widths := defaulted P.allowable_bit_widths - (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil)%nat. + ((if P.montgomery + then [8] + else nil) + ++ (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil))%nat. Definition freeze_allowable_bit_widths := defaulted P.freeze_extra_allowable_bit_widths @@ -109,6 +116,7 @@ Module FillCurveParameters (P : CurveParameters). let P_a24 := P.a24 in let P_coef_div_modulus := P.coef_div_modulus in let P_goldilocks := P.goldilocks in + let P_montgomery := P.montgomery in let P_mul_code := P.mul_code in let P_square_code := P.square_code in let P_upper_bound_of_exponent := P.upper_bound_of_exponent in @@ -117,8 +125,8 @@ Module FillCurveParameters (P : CurveParameters). let P_modinv_fuel := P.modinv_fuel in let v' := (eval cbv [id List.app - sz bitwidth s c carry_chains a24 coef_div_modulus goldilocks modinv_fuel - P_sz P_bitwidth P_s P_c P_carry_chains P_a24 P_coef_div_modulus P_goldilocks P_modinv_fuel + sz bitwidth s c carry_chains a24 coef_div_modulus goldilocks montgomery modinv_fuel + P_sz P_bitwidth P_s P_c P_carry_chains P_a24 P_coef_div_modulus P_goldilocks P_montgomery P_modinv_fuel P_mul_code P_square_code upper_bound_of_exponent allowable_bit_widths freeze_allowable_bit_widths P_upper_bound_of_exponent P_allowable_bit_widths P_freeze_extra_allowable_bit_widths @@ -141,6 +149,7 @@ Module FillCurveParameters (P : CurveParameters). Local Notation P_a24 := a24. Local Notation P_coef_div_modulus := coef_div_modulus. Local Notation P_goldilocks := goldilocks. + Local Notation P_montgomery := montgomery. Local Notation P_upper_bound_of_exponent := upper_bound_of_exponent. Local Notation P_allowable_bit_widths := allowable_bit_widths. Local Notation P_freeze_allowable_bit_widths := freeze_allowable_bit_widths. @@ -183,6 +192,11 @@ Module FillCurveParameters (P : CurveParameters). bool ltac:(let v := do_compute P_goldilocks in exact v) goldilocks. + Ltac pose_montgomery montgomery := + cache_term_with_type_by + bool + ltac:(let v := do_compute P_montgomery in exact v) + montgomery. Ltac pose_modinv_fuel modinv_fuel := cache_term_with_type_by @@ -237,6 +251,11 @@ Module FillCurveParameters (P : CurveParameters). let goldilocks := pose_goldilocks goldilocks in Tag.update pkg TAG.goldilocks goldilocks. + Ltac add_montgomery pkg := + let montgomery := fresh "montgomery" in + let montgomery := pose_montgomery montgomery in + Tag.update pkg TAG.montgomery montgomery. + Ltac add_modinv_fuel pkg := let modinv_fuel := fresh "modinv_fuel" in let modinv_fuel := pose_modinv_fuel modinv_fuel in @@ -256,6 +275,7 @@ Module FillCurveParameters (P : CurveParameters). let pkg := add_a24 pkg in let pkg := add_coef_div_modulus pkg in let pkg := add_goldilocks pkg in + let pkg := add_montgomery pkg in let pkg := add_modinv_fuel pkg in let pkg := add_upper_bound_of_exponent pkg in Tag.strip_local pkg. diff --git a/src/Specific/Framework/CurveParametersPackage.v b/src/Specific/Framework/CurveParametersPackage.v index 782ccdd22..fbc937f7a 100644 --- a/src/Specific/Framework/CurveParametersPackage.v +++ b/src/Specific/Framework/CurveParametersPackage.v @@ -11,6 +11,14 @@ Ltac if_goldilocks pkg tac_true tac_false arg := | false => tac_false arg end. +Ltac if_montgomery pkg tac_true tac_false arg := + let montgomery := Tag.get pkg TAG.montgomery in + let montgomery := (eval vm_compute in (montgomery : bool)) in + lazymatch montgomery with + | true => tac_true arg + | false => tac_false arg + end. + Module MakeCurveParametersPackage (PKG : PrePackage). Module Import MakeCurveParametersPackageInternal := MakePackageBase PKG. @@ -31,6 +39,8 @@ Module MakeCurveParametersPackage (PKG : PrePackage). Notation coef_div_modulus := (ltac:(let v := get_coef_div_modulus () in exact v)) (only parsing). Ltac get_goldilocks _ := get TAG.goldilocks. Notation goldilocks := (ltac:(let v := get_goldilocks () in exact v)) (only parsing). + Ltac get_montgomery _ := get TAG.montgomery. + Notation montgomery := (ltac:(let v := get_montgomery () in exact v)) (only parsing). Ltac get_modinv_fuel _ := get TAG.modinv_fuel. Notation modinv_fuel := (ltac:(let v := get_modinv_fuel () in exact v)) (only parsing). Ltac get_upper_bound_of_exponent _ := get TAG.upper_bound_of_exponent. diff --git a/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v index 687af2c9c..f08605358 100644 --- a/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v +++ b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v @@ -292,3 +292,51 @@ Ltac factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t := Ltac op_sig_side_conditions_t _ := try (hnf; rewrite <- (ZRange.is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. + +Local Open Scope Z_scope. +(* XXX TODO: Clean this up *) +Ltac nonzero_preglue op_sig cbv_runtime := + let phi := lazymatch goal with + | [ |- context[Decidable.dec (?phi _ = _)] ] => phi + end in + let do_red _ := + lazymatch (eval cbv [phi] in phi) with + | (fun x => ?montgomery_to_F (?meval (?feBW_of_feBW_small _))) + => cbv [feBW_of_feBW_small phi meval] + end in + apply_lift_sig; intros; eexists_sig_etransitivity; + do_red (); + [ refine (_ : (if Decidable.dec (_ = 0) then true else false) = _); + lazymatch goal with + | [ |- (if Decidable.dec ?x then _ else _) = (if Decidable.dec ?y then _ else _) ] + => cut (x <-> y); + [ destruct (Decidable.dec x), (Decidable.dec y); try reflexivity; intros [? ?]; + generalize dependent x; generalize dependent y; solve [ intuition congruence ] + | ] + end; + etransitivity; [ | eapply (proj2_sig op_sig) ]; + [ | solve [ op_sig_side_conditions_t () ].. ]; + reflexivity + | ]; + let decP := lazymatch goal with |- { c | _ = if Decidable.dec (?decP = 0) then _ else _ } => decP end in + apply (@proj2_sig_map _ (fun c => BoundedWordToZ 1 _ _ c = decP) _); + [ let a' := fresh "a'" in + let H' := fresh "H'" in + intros a' H'; rewrite H'; + let H := fresh in + lazymatch goal with |- context[Decidable.dec ?x] => destruct (Decidable.dec x) as [H|H]; try rewrite H end; + [ reflexivity + | let H := fresh in + lazymatch goal with |- context[?x =? 0] => destruct (x =? 0) eqn:? end; + try reflexivity; + Z.ltb_to_lt; congruence ] + | ]; + eexists_sig_etransitivity; + [ do_set_sig op_sig; cbv_runtime (); reflexivity + | ]; + sig_dlet_in_rhs_to_context; + cbv [proj1_sig]; + match goal with + | [ |- context[match ?v with exist _ _ => _ end] ] + => is_var v; destruct v as [? _] + end. diff --git a/src/Specific/Framework/MontgomeryReificationTypes.v b/src/Specific/Framework/MontgomeryReificationTypes.v new file mode 100644 index 000000000..1b476dbe4 --- /dev/null +++ b/src/Specific/Framework/MontgomeryReificationTypes.v @@ -0,0 +1,47 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.romega.ROmega. +Require Import Coq.micromega.Lia. +Require Import Coq.Lists.List. +Local Open Scope Z_scope. + +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Util.FixedWordSizes. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.ZRange Crypto.Util.BoundedWord. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Decidable. + +Require Crypto.Arithmetic.Saturated.MontgomeryAPI. + +Require Import Crypto.Util.Tactics.PoseTermWithName. +Require Import Crypto.Util.Tactics.CacheTerm. + +Ltac pose_meval feBW r meval := + cache_term_with_type_by + (feBW -> Z) + ltac:(exact (fun x : feBW => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x))) + meval. + +Ltac pose_feBW_small sz feBW meval r m_enc feBW_small := + cache_term + { v : feBW | meval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) m_enc } + feBW_small. + +Ltac pose_feBW_of_feBW_small feBW feBW_small feBW_of_feBW_small := + cache_term_with_type_by + (feBW_small -> feBW) + ltac:(refine (@proj1_sig _ _)) + feBW_of_feBW_small. + +Ltac pose_phiM feBW m meval montgomery_to_F phiM := + cache_term_with_type_by + (feBW -> F m) + ltac:(exact (fun x : feBW => montgomery_to_F (meval x))) + phiM. + +Ltac pose_phiM_small feBW_small feBW_of_feBW_small m meval montgomery_to_F phiM_small := + cache_term_with_type_by + (feBW_small -> F m) + ltac:(exact (fun x : feBW_small => montgomery_to_F (meval (feBW_of_feBW_small x)))) + phiM_small. diff --git a/src/Specific/Framework/MontgomeryReificationTypesPackage.v b/src/Specific/Framework/MontgomeryReificationTypesPackage.v new file mode 100644 index 000000000..5b440f0e8 --- /dev/null +++ b/src/Specific/Framework/MontgomeryReificationTypesPackage.v @@ -0,0 +1,94 @@ +(* This file is autogenerated from MontgomeryReificationTypes.v by remake_packages.py *) +Require Import Crypto.Specific.Framework.CurveParametersPackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.MontgomeryPackage. +Require Import Crypto.Specific.Framework.ReificationTypesPackage. +Require Export Crypto.Specific.Framework.MontgomeryReificationTypes. +Require Import Crypto.Specific.Framework.Packages. +Require Import Crypto.Util.TagList. + +Module TAG. + Inductive tags := meval | feBW_small | feBW_of_feBW_small | phiM | phiM_small. +End TAG. + +Ltac add_meval pkg := + if_montgomery + pkg + ltac:(fun _ => let feBW := Tag.get pkg TAG.feBW in + let r := Tag.get pkg TAG.r in + let meval := fresh "meval" in + let meval := pose_meval feBW r meval in + Tag.update pkg TAG.meval meval) + ltac:(fun _ => pkg) + (). +Ltac add_feBW_small pkg := + if_montgomery + pkg + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let feBW := Tag.get pkg TAG.feBW in + let meval := Tag.get pkg TAG.meval in + let r := Tag.get pkg TAG.r in + let m_enc := Tag.get pkg TAG.m_enc in + let feBW_small := fresh "feBW_small" in + let feBW_small := pose_feBW_small sz feBW meval r m_enc feBW_small in + Tag.update pkg TAG.feBW_small feBW_small) + ltac:(fun _ => pkg) + (). +Ltac add_feBW_of_feBW_small pkg := + if_montgomery + pkg + ltac:(fun _ => let feBW := Tag.get pkg TAG.feBW in + let feBW_small := Tag.get pkg TAG.feBW_small in + let feBW_of_feBW_small := fresh "feBW_of_feBW_small" in + let feBW_of_feBW_small := pose_feBW_of_feBW_small feBW feBW_small feBW_of_feBW_small in + Tag.update pkg TAG.feBW_of_feBW_small feBW_of_feBW_small) + ltac:(fun _ => pkg) + (). +Ltac add_phiM pkg := + if_montgomery + pkg + ltac:(fun _ => let feBW := Tag.get pkg TAG.feBW in + let m := Tag.get pkg TAG.m in + let meval := Tag.get pkg TAG.meval in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let phiM := fresh "phiM" in + let phiM := pose_phiM feBW m meval montgomery_to_F phiM in + Tag.update pkg TAG.phiM phiM) + ltac:(fun _ => pkg) + (). +Ltac add_phiM_small pkg := + if_montgomery + pkg + ltac:(fun _ => let feBW_small := Tag.get pkg TAG.feBW_small in + let feBW_of_feBW_small := Tag.get pkg TAG.feBW_of_feBW_small in + let m := Tag.get pkg TAG.m in + let meval := Tag.get pkg TAG.meval in + let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in + let phiM_small := fresh "phiM_small" in + let phiM_small := pose_phiM_small feBW_small feBW_of_feBW_small m meval montgomery_to_F phiM_small in + Tag.update pkg TAG.phiM_small phiM_small) + ltac:(fun _ => pkg) + (). +Ltac add_MontgomeryReificationTypes_package pkg := + let pkg := add_meval pkg in + let pkg := add_feBW_small pkg in + let pkg := add_feBW_of_feBW_small pkg in + let pkg := add_phiM pkg in + let pkg := add_phiM_small pkg in + Tag.strip_local pkg. + + +Module MakeMontgomeryReificationTypesPackage (PKG : PrePackage). + Module Import MakeMontgomeryReificationTypesPackageInternal := MakePackageBase PKG. + + Ltac get_meval _ := get TAG.meval. + Notation meval := (ltac:(let v := get_meval () in exact v)) (only parsing). + Ltac get_feBW_small _ := get TAG.feBW_small. + Notation feBW_small := (ltac:(let v := get_feBW_small () in exact v)) (only parsing). + Ltac get_feBW_of_feBW_small _ := get TAG.feBW_of_feBW_small. + Notation feBW_of_feBW_small := (ltac:(let v := get_feBW_of_feBW_small () in exact v)) (only parsing). + Ltac get_phiM _ := get TAG.phiM. + Notation phiM := (ltac:(let v := get_phiM () in exact v)) (only parsing). + Ltac get_phiM_small _ := get TAG.phiM_small. + Notation phiM_small := (ltac:(let v := get_phiM_small () in exact v)) (only parsing). +End MakeMontgomeryReificationTypesPackage. diff --git a/src/Specific/Framework/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v index 617a36212..01f91731e 100644 --- a/src/Specific/Framework/SynthesisFramework.v +++ b/src/Specific/Framework/SynthesisFramework.v @@ -3,8 +3,10 @@ Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage. Require Import Crypto.Specific.Framework.ArithmeticSynthesis.FreezePackage. Require Import Crypto.Specific.Framework.ArithmeticSynthesis.KaratsubaPackage. Require Import Crypto.Specific.Framework.ArithmeticSynthesis.LadderstepPackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.MontgomeryPackage. Require Import Crypto.Specific.Framework.CurveParametersPackage. Require Import Crypto.Specific.Framework.ReificationTypesPackage. +Require Import Crypto.Specific.Framework.MontgomeryReificationTypesPackage. Require Import Crypto.Specific.Framework.Packages. Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.PrimeFieldTheorems. @@ -37,7 +39,9 @@ Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters). let pkg := add_Base_package pkg in let pkg := add_ReificationTypes_package pkg in let pkg := add_Karatsuba_package pkg in - (* N.B. freeze is a "default" and must come after anything that may disable it *) + let pkg := add_Montgomery_package pkg in + let pkg := add_MontgomeryReificationTypes_package pkg in + (* N.B. freeze is a "default" and must come after montgomery, which disables it *) let pkg := add_Freeze_package pkg in (* N.B. the Defaults must come after other possible ways of adding the _sig lemmas *) let pkg := add_Defaults_package pkg P_default_mul P_extra_prove_mul_eq P_default_square P_extra_prove_square_eq in @@ -64,6 +68,8 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack Module FP := MakeFreezePackage PKG. Module LP := MakeLadderstepPackage PKG. Module KP := MakeKaratsubaPackage PKG. + Module MP := MakeMontgomeryPackage PKG. + Module MRP := MakeMontgomeryReificationTypesPackage PKG. Include CP. Include BP. Include DP. @@ -71,6 +77,8 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack Include FP. Include LP. Include KP. + Include MP. + Include MRP. Ltac synthesize_with_carry do_rewrite get_op_sig := let carry_sig := get_carry_sig () in @@ -85,10 +93,39 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack Ltac synthesize_1arg_with_carry get_op_sig := synthesize_with_carry do_rewrite_with_1sig_add_carry get_op_sig. - Ltac synthesize_mul _ := synthesize_2arg_with_carry get_mul_sig. - Ltac synthesize_add _ := synthesize_2arg_with_carry get_add_sig. - Ltac synthesize_sub _ := synthesize_2arg_with_carry get_sub_sig. - Ltac synthesize_opp _ := synthesize_1arg_with_carry get_opp_sig. + Ltac synthesize_montgomery get_op_sig get_op_bounded := + let phi := get_phi_for_preglue () in + let op_sig := get_op_sig () in + let op_bounded := get_op_bounded () in + let do_red _ := + lazymatch (eval cbv [phi] in phi) with + | (fun x => ?montgomery_to_F (?meval (?feBW_of_feBW_small _))) + => cbv [feBW_of_feBW_small meval] + end in + start_preglue; + do_red (); + [ do_rewrite_with_sig_by op_sig op_sig_side_conditions_t; + cbv_runtime + | .. ]; + fin_preglue; + factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t; + refine_reflectively_gen P.allowable_bit_widths anf. + + Ltac synthesize_2arg_choice get_op_sig get_op_bounded := + lazymatch (eval vm_compute in P.montgomery) with + | true => synthesize_montgomery get_op_sig get_op_bounded + | false => synthesize_2arg_with_carry get_op_sig + end. + Ltac synthesize_1arg_choice get_op_sig get_op_bounded := + lazymatch (eval vm_compute in P.montgomery) with + | true => synthesize_montgomery get_op_sig get_op_bounded + | false => synthesize_1arg_with_carry get_op_sig + end. + + Ltac synthesize_mul _ := synthesize_2arg_choice get_mul_sig get_mul_bounded. + Ltac synthesize_add _ := synthesize_2arg_choice get_add_sig get_add_bounded. + Ltac synthesize_sub _ := synthesize_2arg_choice get_sub_sig get_sub_bounded. + Ltac synthesize_opp _ := synthesize_1arg_choice get_opp_sig get_opp_bounded. Ltac synthesize_square _ := synthesize_1arg_with_carry get_square_sig. Ltac synthesize_freeze _ := let freeze_sig := get_freeze_sig () in @@ -110,5 +147,9 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack | .. ]; finish_conjoined_preglue (); refine_reflectively_gen P.allowable_bit_widths default. + Ltac synthesize_nonzero _ := + let op_sig := get_nonzero_sig () in + nonzero_preglue op_sig ltac:(fun _ => cbv_runtime); + refine_reflectively_gen P.allowable_bit_widths anf. End PackageSynthesis. diff --git a/src/Specific/Framework/make_curve.py b/src/Specific/Framework/make_curve.py index aeaef91db..afed1243c 100755 --- a/src/Specific/Framework/make_curve.py +++ b/src/Specific/Framework/make_curve.py @@ -216,7 +216,10 @@ def make_curve_parameters(parameters): ('coef_div_modulus', '%nat'), ('modinv_fuel', '%nat')): replacements[k] = fix_option(nested_list_to_string(replacements.get(k, 'None')), scope_string=scope_string) - for k in ('s', 'c', 'goldilocks'): + for k in ('montgomery', ): + if k not in replacements.keys(): + replacements[k] = False + for k in ('s', 'c', 'goldilocks', 'montgomery'): replacements[k] = nested_list_to_string(replacements[k]) for k in ('extra_prove_mul_eq', 'extra_prove_square_eq'): if k not in replacements.keys(): @@ -240,6 +243,7 @@ Module Curve <: CurveParameters. Definition coef_div_modulus : option nat := %(coef_div_modulus)s. (* add %(coef_div_modulus_raw)s*modulus before subtracting *) Definition goldilocks : bool := %(goldilocks)s. + Definition montgomery : bool := %(montgomery)s. Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) := %(mul)s. @@ -271,9 +275,10 @@ End P. Module Export S := PackageSynthesis Curve P. """ % prefix -def make_synthesized_arg(fearg, prefix): +def make_synthesized_arg(fearg, prefix, montgomery=False): if fearg in ('femul', 'fesub', 'feadd'): - return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems. + if not montgomery: + return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import %(prefix)s.Synthesis. (* TODO : change this to field once field isomorphism happens *) @@ -288,6 +293,22 @@ Time Defined. Print Assumptions %(arg)s. """ % {'prefix':prefix, 'arg':fearg[2:]} + else: + return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import %(prefix)s.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition %(arg)s : + { %(arg)s : feBW_small -> feBW_small -> feBW_small + | forall a b, phiM_small (%(arg)s a b) = F.%(arg)s (phiM_small a) (phiM_small b) }. +Proof. + Set Ltac Profiling. + Time synthesize_%(arg)s (). + Show Ltac Profile. +Time Defined. + +Print Assumptions %(arg)s. +""" % {'prefix':prefix, 'arg':fearg[2:]} elif fearg in ('fesquare',): return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import %(prefix)s.Synthesis. @@ -321,7 +342,8 @@ Time Defined. Print Assumptions freeze. """ % {'prefix':prefix} elif fearg in ('feopp',): - return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems. + if not montgomery: + return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import %(prefix)s.Synthesis. (* TODO : change this to field once field isomorphism happens *) @@ -336,6 +358,43 @@ Time Defined. Print Assumptions %(arg)s. """ % {'prefix':prefix, 'arg':fearg[2:]} + else: + return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import %(prefix)s.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition %(arg)s : + { %(arg)s : feBW_small -> feBW_small + | forall a, phiM_small (%(arg)s a) = F.%(arg)s (phiM_small a) }. +Proof. + Set Ltac Profiling. + Time synthesize_%(arg)s (). + Show Ltac Profile. +Time Defined. + +Print Assumptions %(arg)s. +""" % {'prefix':prefix, 'arg':fearg[2:]} + elif fearg in ('fenz',): + assert(fearg == 'fenz') + assert(montgomery) + full_arg = 'nonzero' + return r"""Require Import Coq.ZArith.ZArith. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import %(prefix)s.Synthesis. +Local Open Scope Z_scope. + +(* TODO : change this to field once field isomorphism happens *) +Definition %(full_arg)s : + { %(full_arg)s : feBW_small -> BoundedWord.BoundedWord 1 adjusted_bitwidth bound1 + | forall a, (BoundedWord.BoundedWordToZ _ _ _ (%(full_arg)s a) =? 0) = (if Decidable.dec (phiM_small a = F.of_Z m 0) then true else false) }. +Proof. + Set Ltac Profiling. + Time synthesize_%(full_arg)s (). + Show Ltac Profile. +Time Defined. + +Print Assumptions %(full_arg)s. +""" % {'prefix':prefix, 'full_arg':full_arg} elif fearg in ('ladderstep', 'xzladderstep'): return r"""Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.PrimeFieldTheorems. @@ -411,7 +470,7 @@ def main(*args): outputs['CurveParameters.v'] = make_curve_parameters(parameters) outputs['Synthesis.v'] = make_synthesis(output_prefix) for arg in parameters['operations']: - outputs[arg + '.v'] = make_synthesized_arg(arg, output_prefix) + outputs[arg + '.v'] = make_synthesized_arg(arg, output_prefix, montgomery=(parameters.get('montgomery', 'false') == 'true')) outputs[arg + 'Display.v'] = make_display_arg(arg, output_prefix) for fname in parameters.get('extra_files', []): outputs[os.path.basename(fname)] = open(os.path.join(parameters_folder, fname), 'r').read() diff --git a/src/Specific/IntegrationTestKaratsubaMulDisplay.log b/src/Specific/IntegrationTestKaratsubaMulDisplay.log deleted file mode 100644 index d085a6e3e..000000000 --- a/src/Specific/IntegrationTestKaratsubaMulDisplay.log +++ /dev/null @@ -1,61 +0,0 @@ -λ x x0 : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64, -Interp-η -(λ var : Syntax.base_type → Type, - λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core, - uint128_t x32 = (((uint128_t)(x11 + x16) * (x25 + x30)) - ((uint128_t)x11 * x25)); - uint128_t x33 = ((((uint128_t)(x9 + x17) * (x25 + x30)) + ((uint128_t)(x11 + x16) * (x23 + x31))) - (((uint128_t)x9 * x25) + ((uint128_t)x11 * x23))); - uint128_t x34 = ((((uint128_t)(x7 + x15) * (x25 + x30)) + (((uint128_t)(x9 + x17) * (x23 + x31)) + ((uint128_t)(x11 + x16) * (x21 + x29)))) - (((uint128_t)x7 * x25) + (((uint128_t)x9 * x23) + ((uint128_t)x11 * x21)))); - uint128_t x35 = ((((uint128_t)(x5 + x13) * (x25 + x30)) + (((uint128_t)(x7 + x15) * (x23 + x31)) + (((uint128_t)(x9 + x17) * (x21 + x29)) + ((uint128_t)(x11 + x16) * (x19 + x27))))) - (((uint128_t)x5 * x25) + (((uint128_t)x7 * x23) + (((uint128_t)x9 * x21) + ((uint128_t)x11 * x19))))); - uint128_t x36 = ((((uint128_t)(x5 + x13) * (x23 + x31)) + (((uint128_t)(x7 + x15) * (x21 + x29)) + ((uint128_t)(x9 + x17) * (x19 + x27)))) - (((uint128_t)x5 * x23) + (((uint128_t)x7 * x21) + ((uint128_t)x9 * x19)))); - uint128_t x37 = ((((uint128_t)(x5 + x13) * (x21 + x29)) + ((uint128_t)(x7 + x15) * (x19 + x27))) - (((uint128_t)x5 * x21) + ((uint128_t)x7 * x19))); - uint128_t x38 = (((uint128_t)(x5 + x13) * (x19 + x27)) - ((uint128_t)x5 * x19)); - uint128_t x39 = (((((uint128_t)x11 * x25) + ((uint128_t)x16 * x30)) + x36) + x32); - uint128_t x40 = ((((((uint128_t)x9 * x25) + ((uint128_t)x11 * x23)) + (((uint128_t)x17 * x30) + ((uint128_t)x16 * x31))) + x37) + x33); - uint128_t x41 = ((((((uint128_t)x7 * x25) + (((uint128_t)x9 * x23) + ((uint128_t)x11 * x21))) + (((uint128_t)x15 * x30) + (((uint128_t)x17 * x31) + ((uint128_t)x16 * x29)))) + x38) + x34); - uint128_t x42 = ((((uint128_t)x5 * x25) + (((uint128_t)x7 * x23) + (((uint128_t)x9 * x21) + ((uint128_t)x11 * x19)))) + (((uint128_t)x13 * x30) + (((uint128_t)x15 * x31) + (((uint128_t)x17 * x29) + ((uint128_t)x16 * x27))))); - uint128_t x43 = (((((uint128_t)x5 * x23) + (((uint128_t)x7 * x21) + ((uint128_t)x9 * x19))) + (((uint128_t)x13 * x31) + (((uint128_t)x15 * x29) + ((uint128_t)x17 * x27)))) + x32); - uint128_t x44 = (((((uint128_t)x5 * x21) + ((uint128_t)x7 * x19)) + (((uint128_t)x13 * x29) + ((uint128_t)x15 * x27))) + x33); - uint128_t x45 = ((((uint128_t)x5 * x19) + ((uint128_t)x13 * x27)) + x34); - uint64_t x46 = (uint64_t) (x42 >> 0x38); - uint64_t x47 = ((uint64_t)x42 & 0xffffffffffffff); - uint64_t x48 = (uint64_t) (x35 >> 0x38); - uint64_t x49 = ((uint64_t)x35 & 0xffffffffffffff); - uint128_t x50 = (((uint128_t)0x100000000000000 * x48) + x49); - uint64_t x51 = (uint64_t) (x50 >> 0x38); - uint64_t x52 = ((uint64_t)x50 & 0xffffffffffffff); - uint128_t x53 = (x45 + x51); - uint64_t x54 = (uint64_t) (x53 >> 0x38); - uint64_t x55 = ((uint64_t)x53 & 0xffffffffffffff); - uint128_t x56 = ((x46 + x41) + x51); - uint64_t x57 = (uint64_t) (x56 >> 0x38); - uint64_t x58 = ((uint64_t)x56 & 0xffffffffffffff); - uint128_t x59 = (x54 + x44); - uint64_t x60 = (uint64_t) (x59 >> 0x38); - uint64_t x61 = ((uint64_t)x59 & 0xffffffffffffff); - uint128_t x62 = (x57 + x40); - uint64_t x63 = (uint64_t) (x62 >> 0x38); - uint64_t x64 = ((uint64_t)x62 & 0xffffffffffffff); - uint128_t x65 = (x60 + x43); - uint64_t x66 = (uint64_t) (x65 >> 0x38); - uint64_t x67 = ((uint64_t)x65 & 0xffffffffffffff); - uint128_t x68 = (x63 + x39); - uint64_t x69 = (uint64_t) (x68 >> 0x38); - uint64_t x70 = ((uint64_t)x68 & 0xffffffffffffff); - uint64_t x71 = (x66 + x47); - uint64_t x72 = (x71 >> 0x38); - uint64_t x73 = (x71 & 0xffffffffffffff); - uint64_t x74 = (x69 + x52); - uint64_t x75 = (x74 >> 0x38); - uint64_t x76 = (x74 & 0xffffffffffffff); - uint64_t x77 = ((0x100000000000000 * x75) + x76); - uint64_t x78 = (x77 >> 0x38); - uint64_t x79 = (x77 & 0xffffffffffffff); - uint64_t x80 = ((x72 + x58) + x78); - uint64_t x81 = (x80 >> 0x38); - uint64_t x82 = (x80 & 0xffffffffffffff); - uint64_t x83 = (x55 + x78); - uint64_t x84 = (x83 >> 0x38); - uint64_t x85 = (x83 & 0xffffffffffffff); - return (Return x79, Return x70, (x81 + x64), Return x82, Return x73, Return x67, (x84 + x61), Return x85)) -(x, x0)%core - : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/IntegrationTestLadderstep130Display.log b/src/Specific/IntegrationTestLadderstep130Display.log deleted file mode 100644 index deff79fe1..000000000 --- a/src/Specific/IntegrationTestLadderstep130Display.log +++ /dev/null @@ -1,220 +0,0 @@ -λ x x0 x1 x2 x3 : word128 * word128 * word128, -let (a, b) := Interp-η -(λ var : Syntax.base_type → Type, - λ '(x11, x12, x10, (x17, x18, x16, (x21, x22, x20)), (x27, x28, x26, (x31, x32, x30)))%core, - uint128_t x33 = (x17 + x21); - uint128_t x34 = (x18 + x22); - uint128_t x35 = (x16 + x20); - uint128_t x36 = ((0x3ffffffffffffffffffffeL + x17) - x21); - uint128_t x37 = ((0x3ffffffffffffffffffffeL + x18) - x22); - uint128_t x38 = ((0x3ffffffffffffffffffff6L + x16) - x20); - uint256_t x39 = (((uint256_t)x35 * x33) + (((uint256_t)x34 * x34) + ((uint256_t)x33 * x35))); - uint256_t x40 = ((((uint256_t)x35 * x34) + ((uint256_t)x34 * x35)) + (0x5 * ((uint256_t)x33 * x33))); - uint256_t x41 = (((uint256_t)x35 * x35) + (0x5 * (((uint256_t)x34 * x33) + ((uint256_t)x33 * x34)))); - uint128_t x42 = (uint128_t) (x41 >> 0x55); - uint128_t x43 = ((uint128_t)x41 & 0x1fffffffffffffffffffffL); - uint256_t x44 = (x42 + x40); - uint128_t x45 = (uint128_t) (x44 >> 0x55); - uint128_t x46 = ((uint128_t)x44 & 0x1fffffffffffffffffffffL); - uint256_t x47 = (x45 + x39); - uint128_t x48 = (uint128_t) (x47 >> 0x55); - uint128_t x49 = ((uint128_t)x47 & 0x1fffffffffffffffffffffL); - uint128_t x50 = (x43 + (0x5 * x48)); - uint128_t x51 = (x50 >> 0x55); - uint128_t x52 = (x50 & 0x1fffffffffffffffffffffL); - uint128_t x53 = (x51 + x46); - uint128_t x54 = (x53 >> 0x55); - uint128_t x55 = (x53 & 0x1fffffffffffffffffffffL); - uint128_t x56 = (x54 + x49); - uint256_t x57 = (((uint256_t)x38 * x36) + (((uint256_t)x37 * x37) + ((uint256_t)x36 * x38))); - uint256_t x58 = ((((uint256_t)x38 * x37) + ((uint256_t)x37 * x38)) + (0x5 * ((uint256_t)x36 * x36))); - uint256_t x59 = (((uint256_t)x38 * x38) + (0x5 * (((uint256_t)x37 * x36) + ((uint256_t)x36 * x37)))); - uint128_t x60 = (uint128_t) (x59 >> 0x55); - uint128_t x61 = ((uint128_t)x59 & 0x1fffffffffffffffffffffL); - uint256_t x62 = (x60 + x58); - uint128_t x63 = (uint128_t) (x62 >> 0x55); - uint128_t x64 = ((uint128_t)x62 & 0x1fffffffffffffffffffffL); - uint256_t x65 = (x63 + x57); - uint128_t x66 = (uint128_t) (x65 >> 0x55); - uint128_t x67 = ((uint128_t)x65 & 0x1fffffffffffffffffffffL); - uint128_t x68 = (x61 + (0x5 * x66)); - uint128_t x69 = (x68 >> 0x55); - uint128_t x70 = (x68 & 0x1fffffffffffffffffffffL); - uint128_t x71 = (x69 + x64); - uint128_t x72 = (x71 >> 0x55); - uint128_t x73 = (x71 & 0x1fffffffffffffffffffffL); - uint128_t x74 = (x72 + x67); - uint256_t x75 = (((uint256_t)x52 * x74) + (((uint256_t)x55 * x73) + ((uint256_t)x56 * x70))); - uint256_t x76 = ((((uint256_t)x52 * x73) + ((uint256_t)x55 * x70)) + (0x5 * ((uint256_t)x56 * x74))); - uint256_t x77 = (((uint256_t)x52 * x70) + (0x5 * (((uint256_t)x55 * x74) + ((uint256_t)x56 * x73)))); - uint128_t x78 = (uint128_t) (x77 >> 0x55); - uint128_t x79 = ((uint128_t)x77 & 0x1fffffffffffffffffffffL); - uint256_t x80 = (x78 + x76); - uint128_t x81 = (uint128_t) (x80 >> 0x55); - uint128_t x82 = ((uint128_t)x80 & 0x1fffffffffffffffffffffL); - uint256_t x83 = (x81 + x75); - uint128_t x84 = (uint128_t) (x83 >> 0x55); - uint128_t x85 = ((uint128_t)x83 & 0x1fffffffffffffffffffffL); - uint128_t x86 = (x79 + (0x5 * x84)); - uint128_t x87 = (x86 >> 0x55); - uint128_t x88 = (x86 & 0x1fffffffffffffffffffffL); - uint128_t x89 = (x87 + x82); - uint128_t x90 = (x89 >> 0x55); - uint128_t x91 = (x89 & 0x1fffffffffffffffffffffL); - uint128_t x92 = (x90 + x85); - uint128_t x93 = ((0x3ffffffffffffffffffffeL + x56) - x74); - uint128_t x94 = ((0x3ffffffffffffffffffffeL + x55) - x73); - uint128_t x95 = ((0x3ffffffffffffffffffff6L + x52) - x70); - uint128_t x96 = (0x1db41 * x93); - uint128_t x97 = (0x1db41 * x94); - uint128_t x98 = (0x1db41 * x95); - uint128_t x99 = (x98 >> 0x55); - uint128_t x100 = (x98 & 0x1fffffffffffffffffffffL); - uint128_t x101 = (x99 + x97); - uint128_t x102 = (x101 >> 0x55); - uint128_t x103 = (x101 & 0x1fffffffffffffffffffffL); - uint128_t x104 = (x102 + x96); - uint128_t x105 = (x104 >> 0x55); - uint128_t x106 = (x104 & 0x1fffffffffffffffffffffL); - uint128_t x107 = (x100 + (0x5 * x105)); - uint128_t x108 = (x107 >> 0x55); - uint128_t x109 = (x107 & 0x1fffffffffffffffffffffL); - uint128_t x110 = (x108 + x103); - uint128_t x111 = (x110 >> 0x55); - uint128_t x112 = (x110 & 0x1fffffffffffffffffffffL); - uint128_t x113 = (x111 + x106); - uint128_t x114 = (x56 + x113); - uint128_t x115 = (x55 + x112); - uint128_t x116 = (x52 + x109); - uint256_t x117 = (((uint256_t)x95 * x114) + (((uint256_t)x94 * x115) + ((uint256_t)x93 * x116))); - uint256_t x118 = ((((uint256_t)x95 * x115) + ((uint256_t)x94 * x116)) + (0x5 * ((uint256_t)x93 * x114))); - uint256_t x119 = (((uint256_t)x95 * x116) + (0x5 * (((uint256_t)x94 * x114) + ((uint256_t)x93 * x115)))); - uint128_t x120 = (uint128_t) (x119 >> 0x55); - uint128_t x121 = ((uint128_t)x119 & 0x1fffffffffffffffffffffL); - uint256_t x122 = (x120 + x118); - uint128_t x123 = (uint128_t) (x122 >> 0x55); - uint128_t x124 = ((uint128_t)x122 & 0x1fffffffffffffffffffffL); - uint256_t x125 = (x123 + x117); - uint128_t x126 = (uint128_t) (x125 >> 0x55); - uint128_t x127 = ((uint128_t)x125 & 0x1fffffffffffffffffffffL); - uint128_t x128 = (x121 + (0x5 * x126)); - uint128_t x129 = (x128 >> 0x55); - uint128_t x130 = (x128 & 0x1fffffffffffffffffffffL); - uint128_t x131 = (x129 + x124); - uint128_t x132 = (x131 >> 0x55); - uint128_t x133 = (x131 & 0x1fffffffffffffffffffffL); - uint128_t x134 = (x132 + x127); - uint128_t x135 = (x27 + x31); - uint128_t x136 = (x28 + x32); - uint128_t x137 = (x26 + x30); - uint128_t x138 = ((0x3ffffffffffffffffffffeL + x27) - x31); - uint128_t x139 = ((0x3ffffffffffffffffffffeL + x28) - x32); - uint128_t x140 = ((0x3ffffffffffffffffffff6L + x26) - x30); - uint256_t x141 = (((uint256_t)x137 * x36) + (((uint256_t)x136 * x37) + ((uint256_t)x135 * x38))); - uint256_t x142 = ((((uint256_t)x137 * x37) + ((uint256_t)x136 * x38)) + (0x5 * ((uint256_t)x135 * x36))); - uint256_t x143 = (((uint256_t)x137 * x38) + (0x5 * (((uint256_t)x136 * x36) + ((uint256_t)x135 * x37)))); - uint128_t x144 = (uint128_t) (x143 >> 0x55); - uint128_t x145 = ((uint128_t)x143 & 0x1fffffffffffffffffffffL); - uint256_t x146 = (x144 + x142); - uint128_t x147 = (uint128_t) (x146 >> 0x55); - uint128_t x148 = ((uint128_t)x146 & 0x1fffffffffffffffffffffL); - uint256_t x149 = (x147 + x141); - uint128_t x150 = (uint128_t) (x149 >> 0x55); - uint128_t x151 = ((uint128_t)x149 & 0x1fffffffffffffffffffffL); - uint128_t x152 = (x145 + (0x5 * x150)); - uint128_t x153 = (x152 >> 0x55); - uint128_t x154 = (x152 & 0x1fffffffffffffffffffffL); - uint128_t x155 = (x153 + x148); - uint128_t x156 = (x155 >> 0x55); - uint128_t x157 = (x155 & 0x1fffffffffffffffffffffL); - uint128_t x158 = (x156 + x151); - uint256_t x159 = (((uint256_t)x140 * x33) + (((uint256_t)x139 * x34) + ((uint256_t)x138 * x35))); - uint256_t x160 = ((((uint256_t)x140 * x34) + ((uint256_t)x139 * x35)) + (0x5 * ((uint256_t)x138 * x33))); - uint256_t x161 = (((uint256_t)x140 * x35) + (0x5 * (((uint256_t)x139 * x33) + ((uint256_t)x138 * x34)))); - uint128_t x162 = (uint128_t) (x161 >> 0x55); - uint128_t x163 = ((uint128_t)x161 & 0x1fffffffffffffffffffffL); - uint256_t x164 = (x162 + x160); - uint128_t x165 = (uint128_t) (x164 >> 0x55); - uint128_t x166 = ((uint128_t)x164 & 0x1fffffffffffffffffffffL); - uint256_t x167 = (x165 + x159); - uint128_t x168 = (uint128_t) (x167 >> 0x55); - uint128_t x169 = ((uint128_t)x167 & 0x1fffffffffffffffffffffL); - uint128_t x170 = (x163 + (0x5 * x168)); - uint128_t x171 = (x170 >> 0x55); - uint128_t x172 = (x170 & 0x1fffffffffffffffffffffL); - uint128_t x173 = (x171 + x166); - uint128_t x174 = (x173 >> 0x55); - uint128_t x175 = (x173 & 0x1fffffffffffffffffffffL); - uint128_t x176 = (x174 + x169); - uint128_t x177 = (x176 + x158); - uint128_t x178 = (x175 + x157); - uint128_t x179 = (x172 + x154); - uint128_t x180 = (x176 + x158); - uint128_t x181 = (x175 + x157); - uint128_t x182 = (x172 + x154); - uint256_t x183 = (((uint256_t)x179 * x180) + (((uint256_t)x178 * x181) + ((uint256_t)x177 * x182))); - uint256_t x184 = ((((uint256_t)x179 * x181) + ((uint256_t)x178 * x182)) + (0x5 * ((uint256_t)x177 * x180))); - uint256_t x185 = (((uint256_t)x179 * x182) + (0x5 * (((uint256_t)x178 * x180) + ((uint256_t)x177 * x181)))); - uint128_t x186 = (uint128_t) (x185 >> 0x55); - uint128_t x187 = ((uint128_t)x185 & 0x1fffffffffffffffffffffL); - uint256_t x188 = (x186 + x184); - uint128_t x189 = (uint128_t) (x188 >> 0x55); - uint128_t x190 = ((uint128_t)x188 & 0x1fffffffffffffffffffffL); - uint256_t x191 = (x189 + x183); - uint128_t x192 = (uint128_t) (x191 >> 0x55); - uint128_t x193 = ((uint128_t)x191 & 0x1fffffffffffffffffffffL); - uint128_t x194 = (x187 + (0x5 * x192)); - uint128_t x195 = (x194 >> 0x55); - uint128_t x196 = (x194 & 0x1fffffffffffffffffffffL); - uint128_t x197 = (x195 + x190); - uint128_t x198 = (x197 >> 0x55); - uint128_t x199 = (x197 & 0x1fffffffffffffffffffffL); - uint128_t x200 = (x198 + x193); - uint128_t x201 = ((0x3ffffffffffffffffffffeL + x176) - x158); - uint128_t x202 = ((0x3ffffffffffffffffffffeL + x175) - x157); - uint128_t x203 = ((0x3ffffffffffffffffffff6L + x172) - x154); - uint128_t x204 = ((0x3ffffffffffffffffffffeL + x176) - x158); - uint128_t x205 = ((0x3ffffffffffffffffffffeL + x175) - x157); - uint128_t x206 = ((0x3ffffffffffffffffffff6L + x172) - x154); - uint256_t x207 = (((uint256_t)x203 * x204) + (((uint256_t)x202 * x205) + ((uint256_t)x201 * x206))); - uint256_t x208 = ((((uint256_t)x203 * x205) + ((uint256_t)x202 * x206)) + (0x5 * ((uint256_t)x201 * x204))); - uint256_t x209 = (((uint256_t)x203 * x206) + (0x5 * (((uint256_t)x202 * x204) + ((uint256_t)x201 * x205)))); - uint128_t x210 = (uint128_t) (x209 >> 0x55); - uint128_t x211 = ((uint128_t)x209 & 0x1fffffffffffffffffffffL); - uint256_t x212 = (x210 + x208); - uint128_t x213 = (uint128_t) (x212 >> 0x55); - uint128_t x214 = ((uint128_t)x212 & 0x1fffffffffffffffffffffL); - uint256_t x215 = (x213 + x207); - uint128_t x216 = (uint128_t) (x215 >> 0x55); - uint128_t x217 = ((uint128_t)x215 & 0x1fffffffffffffffffffffL); - uint128_t x218 = (x211 + (0x5 * x216)); - uint128_t x219 = (x218 >> 0x55); - uint128_t x220 = (x218 & 0x1fffffffffffffffffffffL); - uint128_t x221 = (x219 + x214); - uint128_t x222 = (x221 >> 0x55); - uint128_t x223 = (x221 & 0x1fffffffffffffffffffffL); - uint128_t x224 = (x222 + x217); - uint256_t x225 = (((uint256_t)x10 * x224) + (((uint256_t)x12 * x223) + ((uint256_t)x11 * x220))); - uint256_t x226 = ((((uint256_t)x10 * x223) + ((uint256_t)x12 * x220)) + (0x5 * ((uint256_t)x11 * x224))); - uint256_t x227 = (((uint256_t)x10 * x220) + (0x5 * (((uint256_t)x12 * x224) + ((uint256_t)x11 * x223)))); - uint128_t x228 = (uint128_t) (x227 >> 0x55); - uint128_t x229 = ((uint128_t)x227 & 0x1fffffffffffffffffffffL); - uint256_t x230 = (x228 + x226); - uint128_t x231 = (uint128_t) (x230 >> 0x55); - uint128_t x232 = ((uint128_t)x230 & 0x1fffffffffffffffffffffL); - uint256_t x233 = (x231 + x225); - uint128_t x234 = (uint128_t) (x233 >> 0x55); - uint128_t x235 = ((uint128_t)x233 & 0x1fffffffffffffffffffffL); - uint128_t x236 = (x229 + (0x5 * x234)); - uint128_t x237 = (x236 >> 0x55); - uint128_t x238 = (x236 & 0x1fffffffffffffffffffffL); - uint128_t x239 = (x237 + x232); - uint128_t x240 = (x239 >> 0x55); - uint128_t x241 = (x239 & 0x1fffffffffffffffffffffL); - uint128_t x242 = (x240 + x235); - return (Return x92, Return x91, Return x88, (Return x134, Return x133, Return x130), (Return x200, Return x199, Return x196, (Return x242, Return x241, Return x238)))) -(x, (x0, x1), (x2, x3))%core in -(let (a0, b0) := a in -(a0, b0), let (a0, b0) := b in -(a0, b0))%core - : word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 → word128 * word128 * word128 * (word128 * word128 * word128) * (word128 * word128 * word128 * (word128 * word128 * word128)) diff --git a/src/Specific/IntegrationTestMontgomeryP256_128.v b/src/Specific/IntegrationTestMontgomeryP256_128.v deleted file mode 100644 index d2b64d3b9..000000000 --- a/src/Specific/IntegrationTestMontgomeryP256_128.v +++ /dev/null @@ -1,126 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Local Open Scope Z_scope. - -Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Arithmetic.Core. Import B. -Require Crypto.Arithmetic.Saturated.MontgomeryAPI. -Require Import Crypto.Arithmetic.Saturated.UniformWeight. -Require Import Crypto.Specific.MontgomeryP256_128. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.DestructHead. -Import ListNotations. - -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. - -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Section BoundedField25p5. - Local Coercion Z.of_nat : nat >-> Z. - - Let bounds : Tuple.tuple zrange sz - := Eval compute in - Tuple.repeat {| lower := 0 ; upper := r-1 |} sz. - - Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))). - Let bitwidth := Eval compute in (2^lgbitwidth)%nat. - Let feZ : Type := tuple Z sz. - Let feW : Type := tuple (wordT lgbitwidth) sz. - Let feBW : Type := BoundedWord sz bitwidth bounds. - Let eval : feBW -> Z := - fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x). - Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }. - Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _. - Local Coercion feBW_of_feBW_small : feBW_small >-> feBW. - Let phi : feBW -> F m := - fun x => montgomery_to_F (eval x). - - Local Ltac op_sig_side_conditions_t _ := - try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. - - (* TODO : change this to field once field isomorphism happens *) - Definition mul - : { mul : feBW_small -> feBW_small -> feBW_small - | forall A B, phi (mul A B) = F.mul (phi A) (phi B) }. - Proof. - start_preglue. - all:cbv [feBW_of_feBW_small eval]. - do_rewrite_with_sig_by mulmod_256 op_sig_side_conditions_t. - cbv_runtime. - all:fin_preglue. - factor_out_bounds_and_strip_eval mulmod_256_bounded op_sig_side_conditions_t. - (* jgross start here! *) - Set Ltac Profiling. - (* Set Ltac Profiling. - Print Ltac ReflectiveTactics.solve_side_conditions. - Ltac ReflectiveTactics.solve_side_conditions ::= idtac. - Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - { Time ReflectiveTactics.do_reify. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Require Import CNotations. - Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. } - { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. } - { Time SubstLet.subst_let; clear; vm_compute; reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. } - { Time abstract ReflectiveTactics.handle_bounds_from_hyps. } - { Time ReflectiveTactics.handle_boundedness_side_condition. } *) - Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - Show Ltac Profile. - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s -*) - Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *) - -Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *) - -Print Assumptions mul. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Add.v b/src/Specific/IntegrationTestMontgomeryP256_128_Add.v deleted file mode 100644 index ff94e57ee..000000000 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Add.v +++ /dev/null @@ -1,126 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Local Open Scope Z_scope. - -Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Arithmetic.Core. Import B. -Require Crypto.Arithmetic.Saturated.MontgomeryAPI. -Require Import Crypto.Arithmetic.Saturated.UniformWeight. -Require Import Crypto.Specific.MontgomeryP256_128. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.DestructHead. -Import ListNotations. - -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. - -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Section BoundedField25p5. - Local Coercion Z.of_nat : nat >-> Z. - - Let bounds : Tuple.tuple zrange sz - := Eval compute in - Tuple.repeat {| lower := 0 ; upper := r-1 |} sz. - - Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))). - Let bitwidth := Eval compute in (2^lgbitwidth)%nat. - Let feZ : Type := tuple Z sz. - Let feW : Type := tuple (wordT lgbitwidth) sz. - Let feBW : Type := BoundedWord sz bitwidth bounds. - Let eval : feBW -> Z := - fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x). - Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }. - Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _. - Local Coercion feBW_of_feBW_small : feBW_small >-> feBW. - Let phi : feBW -> F m := - fun x => montgomery_to_F (eval x). - - Local Ltac op_sig_side_conditions_t _ := - try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. - - (* TODO : change this to field once field isomorphism happens *) - Definition add - : { add : feBW_small -> feBW_small -> feBW_small - | forall A B, phi (add A B) = F.add (phi A) (phi B) }. - Proof. - start_preglue. - all:cbv [feBW_of_feBW_small eval]. - do_rewrite_with_sig_by add op_sig_side_conditions_t. - cbv_runtime. - all:fin_preglue. - factor_out_bounds_and_strip_eval add_bounded op_sig_side_conditions_t. - (* jgross start here! *) - Set Ltac Profiling. - (* Set Ltac Profiling. - Print Ltac ReflectiveTactics.solve_side_conditions. - Ltac ReflectiveTactics.solve_side_conditions ::= idtac. - Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - { Time ReflectiveTactics.do_reify. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Require Import CNotations. - Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. } - { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. } - { Time SubstLet.subst_let; clear; vm_compute; reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. } - { Time abstract ReflectiveTactics.handle_bounds_from_hyps. } - { Time ReflectiveTactics.handle_boundedness_side_condition. } *) - Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - Show Ltac Profile. - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s -*) - Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *) - -Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *) - -Print Assumptions add. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v deleted file mode 100644 index 76664255c..000000000 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v +++ /dev/null @@ -1,114 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Local Open Scope Z_scope. - -Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Arithmetic.Core. Import B. -Require Crypto.Arithmetic.Saturated.MontgomeryAPI. -Require Import Crypto.Arithmetic.Saturated.UniformWeight. -Require Import Crypto.Specific.MontgomeryP256_128. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Import ListNotations. - -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. - -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Section BoundedField25p5. - Local Coercion Z.of_nat : nat >-> Z. - - Let bound1 : zrange - := Eval compute in - {| lower := 0 ; upper := r-1 |}. - Let bounds : Tuple.tuple zrange sz - := Eval compute in - Tuple.repeat bound1 sz. - - Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))). - Let bitwidth := Eval compute in (2^lgbitwidth)%nat. - Let feZ : Type := tuple Z sz. - Let feW : Type := tuple (wordT lgbitwidth) sz. - Let feBW : Type := BoundedWord sz bitwidth bounds. - Let eval : feBW -> Z := - fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x). - Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }. - Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _. - Local Coercion feBW_of_feBW_small : feBW_small >-> feBW. - Let phi : feBW -> F m := - fun x => montgomery_to_F (eval x). - - Local Ltac op_sig_side_conditions_t _ := - try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. - - (* TODO : change this to field once field isomorphism happens *) - Definition nonzero - : { nonzero : feBW_small -> BoundedWord 1 bitwidth bound1 - | forall A, (BoundedWordToZ _ _ _ (nonzero A) =? 0) = (if Decidable.dec (phi A = F.of_Z m 0) then true else false) }. - Proof. - apply_lift_sig; intros; eexists_sig_etransitivity. - all:cbv [feBW_of_feBW_small phi eval]. - refine (_ : (if Decidable.dec (_ = 0) then true else false) = _). - lazymatch goal with - | [ |- (if Decidable.dec ?x then _ else _) = (if Decidable.dec ?y then _ else _) ] - => cut (x <-> y); - [ destruct (Decidable.dec x), (Decidable.dec y); try reflexivity; intros [? ?]; - generalize dependent x; generalize dependent y; solve [ intuition congruence ] - | ] - end. - etransitivity; [ | eapply (proj2_sig nonzero) ]; - [ | solve [ op_sig_side_conditions_t () ].. ]. - reflexivity. - let decP := lazymatch goal with |- { c | _ = if Decidable.dec (?decP = 0) then _ else _ } => decP end in - apply (@proj2_sig_map _ (fun c => BoundedWordToZ 1 _ _ c = decP) _). - { intros a' H'; rewrite H'. - let H := fresh in - lazymatch goal with |- context[Decidable.dec ?x] => destruct (Decidable.dec x) as [H|H]; try rewrite H end. - { reflexivity. } - { let H := fresh in - lazymatch goal with |- context[?x =? 0] => destruct (x =? 0) eqn:? end; - try reflexivity. - Z.ltb_to_lt; congruence. } } - eexists_sig_etransitivity. - do_set_sig nonzero. - cbv_runtime. - reflexivity. - sig_dlet_in_rhs_to_context. - cbv [proj1_sig]. - match goal with - | [ H : feBW_small |- _ ] => destruct H as [? _] - end. - (* jgross start here! *) - Set Ltac Profiling. - (* Set Ltac Profiling. - Print Ltac ReflectiveTactics.solve_side_conditions. - Ltac ReflectiveTactics.solve_side_conditions ::= idtac. - Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - { Time ReflectiveTactics.do_reify. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Require Import CNotations. - Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. } - { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. } - { Time SubstLet.subst_let; clear; vm_compute; reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. } - { Time abstract ReflectiveTactics.handle_bounds_from_hyps. } - { Time ReflectiveTactics.handle_boundedness_side_condition. } *) - Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - Show Ltac Profile. - Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *) - -Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *) - -Print Assumptions nonzero. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.log b/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.log deleted file mode 100644 index 53c690df8..000000000 --- a/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.log +++ /dev/null @@ -1,8 +0,0 @@ -λ x : word128 * word128, -Interp-η -(λ var : Syntax.base_type → Type, - λ '(x1, x2)%core, - uint128_t x3 = (x2 | x1); - return x3) -x - : word128 * word128 → ReturnType uint128_t diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v b/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v deleted file mode 100644 index c908c1258..000000000 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v +++ /dev/null @@ -1,126 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Local Open Scope Z_scope. - -Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Arithmetic.Core. Import B. -Require Crypto.Arithmetic.Saturated.MontgomeryAPI. -Require Import Crypto.Arithmetic.Saturated.UniformWeight. -Require Import Crypto.Specific.MontgomeryP256_128. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.DestructHead. -Import ListNotations. - -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. - -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Section BoundedField25p5. - Local Coercion Z.of_nat : nat >-> Z. - - Let bounds : Tuple.tuple zrange sz - := Eval compute in - Tuple.repeat {| lower := 0 ; upper := r-1 |} sz. - - Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))). - Let bitwidth := Eval compute in (2^lgbitwidth)%nat. - Let feZ : Type := tuple Z sz. - Let feW : Type := tuple (wordT lgbitwidth) sz. - Let feBW : Type := BoundedWord sz bitwidth bounds. - Let eval : feBW -> Z := - fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x). - Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }. - Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _. - Local Coercion feBW_of_feBW_small : feBW_small >-> feBW. - Let phi : feBW -> F m := - fun x => montgomery_to_F (eval x). - - Local Ltac op_sig_side_conditions_t _ := - try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. - - (* TODO : change this to field once field isomorphism happens *) - Definition opp - : { opp : feBW_small -> feBW_small - | forall A, phi (opp A) = F.opp (phi A) }. - Proof. - start_preglue. - all:cbv [feBW_of_feBW_small eval]. - do_rewrite_with_sig_by opp op_sig_side_conditions_t. - cbv_runtime. - all:fin_preglue. - factor_out_bounds_and_strip_eval opp_bounded op_sig_side_conditions_t. - (* jgross start here! *) - Set Ltac Profiling. - (* Set Ltac Profiling. - Print Ltac ReflectiveTactics.solve_side_conditions. - Ltac ReflectiveTactics.solve_side_conditions ::= idtac. - Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - { Time ReflectiveTactics.do_reify. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Require Import CNotations. - Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. } - { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. } - { Time SubstLet.subst_let; clear; vm_compute; reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. } - { Time abstract ReflectiveTactics.handle_bounds_from_hyps. } - { Time ReflectiveTactics.handle_boundedness_side_condition. } *) - Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - Show Ltac Profile. - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s -*) - Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *) - -Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *) - -Print Assumptions opp. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v b/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v deleted file mode 100644 index 8f3df4cdf..000000000 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v +++ /dev/null @@ -1,126 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Local Open Scope Z_scope. - -Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Arithmetic.Core. Import B. -Require Crypto.Arithmetic.Saturated.MontgomeryAPI. -Require Import Crypto.Arithmetic.Saturated.UniformWeight. -Require Import Crypto.Specific.MontgomeryP256_128. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.DestructHead. -Import ListNotations. - -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. - -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Section BoundedField25p5. - Local Coercion Z.of_nat : nat >-> Z. - - Let bounds : Tuple.tuple zrange sz - := Eval compute in - Tuple.repeat {| lower := 0 ; upper := r-1 |} sz. - - Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))). - Let bitwidth := Eval compute in (2^lgbitwidth)%nat. - Let feZ : Type := tuple Z sz. - Let feW : Type := tuple (wordT lgbitwidth) sz. - Let feBW : Type := BoundedWord sz bitwidth bounds. - Let eval : feBW -> Z := - fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x). - Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }. - Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _. - Local Coercion feBW_of_feBW_small : feBW_small >-> feBW. - Let phi : feBW -> F m := - fun x => montgomery_to_F (eval x). - - Local Ltac op_sig_side_conditions_t _ := - try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. - - (* TODO : change this to field once field isomorphism happens *) - Definition sub - : { sub : feBW_small -> feBW_small -> feBW_small - | forall A B, phi (sub A B) = F.sub (phi A) (phi B) }. - Proof. - start_preglue. - all:cbv [feBW_of_feBW_small eval]. - do_rewrite_with_sig_by sub op_sig_side_conditions_t. - cbv_runtime. - all:fin_preglue. - factor_out_bounds_and_strip_eval sub_bounded op_sig_side_conditions_t. - (* jgross start here! *) - Set Ltac Profiling. - (* Set Ltac Profiling. - Print Ltac ReflectiveTactics.solve_side_conditions. - Ltac ReflectiveTactics.solve_side_conditions ::= idtac. - Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - { Time ReflectiveTactics.do_reify. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Require Import CNotations. - Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. } - { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. } - { Time SubstLet.subst_let; clear; vm_compute; reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. } - { Time abstract ReflectiveTactics.handle_bounds_from_hyps. } - { Time ReflectiveTactics.handle_boundedness_side_condition. } *) - Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - Show Ltac Profile. - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s -*) - Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *) - -Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *) - -Print Assumptions sub. diff --git a/src/Specific/MontgomeryP256_128.v b/src/Specific/MontgomeryP256_128.v deleted file mode 100644 index b3df2a409..000000000 --- a/src/Specific/MontgomeryP256_128.v +++ /dev/null @@ -1,444 +0,0 @@ -Require Import Coq.micromega.Lia. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Proofs. -Require Import Crypto.Arithmetic.Core. Import B. -Require Crypto.Arithmetic.Saturated.MontgomeryAPI. -Require Import Crypto.Arithmetic.Saturated.UniformWeight. -Require Import Crypto.Util.Sigma.Lift. -Require Import Coq.ZArith.BinInt. -Require Import Coq.PArith.BinPos. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.ZUtil.ModInv. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.BreakMatch. - -Definition wt (i:nat) : Z := Z.shiftl 1 (128*Z.of_nat i). -Definition r := Eval compute in (2^128)%positive. -Definition sz := 2%nat. -Definition m : positive := 2^256-2^224+2^192+2^96-1. -Definition p256 := - Eval vm_compute in - ((Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (Z.pos m))). -Definition r' := Eval vm_compute in Zpow_facts.Zpow_mod (Z.pos r) (Z.pos m - 2) (Z.pos m). -Definition r'_correct := eq_refl : ((Z.pos r * r') mod (Z.pos m) = 1)%Z. -Definition m' : Z := Eval vm_compute in Option.invert_Some (Z.modinv_fueled 10 (-Z.pos m) (Z.pos r)). -Definition m'_correct := eq_refl : ((Z.pos m * m') mod (Z.pos r) = (-1) mod Z.pos r)%Z. -Definition m_p256 := eq_refl (Z.pos m) <: Z.pos m = MontgomeryAPI.eval (n:=sz) (Z.pos r) p256. - -Lemma r'_pow_correct : ((r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 = 1)%Z. -Proof. vm_compute; reflexivity. Qed. - -Definition mulmod_256' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | forall (A B : Tuple.tuple Z sz), - f A B = - (redc (r:=r)(R_numlimbs:=sz) p256 A B m') - }. -Proof. - eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. - (* - cbv [ - r wt sz p256 - CPSUtil.Tuple.tl_cps CPSUtil.Tuple.hd_cps - CPSUtil.to_list_cps CPSUtil.to_list'_cps CPSUtil.to_list_cps' CPSUtil.flat_map_cps CPSUtil.fold_right_cps - CPSUtil.map_cps CPSUtil.Tuple.left_append_cps CPSUtil.firstn_cps CPSUtil.combine_cps CPSUtil.on_tuple_cps CPSUtil.update_nth_cps CPSUtil.from_list_default_cps CPSUtil.from_list_default'_cps - fst snd length List.seq List.hd List.app - redc pre_redc_cps redc_cps redc_loop_cps redc_body_cps - Positional.to_associational_cps - MontgomeryAPI.divmod_cps - MontgomeryAPI.conditional_sub_cps - MontgomeryAPI.scmul_cps - uweight - MontgomeryAPI.Columns.mul_cps - MontgomeryAPI.Associational.mul_cps - (*Z.of_nat Pos.of_succ_nat Nat.pred - Z.pow Z.pow_pos Z.mul Pos.iter Pos.mul Pos.succ*) - Tuple.hd Tuple.append Tuple.tl Tuple.hd' Tuple.tl' CPSUtil.Tuple.left_tl_cps CPSUtil.Tuple.left_hd_cps CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps - CPSUtil.Tuple.map2_cps - MontgomeryAPI.Columns.from_associational_cps - MontgomeryAPI.Associational.multerm_cps - MontgomeryAPI.Positional.sat_add_cps - MontgomeryAPI.Positional.sat_sub_cps - MontgomeryAPI.Positional.chain_op_cps - MontgomeryAPI.Positional.chain_op'_cps - MontgomeryAPI.Columns.compact_cps - MontgomeryAPI.Columns.compact_step_cps - MontgomeryAPI.Columns.compact_digit_cps - MontgomeryAPI.drop_high_cps - MontgomeryAPI.add_cps - MontgomeryAPI.add_S1_cps - MontgomeryAPI.Columns.add_cps - MontgomeryAPI.Columns.cons_to_nth_cps - Nat.pred - MontgomeryAPI.join0 - MontgomeryAPI.join0_cps CPSUtil.Tuple.left_append_cps - CPSUtil.Tuple.mapi_with_cps - id - Positional.zeros MontgomeryAPI.zero MontgomeryAPI.Columns.nils Tuple.repeat Tuple.append - Positional.place_cps - CPSUtil.Tuple.mapi_with'_cps Tuple.hd Tuple.hd' Tuple.tl Tuple.tl' CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps fst snd - Z.of_nat fst snd Z.pow Z.pow_pos Pos.of_succ_nat Z.div Z.mul Pos.mul Z.modulo Z.div_eucl Z.pos_div_eucl Z.leb Z.compare Pos.compare_cont Pos.compare Z.pow_pos Pos.iter Z.mul Pos.succ Z.ltb Z.gtb Z.geb Z.div Z.sub Z.pos_sub Z.add Z.opp Z.double - Decidable.dec Decidable.dec_eq_Z Z.eq_dec Z_rec Z_rec Z_rect - Positional.zeros MontgomeryAPI.zero MontgomeryAPI.Columns.nils Tuple.repeat Tuple.append - (* - MontgomeryAPI.Associational.multerm_cps - MontgomeryAPI.Columns.from_associational_cps Positional.place_cps MontgomeryAPI.Columns.cons_to_nth_cps MontgomeryAPI.Columns.nils -Tuple.append -Tuple.from_list Tuple.from_list' -Tuple.from_list_default Tuple.from_list_default' -Tuple.hd -Tuple.repeat -Tuple.tl -Tuple.tuple *) - (* MontgomeryAPI.add_cps MontgomeryAPI.divmod_cps MontgomeryAPI.drop_high_cps MontgomeryAPI.scmul_cps MontgomeryAPI.zero MontgomeryAPI.Columns.mul_cps MontgomeryAPI.Columns.add_cps uweight MontgomeryAPI.T *) - (* - CPSUtil.to_list_cps CPSUtil.to_list'_cps CPSUtil.to_list_cps' -Positional.zeros -Tuple.to_list -Tuple.to_list' -List.hd -List.tl -Nat.max -Positional.to_associational_cps -Z.of_nat *) - ]. - Unset Printing Notations. - - (* cbv -[runtime_add runtime_mul LetIn.Let_In Definitions.Z.add_get_carry_full Definitions.Z.mul_split]. *) - - (* basesystem_partial_evaluation_RHS. *) - *) - reflexivity. -Defined. - -Definition mulmod_256'' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | forall (A B : Tuple.tuple Z sz), - small (Z.pos r) A -> small (Z.pos r) B -> - let eval := MontgomeryAPI.eval (Z.pos r) in - (small (Z.pos r) (f A B) - /\ (eval B < eval p256 -> 0 <= eval (f A B) < eval p256) - /\ (eval (f A B) mod Z.pos m - = (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z - }. -Proof. - exists (proj1_sig mulmod_256'). - abstract ( - intros; rewrite (proj2_sig mulmod_256'); - split; [ | split ]; - [ apply small_redc with (ri:=r') | apply redc_bound_N with (ri:=r') | apply redc_mod_N ]; - try match goal with - | _ => assumption - | [ |- _ = _ :> Z ] => vm_compute; reflexivity - | _ => reflexivity - | [ |- small (Z.pos r) p256 ] - => hnf; cbv [Tuple.to_list sz p256 r Tuple.to_list' List.In]; intros; destruct_head'_or; - subst; try lia - | [ |- MontgomeryAPI.eval (Z.pos r) p256 <> 0%Z ] - => vm_compute; lia - end - ). -Defined. - -Definition add' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | forall (A B : Tuple.tuple Z sz), - f A B = - (add (r:=r)(R_numlimbs:=sz) p256 A B) - }. -Proof. - eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. - reflexivity. -Defined. - -Definition sub' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | forall (A B : Tuple.tuple Z sz), - f A B = - (sub (r:=r) (R_numlimbs:=sz) p256 A B) - }. -Proof. - eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. - reflexivity. -Defined. - -Definition opp' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz - | forall (A : Tuple.tuple Z sz), - f A = - (opp (r:=r) (R_numlimbs:=sz) p256 A) - }. -Proof. - eapply (lift1_sig (fun A c => c = _)); eexists. - cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. - reflexivity. -Defined. - -Definition nonzero' : { f:Tuple.tuple Z sz -> Z - | forall (A : Tuple.tuple Z sz), - f A = - (nonzero (R_numlimbs:=sz) A) - }. -Proof. - eapply (lift1_sig (fun A c => c = _)); eexists. - cbv -[runtime_lor Let_In]. - reflexivity. -Defined. - -Import ModularArithmetic. - -(*Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - small (Z.pos r) (f A B) - /\ (let eval := MontgomeryAPI.eval (Z.pos r) in - 0 <= eval (f A B) < Z.pos r^Z.of_nat sz - /\ (eval (f A B) mod Z.pos m - = (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z - }. -Proof.*) - -(** TODO: MOVE ME *) -Definition montgomery_to_F (v : Z) : F m - := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F. - -Definition mulmod_256_ext - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }. -Proof. - exists (proj1_sig mulmod_256''). - abstract ( - split; intros A Asm B Bsm; - pose proof (proj2_sig mulmod_256'' A B Asm Bsm) as H; - cbv zeta in *; - try solve [ destruct_head'_and; assumption ]; - rewrite ModularArithmeticTheorems.F.eq_of_Z_iff in H; - unfold montgomery_to_F; - destruct H as [H1 [H2 H3]]; - rewrite H3; - rewrite <- !ModularArithmeticTheorems.F.of_Z_mul; - f_equal; nia - ). -Defined. - -Definition mulmod_256 - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F }. -Proof. - let v := (eval cbv [proj1_sig mulmod_256_ext mulmod_256'' mulmod_256' lift2_sig] in (proj1_sig mulmod_256_ext)) in - (exists v). - abstract apply (proj2_sig mulmod_256_ext). -Defined. - -Lemma mulmod_256_bounded - : let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval B < eval p256 -> 0 <= eval (proj1_sig mulmod_256 A B) < eval p256)%Z. -Proof. apply (proj2_sig mulmod_256_ext). Qed. - -Local Ltac t_fin := - [ > reflexivity - | repeat match goal with - | _ => assumption - | [ |- _ = _ :> Z ] => vm_compute; reflexivity - | _ => reflexivity - | [ |- small (Z.pos r) p256 ] - => hnf; cbv [Tuple.to_list sz p256 r Tuple.to_list' List.In]; intros; destruct_head'_or; - subst; try lia - | [ |- MontgomeryAPI.eval (Z.pos r) p256 <> 0%Z ] - => vm_compute; lia - | [ |- and _ _ ] => split - | [ |- (0 <= MontgomeryAPI.eval (Z.pos r) _)%Z ] => apply MontgomeryAPI.eval_small - end.. ]. - -Definition add_ext - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> 0 <= eval (f A B) < eval p256)))%Z }. -Proof. - exists (proj1_sig add'). - abstract ( - split; intros; rewrite (proj2_sig add'); - unfold montgomery_to_F; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?ModularArithmeticTheorems.F.of_Z_add; - rewrite <- ?Z.mul_add_distr_r; - [ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; push_Zmod; rewrite eval_add_mod_N; pull_Zmod - | apply add_bound ]; - t_fin - ). -Defined. - -Definition sub_ext - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> 0 <= eval (f A B) < eval p256)))%Z }. -Proof. - exists (proj1_sig sub'). - abstract ( - split; intros; rewrite (proj2_sig sub'); - unfold montgomery_to_F; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?ModularArithmeticTheorems.F.of_Z_sub; - rewrite <- ?Z.mul_sub_distr_r; - [ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; push_Zmod; rewrite eval_sub_mod_N; pull_Zmod - | apply sub_bound ]; - t_fin - ). -Defined. - -Definition opp_ext - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> montgomery_to_F (eval (f A)) - = (F.opp (montgomery_to_F (eval A)))%F)) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> 0 <= eval (f A) < eval p256)))%Z }. -Proof. - exists (proj1_sig opp'). - abstract ( - split; intros; rewrite (proj2_sig opp'); - unfold montgomery_to_F; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?F_of_Z_opp; - rewrite <- ?Z.mul_opp_l; - [ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; push_Zmod; rewrite eval_opp_mod_N; pull_Zmod - | apply opp_bound ]; - t_fin - ). -Defined. - -Definition nonzero_ext - : { f:Tuple.tuple Z sz -> Z - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }. -Proof. - exists (proj1_sig nonzero'). - abstract ( - intros eval A H **; rewrite (proj2_sig nonzero'), (@eval_nonzero r) by (eassumption || reflexivity); - subst eval; - unfold montgomery_to_F, uweight in *; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul; - rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; - let H := fresh in - split; intro H; - [ rewrite H; autorewrite with zsimplify_const; reflexivity - | cut ((MontgomeryAPI.eval (Z.pos r) A * (r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz)) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 = 0)%Z; - [ rewrite Z.mul_mod, r'_pow_correct; autorewrite with zsimplify_const; pull_Zmod; [ | vm_compute; congruence ]; - rewrite Z.mod_small; [ trivial | split; try assumption; apply MontgomeryAPI.eval_small; try assumption; lia ] - | rewrite Z.mul_assoc, Z.mul_mod, H by (vm_compute; congruence); autorewrite with zsimplify_const; reflexivity ] ] - ). -Defined. - -Definition add - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)%Z }. -Proof. - let v := (eval cbv [proj1_sig add_ext add' lift2_sig] in (proj1_sig add_ext)) in - (exists v). - abstract apply (proj2_sig add_ext). -Defined. - -Lemma add_bounded - : let eval := MontgomeryAPI.eval (Z.pos r) in - (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> 0 <= eval (proj1_sig add A B) < eval p256))%Z. -Proof. apply (proj2_sig add_ext). Qed. - -Definition sub - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)%Z }. -Proof. - let v := (eval cbv [proj1_sig sub_ext sub' lift2_sig] in (proj1_sig sub_ext)) in - (exists v). - abstract apply (proj2_sig sub_ext). -Defined. - -Lemma sub_bounded - : let eval := MontgomeryAPI.eval (Z.pos r) in - (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> 0 <= eval (proj1_sig sub A B) < eval p256))%Z. -Proof. apply (proj2_sig sub_ext). Qed. - -Definition opp - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> montgomery_to_F (eval (f A)) - = (F.opp (montgomery_to_F (eval A)))%F)%Z }. -Proof. - let v := (eval cbv [proj1_sig opp_ext opp' lift1_sig] in (proj1_sig opp_ext)) in - (exists v). - abstract apply (proj2_sig opp_ext). -Defined. - -Lemma opp_bounded - : let eval := MontgomeryAPI.eval (Z.pos r) in - (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> 0 <= eval (proj1_sig opp A) < eval p256))%Z. -Proof. apply (proj2_sig opp_ext). Qed. - -Definition nonzero - : { f:Tuple.tuple Z sz -> Z - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }. -Proof. - let v := (eval cbv [proj1_sig nonzero_ext nonzero' lift1_sig] in (proj1_sig nonzero_ext)) in - (exists v). - abstract apply (proj2_sig nonzero_ext). -Defined. - - -Local Definition for_assumptions := (mulmod_256, add, sub, opp, nonzero). -Print Assumptions for_assumptions. diff --git a/src/Specific/NISTP256/AMD128/CurveParameters.v b/src/Specific/NISTP256/AMD128/CurveParameters.v new file mode 100644 index 000000000..ea4865b08 --- /dev/null +++ b/src/Specific/NISTP256/AMD128/CurveParameters.v @@ -0,0 +1,34 @@ +Require Import Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Util.LetIn. + +(*** +Modulus : 2^256-2^224+2^192+2^96-1 +Base: 128 +***) + +Module Curve <: CurveParameters. + Definition sz : nat := 2%nat. + Definition bitwidth : Z := 128. + Definition s : Z := 2^256. + Definition c : list limb := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]. + Definition carry_chains : option (list (list nat)) := Eval vm_compute in None. + + Definition a24 : option Z := None. + Definition coef_div_modulus : option nat := None. (* add 0*modulus before subtracting *) + + Definition goldilocks : bool := false. + Definition montgomery : bool := true. + + Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) + := None. + + Definition square_code : option (Z^sz -> Z^sz) + := None. + + Definition upper_bound_of_exponent : option (Z -> Z) := None. + Definition allowable_bit_widths : option (list nat) := None. + Definition freeze_extra_allowable_bit_widths : option (list nat) := None. + Definition modinv_fuel : option nat := None. + Ltac extra_prove_mul_eq := idtac. + Ltac extra_prove_square_eq := idtac. +End Curve. diff --git a/src/Specific/NISTP256/AMD128/Synthesis.v b/src/Specific/NISTP256/AMD128/Synthesis.v new file mode 100644 index 000000000..3871666e1 --- /dev/null +++ b/src/Specific/NISTP256/AMD128/Synthesis.v @@ -0,0 +1,11 @@ +Require Import Crypto.Specific.Framework.SynthesisFramework. +Require Import Crypto.Specific.NISTP256.AMD128.CurveParameters. + +Module Import T := MakeSynthesisTactics Curve. + +Module P <: PrePackage. + Definition package : Tag.Context. + Proof. make_Synthesis_package (). Defined. +End P. + +Module Export S := PackageSynthesis Curve P. diff --git a/src/Specific/NISTP256/AMD128/compiler.sh b/src/Specific/NISTP256/AMD128/compiler.sh new file mode 100644 index 000000000..518f95765 --- /dev/null +++ b/src/Specific/NISTP256/AMD128/compiler.sh @@ -0,0 +1,4 @@ +#!/bin/sh +set -eu + +gcc -fno-peephole2 `#GCC BUG 81300` -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes -Wno-incompatible-pointer-types -fno-strict-aliasing "$@" diff --git a/src/Specific/NISTP256/AMD128/feadd.v b/src/Specific/NISTP256/AMD128/feadd.v new file mode 100644 index 000000000..5ee329e4e --- /dev/null +++ b/src/Specific/NISTP256/AMD128/feadd.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.NISTP256.AMD128.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition add : + { add : feBW_small -> feBW_small -> feBW_small + | forall a b, phiM_small (add a b) = F.add (phiM_small a) (phiM_small b) }. +Proof. + Set Ltac Profiling. + Time synthesize_add (). + Show Ltac Profile. +Time Defined. + +Print Assumptions add. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.log b/src/Specific/NISTP256/AMD128/feaddDisplay.log index ea6db527b..ea6db527b 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.log +++ b/src/Specific/NISTP256/AMD128/feaddDisplay.log diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v b/src/Specific/NISTP256/AMD128/feaddDisplay.v index 13c7937cb..cde97baed 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v +++ b/src/Specific/NISTP256/AMD128/feaddDisplay.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Add. +Require Import Crypto.Specific.NISTP256.AMD128.feadd. Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display add. diff --git a/src/Specific/NISTP256/AMD128/femul.v b/src/Specific/NISTP256/AMD128/femul.v new file mode 100644 index 000000000..7c2ecbec1 --- /dev/null +++ b/src/Specific/NISTP256/AMD128/femul.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.NISTP256.AMD128.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition mul : + { mul : feBW_small -> feBW_small -> feBW_small + | forall a b, phiM_small (mul a b) = F.mul (phiM_small a) (phiM_small b) }. +Proof. + Set Ltac Profiling. + Time synthesize_mul (). + Show Ltac Profile. +Time Defined. + +Print Assumptions mul. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128Display.log b/src/Specific/NISTP256/AMD128/femulDisplay.log index 3edcd5cba..3edcd5cba 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128Display.log +++ b/src/Specific/NISTP256/AMD128/femulDisplay.log diff --git a/src/Specific/IntegrationTestMontgomeryP256_128Display.v b/src/Specific/NISTP256/AMD128/femulDisplay.v index 420ff7dc5..86a058019 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128Display.v +++ b/src/Specific/NISTP256/AMD128/femulDisplay.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128. +Require Import Crypto.Specific.NISTP256.AMD128.femul. Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/NISTP256/AMD128/fenz.v b/src/Specific/NISTP256/AMD128/fenz.v new file mode 100644 index 000000000..c1a91fa38 --- /dev/null +++ b/src/Specific/NISTP256/AMD128/fenz.v @@ -0,0 +1,16 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.NISTP256.AMD128.Synthesis. +Local Open Scope Z_scope. + +(* TODO : change this to field once field isomorphism happens *) +Definition nonzero : + { nonzero : feBW_small -> BoundedWord.BoundedWord 1 adjusted_bitwidth bound1 + | forall a, (BoundedWord.BoundedWordToZ _ _ _ (nonzero a) =? 0) = (if Decidable.dec (phiM_small a = F.of_Z m 0) then true else false) }. +Proof. + Set Ltac Profiling. + Time synthesize_nonzero (). + Show Ltac Profile. +Time Defined. + +Print Assumptions nonzero. diff --git a/src/Specific/NISTP256/AMD128/fenzDisplay.log b/src/Specific/NISTP256/AMD128/fenzDisplay.log new file mode 100644 index 000000000..58f9ac4f9 --- /dev/null +++ b/src/Specific/NISTP256/AMD128/fenzDisplay.log @@ -0,0 +1,20 @@ +λ x : word128 * word128, +Interp-η +(λ var : Syntax.base_type → Type, + λ '(x1, x2)%core, + uint128_t x3 = x2 | x1; + return x3) +x + : word128 * word128 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in + lower) with + | 0%Z => Eq + | Z.pos _ => Lt + | Z.neg _ => Gt + end with + | Eq => true + | Lt => true + | Gt => false + end then Some 7 else None) with + | Some lgsz => Syntax.TWord lgsz + | None => Syntax.TZ + end) diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v b/src/Specific/NISTP256/AMD128/fenzDisplay.v index 0d76f5171..18ff51330 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v +++ b/src/Specific/NISTP256/AMD128/fenzDisplay.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Nonzero. +Require Import Crypto.Specific.NISTP256.AMD128.fenz. Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display nonzero. diff --git a/src/Specific/NISTP256/AMD128/feopp.v b/src/Specific/NISTP256/AMD128/feopp.v new file mode 100644 index 000000000..682541e8c --- /dev/null +++ b/src/Specific/NISTP256/AMD128/feopp.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.NISTP256.AMD128.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition opp : + { opp : feBW_small -> feBW_small + | forall a, phiM_small (opp a) = F.opp (phiM_small a) }. +Proof. + Set Ltac Profiling. + Time synthesize_opp (). + Show Ltac Profile. +Time Defined. + +Print Assumptions opp. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log b/src/Specific/NISTP256/AMD128/feoppDisplay.log index ea60d9f66..ea60d9f66 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.log +++ b/src/Specific/NISTP256/AMD128/feoppDisplay.log diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v b/src/Specific/NISTP256/AMD128/feoppDisplay.v index ca8721d7d..8c84f30d2 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v +++ b/src/Specific/NISTP256/AMD128/feoppDisplay.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Opp. +Require Import Crypto.Specific.NISTP256.AMD128.feopp. Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display opp. diff --git a/src/Specific/NISTP256/AMD128/fesub.v b/src/Specific/NISTP256/AMD128/fesub.v new file mode 100644 index 000000000..f8a59ec86 --- /dev/null +++ b/src/Specific/NISTP256/AMD128/fesub.v @@ -0,0 +1,14 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.NISTP256.AMD128.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition sub : + { sub : feBW_small -> feBW_small -> feBW_small + | forall a b, phiM_small (sub a b) = F.sub (phiM_small a) (phiM_small b) }. +Proof. + Set Ltac Profiling. + Time synthesize_sub (). + Show Ltac Profile. +Time Defined. + +Print Assumptions sub. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log b/src/Specific/NISTP256/AMD128/fesubDisplay.log index 70f224d33..70f224d33 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.log +++ b/src/Specific/NISTP256/AMD128/fesubDisplay.log diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v b/src/Specific/NISTP256/AMD128/fesubDisplay.v index 879a8e0cd..4e46b2272 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v +++ b/src/Specific/NISTP256/AMD128/fesubDisplay.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Sub. +Require Import Crypto.Specific.NISTP256.AMD128.fesub. Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display sub. diff --git a/src/Specific/NISTP256/AMD64/CurveParameters.v b/src/Specific/NISTP256/AMD64/CurveParameters.v new file mode 100644 index 000000000..01cac5db0 --- /dev/null +++ b/src/Specific/NISTP256/AMD64/CurveParameters.v @@ -0,0 +1,34 @@ +Require Import Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Util.LetIn. + +(*** +Modulus : 2^256-2^224+2^192+2^96-1 +Base: 64 +***) + +Module Curve <: CurveParameters. + Definition sz : nat := 4%nat. + Definition bitwidth : Z := 64. + Definition s : Z := 2^256. + Definition c : list limb := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]. + Definition carry_chains : option (list (list nat)) := Eval vm_compute in None. + + Definition a24 : option Z := None. + Definition coef_div_modulus : option nat := None. (* add 0*modulus before subtracting *) + + Definition goldilocks : bool := false. + Definition montgomery : bool := true. + + Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) + := None. + + Definition square_code : option (Z^sz -> Z^sz) + := None. + + Definition upper_bound_of_exponent : option (Z -> Z) := None. + Definition allowable_bit_widths : option (list nat) := None. + Definition freeze_extra_allowable_bit_widths : option (list nat) := None. + Definition modinv_fuel : option nat := None. + Ltac extra_prove_mul_eq := idtac. + Ltac extra_prove_square_eq := idtac. +End Curve. diff --git a/src/Specific/NISTP256/AMD64/MontgomeryP256.v b/src/Specific/NISTP256/AMD64/MontgomeryP256.v deleted file mode 100644 index e8b25a781..000000000 --- a/src/Specific/NISTP256/AMD64/MontgomeryP256.v +++ /dev/null @@ -1,438 +0,0 @@ -Require Import Coq.micromega.Lia. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Proofs. -Require Import Crypto.Arithmetic.Core. Import B. -Require Crypto.Arithmetic.Saturated.MontgomeryAPI. -Require Import Crypto.Arithmetic.Saturated.UniformWeight. -Require Import Crypto.Util.Sigma.Lift. -Require Import Coq.ZArith.BinInt. -Require Import Coq.PArith.BinPos. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.ZUtil.ModInv. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.Tactics.BreakMatch. - -Definition wt (i:nat) : Z := Z.shiftl 1 (64*Z.of_nat i). -Definition r := Eval compute in (2^64)%positive. -Definition sz := 4%nat. -Definition m : positive := 2^256-2^224+2^192+2^96-1. -Definition p256 := - Eval vm_compute in - ((Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (Z.pos m))). -Definition r' := Eval vm_compute in Zpow_facts.Zpow_mod (Z.pos r) (Z.pos m - 2) (Z.pos m). -Definition r'_correct := eq_refl : ((Z.pos r * r') mod (Z.pos m) = 1)%Z. -Definition m' : Z := Eval vm_compute in Option.invert_Some (Z.modinv_fueled 10 (-Z.pos m) (Z.pos r)). -Definition m'_correct := eq_refl : ((Z.pos m * m') mod (Z.pos r) = (-1) mod Z.pos r)%Z. -Definition m_p256 := eq_refl (Z.pos m) <: Z.pos m = MontgomeryAPI.eval (n:=sz) (Z.pos r) p256. - -Lemma r'_pow_correct : ((r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 = 1)%Z. -Proof. vm_compute; reflexivity. Qed. - -Definition mulmod_256' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | forall (A B : Tuple.tuple Z sz), - f A B = - (redc (r:=r)(R_numlimbs:=sz) p256 A B m') - }. -Proof. - eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. - (* - cbv [ - r wt sz p256 - CPSUtil.Tuple.tl_cps CPSUtil.Tuple.hd_cps - CPSUtil.to_list_cps CPSUtil.to_list'_cps CPSUtil.to_list_cps' CPSUtil.flat_map_cps CPSUtil.fold_right_cps - CPSUtil.map_cps CPSUtil.Tuple.left_append_cps CPSUtil.firstn_cps CPSUtil.combine_cps CPSUtil.on_tuple_cps CPSUtil.update_nth_cps CPSUtil.from_list_default_cps CPSUtil.from_list_default'_cps - fst snd length List.seq List.hd List.app - redc redc_cps redc_loop_cps redc_body_cps - Positional.to_associational_cps - MontgomeryAPI.divmod_cps - MontgomeryAPI.scmul_cps - uweight - MontgomeryAPI.Columns.mul_cps - MontgomeryAPI.Associational.mul_cps - (*Z.of_nat Pos.of_succ_nat Nat.pred - Z.pow Z.pow_pos Z.mul Pos.iter Pos.mul Pos.succ*) - Tuple.hd Tuple.append Tuple.tl Tuple.hd' Tuple.tl' CPSUtil.Tuple.left_tl_cps CPSUtil.Tuple.left_hd_cps CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps - MontgomeryAPI.Columns.from_associational_cps - MontgomeryAPI.Associational.multerm_cps - MontgomeryAPI.Columns.compact_cps - MontgomeryAPI.Columns.compact_step_cps - MontgomeryAPI.Columns.compact_digit_cps - MontgomeryAPI.drop_high_cps - MontgomeryAPI.add_cps - MontgomeryAPI.Columns.add_cps - MontgomeryAPI.Columns.cons_to_nth_cps - Nat.pred - MontgomeryAPI.join0 - MontgomeryAPI.join0_cps CPSUtil.Tuple.left_append_cps - CPSUtil.Tuple.mapi_with_cps - id - Positional.zeros MontgomeryAPI.zero MontgomeryAPI.Columns.nils Tuple.repeat Tuple.append - Positional.place_cps - CPSUtil.Tuple.mapi_with'_cps Tuple.hd Tuple.hd' Tuple.tl Tuple.tl' CPSUtil.Tuple.hd_cps CPSUtil.Tuple.tl_cps fst snd - Z.of_nat fst snd Z.pow Z.pow_pos Pos.of_succ_nat Z.div Z.mul Pos.mul Z.modulo Z.div_eucl Z.pos_div_eucl Z.leb Z.compare Pos.compare_cont Pos.compare Z.pow_pos Pos.iter Z.mul Pos.succ Z.ltb Z.gtb Z.geb Z.div Z.sub Z.pos_sub Z.add Z.opp Z.double - Decidable.dec Decidable.dec_eq_Z Z.eq_dec Z_rec Z_rec Z_rect - Positional.zeros MontgomeryAPI.zero MontgomeryAPI.Columns.nils Tuple.repeat Tuple.append - (* - MontgomeryAPI.Associational.multerm_cps - MontgomeryAPI.Columns.from_associational_cps Positional.place_cps MontgomeryAPI.Columns.cons_to_nth_cps MontgomeryAPI.Columns.nils -Tuple.append -Tuple.from_list Tuple.from_list' -Tuple.from_list_default Tuple.from_list_default' -Tuple.hd -Tuple.repeat -Tuple.tl -Tuple.tuple *) - (* MontgomeryAPI.add_cps MontgomeryAPI.divmod_cps MontgomeryAPI.drop_high_cps MontgomeryAPI.scmul_cps MontgomeryAPI.zero MontgomeryAPI.Columns.mul_cps MontgomeryAPI.Columns.add_cps uweight MontgomeryAPI.T *) - (* - CPSUtil.to_list_cps CPSUtil.to_list'_cps CPSUtil.to_list_cps' -Positional.zeros -Tuple.to_list -Tuple.to_list' -List.hd -List.tl -Nat.max -Positional.to_associational_cps -Z.of_nat *) - ]. - Unset Printing Notations. - - (* cbv -[runtime_add runtime_mul LetIn.Let_In Definitions.Z.add_get_carry_full Definitions.Z.mul_split]. *) - - (* basesystem_partial_evaluation_RHS. *) - *) - reflexivity. -Defined. - - -Definition mulmod_256'' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | forall (A B : Tuple.tuple Z sz), - small (Z.pos r) A -> small (Z.pos r) B -> - let eval := MontgomeryAPI.eval (Z.pos r) in - (small (Z.pos r) (f A B) - /\ (eval B < eval p256 -> 0 <= eval (f A B) < eval p256) - /\ (eval (f A B) mod Z.pos m - = (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z - }. -Proof. - exists (proj1_sig mulmod_256'). - abstract ( - intros; rewrite (proj2_sig mulmod_256'); - split; [ | split ]; - [ apply small_redc with (ri:=r') | apply redc_bound_N with (ri:=r') | apply redc_mod_N ]; - try match goal with - | _ => assumption - | [ |- _ = _ :> Z ] => vm_compute; reflexivity - | _ => reflexivity - | [ |- small (Z.pos r) p256 ] - => hnf; cbv [Tuple.to_list sz p256 r Tuple.to_list' List.In]; intros; destruct_head'_or; - subst; try lia - | [ |- MontgomeryAPI.eval (Z.pos r) p256 <> 0%Z ] - => vm_compute; lia - end - ). -Defined. - -Definition add' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | forall (A B : Tuple.tuple Z sz), - f A B = - (add (r:=r)(R_numlimbs:=sz) p256 A B) - }. -Proof. - eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. - reflexivity. -Defined. - -Definition sub' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | forall (A B : Tuple.tuple Z sz), - f A B = - (sub (r:=r) (R_numlimbs:=sz) p256 A B) - }. -Proof. - eapply (lift2_sig (fun A B c => c = _)); eexists. - cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. - reflexivity. -Defined. - -Definition opp' : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz - | forall (A : Tuple.tuple Z sz), - f A = - (opp (r:=r) (R_numlimbs:=sz) p256 A) - }. -Proof. - eapply (lift1_sig (fun A c => c = _)); eexists. - cbv -[Definitions.Z.add_with_get_carry Definitions.Z.add_with_carry Definitions.Z.sub_with_get_borrow Definitions.Z.sub_with_borrow Definitions.Z.mul_split_at_bitwidth Definitions.Z.zselect runtime_add runtime_mul runtime_and runtime_opp Let_In]. - reflexivity. -Defined. - -Definition nonzero' : { f:Tuple.tuple Z sz -> Z - | forall (A : Tuple.tuple Z sz), - f A = - (nonzero (R_numlimbs:=sz) A) - }. -Proof. - eapply (lift1_sig (fun A c => c = _)); eexists. - cbv -[runtime_lor Let_In]. - reflexivity. -Defined. - -Import ModularArithmetic. - -(*Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - small (Z.pos r) (f A B) - /\ (let eval := MontgomeryAPI.eval (Z.pos r) in - 0 <= eval (f A B) < Z.pos r^Z.of_nat sz - /\ (eval (f A B) mod Z.pos m - = (eval A * eval B * r'^(Z.of_nat sz)) mod Z.pos m))%Z - }. -Proof.*) - -(** TODO: MOVE ME *) -Definition montgomery_to_F (v : Z) : F m - := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F. - - -Definition mulmod_256_ext - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }. -Proof. - exists (proj1_sig mulmod_256''). - abstract ( - split; intros A Asm B Bsm; - pose proof (proj2_sig mulmod_256'' A B Asm Bsm) as H; - cbv zeta in *; - try solve [ destruct_head'_and; assumption ]; - rewrite ModularArithmeticTheorems.F.eq_of_Z_iff in H; - unfold montgomery_to_F; - destruct H as [H1 [H2 H3]]; - rewrite H3; - rewrite <- !ModularArithmeticTheorems.F.of_Z_mul; - f_equal; nia - ). -Defined. - -Definition mulmod_256 - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F }. -Proof. - let v := (eval cbv [proj1_sig mulmod_256_ext mulmod_256'' mulmod_256' lift2_sig] in (proj1_sig mulmod_256_ext)) in - (exists v). - abstract apply (proj2_sig mulmod_256_ext). -Defined. - -Lemma mulmod_256_bounded - : let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval B < eval p256 -> 0 <= eval (proj1_sig mulmod_256 A B) < eval p256)%Z. -Proof. apply (proj2_sig mulmod_256_ext). Qed. - -Local Ltac t_fin := - [ > reflexivity - | repeat match goal with - | _ => assumption - | [ |- _ = _ :> Z ] => vm_compute; reflexivity - | _ => reflexivity - | [ |- small (Z.pos r) p256 ] - => hnf; cbv [Tuple.to_list sz p256 r Tuple.to_list' List.In]; intros; destruct_head'_or; - subst; try lia - | [ |- MontgomeryAPI.eval (Z.pos r) p256 <> 0%Z ] - => vm_compute; lia - | [ |- and _ _ ] => split - | [ |- (0 <= MontgomeryAPI.eval (Z.pos r) _)%Z ] => apply MontgomeryAPI.eval_small - end.. ]. - -Definition add_ext - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> 0 <= eval (f A B) < eval p256)))%Z }. -Proof. - exists (proj1_sig add'). - abstract ( - split; intros; rewrite (proj2_sig add'); - unfold montgomery_to_F; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?ModularArithmeticTheorems.F.of_Z_add; - rewrite <- ?Z.mul_add_distr_r; - [ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; push_Zmod; rewrite eval_add_mod_N; pull_Zmod - | apply add_bound ]; - t_fin - ). -Defined. - -Definition sub_ext - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> 0 <= eval (f A B) < eval p256)))%Z }. -Proof. - exists (proj1_sig sub'). - abstract ( - split; intros; rewrite (proj2_sig sub'); - unfold montgomery_to_F; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?ModularArithmeticTheorems.F.of_Z_sub; - rewrite <- ?Z.mul_sub_distr_r; - [ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; push_Zmod; rewrite eval_sub_mod_N; pull_Zmod - | apply sub_bound ]; - t_fin - ). -Defined. - -Definition opp_ext - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> montgomery_to_F (eval (f A)) - = (F.opp (montgomery_to_F (eval A)))%F)) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> 0 <= eval (f A) < eval p256)))%Z }. -Proof. - exists (proj1_sig opp'). - abstract ( - split; intros; rewrite (proj2_sig opp'); - unfold montgomery_to_F; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul, <- ?F_of_Z_opp; - rewrite <- ?Z.mul_opp_l; - [ rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; push_Zmod; rewrite eval_opp_mod_N; pull_Zmod - | apply opp_bound ]; - t_fin - ). -Defined. - -Definition nonzero_ext - : { f:Tuple.tuple Z sz -> Z - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }. -Proof. - exists (proj1_sig nonzero'). - abstract ( - intros eval A H **; rewrite (proj2_sig nonzero'), (@eval_nonzero r) by (eassumption || reflexivity); - subst eval; - unfold montgomery_to_F, uweight in *; rewrite <- ?ModularArithmeticTheorems.F.of_Z_mul; - rewrite <- ModularArithmeticTheorems.F.eq_of_Z_iff, m_p256; - let H := fresh in - split; intro H; - [ rewrite H; autorewrite with zsimplify_const; reflexivity - | cut ((MontgomeryAPI.eval (Z.pos r) A * (r' ^ Z.of_nat sz * Z.pos r ^ Z.of_nat sz)) mod MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 = 0)%Z; - [ rewrite Z.mul_mod, r'_pow_correct; autorewrite with zsimplify_const; pull_Zmod; [ | vm_compute; congruence ]; - rewrite Z.mod_small; [ trivial | split; try assumption; apply MontgomeryAPI.eval_small; try assumption; lia ] - | rewrite Z.mul_assoc, Z.mul_mod, H by (vm_compute; congruence); autorewrite with zsimplify_const; reflexivity ] ] - ). -Defined. - -Definition add - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)%Z }. -Proof. - let v := (eval cbv [proj1_sig add_ext add' lift2_sig] in (proj1_sig add_ext)) in - (exists v). - abstract apply (proj2_sig add_ext). -Defined. - -Lemma add_bounded - : let eval := MontgomeryAPI.eval (Z.pos r) in - (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> 0 <= eval (proj1_sig add A B) < eval p256))%Z. -Proof. apply (proj2_sig add_ext). Qed. - -Definition sub - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)%Z }. -Proof. - let v := (eval cbv [proj1_sig sub_ext sub' lift2_sig] in (proj1_sig sub_ext)) in - (exists v). - abstract apply (proj2_sig sub_ext). -Defined. - -Lemma sub_bounded - : let eval := MontgomeryAPI.eval (Z.pos r) in - (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> 0 <= eval (proj1_sig sub A B) < eval p256))%Z. -Proof. apply (proj2_sig sub_ext). Qed. - -Definition opp - : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> montgomery_to_F (eval (f A)) - = (F.opp (montgomery_to_F (eval A)))%F)%Z }. -Proof. - let v := (eval cbv [proj1_sig opp_ext opp' lift1_sig] in (proj1_sig opp_ext)) in - (exists v). - abstract apply (proj2_sig opp_ext). -Defined. - -Lemma opp_bounded - : let eval := MontgomeryAPI.eval (Z.pos r) in - (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> 0 <= eval (proj1_sig opp A) < eval p256))%Z. -Proof. apply (proj2_sig opp_ext). Qed. - -Definition nonzero - : { f:Tuple.tuple Z sz -> Z - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }. -Proof. - let v := (eval cbv [proj1_sig nonzero_ext nonzero' lift1_sig] in (proj1_sig nonzero_ext)) in - (exists v). - abstract apply (proj2_sig nonzero_ext). -Defined. - -Local Definition for_assumptions := (mulmod_256, add, sub, opp, nonzero). -Print Assumptions for_assumptions. diff --git a/src/Specific/NISTP256/AMD64/Synthesis.v b/src/Specific/NISTP256/AMD64/Synthesis.v new file mode 100644 index 000000000..ede40bb8c --- /dev/null +++ b/src/Specific/NISTP256/AMD64/Synthesis.v @@ -0,0 +1,11 @@ +Require Import Crypto.Specific.Framework.SynthesisFramework. +Require Import Crypto.Specific.NISTP256.AMD64.CurveParameters. + +Module Import T := MakeSynthesisTactics Curve. + +Module P <: PrePackage. + Definition package : Tag.Context. + Proof. make_Synthesis_package (). Defined. +End P. + +Module Export S := PackageSynthesis Curve P. diff --git a/src/Specific/NISTP256/AMD64/compiler.sh b/src/Specific/NISTP256/AMD64/compiler.sh index 9a89c85f7..518f95765 100755 --- a/src/Specific/NISTP256/AMD64/compiler.sh +++ b/src/Specific/NISTP256/AMD64/compiler.sh @@ -1,4 +1,4 @@ #!/bin/sh set -eu -gcc -fno-peephole2 `#GCC BUG 81300` -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes -Wno-incompatible-pointer-types -fno-strict-aliasing $@ +gcc -fno-peephole2 `#GCC BUG 81300` -march=native -mtune=native -std=gnu11 -O3 -flto -fomit-frame-pointer -fwrapv -Wno-attributes -Wno-incompatible-pointer-types -fno-strict-aliasing "$@" diff --git a/src/Specific/NISTP256/AMD64/feadd.v b/src/Specific/NISTP256/AMD64/feadd.v index 23a38978c..cc1154020 100644 --- a/src/Specific/NISTP256/AMD64/feadd.v +++ b/src/Specific/NISTP256/AMD64/feadd.v @@ -1,125 +1,14 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Local Open Scope Z_scope. - -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Arithmetic.Core. Import B. -Require Crypto.Arithmetic.Saturated.MontgomeryAPI. -Require Import Crypto.Arithmetic.Saturated.UniformWeight. -Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.DestructHead. -Import ListNotations. - -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. - -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Section BoundedField25p5. - Local Coercion Z.of_nat : nat >-> Z. - - Let bounds : Tuple.tuple zrange sz - := Eval compute in - Tuple.repeat {| lower := 0 ; upper := r-1 |} sz. - - Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))). - Let bitwidth := Eval compute in (2^lgbitwidth)%nat. - Let feZ : Type := tuple Z sz. - Let feW : Type := tuple (wordT lgbitwidth) sz. - Let feBW : Type := BoundedWord sz bitwidth bounds. - Let eval : feBW -> Z := - fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x). - Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }. - Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _. - Local Coercion feBW_of_feBW_small : feBW_small >-> feBW. - Let phi : feBW -> F m := - fun x => montgomery_to_F (eval x). - - Local Ltac op_sig_side_conditions_t _ := - try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. - - (* TODO : change this to field once field isomorphism happens *) - Definition add - : { add : feBW_small -> feBW_small -> feBW_small - | forall A B, phi (add A B) = F.add (phi A) (phi B) }. - Proof. - start_preglue. - all:cbv [feBW_of_feBW_small eval]. - do_rewrite_with_sig_by add op_sig_side_conditions_t. - cbv_runtime. - all:fin_preglue. - factor_out_bounds_and_strip_eval add_bounded op_sig_side_conditions_t. - (* jgross start here! *) - Set Ltac Profiling. - (* Set Ltac Profiling. - Print Ltac ReflectiveTactics.solve_side_conditions. - Ltac ReflectiveTactics.solve_side_conditions ::= idtac. - Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - { Time ReflectiveTactics.do_reify. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Require Import CNotations. - Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. } - { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. } - { Time SubstLet.subst_let; clear; vm_compute; reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. } - { Time abstract ReflectiveTactics.handle_bounds_from_hyps. } - { Time ReflectiveTactics.handle_boundedness_side_condition. } *) - Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - Show Ltac Profile. - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s -*) - Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *) - -Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *) +Require Import Crypto.Specific.NISTP256.AMD64.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition add : + { add : feBW_small -> feBW_small -> feBW_small + | forall a b, phiM_small (add a b) = F.add (phiM_small a) (phiM_small b) }. +Proof. + Set Ltac Profiling. + Time synthesize_add (). + Show Ltac Profile. +Time Defined. Print Assumptions add. diff --git a/src/Specific/NISTP256/AMD64/femul.v b/src/Specific/NISTP256/AMD64/femul.v index 5904b1fff..3c6dc4bd2 100644 --- a/src/Specific/NISTP256/AMD64/femul.v +++ b/src/Specific/NISTP256/AMD64/femul.v @@ -1,107 +1,14 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Local Open Scope Z_scope. - -Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Arithmetic.Core. Import B. -Require Crypto.Arithmetic.Saturated.MontgomeryAPI. -Require Import Crypto.Arithmetic.Saturated.UniformWeight. -Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.DestructHead. -Import ListNotations. - -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. - -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Section BoundedField25p5. - Local Coercion Z.of_nat : nat >-> Z. - - Let bounds : Tuple.tuple zrange sz - := Eval compute in - Tuple.repeat {| lower := 0 ; upper := r-1 |} sz. - - Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))). - Let bitwidth := Eval compute in (2^lgbitwidth)%nat. - Let feZ : Type := tuple Z sz. - Let feW : Type := tuple (wordT lgbitwidth) sz. - Let feBW : Type := BoundedWord sz bitwidth bounds. - Let eval : feBW -> Z := - fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x). - Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }. - Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _. - Local Coercion feBW_of_feBW_small : feBW_small >-> feBW. - Let phi : feBW -> F m := - fun x => montgomery_to_F (eval x). - - Local Ltac op_sig_side_conditions_t _ := - try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. - - (* TODO : change this to field once field isomorphism happens *) - Definition mul - : { mul : feBW_small -> feBW_small -> feBW_small - | forall A B, phi (mul A B) = F.mul (phi A) (phi B) }. - Proof. - start_preglue. - all:cbv [feBW_of_feBW_small eval]. - do_rewrite_with_sig_by mulmod_256 op_sig_side_conditions_t. - cbv_runtime. - all:fin_preglue. - factor_out_bounds_and_strip_eval mulmod_256_bounded op_sig_side_conditions_t. - (* jgross start here! *) - Set Ltac Profiling. - Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - Show Ltac Profile. - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s -*) - Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *) - -Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *) +Require Import Crypto.Specific.NISTP256.AMD64.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition mul : + { mul : feBW_small -> feBW_small -> feBW_small + | forall a b, phiM_small (mul a b) = F.mul (phiM_small a) (phiM_small b) }. +Proof. + Set Ltac Profiling. + Time synthesize_mul (). + Show Ltac Profile. +Time Defined. Print Assumptions mul. diff --git a/src/Specific/NISTP256/AMD64/fenz.v b/src/Specific/NISTP256/AMD64/fenz.v index 13dc4478f..8b61924a7 100644 --- a/src/Specific/NISTP256/AMD64/fenz.v +++ b/src/Specific/NISTP256/AMD64/fenz.v @@ -1,114 +1,16 @@ Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Local Open Scope Z_scope. - -Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Arithmetic.Core. Import B. -Require Crypto.Arithmetic.Saturated.MontgomeryAPI. -Require Import Crypto.Arithmetic.Saturated.UniformWeight. -Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.DestructHead. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Import ListNotations. - -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. - -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Section BoundedField25p5. - Local Coercion Z.of_nat : nat >-> Z. - - Let bound1 : zrange - := Eval compute in - {| lower := 0 ; upper := r-1 |}. - Let bounds : Tuple.tuple zrange sz - := Eval compute in - Tuple.repeat bound1 sz. - - Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))). - Let bitwidth := Eval compute in (2^lgbitwidth)%nat. - Let feZ : Type := tuple Z sz. - Let feW : Type := tuple (wordT lgbitwidth) sz. - Let feBW : Type := BoundedWord sz bitwidth bounds. - Let eval : feBW -> Z := - fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x). - Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }. - Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _. - Local Coercion feBW_of_feBW_small : feBW_small >-> feBW. - Let phi : feBW -> F m := - fun x => montgomery_to_F (eval x). - - Local Ltac op_sig_side_conditions_t _ := - try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. - - (* TODO : change this to field once field isomorphism happens *) - Definition nonzero - : { nonzero : feBW_small -> BoundedWord 1 bitwidth bound1 - | forall A, (BoundedWordToZ _ _ _ (nonzero A) =? 0) = (if Decidable.dec (phi A = F.of_Z m 0) then true else false) }. - Proof. - apply_lift_sig; intros; eexists_sig_etransitivity. - all:cbv [feBW_of_feBW_small phi eval]. - refine (_ : (if Decidable.dec (_ = 0) then true else false) = _). - lazymatch goal with - | [ |- (if Decidable.dec ?x then _ else _) = (if Decidable.dec ?y then _ else _) ] - => cut (x <-> y); - [ destruct (Decidable.dec x), (Decidable.dec y); try reflexivity; intros [? ?]; - generalize dependent x; generalize dependent y; solve [ intuition congruence ] - | ] - end. - etransitivity; [ | eapply (proj2_sig nonzero) ]; - [ | solve [ op_sig_side_conditions_t () ].. ]. - reflexivity. - let decP := lazymatch goal with |- { c | _ = if Decidable.dec (?decP = 0) then _ else _ } => decP end in - apply (@proj2_sig_map _ (fun c => BoundedWordToZ 1 _ _ c = decP) _). - { intros a' H'; rewrite H'. - let H := fresh in - lazymatch goal with |- context[Decidable.dec ?x] => destruct (Decidable.dec x) as [H|H]; try rewrite H end. - { reflexivity. } - { let H := fresh in - lazymatch goal with |- context[?x =? 0] => destruct (x =? 0) eqn:? end; - try reflexivity. - Z.ltb_to_lt; congruence. } } - eexists_sig_etransitivity. - do_set_sig nonzero. - cbv_runtime. - reflexivity. - sig_dlet_in_rhs_to_context. - cbv [proj1_sig]. - match goal with - | [ H : feBW_small |- _ ] => destruct H as [? _] - end. - (* jgross start here! *) - Set Ltac Profiling. - (* Set Ltac Profiling. - Print Ltac ReflectiveTactics.solve_side_conditions. - Ltac ReflectiveTactics.solve_side_conditions ::= idtac. - Time refine_reflectively128_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - { Time ReflectiveTactics.do_reify. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Require Import CNotations. - Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. } - { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. } - { Time SubstLet.subst_let; clear; vm_compute; reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. } - { Time abstract ReflectiveTactics.handle_bounds_from_hyps. } - { Time ReflectiveTactics.handle_boundedness_side_condition. } *) - Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - Show Ltac Profile. - Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *) +Require Import Crypto.Specific.NISTP256.AMD64.Synthesis. +Local Open Scope Z_scope. -Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *) +(* TODO : change this to field once field isomorphism happens *) +Definition nonzero : + { nonzero : feBW_small -> BoundedWord.BoundedWord 1 adjusted_bitwidth bound1 + | forall a, (BoundedWord.BoundedWordToZ _ _ _ (nonzero a) =? 0) = (if Decidable.dec (phiM_small a = F.of_Z m 0) then true else false) }. +Proof. + Set Ltac Profiling. + Time synthesize_nonzero (). + Show Ltac Profile. +Time Defined. Print Assumptions nonzero. diff --git a/src/Specific/NISTP256/AMD64/fenzDisplay.log b/src/Specific/NISTP256/AMD64/fenzDisplay.log index 65afbc2d6..241c31016 100644 --- a/src/Specific/NISTP256/AMD64/fenzDisplay.log +++ b/src/Specific/NISTP256/AMD64/fenzDisplay.log @@ -7,4 +7,16 @@ Interp-η uint64_t x9 = (x2 | x8); return x9) x - : word64 * word64 * word64 * word64 → ReturnType uint64_t + : word64 * word64 * word64 * word64 → ReturnType (Tbase match (if match match (let (lower, _) := Synthesis.P.bound1 in + lower) with + | 0%Z => Eq + | Z.pos _ => Lt + | Z.neg _ => Gt + end with + | Eq => true + | Lt => true + | Gt => false + end then Some 6 else None) with + | Some lgsz => Syntax.TWord lgsz + | None => Syntax.TZ + end) diff --git a/src/Specific/NISTP256/AMD64/feopp.v b/src/Specific/NISTP256/AMD64/feopp.v index d57948035..e5483c736 100644 --- a/src/Specific/NISTP256/AMD64/feopp.v +++ b/src/Specific/NISTP256/AMD64/feopp.v @@ -1,126 +1,14 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Local Open Scope Z_scope. - -Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Arithmetic.Core. Import B. -Require Crypto.Arithmetic.Saturated.MontgomeryAPI. -Require Import Crypto.Arithmetic.Saturated.UniformWeight. -Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.DestructHead. -Import ListNotations. - -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. - -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Section BoundedField25p5. - Local Coercion Z.of_nat : nat >-> Z. - - Let bounds : Tuple.tuple zrange sz - := Eval compute in - Tuple.repeat {| lower := 0 ; upper := r-1 |} sz. - - Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))). - Let bitwidth := Eval compute in (2^lgbitwidth)%nat. - Let feZ : Type := tuple Z sz. - Let feW : Type := tuple (wordT lgbitwidth) sz. - Let feBW : Type := BoundedWord sz bitwidth bounds. - Let eval : feBW -> Z := - fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x). - Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }. - Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _. - Local Coercion feBW_of_feBW_small : feBW_small >-> feBW. - Let phi : feBW -> F m := - fun x => montgomery_to_F (eval x). - - Local Ltac op_sig_side_conditions_t _ := - try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. - - (* TODO : change this to field once field isomorphism happens *) - Definition opp - : { opp : feBW_small -> feBW_small - | forall A, phi (opp A) = F.opp (phi A) }. - Proof. - start_preglue. - all:cbv [feBW_of_feBW_small eval]. - do_rewrite_with_sig_by opp op_sig_side_conditions_t. - cbv_runtime. - all:fin_preglue. - factor_out_bounds_and_strip_eval opp_bounded op_sig_side_conditions_t. - (* jgross start here! *) - Set Ltac Profiling. - (* Set Ltac Profiling. - Print Ltac ReflectiveTactics.solve_side_conditions. - Ltac ReflectiveTactics.solve_side_conditions ::= idtac. - Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - { Time ReflectiveTactics.do_reify. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Require Import CNotations. - Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. } - { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. } - { Time SubstLet.subst_let; clear; vm_compute; reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. } - { Time abstract ReflectiveTactics.handle_bounds_from_hyps. } - { Time ReflectiveTactics.handle_boundedness_side_condition. } *) - Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - Show Ltac Profile. - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s -*) - Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *) - -Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *) +Require Import Crypto.Specific.NISTP256.AMD64.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition opp : + { opp : feBW_small -> feBW_small + | forall a, phiM_small (opp a) = F.opp (phiM_small a) }. +Proof. + Set Ltac Profiling. + Time synthesize_opp (). + Show Ltac Profile. +Time Defined. Print Assumptions opp. diff --git a/src/Specific/NISTP256/AMD64/fesub.v b/src/Specific/NISTP256/AMD64/fesub.v index 4098ffcfc..680bf71c8 100644 --- a/src/Specific/NISTP256/AMD64/fesub.v +++ b/src/Specific/NISTP256/AMD64/fesub.v @@ -1,126 +1,14 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Local Open Scope Z_scope. - -Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Arithmetic.Core. Import B. -Require Crypto.Arithmetic.Saturated.MontgomeryAPI. -Require Import Crypto.Arithmetic.Saturated.UniformWeight. -Require Import Crypto.Specific.NISTP256.AMD64.MontgomeryP256. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.DestructHead. -Import ListNotations. - -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. - -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Section BoundedField25p5. - Local Coercion Z.of_nat : nat >-> Z. - - Let bounds : Tuple.tuple zrange sz - := Eval compute in - Tuple.repeat {| lower := 0 ; upper := r-1 |} sz. - - Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (Z.log2_up r))). - Let bitwidth := Eval compute in (2^lgbitwidth)%nat. - Let feZ : Type := tuple Z sz. - Let feW : Type := tuple (wordT lgbitwidth) sz. - Let feBW : Type := BoundedWord sz bitwidth bounds. - Let eval : feBW -> Z := - fun x => MontgomeryAPI.eval (Z.pos r) (BoundedWordToZ _ _ _ x). - Let feBW_small : Type := { v : feBW | eval v < MontgomeryAPI.eval (n:=sz) (Z.pos r) p256 }. - Let feBW_of_feBW_small : feBW_small -> feBW := @proj1_sig _ _. - Local Coercion feBW_of_feBW_small : feBW_small >-> feBW. - Let phi : feBW -> F m := - fun x => montgomery_to_F (eval x). - - Local Ltac op_sig_side_conditions_t _ := - try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. - - (* TODO : change this to field once field isomorphism happens *) - Definition sub - : { sub : feBW_small -> feBW_small -> feBW_small - | forall A B, phi (sub A B) = F.sub (phi A) (phi B) }. - Proof. - start_preglue. - all:cbv [feBW_of_feBW_small eval]. - do_rewrite_with_sig_by sub op_sig_side_conditions_t. - cbv_runtime. - all:fin_preglue. - factor_out_bounds_and_strip_eval sub_bounded op_sig_side_conditions_t. - (* jgross start here! *) - Set Ltac Profiling. - (* Set Ltac Profiling. - Print Ltac ReflectiveTactics.solve_side_conditions. - Ltac ReflectiveTactics.solve_side_conditions ::= idtac. - Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - { Time ReflectiveTactics.do_reify. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Require Import CNotations. - Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. } - { Time SubstLet.subst_let; clear; abstract vm_cast_no_check eq_refl. } - { Time SubstLet.subst_let; clear; vm_compute; reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. } - { Time abstract ReflectiveTactics.handle_bounds_from_hyps. } - { Time ReflectiveTactics.handle_boundedness_side_condition. } *) - Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) - Show Ltac Profile. - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s -*) - Time Defined. (* Finished transaction in 21.291 secs (21.231u,0.032s) (successful) *) - -Time End BoundedField25p5. (* Finished transaction in 14.666 secs (14.556u,0.111s) (successful) *) +Require Import Crypto.Specific.NISTP256.AMD64.Synthesis. + +(* TODO : change this to field once field isomorphism happens *) +Definition sub : + { sub : feBW_small -> feBW_small -> feBW_small + | forall a b, phiM_small (sub a b) = F.sub (phiM_small a) (phiM_small b) }. +Proof. + Set Ltac Profiling. + Time synthesize_sub (). + Show Ltac Profile. +Time Defined. Print Assumptions sub. diff --git a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v index 9fe08de2c..cc8393d9b 100644 --- a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v +++ b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v @@ -17,6 +17,7 @@ Module Curve <: CurveParameters. Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) Definition goldilocks : bool := true. + Definition montgomery : bool := false. Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) := None. diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v index 6324acfca..55853a9c1 100644 --- a/src/Specific/X25519/C32/CurveParameters.v +++ b/src/Specific/X25519/C32/CurveParameters.v @@ -17,6 +17,7 @@ Module Curve <: CurveParameters. Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) Definition goldilocks : bool := false. + Definition montgomery : bool := false. Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) := Some (fun a b => diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v index 78db9dd8e..6d9666194 100644 --- a/src/Specific/X25519/C64/CurveParameters.v +++ b/src/Specific/X25519/C64/CurveParameters.v @@ -17,6 +17,7 @@ Module Curve <: CurveParameters. Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) Definition goldilocks : bool := false. + Definition montgomery : bool := false. Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) := Some (fun a b => diff --git a/src/Specific/X2555/C128/CurveParameters.v b/src/Specific/X2555/C128/CurveParameters.v index bb4384cc2..46b56378b 100644 --- a/src/Specific/X2555/C128/CurveParameters.v +++ b/src/Specific/X2555/C128/CurveParameters.v @@ -17,6 +17,7 @@ Module Curve <: CurveParameters. Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) Definition goldilocks : bool := false. + Definition montgomery : bool := false. Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) := None. |