diff options
Diffstat (limited to 'src/Specific/Framework/ArithmeticSynthesisFramework.v')
| -rw-r--r-- | src/Specific/Framework/ArithmeticSynthesisFramework.v | 565 |
1 files changed, 565 insertions, 0 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesisFramework.v b/src/Specific/Framework/ArithmeticSynthesisFramework.v new file mode 100644 index 000000000..77624ed41 --- /dev/null +++ b/src/Specific/Framework/ArithmeticSynthesisFramework.v @@ -0,0 +1,565 @@ +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.Util.Tactics.BreakMatch. +Require Crypto.Util.Tuple. +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_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_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. + (* 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 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 := + cache_term_with_type_by + (forall i (H:In i carry_chain2), wt (S i) / wt i <> 0) + ltac:(let i := fresh "i" in intros i ?; exact (wt_divides' i)) + wt_divides_chain2. + + 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_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_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. + + (* 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 := + 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 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 + 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_chain1 := fresh "carry_chain1" in + let carry_chain2 := fresh "carry_chain2" in + let a24 := fresh "a24" in + let coef_div_modulus := fresh "coef_div_modulus" 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_chain1 := fresh "wt_divides_chain1" in + let wt_divides_chain2 := fresh "wt_divides_chain2" 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 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_chain1 := pose_carry_chain1 carry_chain1 in + let carry_chain2 := pose_carry_chain2 carry_chain2 in + let a24 := pose_a24 a24 in + let coef_div_modulus := pose_coef_div_modulus coef_div_modulus 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_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 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 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)). + + 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_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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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'). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + 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). + Notation ring := (ltac:(let v := get_ring () in exact v)) (only parsing). +End MakeArithmeticSynthesisTest. |