diff options
40 files changed, 1879 insertions, 981 deletions
diff --git a/_CoqProject b/_CoqProject index e2619d54b..5bcc76f6c 100644 --- a/_CoqProject +++ b/_CoqProject @@ -239,14 +239,27 @@ 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/ArithmeticSynthesisFramework.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/LadderstepSynthesisFramework.v +src/Specific/Framework/Packages.v src/Specific/Framework/ReificationTypes.v +src/Specific/Framework/ReificationTypesPackage.v src/Specific/Framework/SynthesisFramework.v +src/Specific/Framework/ArithmeticSynthesis/Base.v +src/Specific/Framework/ArithmeticSynthesis/BasePackage.v +src/Specific/Framework/ArithmeticSynthesis/Defaults.v +src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v +src/Specific/Framework/ArithmeticSynthesis/Freeze.v +src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v +src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v +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/SquareFromMul.v src/Specific/NISTP256/AMD64/MontgomeryP256.v src/Specific/NISTP256/AMD64/feadd.v src/Specific/NISTP256/AMD64/feaddDisplay.v diff --git a/src/Specific/Framework/ArithmeticSynthesis/Base.v b/src/Specific/Framework/ArithmeticSynthesis/Base.v new file mode 100644 index 000000000..092c08705 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/Base.v @@ -0,0 +1,125 @@ +Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. +Require Import Coq.Lists.List. Import ListNotations. +Require Import Crypto.Arithmetic.Core. Import B. +Require Import Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics. +Require Import Crypto.Util.QUtil. +Require Import Crypto.Util.Decidable. +Require Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics.CacheTerm. + + (* emacs for adjusting definitions *) + (* Query replace regexp (default Definition \([a-zA-Z_0-9]+\) : \([A-Za-z0-9_]+\) := P.compute \(.*\)\.\(.*\) -> Ltac pose_\1 \1 :=\4^J cache_term_with_type_by^J \2^J ltac:(let v := P.do_compute \3 in exact v)^J \1.): *) + (* Query replace regexp (default Definition \([a-zA-Z_0-9]+\) : \([A-Za-z0-9_]+\) := P.compute \(.*\)\.\(.*\) -> Ltac pose_\1 \1 :=\4^J cache_term_with_type_by^J \2^J ltac:(let v := P.do_compute \3 in exact v)^J \1.): *) + (* Query replace regexp (default Definition \([a-zA-Z_0-9]+\) : \([A-Za-z0-9_ \.]*\) := P.compute \(.*\)\.\(.*\) -> Ltac pose_\1 \1 :=\4^J cache_term_with_type_by^J (\2)^J ltac:(let v := P.do_compute \3 in exact v)^J \1.): *) + (* Query replace regexp (default Definition \([a-zA-Z_0-9]+\) := P.compute \(.*\)\.\(.*\) -> Ltac pose_\1 \1 :=\3^J let v := P.do_compute \2 in cache_term v \1.): *) + +Ltac pose_r bitwidth r := + cache_term_with_type_by + positive + ltac:(let v := (eval vm_compute in (Z.to_pos (2^bitwidth))) in exact v) + r. + +Ltac pose_m s c m := (* modulus *) + let v := (eval vm_compute in (Z.to_pos (s - Associational.eval c))) in + cache_term v m. + +Section wt. + Import QArith Qround. + Local Coercion QArith_base.inject_Z : Z >-> Q. + Local Coercion Z.of_nat : nat >-> Z. + Local Coercion Z.pos : positive >-> Z. + Definition wt_gen (m : positive) (sz : nat) (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i). +End wt. +Ltac pose_wt m sz wt := + let v := (eval cbv [wt_gen] in (wt_gen m sz)) in + cache_term v wt. + +Ltac pose_sz2 sz sz2 := + let v := (eval vm_compute in ((sz * 2) - 1)%nat) in + cache_term v sz2. + +Ltac pose_half_sz sz half_sz := + let v := (eval compute in (sz / 2)%nat) in + cache_term v half_sz. + +Ltac pose_half_sz_nonzero half_sz half_sz_nonzero := + cache_proof_with_type_by + (half_sz <> 0%nat) + ltac:(cbv; congruence) + half_sz_nonzero. + +Ltac pose_m_enc sz s c wt m_enc := + let v := (eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c))) in + let v := (eval compute in v) in (* compute away the type arguments *) + cache_term v m_enc. +Ltac pose_coef sz wt m_enc coef_div_modulus coef := (* subtraction coefficient *) + let v := (eval vm_compute in + ((fix addm (acc: Z^sz) (ctr : nat) : Z^sz := + match ctr with + | O => acc + | S n => addm (Positional.add_cps wt acc m_enc id) n + end) (Positional.zeros sz) coef_div_modulus)) in + cache_term v coef. + +Ltac pose_coef_mod sz wt m coef coef_mod := + cache_term_with_type_by + (mod_eq m (Positional.eval (n:=sz) wt coef) 0) + ltac:(exact eq_refl) + coef_mod. +Ltac pose_sz_nonzero sz sz_nonzero := + cache_proof_with_type_by + (sz <> 0%nat) + ltac:(vm_decide_no_check) + sz_nonzero. +Ltac pose_wt_nonzero wt wt_nonzero := + cache_proof_with_type_by + (forall i, wt i <> 0) + ltac:(eapply pow_ceil_mul_nat_nonzero; vm_decide_no_check) + wt_nonzero. +Ltac pose_wt_nonneg wt wt_nonneg := + cache_proof_with_type_by + (forall i, 0 <= wt i) + ltac:(apply pow_ceil_mul_nat_nonneg; vm_decide_no_check) + wt_nonneg. +Ltac pose_wt_divides wt wt_divides := + cache_proof_with_type_by + (forall i, wt (S i) / wt i > 0) + ltac:(apply pow_ceil_mul_nat_divide; vm_decide_no_check) + wt_divides. +Ltac pose_wt_divides' wt wt_divides wt_divides' := + cache_proof_with_type_by + (forall i, wt (S i) / wt i <> 0) + ltac:(symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides) + wt_divides'. +Ltac helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chain := + cache_term_with_type_by + (forall i (H:In i carry_chain), wt (S i) / wt i <> 0) + ltac:(let i := fresh "i" in intros i ?; exact (wt_divides' i)) + wt_divides_chain. +Ltac internal_pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains := + lazymatch carry_chains with + | ?carry_chain :: nil + => helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chains + | ?carry_chain :: ?carry_chains + => let wt_divides_chains := fresh wt_divides_chains in + let wt_divides_chain := fresh wt_divides_chains in + let wt_divides_chain := helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chain in + let wt_divides_chains := internal_pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains in + constr:((wt_divides_chain, wt_divides_chains)) + end. +Ltac pose_wt_divides_chains wt carry_chains wt_divides' wt_divides_chains := + let carry_chains := (eval cbv delta [carry_chains] in carry_chains) in + internal_pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains. + +Ltac pose_wt_pos wt wt_pos := + cache_proof_with_type_by + (forall i, wt i > 0) + ltac:(eapply pow_ceil_mul_nat_pos; vm_decide_no_check) + wt_pos. + +Ltac pose_wt_multiples wt wt_multiples := + cache_proof_with_type_by + (forall i, wt (S i) mod (wt i) = 0) + ltac:(apply pow_ceil_mul_nat_multiples; vm_decide_no_check) + wt_multiples. diff --git a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v new file mode 100644 index 000000000..457c9dc11 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v @@ -0,0 +1,185 @@ +(* This file is autogenerated from Base.v by remake_packages.py *) +Require Import Crypto.Specific.Framework.CurveParametersPackage. +Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Base. +Require Import Crypto.Specific.Framework.Packages. +Require Import Crypto.Util.TagList. + +Module TAG. + Inductive tags := r | m | wt | sz2 | half_sz | half_sz_nonzero | m_enc | coef | coef_mod | sz_nonzero | wt_nonzero | wt_nonneg | wt_divides | wt_divides' | wt_divides_chains | wt_pos | wt_multiples. +End TAG. + +Ltac add_r pkg := + let bitwidth := Tag.get pkg TAG.bitwidth in + let r := fresh "r" in + let r := pose_r bitwidth r in + Tag.update pkg TAG.r r. + +Ltac add_m pkg := + let s := Tag.get pkg TAG.s in + let c := Tag.get pkg TAG.c in + let m := fresh "m" in + let m := pose_m s c m in + Tag.update pkg TAG.m m. + +Ltac add_wt pkg := + let m := Tag.get pkg TAG.m in + let sz := Tag.get pkg TAG.sz in + let wt := fresh "wt" in + let wt := pose_wt m sz wt in + Tag.update pkg TAG.wt wt. + +Ltac add_sz2 pkg := + let sz := Tag.get pkg TAG.sz in + let sz2 := fresh "sz2" in + let sz2 := pose_sz2 sz sz2 in + Tag.update pkg TAG.sz2 sz2. + +Ltac add_half_sz pkg := + let sz := Tag.get pkg TAG.sz in + let half_sz := fresh "half_sz" in + let half_sz := pose_half_sz sz half_sz in + Tag.update pkg TAG.half_sz half_sz. + +Ltac add_half_sz_nonzero pkg := + let half_sz := Tag.get pkg TAG.half_sz in + let half_sz_nonzero := fresh "half_sz_nonzero" in + let half_sz_nonzero := pose_half_sz_nonzero half_sz half_sz_nonzero in + Tag.update pkg TAG.half_sz_nonzero half_sz_nonzero. + +Ltac add_m_enc pkg := + let sz := Tag.get pkg TAG.sz in + let s := Tag.get pkg TAG.s in + let c := Tag.get pkg TAG.c in + let wt := Tag.get pkg TAG.wt in + let m_enc := fresh "m_enc" in + let m_enc := pose_m_enc sz s c wt m_enc in + Tag.update pkg TAG.m_enc m_enc. + +Ltac add_coef pkg := + let sz := Tag.get pkg TAG.sz in + let wt := Tag.get pkg TAG.wt in + let m_enc := Tag.get pkg TAG.m_enc in + let coef_div_modulus := Tag.get pkg TAG.coef_div_modulus in + let coef := fresh "coef" in + let coef := pose_coef sz wt m_enc coef_div_modulus coef in + Tag.update pkg TAG.coef coef. + +Ltac add_coef_mod pkg := + let sz := Tag.get pkg TAG.sz in + let wt := Tag.get pkg TAG.wt in + let m := Tag.get pkg TAG.m in + let coef := Tag.get pkg TAG.coef in + let coef_mod := fresh "coef_mod" in + let coef_mod := pose_coef_mod sz wt m coef coef_mod in + Tag.update pkg TAG.coef_mod coef_mod. + +Ltac add_sz_nonzero pkg := + let sz := Tag.get pkg TAG.sz in + let sz_nonzero := fresh "sz_nonzero" in + let sz_nonzero := pose_sz_nonzero sz sz_nonzero in + Tag.update pkg TAG.sz_nonzero sz_nonzero. + +Ltac add_wt_nonzero pkg := + let wt := Tag.get pkg TAG.wt in + let wt_nonzero := fresh "wt_nonzero" in + let wt_nonzero := pose_wt_nonzero wt wt_nonzero in + Tag.update pkg TAG.wt_nonzero wt_nonzero. + +Ltac add_wt_nonneg pkg := + let wt := Tag.get pkg TAG.wt in + let wt_nonneg := fresh "wt_nonneg" in + let wt_nonneg := pose_wt_nonneg wt wt_nonneg in + Tag.update pkg TAG.wt_nonneg wt_nonneg. + +Ltac add_wt_divides pkg := + let wt := Tag.get pkg TAG.wt in + let wt_divides := fresh "wt_divides" in + let wt_divides := pose_wt_divides wt wt_divides in + Tag.update pkg TAG.wt_divides wt_divides. + +Ltac add_wt_divides' pkg := + let wt := Tag.get pkg TAG.wt in + let wt_divides := Tag.get pkg TAG.wt_divides in + let wt_divides' := fresh "wt_divides'" in + let wt_divides' := pose_wt_divides' wt wt_divides wt_divides' in + Tag.update pkg TAG.wt_divides' wt_divides'. + +Ltac add_wt_divides_chains pkg := + let wt := Tag.get pkg TAG.wt in + let carry_chains := Tag.get pkg TAG.carry_chains in + let wt_divides' := Tag.get pkg TAG.wt_divides' in + let wt_divides_chains := fresh "wt_divides_chains" in + let wt_divides_chains := pose_wt_divides_chains wt carry_chains wt_divides' wt_divides_chains in + Tag.update pkg TAG.wt_divides_chains wt_divides_chains. + +Ltac add_wt_pos pkg := + let wt := Tag.get pkg TAG.wt in + let wt_pos := fresh "wt_pos" in + let wt_pos := pose_wt_pos wt wt_pos in + Tag.update pkg TAG.wt_pos wt_pos. + +Ltac add_wt_multiples pkg := + let wt := Tag.get pkg TAG.wt in + let wt_multiples := fresh "wt_multiples" in + let wt_multiples := pose_wt_multiples wt wt_multiples in + Tag.update pkg TAG.wt_multiples wt_multiples. + +Ltac add_Base_package pkg := + let pkg := add_r pkg in + let pkg := add_m pkg in + let pkg := add_wt pkg in + let pkg := add_sz2 pkg in + let pkg := add_half_sz pkg in + let pkg := add_half_sz_nonzero pkg in + let pkg := add_m_enc pkg in + let pkg := add_coef pkg in + let pkg := add_coef_mod pkg in + let pkg := add_sz_nonzero pkg in + let pkg := add_wt_nonzero pkg in + let pkg := add_wt_nonneg pkg in + let pkg := add_wt_divides pkg in + let pkg := add_wt_divides' pkg in + let pkg := add_wt_divides_chains pkg in + let pkg := add_wt_pos pkg in + let pkg := add_wt_multiples pkg in + Tag.strip_local pkg. + + +Module MakeBasePackage (PKG : PrePackage). + Module Import MakeBasePackageInternal := MakePackageBase PKG. + + Ltac get_r _ := get TAG.r. + Notation r := (ltac:(let v := get_r () in exact v)) (only parsing). + Ltac get_m _ := get TAG.m. + Notation m := (ltac:(let v := get_m () in exact v)) (only parsing). + Ltac get_wt _ := get TAG.wt. + Notation wt := (ltac:(let v := get_wt () in exact v)) (only parsing). + Ltac get_sz2 _ := get TAG.sz2. + Notation sz2 := (ltac:(let v := get_sz2 () in exact v)) (only parsing). + Ltac get_half_sz _ := get TAG.half_sz. + Notation half_sz := (ltac:(let v := get_half_sz () in exact v)) (only parsing). + Ltac get_half_sz_nonzero _ := get TAG.half_sz_nonzero. + Notation half_sz_nonzero := (ltac:(let v := get_half_sz_nonzero () in exact v)) (only parsing). + Ltac get_m_enc _ := get TAG.m_enc. + Notation m_enc := (ltac:(let v := get_m_enc () in exact v)) (only parsing). + Ltac get_coef _ := get TAG.coef. + Notation coef := (ltac:(let v := get_coef () in exact v)) (only parsing). + Ltac get_coef_mod _ := get TAG.coef_mod. + Notation coef_mod := (ltac:(let v := get_coef_mod () in exact v)) (only parsing). + Ltac get_sz_nonzero _ := get TAG.sz_nonzero. + Notation sz_nonzero := (ltac:(let v := get_sz_nonzero () in exact v)) (only parsing). + Ltac get_wt_nonzero _ := get TAG.wt_nonzero. + Notation wt_nonzero := (ltac:(let v := get_wt_nonzero () in exact v)) (only parsing). + Ltac get_wt_nonneg _ := get TAG.wt_nonneg. + Notation wt_nonneg := (ltac:(let v := get_wt_nonneg () in exact v)) (only parsing). + Ltac get_wt_divides _ := get TAG.wt_divides. + Notation wt_divides := (ltac:(let v := get_wt_divides () in exact v)) (only parsing). + Ltac get_wt_divides' _ := get TAG.wt_divides'. + Notation wt_divides' := (ltac:(let v := get_wt_divides' () in exact v)) (only parsing). + Ltac get_wt_divides_chains _ := get TAG.wt_divides_chains. + Notation wt_divides_chains := (ltac:(let v := get_wt_divides_chains () in exact v)) (only parsing). + Ltac get_wt_pos _ := get TAG.wt_pos. + Notation wt_pos := (ltac:(let v := get_wt_pos () in exact v)) (only parsing). + Ltac get_wt_multiples _ := get TAG.wt_multiples. + Notation wt_multiples := (ltac:(let v := get_wt_multiples () in exact v)) (only parsing). +End MakeBasePackage. diff --git a/src/Specific/Framework/ArithmeticSynthesis/Defaults.v b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v new file mode 100644 index 000000000..db209c9f1 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v @@ -0,0 +1,187 @@ +Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. +Require Import Coq.Lists.List. Import ListNotations. +Require Import Crypto.Arithmetic.Core. Import B. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.PoseTermWithName. +Require Import Crypto.Util.Tactics.CacheTerm. +Require Crypto.Util.Tuple. + +Local Notation tuple := Tuple.tuple. +Local Open Scope list_scope. +Local Open Scope Z_scope. +Local Infix "^" := tuple : type_scope. + +Module Export Exports. + Export Coq.setoid_ring.ZArithRing. +End Exports. + +Ltac solve_constant_sig := + idtac; + lazymatch goal with + | [ |- { c : Z^?sz | Positional.Fdecode (m:=?M) ?wt c = ?v } ] + => let t := (eval vm_compute in + (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt (F.to_Z (m:=M) v))) in + (exists t; vm_decide) + end. + +(* Performs a full carry loop (as specified by carry_chain) *) +Ltac pose_carry_sig sz m wt s c carry_chains wt_nonzero wt_divides_chains carry_sig := + cache_term_with_type_by + {carry : (Z^sz -> Z^sz)%type | + forall a : Z^sz, + let eval := Positional.Fdecode (m := m) wt in + eval (carry a) = eval a} + ltac:(idtac; + let a := fresh "a" in + eexists; cbv beta zeta; intros a; + pose proof wt_nonzero; pose proof div_mod; + pose_proof_tuple wt_divides_chains; + let x := make_chained_carries_cps sz wt s c a carry_chains in + solve_op_F wt x; reflexivity) + carry_sig. + +Ltac pose_zero_sig sz m wt zero_sig := + cache_term_with_type_by + { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 0%F} + solve_constant_sig + zero_sig. + +Ltac pose_one_sig sz m wt one_sig := + cache_term_with_type_by + { one : Z^sz | Positional.Fdecode (m:=m) wt one = 1%F} + solve_constant_sig + one_sig. + +Ltac pose_a24_sig sz m wt a24 a24_sig := + cache_term_with_type_by + { a24t : Z^sz | Positional.Fdecode (m:=m) wt a24t = F.of_Z m a24 } + solve_constant_sig + a24_sig. + +Ltac pose_add_sig sz m wt wt_nonzero add_sig := + cache_term_with_type_by + { add : (Z^sz -> Z^sz -> Z^sz)%type | + forall a b : Z^sz, + let eval := Positional.Fdecode (m:=m) wt in + eval (add a b) = (eval a + eval b)%F } + ltac:(idtac; + let a := fresh "a" in + let b := fresh "b" in + eexists; cbv beta zeta; intros a b; + pose proof wt_nonzero; + let x := constr:( + Positional.add_cps (n := sz) wt a b id) in + solve_op_F wt x; reflexivity) + add_sig. + +Ltac pose_sub_sig sz m wt wt_nonzero coef sub_sig := + cache_term_with_type_by + {sub : (Z^sz -> Z^sz -> Z^sz)%type | + forall a b : Z^sz, + let eval := Positional.Fdecode (m:=m) wt in + eval (sub a b) = (eval a - eval b)%F} + ltac:(idtac; + let a := fresh "a" in + let b := fresh "b" in + eexists; cbv beta zeta; intros a b; + pose proof wt_nonzero; + let x := constr:( + Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in + solve_op_F wt x; reflexivity) + sub_sig. + +Ltac pose_opp_sig sz m wt wt_nonzero coef opp_sig := + cache_term_with_type_by + {opp : (Z^sz -> Z^sz)%type | + forall a : Z^sz, + let eval := Positional.Fdecode (m := m) wt in + eval (opp a) = F.opp (eval a)} + ltac:(idtac; + let a := fresh in + eexists; cbv beta zeta; intros a; + pose proof wt_nonzero; + let x := constr:( + Positional.opp_cps (n:=sz) (coef := coef) wt a id) in + solve_op_F wt x; reflexivity) + opp_sig. + + +Ltac pose_mul_sig P_default_mul P_extra_prove_mul_eq sz m wt s c sz2 wt_nonzero mul_sig := + cache_term_with_type_by + {mul : (Z^sz -> Z^sz -> Z^sz)%type | + forall a b : Z^sz, + let eval := Positional.Fdecode (m := m) wt in + eval (mul a b) = (eval a * eval b)%F} + ltac:(idtac; + let a := fresh "a" in + let b := fresh "b" in + eexists; cbv beta zeta; intros a b; + pose proof wt_nonzero; + let x := constr:( + Positional.mul_cps (n:=sz) (m:=sz2) wt a b + (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in + solve_op_F wt x; + P_default_mul (); + P_extra_prove_mul_eq (); + break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring) + mul_sig. + + +Ltac pose_square_sig P_default_square P_extra_prove_square_eq sz m wt s c sz2 wt_nonzero square_sig := + cache_term_with_type_by + {square : (Z^sz -> Z^sz)%type | + forall a : Z^sz, + let eval := Positional.Fdecode (m := m) wt in + eval (square a) = (eval a * eval a)%F} + ltac:(idtac; + let a := fresh "a" in + eexists; cbv beta zeta; intros a; + pose proof wt_nonzero; + let x := constr:( + Positional.mul_cps (n:=sz) (m:=sz2) wt a a + (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in + solve_op_F wt x; + P_default_square (); + P_extra_prove_square_eq (); + break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring) + square_sig. + +Ltac pose_ring sz m wt wt_divides' sz_nonzero wt_nonzero zero_sig one_sig opp_sig add_sig sub_sig mul_sig ring := + cache_term + (Ring.ring_by_isomorphism + (F := F m) + (H := Z^sz) + (phi := Positional.Fencode wt) + (phi' := Positional.Fdecode wt) + (zero := proj1_sig zero_sig) + (one := proj1_sig one_sig) + (opp := proj1_sig opp_sig) + (add := proj1_sig add_sig) + (sub := proj1_sig sub_sig) + (mul := proj1_sig mul_sig) + (phi'_zero := proj2_sig zero_sig) + (phi'_one := proj2_sig one_sig) + (phi'_opp := proj2_sig opp_sig) + (Positional.Fdecode_Fencode_id + (sz_nonzero := sz_nonzero) + (div_mod := div_mod) + wt eq_refl wt_nonzero wt_divides') + (Positional.eq_Feq_iff wt) + (proj2_sig add_sig) + (proj2_sig sub_sig) + (proj2_sig mul_sig) + ) + ring. + +(* +Eval cbv [proj1_sig add_sig] in (proj1_sig add_sig). +Eval cbv [proj1_sig sub_sig] in (proj1_sig sub_sig). +Eval cbv [proj1_sig opp_sig] in (proj1_sig opp_sig). +Eval cbv [proj1_sig mul_sig] in (proj1_sig mul_sig). +Eval cbv [proj1_sig carry_sig] in (proj1_sig carry_sig). + *) diff --git a/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v b/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v new file mode 100644 index 000000000..a83adb29c --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v @@ -0,0 +1,177 @@ +(* This file is autogenerated from Defaults.v by remake_packages.py *) +Require Import Crypto.Specific.Framework.CurveParametersPackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage. +Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Defaults. +Require Import Crypto.Specific.Framework.Packages. +Require Import Crypto.Util.TagList. + +Module TAG. + Inductive tags := carry_sig | zero_sig | one_sig | a24_sig | add_sig | sub_sig | opp_sig | mul_sig | square_sig | ring. +End TAG. + +Ltac add_carry_sig pkg := + Tag.update_by_tac_if_not_exists + pkg + TAG.carry_sig + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let s := Tag.get pkg TAG.s in + let c := Tag.get pkg TAG.c in + let carry_chains := Tag.get pkg TAG.carry_chains in + let wt_nonzero := Tag.get pkg TAG.wt_nonzero in + let wt_divides_chains := Tag.get pkg TAG.wt_divides_chains in + let carry_sig := fresh "carry_sig" in + let carry_sig := pose_carry_sig sz m wt s c carry_chains wt_nonzero wt_divides_chains carry_sig in + constr:(carry_sig)). +Ltac add_zero_sig pkg := + Tag.update_by_tac_if_not_exists + pkg + TAG.zero_sig + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let zero_sig := fresh "zero_sig" in + let zero_sig := pose_zero_sig sz m wt zero_sig in + constr:(zero_sig)). +Ltac add_one_sig pkg := + Tag.update_by_tac_if_not_exists + pkg + TAG.one_sig + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let one_sig := fresh "one_sig" in + let one_sig := pose_one_sig sz m wt one_sig in + constr:(one_sig)). +Ltac add_a24_sig pkg := + Tag.update_by_tac_if_not_exists + pkg + TAG.a24_sig + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let a24 := Tag.get pkg TAG.a24 in + let a24_sig := fresh "a24_sig" in + let a24_sig := pose_a24_sig sz m wt a24 a24_sig in + constr:(a24_sig)). +Ltac add_add_sig pkg := + Tag.update_by_tac_if_not_exists + pkg + TAG.add_sig + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let wt_nonzero := Tag.get pkg TAG.wt_nonzero in + let add_sig := fresh "add_sig" in + let add_sig := pose_add_sig sz m wt wt_nonzero add_sig in + constr:(add_sig)). +Ltac add_sub_sig pkg := + Tag.update_by_tac_if_not_exists + pkg + TAG.sub_sig + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let wt_nonzero := Tag.get pkg TAG.wt_nonzero in + let coef := Tag.get pkg TAG.coef in + let sub_sig := fresh "sub_sig" in + let sub_sig := pose_sub_sig sz m wt wt_nonzero coef sub_sig in + constr:(sub_sig)). +Ltac add_opp_sig pkg := + Tag.update_by_tac_if_not_exists + pkg + TAG.opp_sig + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let wt_nonzero := Tag.get pkg TAG.wt_nonzero in + let coef := Tag.get pkg TAG.coef in + let opp_sig := fresh "opp_sig" in + let opp_sig := pose_opp_sig sz m wt wt_nonzero coef opp_sig in + constr:(opp_sig)). +Ltac add_mul_sig pkg P_default_mul P_extra_prove_mul_eq := + Tag.update_by_tac_if_not_exists + pkg + TAG.mul_sig + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let s := Tag.get pkg TAG.s in + let c := Tag.get pkg TAG.c in + let sz2 := Tag.get pkg TAG.sz2 in + let wt_nonzero := Tag.get pkg TAG.wt_nonzero in + let mul_sig := fresh "mul_sig" in + let mul_sig := pose_mul_sig P_default_mul P_extra_prove_mul_eq sz m wt s c sz2 wt_nonzero mul_sig in + constr:(mul_sig)). +Ltac add_square_sig pkg P_default_square P_extra_prove_square_eq := + Tag.update_by_tac_if_not_exists + pkg + TAG.square_sig + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let s := Tag.get pkg TAG.s in + let c := Tag.get pkg TAG.c in + let sz2 := Tag.get pkg TAG.sz2 in + let wt_nonzero := Tag.get pkg TAG.wt_nonzero in + let square_sig := fresh "square_sig" in + let square_sig := pose_square_sig P_default_square P_extra_prove_square_eq sz m wt s c sz2 wt_nonzero square_sig in + constr:(square_sig)). +Ltac add_ring pkg := + Tag.update_by_tac_if_not_exists + pkg + TAG.ring + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let wt_divides' := Tag.get pkg TAG.wt_divides' in + let sz_nonzero := Tag.get pkg TAG.sz_nonzero in + let wt_nonzero := Tag.get pkg TAG.wt_nonzero in + let zero_sig := Tag.get pkg TAG.zero_sig in + let one_sig := Tag.get pkg TAG.one_sig in + let opp_sig := Tag.get pkg TAG.opp_sig in + let add_sig := Tag.get pkg TAG.add_sig in + let sub_sig := Tag.get pkg TAG.sub_sig in + let mul_sig := Tag.get pkg TAG.mul_sig in + let ring := fresh "ring" in + let ring := pose_ring sz m wt wt_divides' sz_nonzero wt_nonzero zero_sig one_sig opp_sig add_sig sub_sig mul_sig ring in + constr:(ring)). +Ltac add_Defaults_package pkg P_default_mul P_extra_prove_mul_eq P_default_square P_extra_prove_square_eq := + let pkg := add_carry_sig pkg in + let pkg := add_zero_sig pkg in + let pkg := add_one_sig pkg in + let pkg := add_a24_sig pkg in + let pkg := add_add_sig pkg in + let pkg := add_sub_sig pkg in + let pkg := add_opp_sig pkg in + let pkg := add_mul_sig pkg P_default_mul P_extra_prove_mul_eq in + let pkg := add_square_sig pkg P_default_square P_extra_prove_square_eq in + let pkg := add_ring pkg in + Tag.strip_local pkg. + + +Module MakeDefaultsPackage (PKG : PrePackage). + Module Import MakeDefaultsPackageInternal := MakePackageBase PKG. + + Ltac get_carry_sig _ := get TAG.carry_sig. + Notation carry_sig := (ltac:(let v := get_carry_sig () in exact v)) (only parsing). + Ltac get_zero_sig _ := get TAG.zero_sig. + Notation zero_sig := (ltac:(let v := get_zero_sig () in exact v)) (only parsing). + Ltac get_one_sig _ := get TAG.one_sig. + Notation one_sig := (ltac:(let v := get_one_sig () in exact v)) (only parsing). + Ltac get_a24_sig _ := get TAG.a24_sig. + Notation a24_sig := (ltac:(let v := get_a24_sig () in exact v)) (only parsing). + Ltac get_add_sig _ := get TAG.add_sig. + Notation add_sig := (ltac:(let v := get_add_sig () in exact v)) (only parsing). + Ltac get_sub_sig _ := get TAG.sub_sig. + Notation sub_sig := (ltac:(let v := get_sub_sig () in exact v)) (only parsing). + Ltac get_opp_sig _ := get TAG.opp_sig. + Notation opp_sig := (ltac:(let v := get_opp_sig () in exact v)) (only parsing). + Ltac get_mul_sig _ := get TAG.mul_sig. + Notation mul_sig := (ltac:(let v := get_mul_sig () in exact v)) (only parsing). + Ltac get_square_sig _ := get TAG.square_sig. + Notation square_sig := (ltac:(let v := get_square_sig () in exact v)) (only parsing). + Ltac get_ring _ := get TAG.ring. + Notation ring := (ltac:(let v := get_ring () in exact v)) (only parsing). +End MakeDefaultsPackage. diff --git a/src/Specific/Framework/ArithmeticSynthesis/Freeze.v b/src/Specific/Framework/ArithmeticSynthesis/Freeze.v new file mode 100644 index 000000000..02daea678 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/Freeze.v @@ -0,0 +1,50 @@ +Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. +Require Import Coq.Lists.List. Import ListNotations. +Require Import Crypto.Arithmetic.Core. Import B. +Require Import Crypto.Arithmetic.Saturated.Freeze. +Require Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.Definitions. +Require Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics.CacheTerm. + +Module Export Exports. + Hint Opaque freeze : uncps. + Hint Rewrite freeze_id : uncps. +End Exports. + +Local Open Scope Z_scope. +Local Infix "^" := Tuple.tuple : type_scope. + +(* kludge to get around name clashes in the following, and the fact + that the python script cares about argument names *) +Local Ltac rewrite_eval_freeze_with_c c' := + rewrite eval_freeze with (c:=c'). + +Ltac pose_freeze_sig sz m wt c m_enc bitwidth wt_nonzero wt_pos wt_divides wt_multiples freeze_sig := + cache_term_with_type_by + {freeze : (Z^sz -> Z^sz)%type | + forall a : Z^sz, + (0 <= Positional.eval wt a < 2 * Z.pos m)-> + let eval := Positional.Fdecode (m := m) wt in + eval (freeze a) = eval a} + ltac:(let a := fresh "a" in + eexists; cbv beta zeta; (intros a ?); + pose proof wt_nonzero; pose proof wt_pos; + pose proof div_mod; pose proof wt_divides; + pose proof wt_multiples; + pose proof div_correct; pose proof modulo_correct; + let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in + F_mod_eq; + transitivity (Positional.eval wt x); repeat autounfold; + [ | autorewrite with uncps push_id push_basesystem_eval; + rewrite_eval_freeze_with_c c; + try eassumption; try omega; try reflexivity; + try solve [auto using B.Positional.select_id, + B.Positional.eval_select(*, zselect_correct*)]; + vm_decide]; + cbv[mod_eq]; apply f_equal2; + [ | reflexivity ]; apply f_equal; + cbv - [runtime_opp runtime_add runtime_mul runtime_shr runtime_and Let_In Z.add_get_carry Z.zselect]; + reflexivity) + freeze_sig. diff --git a/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v new file mode 100644 index 000000000..9314f369e --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v @@ -0,0 +1,39 @@ +(* This file is autogenerated from Freeze.v by remake_packages.py *) +Require Import Crypto.Specific.Framework.CurveParametersPackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage. +Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Freeze. +Require Import Crypto.Specific.Framework.Packages. +Require Import Crypto.Util.TagList. + +Module TAG. + Inductive tags := freeze_sig. +End TAG. + +Ltac add_freeze_sig pkg := + Tag.update_by_tac_if_not_exists + pkg + TAG.freeze_sig + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let c := Tag.get pkg TAG.c in + let m_enc := Tag.get pkg TAG.m_enc in + let bitwidth := Tag.get pkg TAG.bitwidth in + let wt_nonzero := Tag.get pkg TAG.wt_nonzero in + let wt_pos := Tag.get pkg TAG.wt_pos in + let wt_divides := Tag.get pkg TAG.wt_divides in + let wt_multiples := Tag.get pkg TAG.wt_multiples in + let freeze_sig := fresh "freeze_sig" in + let freeze_sig := pose_freeze_sig sz m wt c m_enc bitwidth wt_nonzero wt_pos wt_divides wt_multiples freeze_sig in + constr:(freeze_sig)). +Ltac add_Freeze_package pkg := + let pkg := add_freeze_sig pkg in + Tag.strip_local pkg. + + +Module MakeFreezePackage (PKG : PrePackage). + Module Import MakeFreezePackageInternal := MakePackageBase PKG. + + Ltac get_freeze_sig _ := get TAG.freeze_sig. + Notation freeze_sig := (ltac:(let v := get_freeze_sig () in exact v)) (only parsing). +End MakeFreezePackage. diff --git a/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v b/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v new file mode 100644 index 000000000..e2bc9e6e0 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/HelperTactics.v @@ -0,0 +1,65 @@ +Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. +Require Import Crypto.Arithmetic.Core. Import B. +Require Import Crypto.Util.ZUtil.ModInv. +Require Import Crypto.Util.Tactics.CacheTerm. +Require Crypto.Util.Tuple. + +Local Notation tuple := Tuple.tuple. +Local Open Scope list_scope. +Local Open Scope Z_scope. + +Ltac if_cond_else cond tac default id := + lazymatch (eval compute in cond) with + | true => tac id + | false => default + end. +Ltac if_cond cond tac id := if_cond_else cond tac (0%Z) id. + +Ltac pose_modinv modinv_fuel a modulus modinv := + let v := constr:(Option.invert_Some (Z.modinv_fueled modinv_fuel a modulus)) in + let v := (eval vm_compute in v) in + let v := (eval vm_compute in (v : Z)) in + cache_term v modinv. +Ltac pose_correct_if_Z v mkeqn id := + let T := type of v in + let eqn := + lazymatch (eval vm_compute in T) with + | Z => mkeqn () + | ?T + => let v := (eval vm_compute in v) in + lazymatch T with + | option _ + => lazymatch v with + | None => constr:(v = v) + end + | unit + => lazymatch v with + | tt => constr:(tt = tt) + end + end + end in + cache_proof_with_type_by + eqn + ltac:(vm_compute; reflexivity) + id. + +Ltac pose_proof_tuple ls := + lazymatch ls with + | pair ?x ?y => pose_proof_tuple x; pose_proof_tuple y + | ?ls => pose proof ls + end. + +Ltac make_chained_carries_cps' sz wt s c a carry_chains := + lazymatch carry_chains with + | ?carry_chain :: nil + => constr:(Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain id) + | ?carry_chain :: ?carry_chains + => let r := fresh "r" in + let r' := fresh r in + constr:(Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain + (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r + (fun r' => ltac:(let v := make_chained_carries_cps' sz wt s c r' carry_chains in exact v)))) + end. +Ltac make_chained_carries_cps sz wt s c a carry_chains := + let carry_chains := (eval cbv delta [carry_chains] in carry_chains) in + make_chained_carries_cps' sz wt s c a carry_chains. diff --git a/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v b/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v new file mode 100644 index 000000000..78cc57d68 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v @@ -0,0 +1,140 @@ +Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. +Require Import Coq.Lists.List. Import ListNotations. +Require Import Crypto.Arithmetic.Core. Import B. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.LetIn Crypto.Util.ZUtil. +Require Import Crypto.Arithmetic.Karatsuba. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Crypto.Util.Tuple. +Require Import Crypto.Util.IdfunWithAlt. +Require Import Crypto.Util.Tactics.VM. +Require Import Crypto.Util.QUtil. +Require Import Crypto.Util.ZUtil.ModInv. + +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.SquareFromMul. +Require Import Crypto.Util.Tactics.PoseTermWithName. +Require Import Crypto.Util.Tactics.CacheTerm. + +Local Notation tuple := Tuple.tuple. +Local Open Scope list_scope. +Local Open Scope Z_scope. +Local Coercion Z.of_nat : nat >-> Z. +Local Infix "^" := Tuple.tuple : type_scope. + +(** XXX TODO(jadep) FIXME: Is sqrt(s) the right thing to pass to goldilocks_mul_cps (the original code hard-coded 2^224 *) +Ltac internal_pose_sqrt_s s sqrt_s := + let v := (eval vm_compute in (Z.log2 s / 2)) in + cache_term (2^v) sqrt_s. + +Ltac basesystem_partial_evaluation_RHS := + let t0 := (match goal with + | |- _ _ ?t => t + end) in + let t := + eval + cbv + delta [Positional.to_associational_cps Positional.to_associational + Positional.eval Positional.zeros Positional.add_to_nth_cps + Positional.add_to_nth Positional.place_cps Positional.place + Positional.from_associational_cps Positional.from_associational + Positional.carry_cps Positional.carry + Positional.chained_carries_cps Positional.chained_carries + Positional.sub_cps Positional.sub Positional.split_cps + Positional.scmul_cps Positional.unbalanced_sub_cps + Positional.negate_snd_cps Positional.add_cps Positional.opp_cps + Associational.eval Associational.multerm Associational.mul_cps + Associational.mul Associational.split_cps Associational.split + Associational.reduce_cps Associational.reduce + Associational.carryterm_cps Associational.carryterm + Associational.carry_cps Associational.carry + Associational.negate_snd_cps Associational.negate_snd div modulo + id_tuple_with_alt id_tuple'_with_alt + ] + in t0 + in + let t := eval pattern @runtime_mul in t in + let t := (match t with + | ?t _ => t + end) in + let t := eval pattern @runtime_add in t in + let t := (match t with + | ?t _ => t + end) in + let t := eval pattern @runtime_opp in t in + let t := (match t with + | ?t _ => t + end) in + let t := eval pattern @runtime_shr in t in + let t := (match t with + | ?t _ => t + end) in + let t := eval pattern @runtime_and in t in + let t := (match t with + | ?t _ => t + end) in + let t := eval pattern @Let_In in t in + let t := (match t with + | ?t _ => t + end) in + let t := eval pattern @id_with_alt in t in + let t := (match t with + | ?t _ => t + end) in + let t1 := fresh "t1" in + pose (t1 := t); + transitivity + (t1 (@id_with_alt) (@Let_In) (@runtime_and) (@runtime_shr) (@runtime_opp) (@runtime_add) + (@runtime_mul)); + [ replace_with_vm_compute t1; clear t1 | reflexivity ]. + +Ltac internal_pose_goldilocks_mul_sig sz wt s c half_sz sqrt_s goldilocks_mul_sig := + cache_term_with_type_by + {mul : (Z^sz -> Z^sz -> Z^sz)%type | + forall a b : Z^sz, + mul a b = goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt sqrt_s a b (fun ab => Positional.reduce_cps (n:=sz) wt s c ab id)} + ltac:(eexists; cbv beta zeta; intros; + cbv [goldilocks_mul_cps]; + repeat autounfold; + basesystem_partial_evaluation_RHS; + do_replace_match_with_destructuring_match_in_goal; + reflexivity) + goldilocks_mul_sig. + +Ltac internal_pose_mul_sig_from_goldilocks_mul_sig sz m wt s c half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig := + cache_term_with_type_by + {mul : (Z^sz -> Z^sz -> Z^sz)%type | + forall a b : Z^sz, + let eval := Positional.Fdecode (m := m) wt in + Positional.Fdecode (m := m) wt (mul a b) = (eval a * eval b)%F} + ltac:(idtac; + let a := fresh "a" in + let b := fresh "b" in + eexists; cbv beta zeta; intros a b; + pose proof wt_nonzero; + let x := constr:( + goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt sqrt_s a b (fun ab => Positional.reduce_cps (n:=sz) wt s c ab id)) in + F_mod_eq; + transitivity (Positional.eval wt x); repeat autounfold; + + [ + | autorewrite with uncps push_id push_basesystem_eval; + apply goldilocks_mul_correct; try assumption; cbv; congruence ]; + cbv [mod_eq]; apply f_equal2; + [ | reflexivity ]; + apply f_equal; + etransitivity; [|apply (proj2_sig goldilocks_mul_sig)]; + cbv [proj1_sig goldilocks_mul_sig]; + reflexivity) + mul_sig. + +Ltac pose_mul_sig sz m wt s c half_sz wt_nonzero mul_sig := + let sqrt_s := fresh "sqrt_s" in + let goldilocks_mul_sig := fresh "goldilocks_mul_sig" in + let sqrt_s := internal_pose_sqrt_s s sqrt_s in + let goldilocks_mul_sig := internal_pose_goldilocks_mul_sig sz wt s c half_sz sqrt_s goldilocks_mul_sig in + internal_pose_mul_sig_from_goldilocks_mul_sig sz m wt s c half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig. + +Ltac pose_square_sig sz m wt mul_sig square_sig := + SquareFromMul.pose_square_sig sz m wt mul_sig square_sig. diff --git a/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v b/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v new file mode 100644 index 000000000..a0d2d3528 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.v @@ -0,0 +1,46 @@ +(* This file is autogenerated from Karatsuba.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 Export Crypto.Specific.Framework.ArithmeticSynthesis.Karatsuba. +Require Import Crypto.Specific.Framework.Packages. +Require Import Crypto.Util.TagList. + + +Ltac add_mul_sig pkg := + if_goldilocks + pkg + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let s := Tag.get pkg TAG.s in + let c := Tag.get pkg TAG.c in + let half_sz := Tag.get pkg TAG.half_sz in + let wt_nonzero := Tag.get pkg TAG.wt_nonzero in + let mul_sig := fresh "mul_sig" in + let mul_sig := pose_mul_sig sz m wt s c half_sz wt_nonzero mul_sig in + Tag.update pkg TAG.mul_sig mul_sig) + ltac:(fun _ => pkg) + (). +Ltac add_square_sig pkg := + if_goldilocks + pkg + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let mul_sig := Tag.get pkg TAG.mul_sig in + let square_sig := fresh "square_sig" in + let square_sig := pose_square_sig sz m wt mul_sig square_sig in + Tag.update pkg TAG.square_sig square_sig) + ltac:(fun _ => pkg) + (). +Ltac add_Karatsuba_package pkg := + let pkg := add_mul_sig pkg in + let pkg := add_square_sig pkg in + Tag.strip_local pkg. + + +Module MakeKaratsubaPackage (PKG : PrePackage). + Module Import MakeKaratsubaPackageInternal := MakePackageBase PKG. + +End MakeKaratsubaPackage. diff --git a/src/Specific/Framework/LadderstepSynthesisFramework.v b/src/Specific/Framework/ArithmeticSynthesis/Ladderstep.v index d6afb31eb..ba3fd9078 100644 --- a/src/Specific/Framework/LadderstepSynthesisFramework.v +++ b/src/Specific/Framework/ArithmeticSynthesis/Ladderstep.v @@ -46,7 +46,6 @@ Section with_notations. end. End with_notations. -(** TODO(jadep,andreser): Move to NewBaseSystemTest? *) Ltac pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig Mxzladderstep_sig := cache_term_with_type_by { xzladderstep : tuple Z sz -> tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz -> tuple Z sz * tuple Z sz * (tuple Z sz * tuple Z sz) @@ -66,28 +65,3 @@ Ltac pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig end; reflexivity) Mxzladderstep_sig. - -Ltac get_Ladderstep_package sz wt m add_sig sub_sig mul_sig square_sig carry_sig := - let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in - let Mxzladderstep_sig := pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig Mxzladderstep_sig in - constr:((Mxzladderstep_sig, tt)). -Ltac make_Ladderstep_package sz wt m add_sig sub_sig mul_sig square_sig carry_sig := - lazymatch goal with - | [ |- { T : _ & T } ] => eexists - | [ |- _ ] => idtac - end; - let pkg := get_Ladderstep_package sz wt m add_sig sub_sig mul_sig square_sig carry_sig in - exact pkg. - -Module Type LadderstepPrePackage. - Parameter Ladderstep_package' : { T : _ & T }. - Parameter Ladderstep_package : projT1 Ladderstep_package'. -End LadderstepPrePackage. - -Module MakeLadderstep (LP : LadderstepPrePackage). - Ltac get_Ladderstep_package _ := eval hnf in LP.Ladderstep_package. - Ltac L_reduce_proj x := - eval cbv beta iota zeta in x. - Ltac get_Mxzladderstep_sig _ := let pkg := get_Ladderstep_package () in L_reduce_proj (let '(Mxzladderstep_sig, tt) := pkg in Mxzladderstep_sig). - Notation Mxzladderstep_sig := (ltac:(let v := get_Mxzladderstep_sig () in exact v)) (only parsing). -End MakeLadderstep. diff --git a/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v new file mode 100644 index 000000000..dd7b6c541 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/LadderstepPackage.v @@ -0,0 +1,38 @@ +(* This file is autogenerated from Ladderstep.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 Export Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep. +Require Import Crypto.Specific.Framework.Packages. +Require Import Crypto.Util.TagList. + +Module TAG. + Inductive tags := Mxzladderstep_sig. +End TAG. + +Ltac add_Mxzladderstep_sig pkg := + Tag.update_by_tac_if_not_exists + pkg + TAG.Mxzladderstep_sig + ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + let wt := Tag.get pkg TAG.wt in + let m := Tag.get pkg TAG.m in + let add_sig := Tag.get pkg TAG.add_sig in + let sub_sig := Tag.get pkg TAG.sub_sig in + let mul_sig := Tag.get pkg TAG.mul_sig in + let square_sig := Tag.get pkg TAG.square_sig in + let carry_sig := Tag.get pkg TAG.carry_sig in + let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in + let Mxzladderstep_sig := pose_Mxzladderstep_sig sz wt m add_sig sub_sig mul_sig square_sig carry_sig Mxzladderstep_sig in + constr:(Mxzladderstep_sig)). +Ltac add_Ladderstep_package pkg := + let pkg := add_Mxzladderstep_sig pkg in + Tag.strip_local pkg. + + +Module MakeLadderstepPackage (PKG : PrePackage). + Module Import MakeLadderstepPackageInternal := MakePackageBase PKG. + + Ltac get_Mxzladderstep_sig _ := get TAG.Mxzladderstep_sig. + Notation Mxzladderstep_sig := (ltac:(let v := get_Mxzladderstep_sig () in exact v)) (only parsing). +End MakeLadderstepPackage. diff --git a/src/Specific/Framework/ArithmeticSynthesis/SquareFromMul.v b/src/Specific/Framework/ArithmeticSynthesis/SquareFromMul.v new file mode 100644 index 000000000..8d8946923 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/SquareFromMul.v @@ -0,0 +1,28 @@ +Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. +Require Import Coq.Lists.List. Import ListNotations. +Require Import Crypto.Arithmetic.Core. Import B. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics. +Require Import Crypto.Util.Tactics.CacheTerm. +Require Crypto.Util.Tuple. + +Local Notation tuple := Tuple.tuple. +Local Open Scope list_scope. +Local Open Scope Z_scope. +Local Infix "^" := tuple : type_scope. + +Ltac pose_square_sig sz m wt mul_sig square_sig := + cache_term_with_type_by + {square : (Z^sz -> Z^sz)%type | + forall a : Z^sz, + let eval := Positional.Fdecode (m := m) wt in + Positional.Fdecode (m := m) wt (square a) = (eval a * eval a)%F} + ltac:(idtac; + let a := fresh "a" in + eexists; cbv beta zeta; intros a; + rewrite <-(proj2_sig mul_sig); + apply f_equal; + cbv [proj1_sig mul_sig]; + reflexivity) + square_sig. diff --git a/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py b/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py new file mode 100755 index 000000000..52f5e0f54 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesis/remake_packages.py @@ -0,0 +1,240 @@ +#!/usr/bin/env python +from __future__ import with_statement +import re, os +import io + +PACKAGE_NAMES = [('../CurveParameters.v', [])] +CP_LIST = ['../CurveParametersPackage.v'] +CP_BASE_LIST = ['../CurveParametersPackage.v', 'BasePackage.v'] +CP_BASE_DEFAULTS_LIST = ['../CurveParametersPackage.v', 'BasePackage.v', 'DefaultsPackage.v'] +CP_BASE_DEFAULTS_FREEZE_LADDERSTEP_LIST = ['../CurveParametersPackage.v', 'BasePackage.v', 'DefaultsPackage.v', 'FreezePackage.v', 'LadderstepPackage.v'] +NORMAL_PACKAGE_NAMES = [('Base.v', (CP_LIST, None)), + ('Defaults.v', (CP_BASE_LIST, 'not_exists')), + ('../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'))] +ALL_FILE_NAMES = PACKAGE_NAMES + NORMAL_PACKAGE_NAMES # PACKAGE_CP_NAMES + WITH_CURVE_BASE_NAMES + ['../ReificationTypes.v'] +CONFIGS = ('goldilocks', ) + +EXCLUDES = ('constr:((wt_divides_chain, wt_divides_chains))', ) + +contents = {} +lines = {} +fns = {} + +PY_FILE_NAME = os.path.basename(__file__) + +def init_contents(lines=lines, contents=contents): + for fname, _ in ALL_FILE_NAMES: + with open(fname, 'r') as f: + contents[fname] = f.read() + lines.update(dict((k, v.split('\n')) for k, v in contents.items())) + +def strip_prefix(name, prefix='local_'): + if name.startswith(prefix): return name[len(prefix):] + return name + +def init_fns(lines=lines, fns=fns): + header = 'Ltac pose_' + for fname, _ in ALL_FILE_NAMES: + stripped_lines = [i.strip() for i in lines[fname]] + fns[fname] = [(strip_prefix(name, 'local_'), args.strip(), name.startswith('local_')) + for line in stripped_lines + if line.startswith(header) + for name, args in re.findall('Ltac pose_([^ ]*' + ') ([A-Za-z0-9_\' ]*' + ')', line.strip())] + +def get_file_root(folder=os.path.dirname(__file__), filename='Makefile'): + dir_path = os.path.realpath(folder) + while not os.path.isfile(os.path.join(dir_path, filename)) and dir_path != '/': + dir_path = os.path.realpath(os.path.join(dir_path, '..')) + if not os.path.isfile(os.path.join(dir_path, filename)): + print('ERROR: Could not find Makefile in the root of %s' % folder) + raise Exception + return dir_path + +def modname_of_file_name(fname): + assert(fname[-2:] == '.v') + return 'Crypto.' + os.path.normpath(os.path.relpath(os.path.realpath(fname), os.path.join(root, 'src'))).replace(os.sep, '.')[:-2] + +def split_args(name, args_str, indent=''): + args = [arg.strip() for arg in args_str.split(' ')] + pass_args = [arg for arg in args if arg.startswith('P_')] + extract_args = [arg for arg in args if arg not in pass_args and arg != name] + if name not in args: + print('Error: %s not in %s' % (name, repr(args))) + assert(name in args) + assert(len(pass_args) + len(extract_args) + 1 == len(args)) + pass_args_str = ' '.join(pass_args) + if pass_args_str != '': pass_args_str += ' ' + extract_args_str = '' + nl_indent = ('\n%(indent)s ' % locals()) + if len(extract_args) > 0: + extract_args_str = nl_indent + nl_indent.join('let %s := Tag.get pkg TAG.%s in' % (arg, arg) for arg in extract_args) + return args, pass_args, extract_args, pass_args_str, extract_args_str + +def make_add_from_pose(name, args_str, indent='', only_if=None, local=False): + args, pass_args, extract_args, pass_args_str, extract_args_str = split_args(name, args_str, indent=indent) + ret = r'''%(indent)sLtac add_%(name)s pkg %(pass_args_str)s:=''' % locals() + local_str = ('local_' if local else '') + if_not_exists_str = '' + body = r'''%(extract_args_str)s +%(indent)s let %(name)s := fresh "%(name)s" in +%(indent)s ''' % locals() + body += r'''let %(name)s := pose_%(local_str)s%(name)s %(args_str)s in +%(indent)s ''' % locals() + if only_if == 'not_exists': + assert(not local) + body += 'constr:(%(name)s)' % locals() + body = body.strip('\n ').replace('\n', '\n ') + ret += r''' +%(indent)s Tag.update_by_tac_if_not_exists +%(indent)s pkg +%(indent)s TAG.%(name)s +%(indent)s ltac:(fun _ => %(body)s).''' % locals() + else: + body += r'''Tag.%(local_str)supdate pkg TAG.%(name)s %(name)s''' % locals() + if only_if is None: + ret += body + '.\n' + else: + body = body.strip('\n ').replace('\n', '\n ') + ret += r''' +%(indent)s if_%(only_if)s +%(indent)s pkg +%(indent)s ltac:(fun _ => %(body)s) +%(indent)s ltac:(fun _ => pkg) +%(indent)s ().''' % locals() + return ret + +def make_add_all(fname, indent=''): + modname, ext = os.path.splitext(os.path.basename(fname)) + all_items = [(name, split_args(name, args_str, indent=indent)) for name, args_str, local in fns[fname]] + all_pass_args = [] + for name, (args, pass_args, extract_args, pass_args_str, extract_args_str) in all_items: + for arg in pass_args: + if arg not in all_pass_args: all_pass_args.append(arg) + all_pass_args_str = ' '.join(all_pass_args) + if all_pass_args_str != '': all_pass_args_str += ' ' + ret = r'''%(indent)sLtac add_%(modname)s_package pkg %(all_pass_args_str)s:=''' % locals() + nl_indent = ('\n%(indent)s ' % locals()) + ret += nl_indent + nl_indent.join('let pkg := add_%s pkg %sin' % (name, pass_args_str) + for name, (args, pass_args, extract_args, pass_args_str, extract_args_str) in all_items) + ret += nl_indent + 'Tag.strip_local pkg.\n' + return ret + +def make_if(name, indent=''): + ret = r'''%(indent)sLtac if_%(name)s pkg tac_true tac_false arg := +%(indent)s let %(name)s := Tag.get pkg TAG.%(name)s in +%(indent)s let %(name)s := (eval vm_compute in (%(name)s : bool)) in +%(indent)s lazymatch %(name)s with +%(indent)s | true => tac_true arg +%(indent)s | false => tac_false arg +%(indent)s end. +''' % locals() + return ret + +def write_if_changed(fname, value): + if os.path.isfile(fname): + with open(fname, 'r') as f: + old_value = f.read() + if old_value == value: return + value = unicode(value) + print('Writing %s...' % fname) + with io.open(fname, 'w', newline='\n') as f: + f.write(value) + +def do_replace(fname, headers, new_contents): + lines = contents[fname].split('\n') + ret = [] + for line in lines: + if any(header in line for header in headers): + ret.append(new_contents) + break + else: + ret.append(line) + ret = unicode('\n'.join(ret)) + write_if_changed(fname, ret) + +def get_existing_tags(fname, deps): + return set(name for dep in deps for name, args, local in fns[dep.replace('Package.v', '.v')]) + +def make_package(fname, deps, extra_modname_prefix='', extra_imports=None, prefix=None, add_package=True): + py_file_name = PY_FILE_NAME + existing_tags = get_existing_tags(fname, deps) + full_mod = modname_of_file_name(fname) + modname, ext = os.path.splitext(os.path.basename(fname)) + ret = (r'''(* This file is autogenerated from %(modname)s.v by %(py_file_name)s *) +''' % locals()) + if extra_imports is not None: + ret += extra_imports + ret += (r'''Require Export %(full_mod)s. +Require Import Crypto.Specific.Framework.Packages. +Require Import Crypto.Util.TagList. +''' % locals()) + if prefix is not None: + ret += prefix + new_names = [name for name, args, local in fns[fname] if name not in existing_tags and not local] + if add_package: # and len(new_names) > 0: + ret += (r''' + +Module Make%(extra_modname_prefix)s%(modname)sPackage (PKG : PrePackage). + Module Import Make%(extra_modname_prefix)s%(modname)sPackageInternal := MakePackageBase PKG. +''' % locals()) + for name in new_names: + ret += ("\n Ltac get_%s _ := get TAG.%s." % (name, name)) + ret += ("\n Notation %s := (ltac:(let v := get_%s () in exact v)) (only parsing)." % (name, name)) + ret += ('\nEnd Make%(extra_modname_prefix)s%(modname)sPackage.\n' % locals()) + return ret + +def make_tags(fname, deps): + existing_tags = get_existing_tags(fname, deps) + new_tags = [name for name, args, local in fns[fname] if name not in existing_tags] + if len(new_tags) == 0: return '' + names = ' | '.join(new_tags) + return r'''Module TAG. + Inductive tags := %s. +End TAG. +''' % names + +def write_package(fname, pkg): + pkg_name = fname[:-2] + 'Package.v' + write_if_changed(pkg_name, pkg) + +def update_CurveParameters(fname='../CurveParameters.v'): + endline = contents[fname].strip().split('\n')[-1] + assert(endline.startswith('End ')) + header = '(* Everything below this line autogenerated by %s *)' % PY_FILE_NAME + assert(header in contents[fname]) + ret = ' %s' % header + for name, args, local in fns[fname]: + ret += '\n' + make_add_from_pose(name, args, indent=' ', local=local) + ret += '\n' + make_add_all(fname, indent=' ') + ret += endline + prefix = '' + for name in CONFIGS: + prefix += '\n' + make_if(name, indent='') + pkg = make_package(fname, [], prefix=prefix) + do_replace(fname, (header,), ret) + write_package(fname, pkg) + +def make_normal_package(fname, deps, only_if=None): + prefix = '' + extra_imports = '' + for dep in deps: + extra_imports += 'Require Import %s.\n' % modname_of_file_name(dep) + prefix += '\n' + make_tags(fname, deps) + for name, args, local in fns[fname]: + prefix += '\n' + make_add_from_pose(name, args, indent='', only_if=only_if, local=local) + prefix += '\n' + make_add_all(fname, indent='') + return make_package(fname, deps, extra_imports=extra_imports, prefix=prefix) + +def update_normal_package(fname, deps, only_if=None): + pkg = make_normal_package(fname, deps, only_if=only_if) + write_package(fname, pkg) + +root = get_file_root() +init_contents() +init_fns() +update_CurveParameters() +for fname, (deps, only_if) in NORMAL_PACKAGE_NAMES: + update_normal_package(fname, deps, only_if=only_if) diff --git a/src/Specific/Framework/ArithmeticSynthesisFramework.v b/src/Specific/Framework/ArithmeticSynthesisFramework.v deleted file mode 100644 index 342c759fe..000000000 --- a/src/Specific/Framework/ArithmeticSynthesisFramework.v +++ /dev/null @@ -1,754 +0,0 @@ -Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. -Require Import Coq.Lists.List. Import ListNotations. -Require Import Crypto.Arithmetic.Core. Import B. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Arithmetic.Saturated.Freeze. -Require Crypto.Specific.Framework.CurveParameters. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.LetIn Crypto.Util.ZUtil. -Require Import Crypto.Arithmetic.Karatsuba. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Crypto.Util.Tuple. -Require Import Crypto.Util.IdfunWithAlt. -Require Import Crypto.Util.Tactics.VM. -Require Import Crypto.Util.QUtil. - -Require Import Crypto.Util.Tactics.PoseTermWithName. -Require Import Crypto.Util.Tactics.CacheTerm. - -Local Notation tuple := Tuple.tuple. -Local Open Scope list_scope. -Local Open Scope Z_scope. -Local Coercion Z.of_nat : nat >-> Z. - -Hint Opaque freeze : uncps. -Hint Rewrite freeze_id : uncps. - -Module Export Exports. - Export Coq.setoid_ring.ZArithRing. -End Exports. - -Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParameters). - Module P := CurveParameters.FillCurveParameters Curve. - - Local Infix "^" := tuple : type_scope. - - (* emacs for adjusting definitions *) - (* Query replace regexp (default Definition \([a-zA-Z_0-9]+\) : \([A-Za-z0-9_]+\) := P.compute \(.*\)\.\(.*\) -> Ltac pose_\1 \1 :=\4^J cache_term_with_type_by^J \2^J ltac:(let v := P.do_compute \3 in exact v)^J \1.): *) - (* Query replace regexp (default Definition \([a-zA-Z_0-9]+\) : \([A-Za-z0-9_]+\) := P.compute \(.*\)\.\(.*\) -> Ltac pose_\1 \1 :=\4^J cache_term_with_type_by^J \2^J ltac:(let v := P.do_compute \3 in exact v)^J \1.): *) - (* Query replace regexp (default Definition \([a-zA-Z_0-9]+\) : \([A-Za-z0-9_ \.]*\) := P.compute \(.*\)\.\(.*\) -> Ltac pose_\1 \1 :=\4^J cache_term_with_type_by^J (\2)^J ltac:(let v := P.do_compute \3 in exact v)^J \1.): *) - (* Query replace regexp (default Definition \([a-zA-Z_0-9]+\) := P.compute \(.*\)\.\(.*\) -> Ltac pose_\1 \1 :=\3^J let v := P.do_compute \2 in cache_term v \1.): *) - - (* These definitions will need to be passed as Ltac arguments (or - cleverly inferred) when things are eventually automated *) - Ltac pose_sz sz := - cache_term_with_type_by - nat - ltac:(let v := P.do_compute P.sz in exact v) - sz. - Ltac pose_bitwidth bitwidth := - cache_term_with_type_by - Z - ltac:(let v := P.do_compute P.bitwidth in exact v) - bitwidth. - Ltac pose_s s := (* don't want to compute, e.g., [2^255] *) - cache_term_with_type_by - Z - ltac:(let v := P.do_unfold P.s in exact v) - s. - Ltac pose_c c := - cache_term_with_type_by - (list B.limb) - ltac:(let v := P.do_compute P.c in exact v) - c. - Ltac pose_carry_chains carry_chains := - let v := P.do_compute P.carry_chains in - cache_term v carry_chains. - - Ltac pose_a24 a24 := - let v := P.do_compute P.a24 in - cache_term v a24. - Ltac pose_coef_div_modulus coef_div_modulus := - cache_term_with_type_by - nat - ltac:(let v := P.do_compute P.coef_div_modulus in exact v) - coef_div_modulus. - Ltac pose_goldilocks goldilocks := - cache_term_with_type_by - bool - ltac:(let v := P.do_compute P.goldilocks in exact v) - goldilocks. - (* These definitions are inferred from those above *) - Ltac pose_m s c m := (* modulus *) - let v := (eval vm_compute in (Z.to_pos (s - Associational.eval c))) in - cache_term v m. - Section wt. - Import QArith Qround. - Local Coercion QArith_base.inject_Z : Z >-> Q. - Definition wt_gen (m : positive) (sz : nat) (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i). - End wt. - Ltac pose_wt m sz wt := - let v := (eval cbv [wt_gen] in (wt_gen m sz)) in - cache_term v wt. - Ltac pose_sz2 sz sz2 := - let v := (eval vm_compute in ((sz * 2) - 1)%nat) in - cache_term v sz2. - Ltac pose_m_enc sz s c wt m_enc := - let v := (eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c))) in - cache_term v m_enc. - Ltac pose_coef sz wt m_enc coef_div_modulus coef := (* subtraction coefficient *) - let v := (eval vm_compute in - ((fix addm (acc: Z^sz) (ctr : nat) : Z^sz := - match ctr with - | O => acc - | S n => addm (Positional.add_cps wt acc m_enc id) n - end) (Positional.zeros sz) coef_div_modulus)) in - cache_term v coef. - - Ltac pose_coef_mod sz wt m coef coef_mod := - cache_term_with_type_by - (mod_eq m (Positional.eval (n:=sz) wt coef) 0) - ltac:(exact eq_refl) - coef_mod. - Ltac pose_sz_nonzero sz sz_nonzero := - cache_proof_with_type_by - (sz <> 0%nat) - ltac:(vm_decide_no_check) - sz_nonzero. - Ltac pose_wt_nonzero wt wt_nonzero := - cache_proof_with_type_by - (forall i, wt i <> 0) - ltac:(eapply pow_ceil_mul_nat_nonzero; vm_decide_no_check) - wt_nonzero. - Ltac pose_wt_nonneg wt wt_nonneg := - cache_proof_with_type_by - (forall i, 0 <= wt i) - ltac:(apply pow_ceil_mul_nat_nonneg; vm_decide_no_check) - wt_nonneg. - Ltac pose_wt_divides wt wt_divides := - cache_proof_with_type_by - (forall i, wt (S i) / wt i > 0) - ltac:(apply pow_ceil_mul_nat_divide; vm_decide_no_check) - wt_divides. - Ltac pose_wt_divides' wt wt_divides wt_divides' := - cache_proof_with_type_by - (forall i, wt (S i) / wt i <> 0) - ltac:(symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides) - wt_divides'. - Ltac helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chain := - cache_term_with_type_by - (forall i (H:In i carry_chain), wt (S i) / wt i <> 0) - ltac:(let i := fresh "i" in intros i ?; exact (wt_divides' i)) - wt_divides_chain. - Ltac pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains := - lazymatch carry_chains with - | ?carry_chain :: nil - => helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chains - | ?carry_chain :: ?carry_chains - => let wt_divides_chains := fresh wt_divides_chains in - let wt_divides_chain := fresh wt_divides_chains in - let wt_divides_chain := helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chain in - let wt_divides_chains := pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains in - constr:((wt_divides_chain, wt_divides_chains)) - end. - Ltac pose_wt_divides_chains wt carry_chains wt_divides' wt_divides_chains := - let carry_chains := (eval cbv delta [carry_chains] in carry_chains) in - pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains. - - Local Ltac solve_constant_sig := - idtac; - lazymatch goal with - | [ |- { c : Z^?sz | Positional.Fdecode (m:=?M) ?wt c = ?v } ] - => let t := (eval vm_compute in - (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt (F.to_Z (m:=M) v))) in - (exists t; vm_decide) - end. - - Ltac pose_zero_sig sz m wt zero_sig := - cache_term_with_type_by - { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 0%F} - solve_constant_sig - zero_sig. - - Ltac pose_one_sig sz m wt one_sig := - cache_term_with_type_by - { one : Z^sz | Positional.Fdecode (m:=m) wt one = 1%F} - solve_constant_sig - one_sig. - - Ltac pose_a24_sig sz m wt a24 a24_sig := - cache_term_with_type_by - { a24t : Z^sz | Positional.Fdecode (m:=m) wt a24t = F.of_Z m P.a24 } - solve_constant_sig - a24_sig. - - Ltac pose_add_sig sz m wt wt_nonzero add_sig := - cache_term_with_type_by - { add : (Z^sz -> Z^sz -> Z^sz)%type | - forall a b : Z^sz, - let eval := Positional.Fdecode (m:=m) wt in - eval (add a b) = (eval a + eval b)%F } - ltac:(idtac; - let a := fresh "a" in - let b := fresh "b" in - eexists; cbv beta zeta; intros a b; - pose proof wt_nonzero; - let x := constr:( - Positional.add_cps (n := sz) wt a b id) in - solve_op_F wt x; reflexivity) - add_sig. - - Ltac pose_sub_sig sz m wt wt_nonzero coef sub_sig := - cache_term_with_type_by - {sub : (Z^sz -> Z^sz -> Z^sz)%type | - forall a b : Z^sz, - let eval := Positional.Fdecode (m:=m) wt in - eval (sub a b) = (eval a - eval b)%F} - ltac:(idtac; - let a := fresh "a" in - let b := fresh "b" in - eexists; cbv beta zeta; intros a b; - pose proof wt_nonzero; - let x := constr:( - Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in - solve_op_F wt x; reflexivity) - sub_sig. - - Ltac pose_opp_sig sz m wt wt_nonzero coef opp_sig := - cache_term_with_type_by - {opp : (Z^sz -> Z^sz)%type | - forall a : Z^sz, - let eval := Positional.Fdecode (m := m) wt in - eval (opp a) = F.opp (eval a)} - ltac:(idtac; - let a := fresh in - eexists; cbv beta zeta; intros a; - pose proof wt_nonzero; - let x := constr:( - Positional.opp_cps (n:=sz) (coef := coef) wt a id) in - solve_op_F wt x; reflexivity) - opp_sig. - - Ltac pose_half_sz sz half_sz := - let v := (eval compute in (sz / 2)%nat) in - cache_term v half_sz. - Ltac pose_half_sz_nonzero half_sz half_sz_nonzero := - cache_proof_with_type_by - (half_sz <> 0%nat) - ltac:(cbv; congruence) - half_sz_nonzero. - - Ltac basesystem_partial_evaluation_RHS := - let t0 := (match goal with - | |- _ _ ?t => t - end) in - let t := - eval - cbv - delta [Positional.to_associational_cps Positional.to_associational - Positional.eval Positional.zeros Positional.add_to_nth_cps - Positional.add_to_nth Positional.place_cps Positional.place - Positional.from_associational_cps Positional.from_associational - Positional.carry_cps Positional.carry - Positional.chained_carries_cps Positional.chained_carries - Positional.sub_cps Positional.sub Positional.split_cps - Positional.scmul_cps Positional.unbalanced_sub_cps - Positional.negate_snd_cps Positional.add_cps Positional.opp_cps - Associational.eval Associational.multerm Associational.mul_cps - Associational.mul Associational.split_cps Associational.split - Associational.reduce_cps Associational.reduce - Associational.carryterm_cps Associational.carryterm - Associational.carry_cps Associational.carry - Associational.negate_snd_cps Associational.negate_snd div modulo - id_tuple_with_alt id_tuple'_with_alt - ] - in t0 - in - let t := eval pattern @runtime_mul in t in - let t := (match t with - | ?t _ => t - end) in - let t := eval pattern @runtime_add in t in - let t := (match t with - | ?t _ => t - end) in - let t := eval pattern @runtime_opp in t in - let t := (match t with - | ?t _ => t - end) in - let t := eval pattern @runtime_shr in t in - let t := (match t with - | ?t _ => t - end) in - let t := eval pattern @runtime_and in t in - let t := (match t with - | ?t _ => t - end) in - let t := eval pattern @Let_In in t in - let t := (match t with - | ?t _ => t - end) in - let t := eval pattern @id_with_alt in t in - let t := (match t with - | ?t _ => t - end) in - let t1 := fresh "t1" in - pose (t1 := t); - transitivity - (t1 (@id_with_alt) (@Let_In) (@runtime_and) (@runtime_shr) (@runtime_opp) (@runtime_add) - (@runtime_mul)); - [ replace_with_vm_compute t1; clear t1 | reflexivity ]. - - (** XXX TODO(jadep) FIXME: Is sqrt(s) the right thing to pass to goldilocks_mul_cps (the original code hard-coded 2^224 *) - Ltac pose_sqrt_s s sqrt_s := - let v := (eval vm_compute in (Z.log2 s / 2)) in - cache_term (2^v) sqrt_s. - - Ltac pose_goldilocks_mul_sig goldilocks sz wt s c half_sz sqrt_s goldilocks_mul_sig := - lazymatch eval compute in goldilocks with - | true - => cache_term_with_type_by - {mul : (Z^sz -> Z^sz -> Z^sz)%type | - forall a b : Z^sz, - mul a b = goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt sqrt_s a b (fun ab => Positional.reduce_cps (n:=sz) wt s c ab id)} - ltac:(eexists; cbv beta zeta; intros; - cbv [goldilocks_mul_cps]; - repeat autounfold; - basesystem_partial_evaluation_RHS; - do_replace_match_with_destructuring_match_in_goal; - reflexivity) - goldilocks_mul_sig - | false - => goldilocks_mul_sig - end. - - Ltac pose_mul_sig sz m wt s c sz2 wt_nonzero mul_sig := - cache_term_with_type_by - {mul : (Z^sz -> Z^sz -> Z^sz)%type | - forall a b : Z^sz, - let eval := Positional.Fdecode (m := m) wt in - eval (mul a b) = (eval a * eval b)%F} - ltac:(idtac; - let a := fresh "a" in - let b := fresh "b" in - eexists; cbv beta zeta; intros a b; - pose proof wt_nonzero; - let x := constr:( - Positional.mul_cps (n:=sz) (m:=sz2) wt a b - (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in - solve_op_F wt x; - P.default_mul; - P.extra_prove_mul_eq; - break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring) - mul_sig. - - Ltac pose_mul_sig_from_goldilocks_mul_sig sz m wt s c half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig := - cache_term_with_type_by - {mul : (Z^sz -> Z^sz -> Z^sz)%type | - forall a b : Z^sz, - let eval := Positional.Fdecode (m := m) wt in - Positional.Fdecode (m := m) wt (mul a b) = (eval a * eval b)%F} - ltac:(idtac; - let a := fresh "a" in - let b := fresh "b" in - eexists; cbv beta zeta; intros a b; - pose proof wt_nonzero; - let x := constr:( - goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt sqrt_s a b (fun ab => Positional.reduce_cps (n:=sz) wt s c ab id)) in - F_mod_eq; - transitivity (Positional.eval wt x); repeat autounfold; - - [ - | autorewrite with uncps push_id push_basesystem_eval; - apply goldilocks_mul_correct; try assumption; cbv; congruence ]; - cbv [mod_eq]; apply f_equal2; - [ | reflexivity ]; - apply f_equal; - etransitivity; [|apply (proj2_sig goldilocks_mul_sig)]; - cbv [proj1_sig goldilocks_mul_sig]; - reflexivity) - mul_sig. - - Ltac pose_mul_sig_full goldilocks sz m wt s c sz2 half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig := - lazymatch eval compute in goldilocks with - | true - => pose_mul_sig_from_goldilocks_mul_sig sz m wt s c half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig - | false - => pose_mul_sig sz m wt s c sz2 wt_nonzero mul_sig - end. - - Ltac pose_square_sig sz m wt s c sz2 wt_nonzero square_sig := - cache_term_with_type_by - {square : (Z^sz -> Z^sz)%type | - forall a : Z^sz, - let eval := Positional.Fdecode (m := m) wt in - eval (square a) = (eval a * eval a)%F} - ltac:(idtac; - let a := fresh "a" in - eexists; cbv beta zeta; intros a; - pose proof wt_nonzero; - let x := constr:( - Positional.mul_cps (n:=sz) (m:=sz2) wt a a - (fun ab => Positional.reduce_cps (n:=sz) (m:=sz2) wt s c ab id)) in - solve_op_F wt x; - P.default_square; - P.extra_prove_square_eq; - break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring) - square_sig. - - Ltac pose_square_sig_from_mul_sig sz m wt mul_sig square_sig := - cache_term_with_type_by - {square : (Z^sz -> Z^sz)%type | - forall a : Z^sz, - let eval := Positional.Fdecode (m := m) wt in - Positional.Fdecode (m := m) wt (square a) = (eval a * eval a)%F} - ltac:(idtac; - let a := fresh "a" in - eexists; cbv beta zeta; intros a; - rewrite <-(proj2_sig mul_sig); - apply f_equal; - cbv [proj1_sig mul_sig]; - reflexivity) - square_sig. - - Ltac pose_square_sig_full goldilocks sz m wt s c sz2 wt_nonzero mul_sig square_sig := - lazymatch eval compute in goldilocks with - | true - => pose_square_sig_from_mul_sig sz m wt mul_sig square_sig - | false - => pose_square_sig sz m wt s c sz2 wt_nonzero square_sig - end. - - Ltac pose_proof_tuple ls := - lazymatch ls with - | pair ?x ?y => pose_proof_tuple x; pose_proof_tuple y - | ?ls => pose proof ls - end. - - Ltac make_chained_carries_cps' sz wt s c a carry_chains := - lazymatch carry_chains with - | ?carry_chain :: nil - => constr:(Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain id) - | ?carry_chain :: ?carry_chains - => let r := fresh "r" in - let r' := fresh r in - constr:(Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain - (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r - (fun r' => ltac:(let v := make_chained_carries_cps' sz wt s c r' carry_chains in exact v)))) - end. - Ltac make_chained_carries_cps sz wt s c a carry_chains := - let carry_chains := (eval cbv delta [carry_chains] in carry_chains) in - make_chained_carries_cps' sz wt s c a carry_chains. - (* Performs a full carry loop (as specified by carry_chain) *) - Ltac pose_carry_sig sz m wt s c carry_chains wt_nonzero wt_divides_chains carry_sig := - cache_term_with_type_by - {carry : (Z^sz -> Z^sz)%type | - forall a : Z^sz, - let eval := Positional.Fdecode (m := m) wt in - eval (carry a) = eval a} - ltac:(idtac; - let a := fresh "a" in - eexists; cbv beta zeta; intros a; - pose proof wt_nonzero; pose proof div_mod; - pose_proof_tuple wt_divides_chains; - let x := make_chained_carries_cps sz wt s c a carry_chains in - solve_op_F wt x; reflexivity) - carry_sig. - - Ltac pose_wt_pos wt wt_pos := - cache_proof_with_type_by - (forall i, wt i > 0) - ltac:(eapply pow_ceil_mul_nat_pos; vm_decide_no_check) - wt_pos. - - Ltac pose_wt_multiples wt wt_multiples := - cache_proof_with_type_by - (forall i, wt (S i) mod (wt i) = 0) - ltac:(apply pow_ceil_mul_nat_multiples; vm_decide_no_check) - wt_multiples. - - - (* kludge to get around name clashes in the following, and the fact - that the python script cares about argument names *) - Local Ltac rewrite_eval_freeze_with_c c' := - rewrite eval_freeze with (c:=c'). - - Ltac pose_freeze_sig sz m wt c m_enc bitwidth wt_nonzero wt_pos wt_divides wt_multiples freeze_sig := - cache_term_with_type_by - {freeze : (Z^sz -> Z^sz)%type | - forall a : Z^sz, - (0 <= Positional.eval wt a < 2 * Z.pos m)-> - let eval := Positional.Fdecode (m := m) wt in - eval (freeze a) = eval a} - ltac:(let a := fresh "a" in - eexists; cbv beta zeta; (intros a ?); - pose proof wt_nonzero; pose proof wt_pos; - pose proof div_mod; pose proof wt_divides; - pose proof wt_multiples; - pose proof div_correct; pose proof modulo_correct; - let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in - F_mod_eq; - transitivity (Positional.eval wt x); repeat autounfold; - [ | autorewrite with uncps push_id push_basesystem_eval; - rewrite_eval_freeze_with_c c; - try eassumption; try omega; try reflexivity; - try solve [auto using B.Positional.select_id, - B.Positional.eval_select(*, zselect_correct*)]; - vm_decide]; - cbv[mod_eq]; apply f_equal2; - [ | reflexivity ]; apply f_equal; - cbv - [runtime_opp runtime_add runtime_mul runtime_shr runtime_and Let_In Z.add_get_carry Z.zselect]; - reflexivity) - freeze_sig. - - Ltac pose_ring sz m wt wt_divides' sz_nonzero wt_nonzero zero_sig one_sig opp_sig add_sig sub_sig mul_sig ring := - cache_term - (Ring.ring_by_isomorphism - (F := F m) - (H := Z^sz) - (phi := Positional.Fencode wt) - (phi' := Positional.Fdecode wt) - (zero := proj1_sig zero_sig) - (one := proj1_sig one_sig) - (opp := proj1_sig opp_sig) - (add := proj1_sig add_sig) - (sub := proj1_sig sub_sig) - (mul := proj1_sig mul_sig) - (phi'_zero := proj2_sig zero_sig) - (phi'_one := proj2_sig one_sig) - (phi'_opp := proj2_sig opp_sig) - (Positional.Fdecode_Fencode_id - (sz_nonzero := sz_nonzero) - (div_mod := div_mod) - wt eq_refl wt_nonzero wt_divides') - (Positional.eq_Feq_iff wt) - (proj2_sig add_sig) - (proj2_sig sub_sig) - (proj2_sig mul_sig) - ) - ring. - -(* -Eval cbv [proj1_sig add_sig] in (proj1_sig add_sig). -Eval cbv [proj1_sig sub_sig] in (proj1_sig sub_sig). -Eval cbv [proj1_sig opp_sig] in (proj1_sig opp_sig). -Eval cbv [proj1_sig mul_sig] in (proj1_sig mul_sig). -Eval cbv [proj1_sig carry_sig] in (proj1_sig carry_sig). -*) - - (** -<< -#!/usr/bin/env python -from __future__ import with_statement -import re - -with open('ArithmeticSynthesisFramework.v', 'r') as f: - lines = f.readlines() - -header = 'Ltac pose_' - -fns = [(name, args.strip()) - for line in lines - if line.strip()[:len(header)] == header - for name, args in re.findall('Ltac pose_([^ ]*' + ') ([A-Za-z0-9_\' ]*' + ')', line.strip())] - -print(r''' Ltac get_ArithmeticSynthesis_package _ := - %s''' - % '\n '.join('let %s := fresh "%s" in' % (name, name) for name, args in fns)) -print(' ' + '\n '.join('let %s := pose_%s %s in' % (name, name, args) for name, args in fns)) -print(' constr:((%s)).' % ', '.join(name for name, args in fns)) -print(r''' - Ltac make_ArithmeticSynthesis_package _ := - lazymatch goal with - | [ |- { T : _ & T } ] => eexists - | [ |- _ ] => idtac - end; - let pkg := get_ArithmeticSynthesis_package () in - exact pkg. -End MakeArithmeticSynthesisTestTactics. - -Module Type ArithmeticSynthesisPrePackage. - Parameter ArithmeticSynthesis_package' : { T : _ & T }. - Parameter ArithmeticSynthesis_package : projT1 ArithmeticSynthesis_package'. -End ArithmeticSynthesisPrePackage. - -Module MakeArithmeticSynthesisTest (AP : ArithmeticSynthesisPrePackage). - Ltac get_MakeArithmeticSynthesisTest_package _ := eval hnf in AP.ArithmeticSynthesis_package. - Ltac AS_reduce_proj x := - eval cbv beta iota zeta in x. -''') -terms = ', '.join(name for name, args in fns) -for name, args in fns: - print(" Ltac get_%s _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(%s) := pkg in %s)." % (name, terms, name)) - print(" Notation %s := (ltac:(let v := get_%s () in exact v)) (only parsing)." % (name, name)) -print('End MakeArithmeticSynthesisTest.') ->> **) - Ltac get_ArithmeticSynthesis_package _ := - let sz := fresh "sz" in - let bitwidth := fresh "bitwidth" in - let s := fresh "s" in - let c := fresh "c" in - let carry_chains := fresh "carry_chains" in - let a24 := fresh "a24" in - let coef_div_modulus := fresh "coef_div_modulus" in - let goldilocks := fresh "goldilocks" in - let m := fresh "m" in - let wt := fresh "wt" in - let sz2 := fresh "sz2" in - let m_enc := fresh "m_enc" in - let coef := fresh "coef" in - let coef_mod := fresh "coef_mod" in - let sz_nonzero := fresh "sz_nonzero" in - let wt_nonzero := fresh "wt_nonzero" in - let wt_nonneg := fresh "wt_nonneg" in - let wt_divides := fresh "wt_divides" in - let wt_divides' := fresh "wt_divides'" in - let wt_divides_chains := fresh "wt_divides_chains" in - let zero_sig := fresh "zero_sig" in - let one_sig := fresh "one_sig" in - let a24_sig := fresh "a24_sig" in - let add_sig := fresh "add_sig" in - let sub_sig := fresh "sub_sig" in - let opp_sig := fresh "opp_sig" in - let half_sz := fresh "half_sz" in - let half_sz_nonzero := fresh "half_sz_nonzero" in - let sqrt_s := fresh "sqrt_s" in - let goldilocks_mul_sig := fresh "goldilocks_mul_sig" in - let mul_sig := fresh "mul_sig" in - let square_sig := fresh "square_sig" in - let carry_sig := fresh "carry_sig" in - let wt_pos := fresh "wt_pos" in - let wt_multiples := fresh "wt_multiples" in - let freeze_sig := fresh "freeze_sig" in - let ring := fresh "ring" in - let sz := pose_sz sz in - let bitwidth := pose_bitwidth bitwidth in - let s := pose_s s in - let c := pose_c c in - let carry_chains := pose_carry_chains carry_chains in - let a24 := pose_a24 a24 in - let coef_div_modulus := pose_coef_div_modulus coef_div_modulus in - let goldilocks := pose_goldilocks goldilocks in - let m := pose_m s c m in - let wt := pose_wt m sz wt in - let sz2 := pose_sz2 sz sz2 in - let m_enc := pose_m_enc sz s c wt m_enc in - let coef := pose_coef sz wt m_enc coef_div_modulus coef in - let coef_mod := pose_coef_mod sz wt m coef coef_mod in - let sz_nonzero := pose_sz_nonzero sz sz_nonzero in - let wt_nonzero := pose_wt_nonzero wt wt_nonzero in - let wt_nonneg := pose_wt_nonneg wt wt_nonneg in - let wt_divides := pose_wt_divides wt wt_divides in - let wt_divides' := pose_wt_divides' wt wt_divides wt_divides' in - let wt_divides_chains := pose_wt_divides_chains wt carry_chains wt_divides' wt_divides_chains in - let zero_sig := pose_zero_sig sz m wt zero_sig in - let one_sig := pose_one_sig sz m wt one_sig in - let a24_sig := pose_a24_sig sz m wt a24 a24_sig in - let add_sig := pose_add_sig sz m wt wt_nonzero add_sig in - let sub_sig := pose_sub_sig sz m wt wt_nonzero coef sub_sig in - let opp_sig := pose_opp_sig sz m wt wt_nonzero coef opp_sig in - let half_sz := pose_half_sz sz half_sz in - let half_sz_nonzero := pose_half_sz_nonzero half_sz half_sz_nonzero in - let sqrt_s := pose_sqrt_s s sqrt_s in - let goldilocks_mul_sig := pose_goldilocks_mul_sig goldilocks sz wt s c half_sz sqrt_s goldilocks_mul_sig in - let mul_sig := pose_mul_sig_full goldilocks sz m wt s c sz2 half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig in - let square_sig := pose_square_sig_full goldilocks sz m wt s c sz2 wt_nonzero mul_sig square_sig in - let carry_sig := pose_carry_sig sz m wt s c carry_chains wt_nonzero wt_divides_chains carry_sig in - let wt_pos := pose_wt_pos wt wt_pos in - let wt_multiples := pose_wt_multiples wt wt_multiples in - let freeze_sig := pose_freeze_sig sz m wt c m_enc bitwidth wt_nonzero wt_pos wt_divides wt_multiples freeze_sig in - let ring := pose_ring sz m wt wt_divides' sz_nonzero wt_nonzero zero_sig one_sig opp_sig add_sig sub_sig mul_sig ring in - constr:((sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring)). - - Ltac make_ArithmeticSynthesis_package _ := - lazymatch goal with - | [ |- { T : _ & T } ] => eexists - | [ |- _ ] => idtac - end; - let pkg := get_ArithmeticSynthesis_package () in - exact pkg. -End MakeArithmeticSynthesisTestTactics. - -Module Type ArithmeticSynthesisPrePackage. - Parameter ArithmeticSynthesis_package' : { T : _ & T }. - Parameter ArithmeticSynthesis_package : projT1 ArithmeticSynthesis_package'. -End ArithmeticSynthesisPrePackage. - -Module MakeArithmeticSynthesisTest (AP : ArithmeticSynthesisPrePackage). - Ltac get_MakeArithmeticSynthesisTest_package _ := eval hnf in AP.ArithmeticSynthesis_package. - Ltac AS_reduce_proj x := - eval cbv beta iota zeta in x. - - Ltac get_sz _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz). - Notation sz := (ltac:(let v := get_sz () in exact v)) (only parsing). - Ltac get_bitwidth _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in bitwidth). - Notation bitwidth := (ltac:(let v := get_bitwidth () in exact v)) (only parsing). - Ltac get_s _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in s). - Notation s := (ltac:(let v := get_s () in exact v)) (only parsing). - Ltac get_c _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in c). - Notation c := (ltac:(let v := get_c () in exact v)) (only parsing). - Ltac get_carry_chains _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_chains). - Notation carry_chains := (ltac:(let v := get_carry_chains () in exact v)) (only parsing). - Ltac get_a24 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in a24). - Notation a24 := (ltac:(let v := get_a24 () in exact v)) (only parsing). - Ltac get_coef_div_modulus _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef_div_modulus). - Notation coef_div_modulus := (ltac:(let v := get_coef_div_modulus () in exact v)) (only parsing). - Ltac get_goldilocks _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in goldilocks). - Notation goldilocks := (ltac:(let v := get_goldilocks () in exact v)) (only parsing). - Ltac get_m _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in m). - Notation m := (ltac:(let v := get_m () in exact v)) (only parsing). - Ltac get_wt _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt). - Notation wt := (ltac:(let v := get_wt () in exact v)) (only parsing). - Ltac get_sz2 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz2). - Notation sz2 := (ltac:(let v := get_sz2 () in exact v)) (only parsing). - Ltac get_m_enc _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in m_enc). - Notation m_enc := (ltac:(let v := get_m_enc () in exact v)) (only parsing). - Ltac get_coef _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef). - Notation coef := (ltac:(let v := get_coef () in exact v)) (only parsing). - Ltac get_coef_mod _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef_mod). - Notation coef_mod := (ltac:(let v := get_coef_mod () in exact v)) (only parsing). - Ltac get_sz_nonzero _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz_nonzero). - Notation sz_nonzero := (ltac:(let v := get_sz_nonzero () in exact v)) (only parsing). - Ltac get_wt_nonzero _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_nonzero). - Notation wt_nonzero := (ltac:(let v := get_wt_nonzero () in exact v)) (only parsing). - Ltac get_wt_nonneg _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_nonneg). - Notation wt_nonneg := (ltac:(let v := get_wt_nonneg () in exact v)) (only parsing). - Ltac get_wt_divides _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides). - Notation wt_divides := (ltac:(let v := get_wt_divides () in exact v)) (only parsing). - Ltac get_wt_divides' _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides'). - Notation wt_divides' := (ltac:(let v := get_wt_divides' () in exact v)) (only parsing). - Ltac get_wt_divides_chains _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides_chains). - Notation wt_divides_chains := (ltac:(let v := get_wt_divides_chains () in exact v)) (only parsing). - Ltac get_zero_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in zero_sig). - Notation zero_sig := (ltac:(let v := get_zero_sig () in exact v)) (only parsing). - Ltac get_one_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in one_sig). - Notation one_sig := (ltac:(let v := get_one_sig () in exact v)) (only parsing). - Ltac get_a24_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in a24_sig). - Notation a24_sig := (ltac:(let v := get_a24_sig () in exact v)) (only parsing). - Ltac get_add_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in add_sig). - Notation add_sig := (ltac:(let v := get_add_sig () in exact v)) (only parsing). - Ltac get_sub_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sub_sig). - Notation sub_sig := (ltac:(let v := get_sub_sig () in exact v)) (only parsing). - Ltac get_opp_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in opp_sig). - Notation opp_sig := (ltac:(let v := get_opp_sig () in exact v)) (only parsing). - Ltac get_half_sz _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in half_sz). - Notation half_sz := (ltac:(let v := get_half_sz () in exact v)) (only parsing). - Ltac get_half_sz_nonzero _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in half_sz_nonzero). - Notation half_sz_nonzero := (ltac:(let v := get_half_sz_nonzero () in exact v)) (only parsing). - Ltac get_sqrt_s _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sqrt_s). - Notation sqrt_s := (ltac:(let v := get_sqrt_s () in exact v)) (only parsing). - Ltac get_mul_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in mul_sig). - Notation mul_sig := (ltac:(let v := get_mul_sig () in exact v)) (only parsing). - Ltac get_square_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in square_sig). - Notation square_sig := (ltac:(let v := get_square_sig () in exact v)) (only parsing). - Ltac get_carry_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_sig). - Notation carry_sig := (ltac:(let v := get_carry_sig () in exact v)) (only parsing). - Ltac get_wt_pos _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_pos). - Notation wt_pos := (ltac:(let v := get_wt_pos () in exact v)) (only parsing). - Ltac get_wt_multiples _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_multiples). - Notation wt_multiples := (ltac:(let v := get_wt_multiples () in exact v)) (only parsing). - Ltac get_freeze_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in freeze_sig). - Notation freeze_sig := (ltac:(let v := get_freeze_sig () in exact v)) (only parsing). - Ltac get_ring _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in ring). - Notation ring := (ltac:(let v := get_ring () in exact v)) (only parsing). -End MakeArithmeticSynthesisTest. diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v index 2d0bf5152..7078d4bec 100644 --- a/src/Specific/Framework/CurveParameters.v +++ b/src/Specific/Framework/CurveParameters.v @@ -1,6 +1,8 @@ Require Export Coq.ZArith.BinInt. Require Export Coq.Lists.List. Require Export Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.Tactics.CacheTerm. +Require Import Crypto.Util.TagList. Require Crypto.Util.Tuple. Module Export Notations. @@ -23,7 +25,7 @@ Module Type CurveParameters. Parameter carry_chains : option (list (list nat)). (* defaults to [seq 0 (pred sz) :: (0 :: 1 :: nil) :: nil] *) Parameter a24 : option Z. - Parameter coef_div_modulus : nat. + Parameter coef_div_modulus : option nat. Parameter goldilocks : bool. @@ -35,10 +37,15 @@ Module Type CurveParameters. : option (list nat). (* defaults to [bitwidth :: 2*bitwidth :: nil] *) Parameter freeze_extra_allowable_bit_widths : option (list nat). (* defaults to [8 :: nil] *) + Parameter modinv_fuel : option nat. Ltac extra_prove_mul_eq := idtac. Ltac extra_prove_square_eq := idtac. 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. +End TAG. + Module FillCurveParameters (P : CurveParameters). Local Notation defaulted opt_v default := (match opt_v with @@ -56,7 +63,7 @@ Module FillCurveParameters (P : CurveParameters). Definition c := P.c. Definition carry_chains := defaulted P.carry_chains [seq 0 (pred sz); [0; 1]]%nat. Definition a24 := defaulted P.a24 0. - Definition coef_div_modulus := P.coef_div_modulus. + Definition coef_div_modulus := defaulted P.coef_div_modulus 0%nat. Definition goldilocks := P.goldilocks. @@ -74,11 +81,23 @@ Module FillCurveParameters (P : CurveParameters). end. Definition upper_bound_of_exponent - := defaulted P.upper_bound_of_exponent (fun exp => (2^exp + 2^(exp-3))%Z). + := defaulted P.upper_bound_of_exponent + (fun exp => (2^exp + 2^(exp-3))%Z). + Local Notation list_8_if_not_exists ls := + (if existsb (Nat.eqb 8) ls + then nil + else [8]%nat) + (only parsing). Definition allowable_bit_widths - := defaulted P.allowable_bit_widths (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil)%nat. + := defaulted + P.allowable_bit_widths + (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil)%nat. Definition freeze_allowable_bit_widths - := defaulted P.freeze_extra_allowable_bit_widths [8]%nat ++ allowable_bit_widths. + := defaulted + P.freeze_extra_allowable_bit_widths + (list_8_if_not_exists allowable_bit_widths) + ++ allowable_bit_widths. + Definition modinv_fuel := defaulted P.modinv_fuel 10%nat. (* hack around https://coq.inria.fr/bugs/show_bug.cgi?id=5764 *) Ltac do_unfold v' := @@ -95,10 +114,11 @@ Module FillCurveParameters (P : CurveParameters). let P_upper_bound_of_exponent := P.upper_bound_of_exponent in let P_allowable_bit_widths := P.allowable_bit_widths in let P_freeze_extra_allowable_bit_widths := P.freeze_extra_allowable_bit_widths in + 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 - P_sz P_bitwidth P_s P_c P_carry_chains P_a24 P_coef_div_modulus P_goldilocks + 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 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 @@ -112,4 +132,131 @@ Module FillCurveParameters (P : CurveParameters). (only parsing). Ltac extra_prove_mul_eq := P.extra_prove_mul_eq. Ltac extra_prove_square_eq := P.extra_prove_square_eq. -End FillCurveParameters. + + Local Notation P_sz := sz. + Local Notation P_bitwidth := bitwidth. + Local Notation P_s := s. + Local Notation P_c := c. + Local Notation P_carry_chains := carry_chains. + Local Notation P_a24 := a24. + Local Notation P_coef_div_modulus := coef_div_modulus. + Local Notation P_goldilocks := goldilocks. + 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. + Local Notation P_modinv_fuel := modinv_fuel. + + Ltac pose_sz sz := + cache_term_with_type_by + nat + ltac:(let v := do_compute P_sz in exact v) + sz. + Ltac pose_bitwidth bitwidth := + cache_term_with_type_by + Z + ltac:(let v := do_compute P_bitwidth in exact v) + bitwidth. + Ltac pose_s s := (* don't want to compute, e.g., [2^255] *) + cache_term_with_type_by + Z + ltac:(let v := do_unfold P_s in exact v) + s. + Ltac pose_c c := + cache_term_with_type_by + (list limb) + ltac:(let v := do_compute P_c in exact v) + c. + Ltac pose_carry_chains carry_chains := + let v := do_compute P_carry_chains in + cache_term v carry_chains. + + Ltac pose_a24 a24 := + let v := do_compute P_a24 in + cache_term v a24. + Ltac pose_coef_div_modulus coef_div_modulus := + cache_term_with_type_by + nat + ltac:(let v := do_compute P_coef_div_modulus in exact v) + coef_div_modulus. + Ltac pose_goldilocks goldilocks := + cache_term_with_type_by + bool + ltac:(let v := do_compute P_goldilocks in exact v) + goldilocks. + + Ltac pose_modinv_fuel modinv_fuel := + cache_term_with_type_by + nat + ltac:(let v := do_compute P_modinv_fuel in exact v) + modinv_fuel. + + Ltac pose_upper_bound_of_exponent upper_bound_of_exponent := + cache_term_with_type_by + (Z -> Z) + ltac:(let v := do_unfold P_upper_bound_of_exponent in exact v) + upper_bound_of_exponent. + + (* Everything below this line autogenerated by remake_packages.py *) + Ltac add_sz pkg := + let sz := fresh "sz" in + let sz := pose_sz sz in + Tag.update pkg TAG.sz sz. + + Ltac add_bitwidth pkg := + let bitwidth := fresh "bitwidth" in + let bitwidth := pose_bitwidth bitwidth in + Tag.update pkg TAG.bitwidth bitwidth. + + Ltac add_s pkg := + let s := fresh "s" in + let s := pose_s s in + Tag.update pkg TAG.s s. + + Ltac add_c pkg := + let c := fresh "c" in + let c := pose_c c in + Tag.update pkg TAG.c c. + + Ltac add_carry_chains pkg := + let carry_chains := fresh "carry_chains" in + let carry_chains := pose_carry_chains carry_chains in + Tag.update pkg TAG.carry_chains carry_chains. + + Ltac add_a24 pkg := + let a24 := fresh "a24" in + let a24 := pose_a24 a24 in + Tag.update pkg TAG.a24 a24. + + Ltac add_coef_div_modulus pkg := + let coef_div_modulus := fresh "coef_div_modulus" in + let coef_div_modulus := pose_coef_div_modulus coef_div_modulus in + Tag.update pkg TAG.coef_div_modulus coef_div_modulus. + + Ltac add_goldilocks pkg := + let goldilocks := fresh "goldilocks" in + let goldilocks := pose_goldilocks goldilocks in + Tag.update pkg TAG.goldilocks goldilocks. + + Ltac add_modinv_fuel pkg := + let modinv_fuel := fresh "modinv_fuel" in + let modinv_fuel := pose_modinv_fuel modinv_fuel in + Tag.update pkg TAG.modinv_fuel modinv_fuel. + + Ltac add_upper_bound_of_exponent pkg := + let upper_bound_of_exponent := fresh "upper_bound_of_exponent" in + let upper_bound_of_exponent := pose_upper_bound_of_exponent upper_bound_of_exponent in + Tag.update pkg TAG.upper_bound_of_exponent upper_bound_of_exponent. + + Ltac add_CurveParameters_package pkg := + let pkg := add_sz pkg in + let pkg := add_bitwidth pkg in + let pkg := add_s pkg in + let pkg := add_c pkg in + let pkg := add_carry_chains pkg in + let pkg := add_a24 pkg in + let pkg := add_coef_div_modulus pkg in + let pkg := add_goldilocks pkg in + let pkg := add_modinv_fuel pkg in + let pkg := add_upper_bound_of_exponent pkg in + Tag.strip_local pkg. +End FillCurveParameters.
\ No newline at end of file diff --git a/src/Specific/Framework/CurveParametersPackage.v b/src/Specific/Framework/CurveParametersPackage.v new file mode 100644 index 000000000..782ccdd22 --- /dev/null +++ b/src/Specific/Framework/CurveParametersPackage.v @@ -0,0 +1,38 @@ +(* This file is autogenerated from CurveParameters.v by remake_packages.py *) +Require Export Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Specific.Framework.Packages. +Require Import Crypto.Util.TagList. + +Ltac if_goldilocks pkg tac_true tac_false arg := + let goldilocks := Tag.get pkg TAG.goldilocks in + let goldilocks := (eval vm_compute in (goldilocks : bool)) in + lazymatch goldilocks with + | true => tac_true arg + | false => tac_false arg + end. + + +Module MakeCurveParametersPackage (PKG : PrePackage). + Module Import MakeCurveParametersPackageInternal := MakePackageBase PKG. + + Ltac get_sz _ := get TAG.sz. + Notation sz := (ltac:(let v := get_sz () in exact v)) (only parsing). + Ltac get_bitwidth _ := get TAG.bitwidth. + Notation bitwidth := (ltac:(let v := get_bitwidth () in exact v)) (only parsing). + Ltac get_s _ := get TAG.s. + Notation s := (ltac:(let v := get_s () in exact v)) (only parsing). + Ltac get_c _ := get TAG.c. + Notation c := (ltac:(let v := get_c () in exact v)) (only parsing). + Ltac get_carry_chains _ := get TAG.carry_chains. + Notation carry_chains := (ltac:(let v := get_carry_chains () in exact v)) (only parsing). + Ltac get_a24 _ := get TAG.a24. + Notation a24 := (ltac:(let v := get_a24 () in exact v)) (only parsing). + Ltac get_coef_div_modulus _ := get TAG.coef_div_modulus. + 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_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. + Notation upper_bound_of_exponent := (ltac:(let v := get_upper_bound_of_exponent () in exact v)) (only parsing). +End MakeCurveParametersPackage. diff --git a/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v index 41bef884c..687af2c9c 100644 --- a/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v +++ b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v @@ -2,9 +2,12 @@ Require Import Coq.ZArith.BinInt. Require Import Coq.Classes.Morphisms. Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.BoundedWord. Require Import Crypto.Util.Sigma.Lift. Require Import Crypto.Util.Sigma.Associativity. Require Import Crypto.Util.Sigma.MapProjections. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. @@ -286,3 +289,6 @@ Ltac factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t := repeat match goal with | [ H : feBW_small |- _ ] => destruct H as [? _] end ]. + +Ltac op_sig_side_conditions_t _ := + try (hnf; rewrite <- (ZRange.is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. diff --git a/src/Specific/Framework/Packages.v b/src/Specific/Framework/Packages.v new file mode 100644 index 000000000..14b02b766 --- /dev/null +++ b/src/Specific/Framework/Packages.v @@ -0,0 +1,12 @@ +Require Import Crypto.Util.TagList. + +Module Type PrePackage. + Parameter package : Tag.Context. +End PrePackage. + +Module MakePackageBase (PKG : PrePackage). + Ltac get_package _ := eval hnf in PKG.package. + Ltac get key := + let pkg := get_package () in + Tag.get pkg key. +End MakePackageBase. diff --git a/src/Specific/Framework/ReificationTypes.v b/src/Specific/Framework/ReificationTypes.v index 3a160e04d..872005958 100644 --- a/src/Specific/Framework/ReificationTypes.v +++ b/src/Specific/Framework/ReificationTypes.v @@ -15,7 +15,7 @@ Require Import Crypto.Util.Decidable. Require Import Crypto.Util.Tactics.PoseTermWithName. Require Import Crypto.Util.Tactics.CacheTerm. -Ltac pose_limb_widths wt sz limb_widths := +Ltac pose_local_limb_widths wt sz limb_widths := pose_term_with ltac:(fun _ => (eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)))) limb_widths. @@ -26,31 +26,40 @@ Ltac get_b_of upper_bound_of_exponent := (* The definition [bounds_exp] is a tuple-version of the limb-widths, which are the [exp] argument in [b_of] above, i.e., the approximate base-2 exponent of the bounds on the limb in that position. *) -Ltac pose_bounds_exp sz limb_widths bounds_exp := +Ltac pose_local_bounds_exp sz limb_widths bounds_exp := pose_term_with_type (Tuple.tuple Z sz) ltac:(fun _ => eval compute in (Tuple.from_list sz limb_widths eq_refl)) bounds_exp. -Ltac pose_bounds sz b_of bounds_exp bounds := +Ltac pose_local_bounds sz upper_bound_of_exponent bounds_exp bounds := + let b_of := get_b_of upper_bound_of_exponent in pose_term_with_type (Tuple.tuple zrange sz) ltac:(fun _ => eval compute in (Tuple.map (fun e => b_of e) bounds_exp)) bounds. -Ltac pose_lgbitwidth limb_widths lgbitwidth := +Ltac pose_bound1 r bound1 := + cache_term_with_type_by + zrange + ltac:(exact {| lower := 0 ; upper := Z.pos r-1 |}) + bound1. + +Ltac pose_local_lgbitwidth limb_widths lgbitwidth := pose_term_with ltac:(fun _ => eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths)))) lgbitwidth. -Ltac pose_bitwidth lgbitwidth bitwidth := +Ltac pose_local_adjusted_bitwidth' lgbitwidth adjusted_bitwidth' := pose_term_with ltac:(fun _ => eval compute in (2^lgbitwidth)%nat) - bitwidth. + adjusted_bitwidth'. +Ltac pose_adjusted_bitwidth adjusted_bitwidth' adjusted_bitwidth := + cache_term adjusted_bitwidth' adjusted_bitwidth. -Ltac pose_feZ sz feZ := +Ltac pose_local_feZ sz feZ := pose_term_with ltac:(fun _ => constr:(tuple Z sz)) feZ. @@ -65,20 +74,20 @@ Ltac pose_feW_bounded feW bounds feW_bounded := (feW -> Prop) ltac:(let v := eval cbv [bounds] in (fun w : feW => is_bounded_by None bounds (map wordToZ w)) in exact_no_check v) feW_bounded. -Ltac pose_feBW sz bitwidth bounds feBW := +Ltac pose_feBW sz adjusted_bitwidth' bounds feBW := cache_term_with_type_by Type - ltac:(let v := eval cbv [bitwidth bounds] in (BoundedWord sz bitwidth bounds) in exact v) + ltac:(let v := eval cbv [adjusted_bitwidth' bounds] in (BoundedWord sz adjusted_bitwidth' bounds) in exact v) feBW. Lemma feBW_bounded_helper' - sz bitwidth bounds - (feBW := BoundedWord sz bitwidth bounds) + sz adjusted_bitwidth' bounds + (feBW := BoundedWord sz adjusted_bitwidth' bounds) (wt : nat -> Z) (Hwt : forall i, 0 <= wt i) : forall (a : feBW), B.Positional.eval wt (map lower bounds) - <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) + <= B.Positional.eval wt (BoundedWordToZ sz adjusted_bitwidth' bounds a) <= B.Positional.eval wt (map upper bounds). Proof. let a := fresh "a" in @@ -105,15 +114,15 @@ Proof. nia. } } Qed. Lemma feBW_bounded_helper - sz bitwidth bounds - (feBW := BoundedWord sz bitwidth bounds) + sz adjusted_bitwidth' bounds + (feBW := BoundedWord sz adjusted_bitwidth' bounds) (wt : nat -> Z) (Hwt : forall i, 0 <= wt i) l u : l <= B.Positional.eval wt (map lower bounds) /\ B.Positional.eval wt (map upper bounds) < u -> forall (a : feBW), - l <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < u. + l <= B.Positional.eval wt (BoundedWordToZ sz adjusted_bitwidth' bounds a) < u. Proof. intros [Hl Hu] a; split; [ eapply Z.le_trans | eapply Z.le_lt_trans ]; @@ -121,10 +130,10 @@ Proof. assumption. Qed. -Ltac pose_feBW_bounded wt sz feBW bitwidth bounds m wt_nonneg feBW_bounded := +Ltac pose_feBW_bounded wt sz feBW adjusted_bitwidth' bounds m wt_nonneg feBW_bounded := cache_proof_with_type_by - (forall a : feBW, 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m) - ltac:(apply (@feBW_bounded_helper sz bitwidth bounds wt wt_nonneg); + (forall a : feBW, 0 <= B.Positional.eval wt (BoundedWordToZ sz adjusted_bitwidth' bounds a) < 2 * Z.pos m) + ltac:(apply (@feBW_bounded_helper sz adjusted_bitwidth' bounds wt wt_nonneg); vm_compute; clear; split; congruence) feBW_bounded. @@ -138,70 +147,3 @@ Ltac pose_phiBW feBW m wt phiBW := (feBW -> F m) ltac:(exact (fun x : feBW => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x))) phiBW. - -Ltac get_ReificationTypes_package wt sz m wt_nonneg upper_bound_of_exponent := - let limb_widths := fresh "limb_widths" in - let bounds_exp := fresh "bounds_exp" in - let bounds := fresh "bounds" in - let lgbitwidth := fresh "lgbitwidth" in - let bitwidth := fresh "bitwidth" in - let feZ := fresh "feZ" in - let feW := fresh "feW" in - let feW_bounded := fresh "feW_bounded" in - let feBW := fresh "feBW" in - let feBW_bounded := fresh "feBW_bounded" in - let phiW := fresh "phiW" in - let phiBW := fresh "phiBW" in - let limb_widths := pose_limb_widths wt sz limb_widths in - let b_of := get_b_of upper_bound_of_exponent in - let bounds_exp := pose_bounds_exp sz limb_widths bounds_exp in - let bounds := pose_bounds sz b_of bounds_exp bounds in - let lgbitwidth := pose_lgbitwidth limb_widths lgbitwidth in - let bitwidth := pose_bitwidth lgbitwidth bitwidth in - let feZ := pose_feZ sz feZ in - let feW := pose_feW sz lgbitwidth feW in - let feW_bounded := pose_feW_bounded feW bounds feW_bounded in - let feBW := pose_feBW sz bitwidth bounds feBW in - let feBW_bounded := pose_feBW_bounded wt sz feBW bitwidth bounds m wt_nonneg feBW_bounded in - let phiW := pose_phiW feW m wt phiW in - let phiBW := pose_phiBW feBW m wt phiBW in - constr:((feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW)). -Ltac make_ReificationTypes_package wt sz m wt_nonneg upper_bound_of_exponent := - lazymatch goal with - | [ |- { T : _ & T } ] => eexists - | [ |- _ ] => idtac - end; - let pkg := get_ReificationTypes_package wt sz m wt_nonneg upper_bound_of_exponent in - exact pkg. - -Module Type ReificationTypesPrePackage. - Parameter ReificationTypes_package' : { T : _ & T }. - Parameter ReificationTypes_package : projT1 ReificationTypes_package'. -End ReificationTypesPrePackage. - -Module MakeReificationTypes (RP : ReificationTypesPrePackage). - Ltac get_ReificationTypes_package _ := eval hnf in RP.ReificationTypes_package. - Ltac RT_reduce_proj x := - eval cbv beta iota zeta in x. - (** -<< -terms = 'feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW' -for i in terms.split(', '): - print(" Ltac get_%s _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(%s) := pkg in %s)." % (i, terms, i)) - print(" Notation %s := (ltac:(let v := get_%s () in exact v)) (only parsing)." % (i, i)) ->> *) - Ltac get_feZ _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feZ). - Notation feZ := (ltac:(let v := get_feZ () in exact v)) (only parsing). - Ltac get_feW _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feW). - Notation feW := (ltac:(let v := get_feW () in exact v)) (only parsing). - Ltac get_feW_bounded _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feW_bounded). - Notation feW_bounded := (ltac:(let v := get_feW_bounded () in exact v)) (only parsing). - Ltac get_feBW _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feBW). - Notation feBW := (ltac:(let v := get_feBW () in exact v)) (only parsing). - Ltac get_feBW_bounded _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in feBW_bounded). - Notation feBW_bounded := (ltac:(let v := get_feBW_bounded () in exact v)) (only parsing). - Ltac get_phiW _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in phiW). - Notation phiW := (ltac:(let v := get_phiW () in exact v)) (only parsing). - Ltac get_phiBW _ := let pkg := get_ReificationTypes_package () in RT_reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := pkg in phiBW). - Notation phiBW := (ltac:(let v := get_phiBW () in exact v)) (only parsing). -End MakeReificationTypes. diff --git a/src/Specific/Framework/ReificationTypesPackage.v b/src/Specific/Framework/ReificationTypesPackage.v new file mode 100644 index 000000000..4a868856e --- /dev/null +++ b/src/Specific/Framework/ReificationTypesPackage.v @@ -0,0 +1,151 @@ +(* This file is autogenerated from ReificationTypes.v by remake_packages.py *) +Require Import Crypto.Specific.Framework.CurveParametersPackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage. +Require Export Crypto.Specific.Framework.ReificationTypes. +Require Import Crypto.Specific.Framework.Packages. +Require Import Crypto.Util.TagList. + +Module TAG. + Inductive tags := limb_widths | bounds_exp | bounds | bound1 | lgbitwidth | adjusted_bitwidth' | adjusted_bitwidth | feZ | feW | feW_bounded | feBW | feBW_bounded | phiW | phiBW. +End TAG. + +Ltac add_limb_widths pkg := + let wt := Tag.get pkg TAG.wt in + let sz := Tag.get pkg TAG.sz in + let limb_widths := fresh "limb_widths" in + let limb_widths := pose_local_limb_widths wt sz limb_widths in + Tag.local_update pkg TAG.limb_widths limb_widths. + +Ltac add_bounds_exp pkg := + let sz := Tag.get pkg TAG.sz in + let limb_widths := Tag.get pkg TAG.limb_widths in + let bounds_exp := fresh "bounds_exp" in + let bounds_exp := pose_local_bounds_exp sz limb_widths bounds_exp in + Tag.local_update pkg TAG.bounds_exp bounds_exp. + +Ltac add_bounds pkg := + let sz := Tag.get pkg TAG.sz in + let upper_bound_of_exponent := Tag.get pkg TAG.upper_bound_of_exponent in + let bounds_exp := Tag.get pkg TAG.bounds_exp in + let bounds := fresh "bounds" in + let bounds := pose_local_bounds sz upper_bound_of_exponent bounds_exp bounds in + Tag.local_update pkg TAG.bounds bounds. + +Ltac add_bound1 pkg := + let r := Tag.get pkg TAG.r in + let bound1 := fresh "bound1" in + let bound1 := pose_bound1 r bound1 in + Tag.update pkg TAG.bound1 bound1. + +Ltac add_lgbitwidth pkg := + let limb_widths := Tag.get pkg TAG.limb_widths in + let lgbitwidth := fresh "lgbitwidth" in + let lgbitwidth := pose_local_lgbitwidth limb_widths lgbitwidth in + Tag.local_update pkg TAG.lgbitwidth lgbitwidth. + +Ltac add_adjusted_bitwidth' pkg := + let lgbitwidth := Tag.get pkg TAG.lgbitwidth in + let adjusted_bitwidth' := fresh "adjusted_bitwidth'" in + let adjusted_bitwidth' := pose_local_adjusted_bitwidth' lgbitwidth adjusted_bitwidth' in + Tag.local_update pkg TAG.adjusted_bitwidth' adjusted_bitwidth'. + +Ltac add_adjusted_bitwidth pkg := + let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in + let adjusted_bitwidth := fresh "adjusted_bitwidth" in + let adjusted_bitwidth := pose_adjusted_bitwidth adjusted_bitwidth' adjusted_bitwidth in + Tag.update pkg TAG.adjusted_bitwidth adjusted_bitwidth. + +Ltac add_feZ pkg := + let sz := Tag.get pkg TAG.sz in + let feZ := fresh "feZ" in + let feZ := pose_local_feZ sz feZ in + Tag.local_update pkg TAG.feZ feZ. + +Ltac add_feW pkg := + let sz := Tag.get pkg TAG.sz in + let lgbitwidth := Tag.get pkg TAG.lgbitwidth in + let feW := fresh "feW" in + let feW := pose_feW sz lgbitwidth feW in + Tag.update pkg TAG.feW feW. + +Ltac add_feW_bounded pkg := + let feW := Tag.get pkg TAG.feW in + let bounds := Tag.get pkg TAG.bounds in + let feW_bounded := fresh "feW_bounded" in + let feW_bounded := pose_feW_bounded feW bounds feW_bounded in + Tag.update pkg TAG.feW_bounded feW_bounded. + +Ltac add_feBW pkg := + let sz := Tag.get pkg TAG.sz in + let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in + let bounds := Tag.get pkg TAG.bounds in + let feBW := fresh "feBW" in + let feBW := pose_feBW sz adjusted_bitwidth' bounds feBW in + Tag.update pkg TAG.feBW feBW. + +Ltac add_feBW_bounded pkg := + let wt := Tag.get pkg TAG.wt in + let sz := Tag.get pkg TAG.sz in + let feBW := Tag.get pkg TAG.feBW in + let adjusted_bitwidth' := Tag.get pkg TAG.adjusted_bitwidth' in + let bounds := Tag.get pkg TAG.bounds in + let m := Tag.get pkg TAG.m in + let wt_nonneg := Tag.get pkg TAG.wt_nonneg in + let feBW_bounded := fresh "feBW_bounded" in + let feBW_bounded := pose_feBW_bounded wt sz feBW adjusted_bitwidth' bounds m wt_nonneg feBW_bounded in + Tag.update pkg TAG.feBW_bounded feBW_bounded. + +Ltac add_phiW pkg := + let feW := Tag.get pkg TAG.feW in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let phiW := fresh "phiW" in + let phiW := pose_phiW feW m wt phiW in + Tag.update pkg TAG.phiW phiW. + +Ltac add_phiBW pkg := + let feBW := Tag.get pkg TAG.feBW in + let m := Tag.get pkg TAG.m in + let wt := Tag.get pkg TAG.wt in + let phiBW := fresh "phiBW" in + let phiBW := pose_phiBW feBW m wt phiBW in + Tag.update pkg TAG.phiBW phiBW. + +Ltac add_ReificationTypes_package pkg := + let pkg := add_limb_widths pkg in + let pkg := add_bounds_exp pkg in + let pkg := add_bounds pkg in + let pkg := add_bound1 pkg in + let pkg := add_lgbitwidth pkg in + let pkg := add_adjusted_bitwidth' pkg in + let pkg := add_adjusted_bitwidth pkg in + let pkg := add_feZ pkg in + let pkg := add_feW pkg in + let pkg := add_feW_bounded pkg in + let pkg := add_feBW pkg in + let pkg := add_feBW_bounded pkg in + let pkg := add_phiW pkg in + let pkg := add_phiBW pkg in + Tag.strip_local pkg. + + +Module MakeReificationTypesPackage (PKG : PrePackage). + Module Import MakeReificationTypesPackageInternal := MakePackageBase PKG. + + Ltac get_bound1 _ := get TAG.bound1. + Notation bound1 := (ltac:(let v := get_bound1 () in exact v)) (only parsing). + Ltac get_adjusted_bitwidth _ := get TAG.adjusted_bitwidth. + Notation adjusted_bitwidth := (ltac:(let v := get_adjusted_bitwidth () in exact v)) (only parsing). + Ltac get_feW _ := get TAG.feW. + Notation feW := (ltac:(let v := get_feW () in exact v)) (only parsing). + Ltac get_feW_bounded _ := get TAG.feW_bounded. + Notation feW_bounded := (ltac:(let v := get_feW_bounded () in exact v)) (only parsing). + Ltac get_feBW _ := get TAG.feBW. + Notation feBW := (ltac:(let v := get_feBW () in exact v)) (only parsing). + Ltac get_feBW_bounded _ := get TAG.feBW_bounded. + Notation feBW_bounded := (ltac:(let v := get_feBW_bounded () in exact v)) (only parsing). + Ltac get_phiW _ := get TAG.phiW. + Notation phiW := (ltac:(let v := get_phiW () in exact v)) (only parsing). + Ltac get_phiBW _ := get TAG.phiBW. + Notation phiBW := (ltac:(let v := get_phiBW () in exact v)) (only parsing). +End MakeReificationTypesPackage. diff --git a/src/Specific/Framework/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v index 9c80efaa0..617a36212 100644 --- a/src/Specific/Framework/SynthesisFramework.v +++ b/src/Specific/Framework/SynthesisFramework.v @@ -1,72 +1,76 @@ -Require Import Crypto.Specific.Framework.ArithmeticSynthesisFramework. -Require Import Crypto.Specific.Framework.ReificationTypes. -Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework. +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.KaratsubaPackage. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.LadderstepPackage. +Require Import Crypto.Specific.Framework.CurveParametersPackage. +Require Import Crypto.Specific.Framework.ReificationTypesPackage. +Require Import Crypto.Specific.Framework.Packages. Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import Crypto.Util.BoundedWord. +Require Import Crypto.Util.TagList. +Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. -Require Crypto.Specific.Framework.CurveParameters. Module Export Exports. - Export ArithmeticSynthesisFramework.Exports. + Export ArithmeticSynthesis.Defaults.Exports. + Export ArithmeticSynthesis.Freeze.Exports. End Exports. -Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters). - Module AS := MakeArithmeticSynthesisTestTactics Curve. +(* Alisases for exporting *) +Module Type PrePackage := PrePackage. +Module Tag. + Notation Context := Tag.Context (only parsing). +End Tag. - Ltac get_synthesis_package _ := - let arithmetic_synthesis_pkg := AS.get_ArithmeticSynthesis_package () in - lazymatch arithmetic_synthesis_pkg with - | (?sz, ?bitwidth, ?s, ?c, ?carry_chains, ?a24, ?coef_div_modulus, ?goldilocks, ?m, ?wt, ?sz2, ?m_enc, ?coef, ?coef_mod, ?sz_nonzero, ?wt_nonzero, ?wt_nonneg, ?wt_divides, ?wt_divides', ?wt_divides_chains, ?zero_sig, ?one_sig, ?a24_sig, ?add_sig, ?sub_sig, ?opp_sig, ?half_sz, ?half_sz_nonzero, ?sqrt_s, ?mul_sig, ?square_sig, ?carry_sig, ?wt_pos, ?wt_multiples, ?freeze_sig, ?ring) - => let reification_types_pkg := get_ReificationTypes_package wt sz m wt_nonneg AS.P.upper_bound_of_exponent in - let ladderstep_pkg := get_Ladderstep_package sz wt m add_sig sub_sig mul_sig square_sig carry_sig in - constr:((arithmetic_synthesis_pkg, reification_types_pkg, ladderstep_pkg)) - | _ => let dummy := match goal with - | _ => fail "Did you update get_ArithmeticSynthesis_package but forget to update get_synthesis_package?" - end in - constr:(I : I) - end. - Ltac make_synthesis_package _ := - lazymatch goal with - | [ |- { T : _ & _ } ] - => first [ eexists (_, _, _) - | eexists (_, _) - | eexists ] - | [ |- _ ] => idtac - end; - let pkg := get_synthesis_package () in - exact pkg. -End MakeSynthesisTactics. +Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters). + Module P := FillCurveParameters Curve. -Local Notation eta2 x := (fst x, snd x) (only parsing). -Local Notation eta3 x := (eta2 (fst x), snd x) (only parsing). + Ltac add_Synthesis_package pkg := + let P_default_mul _ := P.default_mul in + let P_extra_prove_mul_eq _ := P.extra_prove_mul_eq in + let P_default_square _ := P.default_square in + let P_extra_prove_square_eq _ := P.extra_prove_square_eq in + let pkg := P.add_CurveParameters_package pkg in + 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_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 + (* N.B. Ladderstep must come after Defaults *) + let pkg := add_Ladderstep_package pkg in + pkg. -Notation Synthesis_package'_Type := - { ABC : _ & let '(a, b, c) := eta3 ABC in (a * b * c)%type } (only parsing). + Ltac get_Synthesis_package _ := + let pkg := constr:(Tag.empty) in + add_Synthesis_package pkg. -Module Type SynthesisPrePackage. - Parameter Synthesis_package' : Synthesis_package'_Type. - Parameter Synthesis_package : let '(a, b, c) := eta3 (projT1 Synthesis_package') in (a * b * c)%type. -End SynthesisPrePackage. + Ltac make_Synthesis_package _ := + let pkg := get_Synthesis_package () in + exact pkg. +End MakeSynthesisTactics. -Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : SynthesisPrePackage). - Module CP := CurveParameters.FillCurveParameters Curve. +Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePackage). + Module P := CurveParameters.FillCurveParameters Curve. - Module PP <: ReificationTypesPrePackage <: ArithmeticSynthesisPrePackage <: LadderstepPrePackage. - Definition ArithmeticSynthesis_package := Eval compute in let '(a, b, c) := P.Synthesis_package in a. - Definition ArithmeticSynthesis_package' : { T : _ & T } := existT _ _ ArithmeticSynthesis_package. - Definition ReificationTypes_package := Eval compute in let '(a, b, c) := P.Synthesis_package in b. - Definition ReificationTypes_package' : { T : _ & T } := existT _ _ ReificationTypes_package. - Definition Ladderstep_package := Eval compute in let '(a, b, c) := P.Synthesis_package in c. - Definition Ladderstep_package' : { T : _ & T } := existT _ _ Ladderstep_package. - End PP. - Module RT := MakeReificationTypes PP. - Module AS := MakeArithmeticSynthesisTest PP. - Module LS := MakeLadderstep PP. - Include RT. - Include AS. - Include LS. + Module CP := MakeCurveParametersPackage PKG. + Module BP := MakeBasePackage PKG. + Module DP := MakeDefaultsPackage PKG. + Module RP := MakeReificationTypesPackage PKG. + Module FP := MakeFreezePackage PKG. + Module LP := MakeLadderstepPackage PKG. + Module KP := MakeKaratsubaPackage PKG. + Include CP. + Include BP. + Include DP. + Include RP. + Include FP. + Include LP. + Include KP. Ltac synthesize_with_carry do_rewrite get_op_sig := let carry_sig := get_carry_sig () in @@ -75,7 +79,7 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : Synthesis [ do_rewrite op_sig carry_sig; cbv_runtime | .. ]; fin_preglue; - refine_reflectively_gen CP.allowable_bit_widths default. + refine_reflectively_gen P.allowable_bit_widths default. Ltac synthesize_2arg_with_carry get_op_sig := synthesize_with_carry do_rewrite_with_2sig_add_carry get_op_sig. Ltac synthesize_1arg_with_carry get_op_sig := @@ -84,6 +88,7 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : Synthesis 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_square _ := synthesize_1arg_with_carry get_square_sig. Ltac synthesize_freeze _ := let freeze_sig := get_freeze_sig () in @@ -92,7 +97,7 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : Synthesis [ do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime | .. ]; fin_preglue; - refine_reflectively_gen CP.freeze_allowable_bit_widths anf. + refine_reflectively_gen P.freeze_allowable_bit_widths anf. Ltac synthesize_xzladderstep _ := let Mxzladderstep_sig := get_Mxzladderstep_sig () in let a24_sig := get_a24_sig () in @@ -104,5 +109,6 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : Synthesis cbv_runtime | .. ]; finish_conjoined_preglue (); - refine_reflectively_gen CP.allowable_bit_widths default. + refine_reflectively_gen P.allowable_bit_widths default. + End PackageSynthesis. diff --git a/src/Specific/Framework/make_curve.py b/src/Specific/Framework/make_curve.py index 56c91e577..aeaef91db 100755 --- a/src/Specific/Framework/make_curve.py +++ b/src/Specific/Framework/make_curve.py @@ -1,6 +1,6 @@ #!/usr/bin/env python from __future__ import with_statement -import json, sys, os, math, re, shutil +import json, sys, os, math, re, shutil, io def compute_bitwidth(base): return 2**int(math.ceil(math.log(base, 2))) @@ -175,12 +175,13 @@ def nested_list_to_string(v): assert(False) def make_curve_parameters(parameters): - def fix_option(term): + def fix_option(term, scope_string=''): if not isinstance(term, str) and not isinstance(term, unicode): return term if term[:len('Some ')] != 'Some ' and term != 'None': - if ' ' in term: return 'Some (%s)' % term - return 'Some %s' % term + if ' ' in term and (term[0] + term[-1]) not in ('()', '[]'): + return 'Some (%s)%s' % (term, scope_string) + return 'Some %s%s' % (term, scope_string) return term replacements = dict(parameters) assert(all(ch in '0123456789^+- ' for ch in parameters['modulus'])) @@ -208,9 +209,13 @@ def make_curve_parameters(parameters): parameters.get(op + '_code', None), nargs, sz) - for k in ('upper_bound_of_exponent', 'allowable_bit_widths', 'freeze_extra_allowable_bit_widths'): - if k not in replacements.keys(): - replacements[k] = 'None' + replacements['coef_div_modulus_raw'] = replacements.get('coef_div_modulus', '0') + for k, scope_string in (('upper_bound_of_exponent', ''), + ('allowable_bit_widths', '%nat'), + ('freeze_extra_allowable_bit_widths', '%nat'), + ('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'): replacements[k] = nested_list_to_string(replacements[k]) for k in ('extra_prove_mul_eq', 'extra_prove_square_eq'): @@ -232,7 +237,7 @@ Module Curve <: CurveParameters. Definition carry_chains : option (list (list nat)) := Eval vm_compute in %(carry_chains)s. Definition a24 : option Z := %(a24)s. - Definition coef_div_modulus : nat := %(coef_div_modulus)s%%nat. (* add %(coef_div_modulus)s*modulus before subtracting *) + Definition coef_div_modulus : option nat := %(coef_div_modulus)s. (* add %(coef_div_modulus_raw)s*modulus before subtracting *) Definition goldilocks : bool := %(goldilocks)s. @@ -245,6 +250,7 @@ Module Curve <: CurveParameters. Definition upper_bound_of_exponent : option (Z -> Z) := %(upper_bound_of_exponent)s. Definition allowable_bit_widths : option (list nat) := %(allowable_bit_widths)s. Definition freeze_extra_allowable_bit_widths : option (list nat) := %(freeze_extra_allowable_bit_widths)s. + Definition modinv_fuel : option nat := %(modinv_fuel)s. Ltac extra_prove_mul_eq := %(extra_prove_mul_eq)s. Ltac extra_prove_square_eq := %(extra_prove_square_eq)s. End Curve. @@ -257,12 +263,9 @@ Require Import %s.CurveParameters. Module Import T := MakeSynthesisTactics Curve. -Module P <: SynthesisPrePackage. - Definition Synthesis_package' : Synthesis_package'_Type. - Proof. make_synthesis_package (). Defined. - - Definition Synthesis_package - := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'. +Module P <: PrePackage. + Definition package : Tag.Context. + Proof. make_Synthesis_package (). Defined. End P. Module Export S := PackageSynthesis Curve P. @@ -282,6 +285,8 @@ Proof. 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. @@ -296,6 +301,8 @@ Proof. Time synthesize_square (). Show Ltac Profile. Time Defined. + +Print Assumptions square. """ % {'prefix':prefix} elif fearg in ('freeze',): return r"""Require Import Crypto.Arithmetic.PrimeFieldTheorems. @@ -310,11 +317,29 @@ Proof. Time synthesize_freeze (). Show Ltac Profile. Time Defined. + +Print Assumptions freeze. """ % {'prefix':prefix} + elif fearg in ('feopp',): + 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 -> feBW + | forall a, phiBW (%(arg)s a) = F.%(arg)s (phiBW 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 ('ladderstep', 'xzladderstep'): return r"""Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep. Require Import %(prefix)s.Synthesis. (* TODO : change this to field once field isomorphism happens *) @@ -334,6 +359,8 @@ Proof. synthesize_xzladderstep (). Show Ltac Profile. Time Defined. + +Print Assumptions xzladderstep. """ % {'prefix':prefix} else: print('ERROR: Unsupported operation: %s' % fearg) @@ -343,10 +370,12 @@ Time Defined. def make_display_arg(fearg, prefix): file_name = fearg function_name = fearg - if fearg in ('femul', 'fesub', 'feadd', 'fesquare'): + if fearg in ('femul', 'fesub', 'feadd', 'fesquare', 'feopp'): function_name = fearg[2:] elif fearg in ('freeze', 'xzladderstep'): pass + elif fearg in ('fenz',): + function_name = 'nonzero' elif fearg in ('ladderstep', ): function_name = 'xzladderstep' else: @@ -404,12 +433,16 @@ def main(*args): if open(fname, 'r').read() == outputs[k]: continue new_files.append(fname) - with open(fname, 'w') as f: - f.write(outputs[k]) + with io.open(fname, 'w', newline='\n') as f: + f.write(unicode(outputs[k])) if fname[-len('compiler.sh'):] == 'compiler.sh': mode = os.fstat(f.fileno()).st_mode mode |= 0o111 - os.fchmod(f.fileno(), mode & 0o7777) + mode &= 0o7777 + if 'fchmod' in os.__dict__.keys(): + os.fchmod(f.fileno(), mode) + else: + os.chmod(f.name, mode) if len(new_files) > 0: print('git add ' + ' '.join('"%s"' % i for i in new_files)) diff --git a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v index aa8fd5614..9fe08de2c 100644 --- a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v +++ b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v @@ -14,7 +14,7 @@ Module Curve <: CurveParameters. Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [[3; 7]; [0; 4; 1; 5; 2; 6; 3; 7]; [4; 0]]%nat. Definition a24 : option Z := None. - Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *) + Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) Definition goldilocks : bool := true. @@ -27,6 +27,7 @@ Module Curve <: CurveParameters. 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/X2448/Karatsuba/C64/Synthesis.v b/src/Specific/X2448/Karatsuba/C64/Synthesis.v index 8ea8aa5c9..500671c90 100644 --- a/src/Specific/X2448/Karatsuba/C64/Synthesis.v +++ b/src/Specific/X2448/Karatsuba/C64/Synthesis.v @@ -3,12 +3,9 @@ Require Import Crypto.Specific.X2448.Karatsuba.C64.CurveParameters. Module Import T := MakeSynthesisTactics Curve. -Module P <: SynthesisPrePackage. - Definition Synthesis_package' : Synthesis_package'_Type. - Proof. make_synthesis_package (). Defined. - - Definition Synthesis_package - := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'. +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/X2448/Karatsuba/C64/femul.v b/src/Specific/X2448/Karatsuba/C64/femul.v index 2f890a88f..07dd9b26d 100644 --- a/src/Specific/X2448/Karatsuba/C64/femul.v +++ b/src/Specific/X2448/Karatsuba/C64/femul.v @@ -10,3 +10,5 @@ Proof. Time synthesize_mul (). Show Ltac Profile. Time Defined. + +Print Assumptions mul. diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v index e8a46ea9e..6324acfca 100644 --- a/src/Specific/X25519/C32/CurveParameters.v +++ b/src/Specific/X25519/C32/CurveParameters.v @@ -14,7 +14,7 @@ Module Curve <: CurveParameters. Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat. Definition a24 : option Z := Some 121665. - Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *) + Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) Definition goldilocks : bool := false. @@ -245,6 +245,7 @@ Module Curve <: CurveParameters. 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/X25519/C32/Synthesis.v b/src/Specific/X25519/C32/Synthesis.v index 3b9b35078..0b3336b20 100644 --- a/src/Specific/X25519/C32/Synthesis.v +++ b/src/Specific/X25519/C32/Synthesis.v @@ -3,12 +3,9 @@ Require Import Crypto.Specific.X25519.C32.CurveParameters. Module Import T := MakeSynthesisTactics Curve. -Module P <: SynthesisPrePackage. - Definition Synthesis_package' : Synthesis_package'_Type. - Proof. make_synthesis_package (). Defined. - - Definition Synthesis_package - := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'. +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/X25519/C32/femul.v b/src/Specific/X25519/C32/femul.v index 81bf1f255..bc62814e9 100644 --- a/src/Specific/X25519/C32/femul.v +++ b/src/Specific/X25519/C32/femul.v @@ -10,3 +10,5 @@ Proof. Time synthesize_mul (). Show Ltac Profile. Time Defined. + +Print Assumptions mul. diff --git a/src/Specific/X25519/C32/fesquare.v b/src/Specific/X25519/C32/fesquare.v index 3fa837bd2..2bea3bf8b 100644 --- a/src/Specific/X25519/C32/fesquare.v +++ b/src/Specific/X25519/C32/fesquare.v @@ -10,3 +10,5 @@ Proof. Time synthesize_square (). Show Ltac Profile. Time Defined. + +Print Assumptions square. diff --git a/src/Specific/X25519/C32/freeze.v b/src/Specific/X25519/C32/freeze.v index 9af1e8e0f..bac5a019f 100644 --- a/src/Specific/X25519/C32/freeze.v +++ b/src/Specific/X25519/C32/freeze.v @@ -10,3 +10,5 @@ Proof. Time synthesize_freeze (). Show Ltac Profile. Time Defined. + +Print Assumptions freeze. diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v index 54c578a08..78db9dd8e 100644 --- a/src/Specific/X25519/C64/CurveParameters.v +++ b/src/Specific/X25519/C64/CurveParameters.v @@ -14,7 +14,7 @@ Module Curve <: CurveParameters. Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat. Definition a24 : option Z := Some 121665. - Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *) + Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) Definition goldilocks : bool := false. @@ -62,6 +62,7 @@ Module Curve <: CurveParameters. 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/X25519/C64/Synthesis.v b/src/Specific/X25519/C64/Synthesis.v index 3c3bac04d..2ea78caba 100644 --- a/src/Specific/X25519/C64/Synthesis.v +++ b/src/Specific/X25519/C64/Synthesis.v @@ -3,12 +3,9 @@ Require Import Crypto.Specific.X25519.C64.CurveParameters. Module Import T := MakeSynthesisTactics Curve. -Module P <: SynthesisPrePackage. - Definition Synthesis_package' : Synthesis_package'_Type. - Proof. make_synthesis_package (). Defined. - - Definition Synthesis_package - := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'. +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/X25519/C64/femul.v b/src/Specific/X25519/C64/femul.v index 1e015ddd9..7292df912 100644 --- a/src/Specific/X25519/C64/femul.v +++ b/src/Specific/X25519/C64/femul.v @@ -10,3 +10,5 @@ Proof. Time synthesize_mul (). Show Ltac Profile. Time Defined. + +Print Assumptions mul. diff --git a/src/Specific/X25519/C64/fesquare.v b/src/Specific/X25519/C64/fesquare.v index cfad2d111..fa692f559 100644 --- a/src/Specific/X25519/C64/fesquare.v +++ b/src/Specific/X25519/C64/fesquare.v @@ -10,3 +10,5 @@ Proof. Time synthesize_square (). Show Ltac Profile. Time Defined. + +Print Assumptions square. diff --git a/src/Specific/X25519/C64/freeze.v b/src/Specific/X25519/C64/freeze.v index ef826dba5..2c7fe8b85 100644 --- a/src/Specific/X25519/C64/freeze.v +++ b/src/Specific/X25519/C64/freeze.v @@ -10,3 +10,5 @@ Proof. Time synthesize_freeze (). Show Ltac Profile. Time Defined. + +Print Assumptions freeze. diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v index adb20912e..fc62c9317 100644 --- a/src/Specific/X25519/C64/ladderstep.v +++ b/src/Specific/X25519/C64/ladderstep.v @@ -1,6 +1,6 @@ Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep. Require Import Crypto.Specific.X25519.C64.Synthesis. (* TODO : change this to field once field isomorphism happens *) @@ -20,3 +20,5 @@ Proof. synthesize_xzladderstep (). Show Ltac Profile. Time Defined. + +Print Assumptions xzladderstep. diff --git a/src/Specific/X2555/C128/CurveParameters.v b/src/Specific/X2555/C128/CurveParameters.v index 40c57e8e0..bb4384cc2 100644 --- a/src/Specific/X2555/C128/CurveParameters.v +++ b/src/Specific/X2555/C128/CurveParameters.v @@ -14,7 +14,7 @@ Module Curve <: CurveParameters. Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat. Definition a24 : option Z := Some (121665 (* XXX TODO(andreser) FIXME? Is this right for this curve? *)). - Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *) + Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) Definition goldilocks : bool := false. @@ -27,6 +27,7 @@ Module Curve <: CurveParameters. 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/X2555/C128/Synthesis.v b/src/Specific/X2555/C128/Synthesis.v index f88491af2..1fa3b4a6c 100644 --- a/src/Specific/X2555/C128/Synthesis.v +++ b/src/Specific/X2555/C128/Synthesis.v @@ -3,12 +3,9 @@ Require Import Crypto.Specific.X2555.C128.CurveParameters. Module Import T := MakeSynthesisTactics Curve. -Module P <: SynthesisPrePackage. - Definition Synthesis_package' : Synthesis_package'_Type. - Proof. make_synthesis_package (). Defined. - - Definition Synthesis_package - := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'. +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/X2555/C128/ladderstep.v b/src/Specific/X2555/C128/ladderstep.v index b1d83df4a..902b6c1b0 100644 --- a/src/Specific/X2555/C128/ladderstep.v +++ b/src/Specific/X2555/C128/ladderstep.v @@ -1,6 +1,6 @@ Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework. +Require Import Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep. Require Import Crypto.Specific.X2555.C128.Synthesis. (* TODO : change this to field once field isomorphism happens *) @@ -20,3 +20,5 @@ Proof. synthesize_xzladderstep (). Show Ltac Profile. Time Defined. + +Print Assumptions xzladderstep. |