From ffa0731cc244091460586b46bf4817e5a918ba49 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 5 Oct 2017 22:32:49 -0400 Subject: Reorgainze synthesis framework files into a Framework folder --- src/Specific/ArithmeticSynthesisFramework.v | 565 --------------------- src/Specific/CurveParameters.v | 114 ----- .../Framework/ArithmeticSynthesisFramework.v | 565 +++++++++++++++++++++ src/Specific/Framework/CurveParameters.v | 114 +++++ .../Framework/IntegrationTestDisplayCommon.v | 24 + .../IntegrationTestDisplayCommonTactics.v | 149 ++++++ .../Framework/IntegrationTestTemporaryMiscCommon.v | 288 +++++++++++ .../Framework/LadderstepSynthesisFramework.v | 93 ++++ src/Specific/Framework/ReificationTypes.v | 207 ++++++++ src/Specific/Framework/SynthesisFramework.v | 104 ++++ src/Specific/IntegrationTestDisplayCommon.v | 24 - src/Specific/IntegrationTestDisplayCommonTactics.v | 149 ------ src/Specific/IntegrationTestFreezeDisplay.v | 2 +- src/Specific/IntegrationTestKaratsubaMul.v | 2 +- src/Specific/IntegrationTestKaratsubaMulDisplay.v | 2 +- src/Specific/IntegrationTestLadderstep130.v | 2 +- src/Specific/IntegrationTestLadderstep130Display.v | 2 +- src/Specific/IntegrationTestMontgomeryP256_128.v | 2 +- .../IntegrationTestMontgomeryP256_128Display.v | 2 +- .../IntegrationTestMontgomeryP256_128_Add.v | 2 +- .../IntegrationTestMontgomeryP256_128_AddDisplay.v | 2 +- .../IntegrationTestMontgomeryP256_128_Nonzero.v | 2 +- ...egrationTestMontgomeryP256_128_NonzeroDisplay.v | 2 +- .../IntegrationTestMontgomeryP256_128_Opp.v | 2 +- .../IntegrationTestMontgomeryP256_128_OppDisplay.v | 2 +- .../IntegrationTestMontgomeryP256_128_Sub.v | 2 +- .../IntegrationTestMontgomeryP256_128_SubDisplay.v | 2 +- src/Specific/IntegrationTestSubDisplay.v | 2 +- src/Specific/IntegrationTestTemporaryMiscCommon.v | 288 ----------- src/Specific/LadderstepSynthesisFramework.v | 93 ---- src/Specific/NISTP256/AMD64/feadd.v | 2 +- src/Specific/NISTP256/AMD64/feaddDisplay.v | 2 +- src/Specific/NISTP256/AMD64/femul.v | 2 +- src/Specific/NISTP256/AMD64/femulDisplay.v | 2 +- src/Specific/NISTP256/AMD64/fenz.v | 2 +- src/Specific/NISTP256/AMD64/fenzDisplay.v | 2 +- src/Specific/NISTP256/AMD64/feopp.v | 2 +- src/Specific/NISTP256/AMD64/feoppDisplay.v | 2 +- src/Specific/NISTP256/AMD64/fesub.v | 2 +- src/Specific/NISTP256/AMD64/fesubDisplay.v | 2 +- src/Specific/ReificationTypes.v | 207 -------- src/Specific/SynthesisFramework.v | 104 ---- src/Specific/X25519/C32/CurveParameters.v | 2 +- src/Specific/X25519/C32/Synthesis.v | 2 +- src/Specific/X25519/C32/femulDisplay.v | 2 +- src/Specific/X25519/C32/fesquareDisplay.v | 2 +- src/Specific/X25519/C64/CurveParameters.v | 2 +- src/Specific/X25519/C64/Synthesis.v | 2 +- src/Specific/X25519/C64/femulDisplay.v | 2 +- src/Specific/X25519/C64/fesquareDisplay.v | 2 +- src/Specific/X25519/C64/ladderstep.v | 2 +- src/Specific/X25519/C64/ladderstepDisplay.v | 2 +- 52 files changed, 1580 insertions(+), 1580 deletions(-) delete mode 100644 src/Specific/ArithmeticSynthesisFramework.v delete mode 100644 src/Specific/CurveParameters.v create mode 100644 src/Specific/Framework/ArithmeticSynthesisFramework.v create mode 100644 src/Specific/Framework/CurveParameters.v create mode 100644 src/Specific/Framework/IntegrationTestDisplayCommon.v create mode 100644 src/Specific/Framework/IntegrationTestDisplayCommonTactics.v create mode 100644 src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v create mode 100644 src/Specific/Framework/LadderstepSynthesisFramework.v create mode 100644 src/Specific/Framework/ReificationTypes.v create mode 100644 src/Specific/Framework/SynthesisFramework.v delete mode 100644 src/Specific/IntegrationTestDisplayCommon.v delete mode 100644 src/Specific/IntegrationTestDisplayCommonTactics.v delete mode 100644 src/Specific/IntegrationTestTemporaryMiscCommon.v delete mode 100644 src/Specific/LadderstepSynthesisFramework.v delete mode 100644 src/Specific/ReificationTypes.v delete mode 100644 src/Specific/SynthesisFramework.v (limited to 'src') diff --git a/src/Specific/ArithmeticSynthesisFramework.v b/src/Specific/ArithmeticSynthesisFramework.v deleted file mode 100644 index 352ac7d41..000000000 --- a/src/Specific/ArithmeticSynthesisFramework.v +++ /dev/null @@ -1,565 +0,0 @@ -Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. -Require Import Coq.Lists.List. Import ListNotations. -Require Import Crypto.Arithmetic.Core. Import B. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Arithmetic.Saturated.Freeze. -Require Crypto.Specific.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/CurveParameters.v b/src/Specific/CurveParameters.v deleted file mode 100644 index aa679a4d3..000000000 --- a/src/Specific/CurveParameters.v +++ /dev/null @@ -1,114 +0,0 @@ -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/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. diff --git a/src/Specific/IntegrationTestDisplayCommon.v b/src/Specific/IntegrationTestDisplayCommon.v deleted file mode 100644 index 6d68da21a..000000000 --- a/src/Specific/IntegrationTestDisplayCommon.v +++ /dev/null @@ -1,24 +0,0 @@ -Require Import Crypto.Util.Sigma.Lift. -Require Import Crypto.Util.Sigma.Associativity. -Require Import Crypto.Util.Sigma.MapProjections. -Require Import Crypto.Specific.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.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/IntegrationTestDisplayCommonTactics.v b/src/Specific/IntegrationTestDisplayCommonTactics.v deleted file mode 100644 index 999fbe1ed..000000000 --- a/src/Specific/IntegrationTestDisplayCommonTactics.v +++ /dev/null @@ -1,149 +0,0 @@ -Require Import Crypto.Util.Sigma.Lift. -Require Import Crypto.Util.Sigma.Associativity. -Require Import Crypto.Util.Sigma.MapProjections. -Require Import Crypto.Specific.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/IntegrationTestFreezeDisplay.v b/src/Specific/IntegrationTestFreezeDisplay.v index c6d13e05a..ab17a7e93 100644 --- a/src/Specific/IntegrationTestFreezeDisplay.v +++ b/src/Specific/IntegrationTestFreezeDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestFreeze. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display freeze. diff --git a/src/Specific/IntegrationTestKaratsubaMul.v b/src/Specific/IntegrationTestKaratsubaMul.v index 0a29973a1..8474a05c9 100644 --- a/src/Specific/IntegrationTestKaratsubaMul.v +++ b/src/Specific/IntegrationTestKaratsubaMul.v @@ -11,7 +11,7 @@ Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Tactics.MoveLetIn. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestKaratsubaMulDisplay.v b/src/Specific/IntegrationTestKaratsubaMulDisplay.v index 96312713b..7649ca88b 100644 --- a/src/Specific/IntegrationTestKaratsubaMulDisplay.v +++ b/src/Specific/IntegrationTestKaratsubaMulDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestKaratsubaMul. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v index e97784c5a..aba794f4b 100644 --- a/src/Specific/IntegrationTestLadderstep130.v +++ b/src/Specific/IntegrationTestLadderstep130.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.SubstEvars. Require Import Crypto.Curves.Montgomery.XZ. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestLadderstep130Display.v b/src/Specific/IntegrationTestLadderstep130Display.v index 41efe786d..fa498e475 100644 --- a/src/Specific/IntegrationTestLadderstep130Display.v +++ b/src/Specific/IntegrationTestLadderstep130Display.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestLadderstep130. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display xzladderstep. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128.v b/src/Specific/IntegrationTestMontgomeryP256_128.v index feca5ad9a..d2b64d3b9 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128Display.v b/src/Specific/IntegrationTestMontgomeryP256_128Display.v index 6b96923fc..420ff7dc5 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128Display.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128Display.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Add.v b/src/Specific/IntegrationTestMontgomeryP256_128_Add.v index a9fea3ef1..ff94e57ee 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Add.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Add.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v b/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v index dcacc2227..13c7937cb 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_AddDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Add. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display add. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v index 27e710fe6..76664255c 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v @@ -17,7 +17,7 @@ Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v b/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v index 0f9c0c284..0d76f5171 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_NonzeroDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Nonzero. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display nonzero. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v b/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v index 1869a7952..c908c1258 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v b/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v index 0abe0f38d..ca8721d7d 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Opp. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display opp. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v b/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v index 62b1ef328..8f3df4cdf 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v b/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v index 55e6595fe..879a8e0cd 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestMontgomeryP256_128_Sub. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display sub. diff --git a/src/Specific/IntegrationTestSubDisplay.v b/src/Specific/IntegrationTestSubDisplay.v index 9f8e5eadc..37a060f26 100644 --- a/src/Specific/IntegrationTestSubDisplay.v +++ b/src/Specific/IntegrationTestSubDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.IntegrationTestSub. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display sub. diff --git a/src/Specific/IntegrationTestTemporaryMiscCommon.v b/src/Specific/IntegrationTestTemporaryMiscCommon.v deleted file mode 100644 index 41bef884c..000000000 --- a/src/Specific/IntegrationTestTemporaryMiscCommon.v +++ /dev/null @@ -1,288 +0,0 @@ -(*** 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/LadderstepSynthesisFramework.v b/src/Specific/LadderstepSynthesisFramework.v deleted file mode 100644 index d6afb31eb..000000000 --- a/src/Specific/LadderstepSynthesisFramework.v +++ /dev/null @@ -1,93 +0,0 @@ -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/NISTP256/AMD64/feadd.v b/src/Specific/NISTP256/AMD64/feadd.v index 5de6fc03a..23a38978c 100644 --- a/src/Specific/NISTP256/AMD64/feadd.v +++ b/src/Specific/NISTP256/AMD64/feadd.v @@ -15,7 +15,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/NISTP256/AMD64/feaddDisplay.v b/src/Specific/NISTP256/AMD64/feaddDisplay.v index 452044402..b6e79f393 100644 --- a/src/Specific/NISTP256/AMD64/feaddDisplay.v +++ b/src/Specific/NISTP256/AMD64/feaddDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.NISTP256.AMD64.feadd. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display add. diff --git a/src/Specific/NISTP256/AMD64/femul.v b/src/Specific/NISTP256/AMD64/femul.v index f87e6d26b..5904b1fff 100644 --- a/src/Specific/NISTP256/AMD64/femul.v +++ b/src/Specific/NISTP256/AMD64/femul.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/NISTP256/AMD64/femulDisplay.v b/src/Specific/NISTP256/AMD64/femulDisplay.v index f47c0ba06..acde66b0e 100644 --- a/src/Specific/NISTP256/AMD64/femulDisplay.v +++ b/src/Specific/NISTP256/AMD64/femulDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.NISTP256.AMD64.femul. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/NISTP256/AMD64/fenz.v b/src/Specific/NISTP256/AMD64/fenz.v index c74e7a872..13dc4478f 100644 --- a/src/Specific/NISTP256/AMD64/fenz.v +++ b/src/Specific/NISTP256/AMD64/fenz.v @@ -17,7 +17,7 @@ Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/NISTP256/AMD64/fenzDisplay.v b/src/Specific/NISTP256/AMD64/fenzDisplay.v index c4119449f..77c48f76f 100644 --- a/src/Specific/NISTP256/AMD64/fenzDisplay.v +++ b/src/Specific/NISTP256/AMD64/fenzDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.NISTP256.AMD64.fenz. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display nonzero. diff --git a/src/Specific/NISTP256/AMD64/feopp.v b/src/Specific/NISTP256/AMD64/feopp.v index 14342c238..d57948035 100644 --- a/src/Specific/NISTP256/AMD64/feopp.v +++ b/src/Specific/NISTP256/AMD64/feopp.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/NISTP256/AMD64/feoppDisplay.v b/src/Specific/NISTP256/AMD64/feoppDisplay.v index 9075af2f2..7d2a65b6f 100644 --- a/src/Specific/NISTP256/AMD64/feoppDisplay.v +++ b/src/Specific/NISTP256/AMD64/feoppDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.NISTP256.AMD64.feopp. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display opp. diff --git a/src/Specific/NISTP256/AMD64/fesub.v b/src/Specific/NISTP256/AMD64/fesub.v index adf278faa..4098ffcfc 100644 --- a/src/Specific/NISTP256/AMD64/fesub.v +++ b/src/Specific/NISTP256/AMD64/fesub.v @@ -16,7 +16,7 @@ Require Import Crypto.Util.Tactics.MoveLetIn. Require Import Crypto.Util.Tactics.DestructHead. Import ListNotations. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. +Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. Require Import Crypto.Compilers.Z.Bounds.Pipeline. diff --git a/src/Specific/NISTP256/AMD64/fesubDisplay.v b/src/Specific/NISTP256/AMD64/fesubDisplay.v index 0f771869c..01559b019 100644 --- a/src/Specific/NISTP256/AMD64/fesubDisplay.v +++ b/src/Specific/NISTP256/AMD64/fesubDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.NISTP256.AMD64.fesub. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display sub. diff --git a/src/Specific/ReificationTypes.v b/src/Specific/ReificationTypes.v deleted file mode 100644 index 3a160e04d..000000000 --- a/src/Specific/ReificationTypes.v +++ /dev/null @@ -1,207 +0,0 @@ -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/SynthesisFramework.v b/src/Specific/SynthesisFramework.v deleted file mode 100644 index a09e2fd61..000000000 --- a/src/Specific/SynthesisFramework.v +++ /dev/null @@ -1,104 +0,0 @@ -Require Import Crypto.Specific.ArithmeticSynthesisFramework. -Require Import Crypto.Specific.ReificationTypes. -Require Import Crypto.Specific.LadderstepSynthesisFramework. -Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.BoundedWord. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. -Require Import Crypto.Compilers.Z.Bounds.Pipeline. -Require Crypto.Specific.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. diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v index 8e7848bc1..5040bf182 100644 --- a/src/Specific/X25519/C32/CurveParameters.v +++ b/src/Specific/X25519/C32/CurveParameters.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.CurveParameters. +Require Import Crypto.Specific.Framework.CurveParameters. Require Import Crypto.Util.LetIn. (*** diff --git a/src/Specific/X25519/C32/Synthesis.v b/src/Specific/X25519/C32/Synthesis.v index f4068d043..3b9b35078 100644 --- a/src/Specific/X25519/C32/Synthesis.v +++ b/src/Specific/X25519/C32/Synthesis.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.SynthesisFramework. +Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import Crypto.Specific.X25519.C32.CurveParameters. Module Import T := MakeSynthesisTactics Curve. diff --git a/src/Specific/X25519/C32/femulDisplay.v b/src/Specific/X25519/C32/femulDisplay.v index e603a33c0..d37a0e668 100644 --- a/src/Specific/X25519/C32/femulDisplay.v +++ b/src/Specific/X25519/C32/femulDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C32.femul. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/X25519/C32/fesquareDisplay.v b/src/Specific/X25519/C32/fesquareDisplay.v index 1cc917c7e..5075db1fd 100644 --- a/src/Specific/X25519/C32/fesquareDisplay.v +++ b/src/Specific/X25519/C32/fesquareDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C32.fesquare. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display square. diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v index 1e15eea24..3b8016e96 100644 --- a/src/Specific/X25519/C64/CurveParameters.v +++ b/src/Specific/X25519/C64/CurveParameters.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.CurveParameters. +Require Import Crypto.Specific.Framework.CurveParameters. Require Import Crypto.Util.LetIn. (*** diff --git a/src/Specific/X25519/C64/Synthesis.v b/src/Specific/X25519/C64/Synthesis.v index d77bb5cee..3c3bac04d 100644 --- a/src/Specific/X25519/C64/Synthesis.v +++ b/src/Specific/X25519/C64/Synthesis.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.SynthesisFramework. +Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import Crypto.Specific.X25519.C64.CurveParameters. Module Import T := MakeSynthesisTactics Curve. diff --git a/src/Specific/X25519/C64/femulDisplay.v b/src/Specific/X25519/C64/femulDisplay.v index 35c557ce5..0e77976ca 100644 --- a/src/Specific/X25519/C64/femulDisplay.v +++ b/src/Specific/X25519/C64/femulDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C64.femul. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/X25519/C64/fesquareDisplay.v b/src/Specific/X25519/C64/fesquareDisplay.v index f39710fec..e722863e2 100644 --- a/src/Specific/X25519/C64/fesquareDisplay.v +++ b/src/Specific/X25519/C64/fesquareDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C64.fesquare. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display square. diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v index 11238e0b2..adb20912e 100644 --- a/src/Specific/X25519/C64/ladderstep.v +++ b/src/Specific/X25519/C64/ladderstep.v @@ -1,6 +1,6 @@ Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.LadderstepSynthesisFramework. +Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework. Require Import Crypto.Specific.X25519.C64.Synthesis. (* TODO : change this to field once field isomorphism happens *) diff --git a/src/Specific/X25519/C64/ladderstepDisplay.v b/src/Specific/X25519/C64/ladderstepDisplay.v index 73aab21ab..0716f8ef1 100644 --- a/src/Specific/X25519/C64/ladderstepDisplay.v +++ b/src/Specific/X25519/C64/ladderstepDisplay.v @@ -1,4 +1,4 @@ Require Import Crypto.Specific.X25519.C64.ladderstep. -Require Import Crypto.Specific.IntegrationTestDisplayCommon. +Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display xzladderstep. -- cgit v1.2.3