diff options
Diffstat (limited to 'src/Specific/Framework')
-rw-r--r-- | src/Specific/Framework/ArithmeticSynthesisFramework.v | 565 | ||||
-rw-r--r-- | src/Specific/Framework/CurveParameters.v | 114 | ||||
-rw-r--r-- | src/Specific/Framework/IntegrationTestDisplayCommon.v | 24 | ||||
-rw-r--r-- | src/Specific/Framework/IntegrationTestDisplayCommonTactics.v | 149 | ||||
-rw-r--r-- | src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v | 288 | ||||
-rw-r--r-- | src/Specific/Framework/LadderstepSynthesisFramework.v | 93 | ||||
-rw-r--r-- | src/Specific/Framework/ReificationTypes.v | 207 | ||||
-rw-r--r-- | src/Specific/Framework/SynthesisFramework.v | 104 |
8 files changed, 1544 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. diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v new file mode 100644 index 000000000..aa679a4d3 --- /dev/null +++ b/src/Specific/Framework/CurveParameters.v @@ -0,0 +1,114 @@ +Require Export Coq.ZArith.BinInt. +Require Export Coq.Lists.List. +Require Export Crypto.Util.ZUtil.Notations. +Require Crypto.Util.Tuple. + +Module Export Notations. + Export ListNotations. + + Open Scope list_scope. + Open Scope Z_scope. + + Notation limb := (Z * Z)%type. + Infix "^" := Tuple.tuple : type_scope. +End Notations. + +(* These definitions will need to be passed as Ltac arguments (or + cleverly inferred) when things are eventually automated *) +Module Type CurveParameters. + Parameter sz : nat. + Parameter bitwidth : Z. + Parameter s : Z. + Parameter c : list limb. + Parameter carry_chain1 + : option (list nat). (* defaults to [seq 0 (pred sz)] *) + Parameter carry_chain2 + : option (list nat). (* defaults to [0 :: 1 :: nil] *) + Parameter a24 : Z. + Parameter coef_div_modulus : nat. + + Parameter mul_code : option (Z^sz -> Z^sz -> Z^sz). + Parameter square_code : option (Z^sz -> Z^sz). + Parameter upper_bound_of_exponent + : option (Z -> Z). (* defaults to [fun exp => 2^exp + 2^(exp-3)] *) + Parameter allowable_bit_widths + : option (list nat). (* defaults to [bitwidth :: 2*bitwidth :: nil] *) + Parameter freeze_extra_allowable_bit_widths + : option (list nat). (* defaults to [8 :: nil] *) + Ltac extra_prove_mul_eq := idtac. + Ltac extra_prove_square_eq := idtac. +End CurveParameters. + +Module FillCurveParameters (P : CurveParameters). + Local Notation defaulted opt_v default + := (match opt_v with + | Some v => v + | None => default + end). + Ltac do_compute v := + let v' := (eval vm_compute in v) in v'. + Notation compute v + := (ltac:(let v' := do_compute v in exact v')) + (only parsing). + Definition sz := P.sz. + Definition bitwidth := P.bitwidth. + Definition s := P.s. + Definition c := P.c. + Definition carry_chain1 := defaulted P.carry_chain1 (seq 0 (pred sz)). + Definition carry_chain2 := defaulted P.carry_chain2 (0 :: 1 :: nil)%nat. + Definition a24 := P.a24. + Definition coef_div_modulus := P.coef_div_modulus. + + Ltac default_mul := + lazymatch (eval hnf in P.mul_code) with + | None => reflexivity + | Some ?mul_code + => instantiate (1:=mul_code) + end. + Ltac default_square := + lazymatch (eval hnf in P.square_code) with + | None => reflexivity + | Some ?square_code + => instantiate (1:=square_code) + end. + + Definition upper_bound_of_exponent + := defaulted P.upper_bound_of_exponent (fun exp => (2^exp + 2^(exp-3))%Z). + Definition allowable_bit_widths + := 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. + + (* hack around https://coq.inria.fr/bugs/show_bug.cgi?id=5764 *) + Ltac do_unfold v' := + let P_sz := P.sz in + let P_bitwidth := P.bitwidth in + let P_s := P.s in + let P_c := P.c in + let P_carry_chain1 := P.carry_chain1 in + let P_carry_chain2 := P.carry_chain2 in + let P_a24 := P.a24 in + let P_coef_div_modulus := P.coef_div_modulus in + let P_mul_code := P.mul_code in + let P_square_code := P.square_code in + let P_upper_bound_of_exponent := P.upper_bound_of_exponent in + 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 v' := (eval cbv [id + List.app + sz bitwidth s c carry_chain1 carry_chain2 a24 coef_div_modulus + P_sz P_bitwidth P_s P_c P_carry_chain1 P_carry_chain2 P_a24 P_coef_div_modulus + 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 + pred seq] + in v') in + v'. + Notation unfold v + := (ltac:(let v' := v in + let v' := do_unfold v' in + exact v')) + (only parsing). + Ltac extra_prove_mul_eq := P.extra_prove_mul_eq. + Ltac extra_prove_square_eq := P.extra_prove_square_eq. +End FillCurveParameters. diff --git a/src/Specific/Framework/IntegrationTestDisplayCommon.v b/src/Specific/Framework/IntegrationTestDisplayCommon.v new file mode 100644 index 000000000..a3bf52d85 --- /dev/null +++ b/src/Specific/Framework/IntegrationTestDisplayCommon.v @@ -0,0 +1,24 @@ +Require Import Crypto.Util.Sigma.Lift. +Require Import Crypto.Util.Sigma.Associativity. +Require Import Crypto.Util.Sigma.MapProjections. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Compilers.Z.Bounds.Interpretation. +Require Import Crypto.Compilers.Eta. +Require Export Coq.ZArith.ZArith. +Require Export Crypto.Util.LetIn. +Require Export Crypto.Util.FixedWordSizes. +Require Export Crypto.Compilers.Syntax. +Require Export Crypto.Specific.Framework.IntegrationTestDisplayCommonTactics. +Require Export Crypto.Compilers.Z.HexNotationConstants. +Require Export Crypto.Util.Notations. +Require Export Crypto.Compilers.Z.CNotations. + +Global Arguments Pos.to_nat !_ / . +Global Arguments InterpEta {_ _ _ _ _}. +Global Set Printing Width 2000000. + +Notation "'Interp-η' f x" := (Eta.InterpEta f x) (format "'Interp-η' '//' f '//' x", at level 200, f at next level, x at next level). +Notation ReturnType := (interp_flat_type _). +Notation "'let' ( a , b ) := c 'in' d" := (let (a, b) := c in d) (at level 200, d at level 200, format "'let' ( a , b ) := c 'in' '//' d"). + +Require Export Coq.Unicode.Utf8. (* for better line breaks at function display; must come last *) diff --git a/src/Specific/Framework/IntegrationTestDisplayCommonTactics.v b/src/Specific/Framework/IntegrationTestDisplayCommonTactics.v new file mode 100644 index 000000000..2b15616fe --- /dev/null +++ b/src/Specific/Framework/IntegrationTestDisplayCommonTactics.v @@ -0,0 +1,149 @@ +Require Import Crypto.Util.Sigma.Lift. +Require Import Crypto.Util.Sigma.Associativity. +Require Import Crypto.Util.Sigma.MapProjections. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Compilers.Z.Bounds.Interpretation. +Require Import Crypto.Compilers.Eta. +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.FixedWordSizes. +Require Import Crypto.Compilers.Syntax. +Require Export Crypto.Util.Notations. + +Global Arguments Pos.to_nat !_ / . + +Ltac display_helper_gen f make_hole := + let display_helper f := display_helper_gen f make_hole in + let do_make_hole _ := + match goal with + | [ |- ?T ] => let h := make_hole T in + refine h + end in + let t := type of f in + lazymatch (eval hnf in t) with + | forall _ : ?A, ?B + => let x := fresh "x" in + lazymatch (eval hnf in A) with + | @sig ?A ?P + => lazymatch (eval hnf in A) with + | sig _ + => let f' := constr:(fun x : A => f (exist P x ltac:(do_make_hole ()))) in + display_helper f' + | _ + => refine (fun x : A => _); + let f' := constr:(f (exist P x ltac:(do_make_hole ()))) in + display_helper f' + end + | _ + => lazymatch A with + | prod ?A ?B + => let f' := constr:(fun (a : A) (b : B) => f (a, b)%core) in + display_helper f' + | _ + => refine (fun x : A => _); + let f' := constr:(f x) in + display_helper f' + end + end + | @sig ?A _ + => lazymatch (eval hnf in A) with + | sig _ => display_helper (proj1_sig f) + | _ => refine (proj1_sig f) + end + | _ + => lazymatch t with + | prod _ _ + => let a := fresh "a" in + let b := fresh "b" in + refine (let (a, b) := f in + pair _ _); + [ display_helper a | display_helper b ] + | _ => refine f + end + end. +Ltac display_helper f := display_helper_gen f ltac:(fun T => open_constr:(_)). +Ltac display_helper_with_admit f := + constr:(fun admit : forall T, T + => ltac:(display_helper_gen f ltac:(fun T => constr:(admit T)))). +Ltac try_strip_admit f := + lazymatch f with + | fun _ : forall T, T => ?P => P + | ?P => P + end. +Ltac refine_display f := + let do_red F := (eval cbv [f + proj1_sig fst snd + Tuple.map Tuple.map' + Lift.lift1_sig Lift.lift2_sig Lift.lift3_sig Lift.lift4_sig Lift.lift4_sig_sig + MapProjections.proj2_sig_map Associativity.sig_sig_assoc + sig_conj_by_impl2 + sig_eq_trans_exist1 sig_R_trans_exist1 sig_eq_trans_rewrite_fun_exist1 + sig_R_trans_rewrite_fun_exist1 + adjust_tuple2_tuple2_sig + Tuple.tuple Tuple.tuple' + FixedWordSizes.wordT FixedWordSizes.word_case FixedWordSizes.ZToWord FixedWordSizes.word_case_dep + Bounds.actual_logsz Bounds.round_up_to_in_list Bounds.option_min + List.map List.filter List.fold_right List.fold_left + Nat.leb Nat.min + PeanoNat.Nat.log2 PeanoNat.Nat.log2_iter PeanoNat.Nat.pred + Bounds.bounds_to_base_type + interp_flat_type + Z.leb Z.compare Pos.compare Pos.compare_cont + ZRange.lower ZRange.upper + BinPos.Pos.to_nat PeanoNat.Nat.pow + ] in F) in + let ret := display_helper_with_admit (proj1_sig f) in + let ret := do_red ret in + let ret := lazymatch ret with + | context[match ?sz with O => _ | _ => _ end] => (eval cbv [sz] in ret) + | _ => ret + end in + let ret := (eval simpl @Z.to_nat in ret) in + let ret := (eval cbv [interp_flat_type] in ret) in + let ret := try_strip_admit ret in + refine ret. +Tactic Notation "display" open_constr(f) := + refine_display f. +Notation display f := (ltac:(let v := f in display v)) (only parsing). + +(** Some helper tactics for actually pulling out the expression *) +Ltac strip_InterpEta term := + let retype e := + lazymatch type of e with + | forall var, @Syntax.expr ?base_type_code ?op var ?T + => constr:(e : @Syntax.Expr base_type_code op T) + | _ => e + end in + lazymatch term with + | fun x : ?T => ?P + => let maybe_x := fresh x in + let probably_not_x := fresh maybe_x in + let not_x := fresh probably_not_x in + lazymatch + constr:(fun x : T + => match P with + | not_x => ltac:(let v := (eval cbv delta [not_x] in not_x) in + let v' := strip_InterpEta v in + exact v') + end) + with + | fun _ => ?P => retype P + | ?P => retype P + end + | @Eta.InterpEta _ _ _ _ _ ?e + => e + | @Eta.InterpEta _ _ _ _ _ ?e _ + => e + | let (a, b) := ?f in _ + => f + | _ => let dummy := match goal with + | _ => fail 1 "strip_InterpEta:" term + end in + I + end. + +Ltac extract_Expr f := + let k := constr:(ltac:(refine_display f)) in + let k := strip_InterpEta k in + k. +Notation extract_Expr f := (ltac:(let v := f in let v := extract_Expr v in refine v)) (only parsing). diff --git a/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v new file mode 100644 index 000000000..41bef884c --- /dev/null +++ b/src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v @@ -0,0 +1,288 @@ +(*** XXX TODO MOVE ALL THINGS IN THIS FILE TO BETTER PLACES *) +Require Import Coq.ZArith.BinInt. +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Sigma.Lift. +Require Import Crypto.Util.Sigma.Associativity. +Require Import Crypto.Util.Sigma.MapProjections. +Require Import Crypto.Util.Tactics.MoveLetIn. +Require Import Crypto.Util.Tactics.DestructHead. + +Definition adjust_tuple2_tuple2_sig {A P Q} + (v : { a : { a : tuple (tuple A 2) 2 | (P (fst (fst a)) /\ P (snd (fst a))) /\ (P (fst (snd a)) /\ P (snd (snd a))) } + | Q (exist _ _ (proj1 (proj1 (proj2_sig a))), + exist _ _ (proj2 (proj1 (proj2_sig a))), + (exist _ _ (proj1 (proj2 (proj2_sig a))), + exist _ _ (proj2 (proj2 (proj2_sig a))))) }) + : { a : tuple (tuple (@sig A P) 2) 2 | Q a }. +Proof. + eexists. + exact (proj2_sig v). +Defined. + +(** TODO MOVE ME *) +(** The [eexists_sig_etransitivity_R R] tactic takes a goal of the form + [{ a | R (f a) b }], and splits it into two goals, [R ?b' b] and + [{ a | R (f a) ?b' }], where [?b'] is a fresh evar. *) +Definition sig_R_trans_exist1 {B} (R : B -> B -> Prop) {HT : Transitive R} {A} (f : A -> B) + (b b' : B) + (pf : R b' b) + (y : { a : A | R (f a) b' }) + : { a : A | R (f a) b } + := let 'exist a p := y in exist _ a (transitivity (R:=R) p pf). +Ltac eexists_sig_etransitivity_R R := + lazymatch goal with + | [ |- @sig ?A ?P ] + => let RT := type of R in + let B := lazymatch (eval hnf in RT) with ?B -> _ => B end in + let lem := constr:(@sig_R_trans_exist1 B R _ A _ _ : forall b' pf y, @sig A P) in + let lem := open_constr:(lem _) in + simple refine (lem _ _) + end. +Tactic Notation "eexists_sig_etransitivity_R" open_constr(R) := eexists_sig_etransitivity_R R. +(** The [eexists_sig_etransitivity] tactic takes a goal of the form + [{ a | f a = b }], and splits it into two goals, [?b' = b] and + [{ a | f a = ?b' }], where [?b'] is a fresh evar. *) +Definition sig_eq_trans_exist1 {A B} + := @sig_R_trans_exist1 B (@eq B) _ A. +Ltac eexists_sig_etransitivity := + lazymatch goal with + | [ |- { a : ?A | @?f a = ?b } ] + => let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in + simple refine (lem _ (_ : { a : A | _ })) + end. +Definition sig_R_trans_rewrite_fun_exist1 {B} (R : B -> B -> Prop) {HT : Transitive R} +{A} (f : A -> B) (b : B) (f' : A -> B) + (pf : forall a, R (f a) (f' a)) + (y : { a : A | R (f' a) b }) + : { a : A | R (f a) b } + := let 'exist a p := y in exist _ a (transitivity (R:=R) (pf a) p). +Ltac eexists_sig_etransitivity_for_rewrite_fun_R R := + lazymatch goal with + | [ |- @sig ?A ?P ] + => let RT := type of R in + let B := lazymatch (eval hnf in RT) with ?B -> _ => B end in + let lem := constr:(@sig_R_trans_rewrite_fun_exist1 B R _ A _ _ : forall f' pf y, @sig A P) in + let lem := open_constr:(lem _) in + simple refine (lem _ _); cbv beta + end. +Tactic Notation "eexists_sig_etransitivity_for_rewrite_fun_R" open_constr(R) + := eexists_sig_etransitivity_for_rewrite_fun_R R. +Definition sig_eq_trans_rewrite_fun_exist1 {A B} (f f' : A -> B) + (b : B) + (pf : forall a, f' a = f a) + (y : { a : A | f' a = b }) + : { a : A | f a = b } + := let 'exist a p := y in exist _ a (eq_trans (eq_sym (pf a)) p). +Ltac eexists_sig_etransitivity_for_rewrite_fun := + lazymatch goal with + | [ |- { a : ?A | @?f a = ?b } ] + => let lem := open_constr:(@sig_eq_trans_rewrite_fun_exist1 A _ f _ b) in + simple refine (lem _ _); cbv beta + end. +Definition sig_conj_by_impl2 {A} {P Q : A -> Prop} (H : forall a : A, Q a -> P a) + (H' : { a : A | Q a }) + : { a : A | P a /\ Q a } + := let (a, p) := H' in exist _ a (conj (H a p) p). + + +(** [apply_lift_sig] picks out which version of the [liftN_sig] lemma + to apply, and builds the appropriate arguments *) +Ltac make_P_for_apply_lift_sig P := + lazymatch P with + | fun (f : ?F) => forall (a : ?A), @?P f a + => constr:(fun (a : A) + => ltac:(lazymatch constr:(fun (f : F) + => ltac:(let v := (eval cbv beta in (P f a)) in + lazymatch (eval pattern (f a) in v) with + | ?k _ => exact k + end)) + with + | fun _ => ?P + => let v := make_P_for_apply_lift_sig P in + exact v + end)) + | _ => P + end. +Ltac apply_lift_sig := + let P := lazymatch goal with |- sig ?P => P end in + let P := make_P_for_apply_lift_sig P in + lazymatch goal with + | [ |- { f | forall a b c d e, _ } ] + => fail "apply_lift_sig does not yet support ≥ 5 binders" + | [ |- { f | forall (a : ?A) (b : ?B) (c : ?C) (d : ?D), _ } ] + => apply (@lift4_sig A B C D _ P) + | [ |- { f | forall (a : ?A) (b : ?B) (c : ?C), _ } ] + => apply (@lift3_sig A B C _ P) + | [ |- { f | forall (a : ?A) (b : ?B), _ } ] + => apply (@lift2_sig A B _ P) + | [ |- { f | forall (a : ?A), _ } ] + => apply (@lift1_sig A _ P) + | [ |- { f | _ } ] + => idtac + end. +Ltac get_proj2_sig_map_arg_helper P := + lazymatch P with + | (fun e => ?A -> @?B e) + => let B' := get_proj2_sig_map_arg_helper B in + uconstr:(A -> B') + | _ => uconstr:(_ : Prop) + end. +Ltac get_proj2_sig_map_arg _ := + lazymatch goal with + | [ |- { e : ?T | @?E e } ] + => let P := get_proj2_sig_map_arg_helper E in + uconstr:(fun e : T => P) + end. +Ltac get_phi_for_preglue _ := + lazymatch goal with + | [ |- { e | @?E e } ] + => lazymatch E with + | context[Tuple.map (Tuple.map ?phi) _ = _] + => phi + | context[?phi _ = _] + => phi + end + end. +Ltac start_preglue := + apply_lift_sig; intros; cbv beta iota zeta; + let phi := get_phi_for_preglue () in + let P' := get_proj2_sig_map_arg () in + refine (proj2_sig_map (P:=P') _ _); + [ let FINAL := fresh "FINAL" in + let a := fresh "a" in + intros a FINAL; + repeat (let H := fresh in intro H; specialize (FINAL H)); + lazymatch goal with + | [ |- ?phi _ = ?RHS ] + => refine (@eq_trans _ _ _ RHS FINAL _); cbv [phi]; clear a FINAL + | [ |- _ /\ Tuple.map (Tuple.map ?phi) _ = _ ] + => split; cbv [phi]; [ refine (proj1 FINAL); shelve | ] + end + | cbv [phi] ]. +Ltac do_set_sig f_sig := + let fZ := fresh f_sig in + set (fZ := proj1_sig f_sig); + context_to_dlet_in_rhs fZ; + try cbv beta iota delta [proj1_sig f_sig] in fZ; + cbv beta delta [fZ]; clear fZ; + cbv beta iota delta [fst snd]. +Ltac do_set_sig_1arg f_sig := + let fZ := fresh f_sig in + set (fZ := proj1_sig f_sig); + context_to_dlet_in_rhs (fZ _); + try cbn beta iota delta [proj1_sig f_sig] in fZ; + try cbv [f_sig] in fZ; + cbv beta delta [fZ]; clear fZ; + cbv beta iota delta [fst snd]. +Ltac do_set_sigs _ := + lazymatch goal with + | [ |- context[@proj1_sig ?a ?b ?f_sig] ] + => let fZ := fresh f_sig in + set (fZ := proj1_sig f_sig); + context_to_dlet_in_rhs fZ; + do_set_sigs (); (* we recurse before unfolding, because that's faster *) + try cbv beta iota delta [proj1_sig f_sig] in fZ; + cbv beta delta [fZ]; + cbv beta iota delta [fst snd] + | _ => idtac + end. +Ltac trim_after_do_rewrite_with_sig _ := + repeat match goal with + | [ |- Tuple.map ?f _ = Tuple.map ?f _ ] + => apply f_equal + end. +Ltac do_rewrite_with_sig_no_set_by f_sig by_tac := + let lem := constr:(proj2_sig f_sig) in + let lemT := type of lem in + let lemT := (eval cbv beta zeta in lemT) in + rewrite <- (lem : lemT) by by_tac (); + trim_after_do_rewrite_with_sig (). +Ltac do_rewrite_with_sig_by f_sig by_tac := + do_rewrite_with_sig_no_set_by f_sig by_tac; + do_set_sig f_sig. +Ltac do_rewrite_with_sig_1arg_by f_sig by_tac := + do_rewrite_with_sig_no_set_by f_sig by_tac; + do_set_sig_1arg f_sig. +Ltac do_rewrite_with_sig f_sig := do_rewrite_with_sig_by f_sig ltac:(fun _ => idtac). +Ltac do_rewrite_with_sig_1arg f_sig := do_rewrite_with_sig_1arg_by f_sig ltac:(fun _ => idtac). +Ltac do_rewrite_with_1sig_add_carry_by f_sig carry_sig by_tac := + let fZ := fresh f_sig in + rewrite <- (proj2_sig f_sig) by by_tac (); + symmetry; rewrite <- (proj2_sig carry_sig) by by_tac (); symmetry; + pose (fun a => proj1_sig carry_sig (proj1_sig f_sig a)) as fZ; + lazymatch goal with + | [ |- context G[proj1_sig carry_sig (proj1_sig f_sig ?a)] ] + => let G' := context G[fZ a] in change G' + end; + context_to_dlet_in_rhs fZ; cbv beta delta [fZ]; + try cbv beta iota delta [proj1_sig f_sig carry_sig]; + cbv beta iota delta [fst snd]. +Ltac do_rewrite_with_1sig_add_carry f_sig carry_sig := do_rewrite_with_1sig_add_carry_by f_sig carry_sig ltac:(fun _ => idtac). +Ltac do_rewrite_with_2sig_add_carry_by f_sig carry_sig by_tac := + let fZ := fresh f_sig in + rewrite <- (proj2_sig f_sig) by by_tac (); + symmetry; rewrite <- (proj2_sig carry_sig) by by_tac (); symmetry; + pose (fun a b => proj1_sig carry_sig (proj1_sig f_sig a b)) as fZ; + lazymatch goal with + | [ |- context G[proj1_sig carry_sig (proj1_sig f_sig ?a ?b)] ] + => let G' := context G[fZ a b] in change G' + end; + context_to_dlet_in_rhs fZ; cbv beta delta [fZ]; + try cbv beta iota delta [proj1_sig f_sig carry_sig]; + cbv beta iota delta [fst snd]. +Ltac do_rewrite_with_2sig_add_carry f_sig carry_sig := do_rewrite_with_2sig_add_carry_by f_sig carry_sig ltac:(fun _ => idtac). +Ltac unmap_map_tuple _ := + repeat match goal with + | [ |- context[Tuple.map (n:=?N) (fun x : ?T => ?f (?g x))] ] + => rewrite <- (Tuple.map_map (n:=N) f g + : pointwise_relation _ eq _ (Tuple.map (n:=N) (fun x : T => f (g x)))) + end. +Ltac get_feW_bounded boundedT := + lazymatch boundedT with + | and ?X ?Y => get_feW_bounded X + | ?feW_bounded _ => feW_bounded + end. +Ltac subst_feW _ := + let T := lazymatch goal with |- @sig ?T _ => T end in + let boundedT := lazymatch goal with |- { e | ?A -> _ } => A end in + let feW_bounded := get_feW_bounded boundedT in + let feW := lazymatch type of feW_bounded with ?feW -> Prop => feW end in + cbv [feW feW_bounded]; + try clear feW feW_bounded. +Ltac finish_conjoined_preglue _ := + [ > match goal with + | [ FINAL : _ /\ ?e |- _ ] => is_evar e; refine (proj2 FINAL) + end + | try subst_feW () ]. +Ltac fin_preglue := + [ > reflexivity + | repeat sig_dlet_in_rhs_to_context; + apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)) ]. + +Ltac factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t := + let feBW_small := lazymatch goal with |- { f : ?feBW_small | _ } => feBW_small end in + Associativity.sig_sig_assoc; + apply sig_conj_by_impl2; + [ let H := fresh in + intros ? H; + try lazymatch goal with + | [ |- (?eval _ < _)%Z ] + => cbv [eval] + end; + rewrite H; clear H; + eapply Z.le_lt_trans; + [ apply Z.eq_le_incl, f_equal | apply op_bounded ]; + [ repeat match goal with + | [ |- ?f ?x = ?g ?y ] + => is_evar y; unify x y; + apply (f_equal (fun fg => fg x)) + end; + clear; abstract reflexivity + | .. ]; + op_sig_side_conditions_t () + | apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)); + cbv [proj1_sig]; + repeat match goal with + | [ H : feBW_small |- _ ] => destruct H as [? _] + end ]. diff --git a/src/Specific/Framework/LadderstepSynthesisFramework.v b/src/Specific/Framework/LadderstepSynthesisFramework.v new file mode 100644 index 000000000..d6afb31eb --- /dev/null +++ b/src/Specific/Framework/LadderstepSynthesisFramework.v @@ -0,0 +1,93 @@ +Require Import Coq.ZArith.BinIntDef. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Curves.Montgomery.XZ. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Tactics.PoseTermWithName. +Require Import Crypto.Util.Tactics.CacheTerm. + +(** TODO(jadep,andreser): Move to NewBaseSystemTest? *) +Definition FMxzladderstep {m} := @M.donnaladderstep (F m) F.add F.sub F.mul. + +Section with_notations. + Context sz (add sub mul : tuple Z sz -> tuple Z sz -> tuple Z sz) + (square carry : tuple Z sz -> tuple Z sz). + Local Infix "+" := add. + Local Notation "a * b" := (carry (mul a b)). + Local Notation "x ^ 2" := (carry (square x)). + Local Infix "-" := sub. + Definition Mxzladderstep a24 x1 Q Q' + := match Q, Q' with + | (x, z), (x', z') => + dlet origx := x in + dlet x := x + z in + dlet z := origx - z in + dlet origx' := x' in + dlet x' := x' + z' in + dlet z' := origx' - z' in + dlet xx' := x' * z in + dlet zz' := x * z' in + dlet origx' := xx' in + dlet xx' := xx' + zz' in + dlet zz' := origx' - zz' in + dlet x3 := xx'^2 in + dlet zzz' := zz'^2 in + dlet z3 := zzz' * x1 in + dlet xx := x^2 in + dlet zz := z^2 in + dlet x2 := xx * zz in + dlet zz := xx - zz in + dlet zzz := zz * a24 in + dlet zzz := zzz + xx in + dlet z2 := zz * zzz in + ((x2, z2), (x3, z3))%core + 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) + | forall a24 x1 Q Q', let eval := B.Positional.Fdecode wt in Tuple.map (n:=2) (Tuple.map (n:=2) eval) (xzladderstep a24 x1 Q Q') = FMxzladderstep (m:=m) (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') } + ltac:((exists (Mxzladderstep sz (proj1_sig add_sig) (proj1_sig sub_sig) (proj1_sig mul_sig) (proj1_sig square_sig) (proj1_sig carry_sig))); + let a24 := fresh "a24" in + let x1 := fresh "x1" in + let Q := fresh "Q" in + let Q' := fresh "Q'" in + let eval := fresh "eval" in + intros a24 x1 Q Q' eval; + cbv [Mxzladderstep FMxzladderstep M.donnaladderstep]; + destruct Q, Q'; cbv [map map' fst snd Let_In eval]; + repeat match goal with + | [ |- context[@proj1_sig ?a ?b ?s] ] + => rewrite !(@proj2_sig a b s) + 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/ReificationTypes.v b/src/Specific/Framework/ReificationTypes.v new file mode 100644 index 000000000..3a160e04d --- /dev/null +++ b/src/Specific/Framework/ReificationTypes.v @@ -0,0 +1,207 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.romega.ROmega. +Require Import Coq.micromega.Lia. +Require Import Coq.Lists.List. +Local Open Scope Z_scope. + +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Util.FixedWordSizes. +Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.ZRange Crypto.Util.BoundedWord. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Decidable. + +Require Import Crypto.Util.Tactics.PoseTermWithName. +Require Import Crypto.Util.Tactics.CacheTerm. + +Ltac pose_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. + +Ltac get_b_of upper_bound_of_exponent := + constr:(fun exp => {| lower := 0 ; upper := upper_bound_of_exponent exp |}%Z). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *) + +(* 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 := + 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 := + 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 := + 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 := + pose_term_with + ltac:(fun _ => eval compute in (2^lgbitwidth)%nat) + bitwidth. + +Ltac pose_feZ sz feZ := + pose_term_with + ltac:(fun _ => constr:(tuple Z sz)) + feZ. + +Ltac pose_feW sz lgbitwidth feW := + cache_term_with_type_by + Type + ltac:(let v := eval cbv [lgbitwidth] in (tuple (wordT lgbitwidth) sz) in exact v) + feW. +Ltac pose_feW_bounded feW bounds feW_bounded := + cache_term_with_type_by + (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 := + cache_term_with_type_by + Type + ltac:(let v := eval cbv [bitwidth bounds] in (BoundedWord sz bitwidth bounds) in exact v) + feBW. + +Lemma feBW_bounded_helper' + sz bitwidth bounds + (feBW := BoundedWord sz 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 (map upper bounds). +Proof. + let a := fresh "a" in + intro a; + destruct a as [a H]; unfold BoundedWordToZ, proj1_sig. + destruct sz as [|sz]. + { cbv -[Z.le Z.lt Z.mul]; lia. } + { cbn [tuple map] in *. + revert dependent wt; induction sz as [|sz IHsz]; intros. + { cbv -[Z.le Z.lt wordToZ Z.mul Z.pow Z.add lower upper Nat.log2 wordT] in *. + repeat match goal with + | [ |- context[@wordToZ ?n ?x] ] + => generalize dependent (@wordToZ n x); intros + | [ H : forall j, 0 <= wt j |- context[wt ?i] ] + => pose proof (H i); generalize dependent (wt i); intros + end. + nia. } + { pose proof (Hwt 0%nat). + cbn [tuple' map'] in *. + destruct a as [a' a], bounds as [bounds b], H as [H [H' _]]. + cbn [fst snd] in *. + setoid_rewrite (@B.Positional.eval_step (S _)). + specialize (IHsz bounds a' H (fun i => wt (S i)) (fun i => Hwt _)). + nia. } } +Qed. +Lemma feBW_bounded_helper + sz bitwidth bounds + (feBW := BoundedWord sz 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. +Proof. + intros [Hl Hu] a; split; + [ eapply Z.le_trans | eapply Z.le_lt_trans ]; + [ | eapply feBW_bounded_helper' | eapply feBW_bounded_helper' | ]; + assumption. +Qed. + +Ltac pose_feBW_bounded wt sz feBW 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); + vm_compute; clear; split; congruence) + feBW_bounded. + +Ltac pose_phiW feW m wt phiW := + cache_term_with_type_by + (feW -> F m) + ltac:(exact (fun x : feW => B.Positional.Fdecode wt (Tuple.map wordToZ x))) + phiW. +Ltac pose_phiBW feBW m wt phiBW := + cache_term_with_type_by + (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/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v new file mode 100644 index 000000000..c30024181 --- /dev/null +++ b/src/Specific/Framework/SynthesisFramework.v @@ -0,0 +1,104 @@ +Require Import Crypto.Specific.Framework.ArithmeticSynthesisFramework. +Require Import Crypto.Specific.Framework.ReificationTypes. +Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Util.BoundedWord. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Compilers.Z.Bounds.Pipeline. +Require Crypto.Specific.Framework.CurveParameters. + +Module Export Exports. + Export ArithmeticSynthesisFramework.Exports. +End Exports. + +Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters). + Module AS := MakeArithmeticSynthesisTestTactics Curve. + + Ltac get_synthesis_package _ := + let arithmetic_synthesis_pkg := AS.get_ArithmeticSynthesis_package () in + lazymatch arithmetic_synthesis_pkg with + | (?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) + => 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)) + 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. + +Local Notation eta2 x := (fst x, snd x) (only parsing). +Local Notation eta3 x := (eta2 (fst x), snd x) (only parsing). + +Notation Synthesis_package'_Type := + { ABC : _ & let '(a, b, c) := eta3 ABC in (a * b * c)%type } (only parsing). + +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. + +Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (P : SynthesisPrePackage). + Module CP := 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. + + Ltac synthesize_with_carry do_rewrite get_op_sig := + let carry_sig := get_carry_sig () in + let op_sig := get_op_sig () in + start_preglue; + [ do_rewrite op_sig carry_sig; cbv_runtime + | .. ]; + fin_preglue; + refine_reflectively_gen CP.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 := + synthesize_with_carry do_rewrite_with_1sig_add_carry get_op_sig. + + Ltac synthesize_mul _ := synthesize_2arg_with_carry get_mul_sig. + Ltac synthesize_add _ := synthesize_2arg_with_carry get_add_sig. + Ltac synthesize_sub _ := synthesize_2arg_with_carry get_sub_sig. + Ltac synthesize_square _ := synthesize_1arg_with_carry get_square_sig. + Ltac synthesize_freeze _ := + let freeze_sig := get_freeze_sig () in + let feBW_bounded := get_feBW_bounded () in + start_preglue; + [ 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. + Ltac synthesize_xzladderstep _ := + let Mxzladderstep_sig := get_Mxzladderstep_sig () in + let a24_sig := get_a24_sig () in + start_preglue; + [ unmap_map_tuple (); + do_rewrite_with_sig_1arg Mxzladderstep_sig; + cbv [Mxzladderstep XZ.M.xzladderstep a24_sig]; cbn [proj1_sig]; + do_set_sigs (); + cbv_runtime + | .. ]; + finish_conjoined_preglue (); + refine_reflectively_gen CP.allowable_bit_widths default. +End PackageSynthesis. |