diff options
Diffstat (limited to 'src/Specific/Framework/ArithmeticSynthesisFramework.v')
| -rw-r--r-- | src/Specific/Framework/ArithmeticSynthesisFramework.v | 337 |
1 files changed, 263 insertions, 74 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesisFramework.v b/src/Specific/Framework/ArithmeticSynthesisFramework.v index 77624ed41..342c759fe 100644 --- a/src/Specific/Framework/ArithmeticSynthesisFramework.v +++ b/src/Specific/Framework/ArithmeticSynthesisFramework.v @@ -6,8 +6,11 @@ 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. @@ -58,12 +61,9 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete (list B.limb) ltac:(let v := P.do_compute P.c in exact v) c. - Ltac pose_carry_chain1 carry_chain1 := - let v := P.do_compute P.carry_chain1 in - cache_term v carry_chain1. - Ltac pose_carry_chain2 carry_chain2 := - let v := P.do_compute P.carry_chain2 in - cache_term v carry_chain2. + 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 @@ -73,6 +73,11 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete 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 @@ -130,16 +135,25 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete (forall i, wt (S i) / wt i <> 0) ltac:(symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides) wt_divides'. - Ltac pose_wt_divides_chain1 wt carry_chain1 wt_divides' wt_divides_chain1 := - cache_term_with_type_by - (forall i (H:In i carry_chain1), wt (S i) / wt i <> 0) - ltac:(let i := fresh "i" in intros i ?; exact (wt_divides' i)) - wt_divides_chain1. - Ltac pose_wt_divides_chain2 wt carry_chain2 wt_divides' wt_divides_chain2 := + 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_chain2), wt (S i) / wt i <> 0) + (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_chain2. + 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; @@ -215,6 +229,99 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete 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 | @@ -235,6 +342,41 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete 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 | @@ -254,8 +396,51 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete 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_chain1 carry_chain2 wt_nonzero wt_divides_chain1 wt_divides_chain2 carry_sig := + 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, @@ -264,15 +449,9 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete ltac:(idtac; let a := fresh "a" in eexists; cbv beta zeta; intros a; - pose proof wt_nonzero; pose proof wt_divides_chain1; - pose proof div_mod; pose proof wt_divides_chain2; - let x := constr:( - Positional.chained_carries_cps - (n:=sz) (div:=div)(modulo:=modulo) wt a carry_chain1 - (fun r => Positional.carry_reduce_cps - (n:=sz) (div:=div) (modulo:=modulo) wt s c r - (fun rrr => Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt rrr carry_chain2 id - ))) in + 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. @@ -409,10 +588,10 @@ print('End MakeArithmeticSynthesisTest.') let bitwidth := fresh "bitwidth" in let s := fresh "s" in let c := fresh "c" in - let carry_chain1 := fresh "carry_chain1" in - let carry_chain2 := fresh "carry_chain2" 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 @@ -424,14 +603,17 @@ print('End MakeArithmeticSynthesisTest.') let wt_nonneg := fresh "wt_nonneg" in let wt_divides := fresh "wt_divides" in let wt_divides' := fresh "wt_divides'" in - let wt_divides_chain1 := fresh "wt_divides_chain1" in - let wt_divides_chain2 := fresh "wt_divides_chain2" 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 @@ -443,10 +625,10 @@ print('End MakeArithmeticSynthesisTest.') let bitwidth := pose_bitwidth bitwidth in let s := pose_s s in let c := pose_c c in - let carry_chain1 := pose_carry_chain1 carry_chain1 in - let carry_chain2 := pose_carry_chain2 carry_chain2 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 @@ -458,22 +640,25 @@ print('End MakeArithmeticSynthesisTest.') 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_chain1 := pose_wt_divides_chain1 wt carry_chain1 wt_divides' wt_divides_chain1 in - let wt_divides_chain2 := pose_wt_divides_chain2 wt carry_chain2 wt_divides' wt_divides_chain2 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 mul_sig := pose_mul_sig sz m wt s c sz2 wt_nonzero mul_sig in - let square_sig := pose_square_sig sz m wt s c sz2 wt_nonzero square_sig in - let carry_sig := pose_carry_sig sz m wt s c carry_chain1 carry_chain2 wt_nonzero wt_divides_chain1 wt_divides_chain2 carry_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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring)). + 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 @@ -494,72 +679,76 @@ Module MakeArithmeticSynthesisTest (AP : ArithmeticSynthesisPrePackage). 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in bitwidth). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in s). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in c). + 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_chain1 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_chain1). - Notation carry_chain1 := (ltac:(let v := get_carry_chain1 () in exact v)) (only parsing). - Ltac get_carry_chain2 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_chain2). - Notation carry_chain2 := (ltac:(let v := get_carry_chain2 () in exact v)) (only parsing). - Ltac get_a24 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in a24). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef_div_modulus). + 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_m _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in m). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz2). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in m_enc). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef_mod). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz_nonzero). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_nonzero). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_nonneg). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides'). + 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_chain1 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides_chain1). - Notation wt_divides_chain1 := (ltac:(let v := get_wt_divides_chain1 () in exact v)) (only parsing). - Ltac get_wt_divides_chain2 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides_chain2). - Notation wt_divides_chain2 := (ltac:(let v := get_wt_divides_chain2 () in exact v)) (only parsing). - Ltac get_zero_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in zero_sig). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in one_sig). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in a24_sig). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in add_sig). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sub_sig). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in opp_sig). + 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_mul_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in mul_sig). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in square_sig). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_sig). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_pos). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_multiples). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in freeze_sig). + 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_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in ring). + 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. |