diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-05 22:00:28 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-10-18 23:01:29 -0400 |
| commit | b6e37eee58b0a8f43711533d49392172786e2cb5 (patch) | |
| tree | 8484c906ed9edfedd5ae8d3aedde0a08022e2013 | |
| parent | 6983ac1dce0411657dda4be7f49a0899e8a2b326 (diff) | |
Replace curve-specific definitions with tactics
This requires Coq >= 8.7
After | File Name | Before || Change
---------------------------------------------------------------------------------------
11m15.52s | Total | 11m14.53s || +0m00.99s
---------------------------------------------------------------------------------------
0m31.11s | Specific/X25519/C32/Synthesis | N/A || +0m31.10s
N/A | Specific/X25519/C32/ArithmeticSynthesisTest | 0m30.80s || -0m30.80s
0m09.61s | Specific/X25519/C64/Synthesis | N/A || +0m09.60s
N/A | Specific/X25519/C64/ArithmeticSynthesisTest | 0m08.56s || -0m08.56s
1m54.56s | Specific/X25519/C64/ladderstep | 1m56.56s || -0m02.00s
1m21.50s | Specific/IntegrationTestKaratsubaMul | 1m22.98s || -0m01.48s
1m15.96s | Specific/IntegrationTestLadderstep130 | 1m14.08s || +0m01.88s
0m51.80s | Specific/X25519/C32/femul | 0m53.79s || -0m01.99s
1m51.81s | Specific/NISTP256/AMD64/femul | 1m51.27s || +0m00.53s
0m28.68s | Specific/X25519/C32/fesquare | 0m28.30s || +0m00.37s
0m25.45s | Specific/IntegrationTestMontgomeryP256_128 | 0m25.60s || -0m00.15s
0m18.81s | Specific/NISTP256/AMD64/fesub | 0m18.32s || +0m00.48s
0m16.01s | Specific/NISTP256/AMD64/feadd | 0m15.86s || +0m00.15s
0m15.15s | Specific/NISTP256/AMD64/feopp | 0m14.95s || +0m00.20s
0m12.42s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m12.15s || +0m00.26s
0m12.41s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m12.31s || +0m00.09s
0m11.10s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m11.31s || -0m00.21s
0m10.70s | Specific/X25519/C64/femul | 0m10.17s || +0m00.52s
0m09.94s | Specific/NISTP256/AMD64/fenz | 0m09.94s || +0m00.00s
0m09.37s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.36s || +0m00.00s
0m08.78s | Specific/IntegrationTestSub | 0m08.84s || -0m00.06s
0m07.98s | Specific/IntegrationTestFreeze | 0m08.12s || -0m00.13s
0m07.42s | Specific/X25519/C64/fesquare | 0m07.22s || +0m00.20s
0m00.99s | Specific/SynthesisFramework | N/A || +0m00.99s
0m00.88s | Specific/ReificationTypes | 0m00.91s || -0m00.03s
0m00.85s | Specific/ArithmeticSynthesisFramework | N/A || +0m00.85s
N/A | Specific/X25519/C32/ReificationTypes | 0m00.82s || -0m00.82s
N/A | Specific/X25519/C64/ReificationTypes | 0m00.77s || -0m00.77s
0m00.77s | Specific/IntegrationTestTemporaryMiscCommon | 0m00.79s || -0m00.02s
0m00.72s | Specific/LadderstepSynthesisFramework | N/A || +0m00.72s
0m00.38s | Specific/IntegrationTestDisplayCommon | 0m00.40s || -0m00.02s
0m00.36s | Specific/IntegrationTestDisplayCommonTactics | 0m00.35s || +0m00.01s
20 files changed, 855 insertions, 983 deletions
diff --git a/_CoqProject b/_CoqProject index 3f2d895f5..afeab0c02 100644 --- a/_CoqProject +++ b/_CoqProject @@ -228,6 +228,7 @@ src/Spec/MontgomeryCurve.v src/Spec/MxDH.v src/Spec/WeierstrassCurve.v src/Spec/Test/X25519.v +src/Specific/ArithmeticSynthesisFramework.v src/Specific/ArithmeticSynthesisTest130.v src/Specific/CurveParameters.v src/Specific/IntegrationTestDisplayCommon.v @@ -252,8 +253,10 @@ src/Specific/IntegrationTestSub.v src/Specific/IntegrationTestSubDisplay.v src/Specific/IntegrationTestTemporaryMiscCommon.v src/Specific/Karatsuba.v +src/Specific/LadderstepSynthesisFramework.v src/Specific/MontgomeryP256_128.v src/Specific/ReificationTypes.v +src/Specific/SynthesisFramework.v src/Specific/NISTP256/AMD64/MontgomeryP256.v src/Specific/NISTP256/AMD64/feadd.v src/Specific/NISTP256/AMD64/feaddDisplay.v @@ -268,16 +271,14 @@ src/Specific/NISTP256/AMD64/fesubDisplay.v src/Specific/NISTP256/FancyMachine256/Barrett.v src/Specific/NISTP256/FancyMachine256/Core.v src/Specific/NISTP256/FancyMachine256/Montgomery.v -src/Specific/X25519/C32/ArithmeticSynthesisTest.v src/Specific/X25519/C32/CurveParameters.v -src/Specific/X25519/C32/ReificationTypes.v +src/Specific/X25519/C32/Synthesis.v src/Specific/X25519/C32/femul.v src/Specific/X25519/C32/femulDisplay.v src/Specific/X25519/C32/fesquare.v src/Specific/X25519/C32/fesquareDisplay.v -src/Specific/X25519/C64/ArithmeticSynthesisTest.v src/Specific/X25519/C64/CurveParameters.v -src/Specific/X25519/C64/ReificationTypes.v +src/Specific/X25519/C64/Synthesis.v src/Specific/X25519/C64/femul.v src/Specific/X25519/C64/femulDisplay.v src/Specific/X25519/C64/fesquare.v diff --git a/src/Specific/ArithmeticSynthesisFramework.v b/src/Specific/ArithmeticSynthesisFramework.v new file mode 100644 index 000000000..352ac7d41 --- /dev/null +++ b/src/Specific/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.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/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v index 79466b8d6..ef826dba5 100644 --- a/src/Specific/IntegrationTestFreeze.v +++ b/src/Specific/IntegrationTestFreeze.v @@ -1,62 +1,12 @@ -Require Import Crypto.Specific.X25519.C64.ReificationTypes. -Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest. -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 Import Crypto.Specific.X25519.C64.Synthesis. (* TODO : change this to field once field isomorphism happens *) Definition freeze : { freeze : feBW -> feBW | forall a, phiBW (freeze a) = phiBW a }. Proof. - start_preglue. - do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime. - all:fin_preglue. - (* jgross start here! *) - (*Set Ltac Profiling.*) - Time refine_reflectively_gen P.freeze_allowable_bit_widths anf. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *) - (*Show Ltac Profile.*) - (* total time: 5.680s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively_gen --------------- 0.0% 100.0% 1 5.680s -─ReflectiveTactics.do_reflective_pipelin 0.0% 95.8% 1 5.444s -─ReflectiveTactics.solve_side_conditions 0.4% 95.6% 1 5.428s -─ReflectiveTactics.do_reify ------------ 46.0% 61.7% 1 3.504s -─UnifyAbstractReflexivity.unify_transfor 22.9% 28.4% 7 0.372s -─Reify_rhs_gen ------------------------- 0.7% 8.3% 1 0.472s -─eexact -------------------------------- 7.2% 7.2% 131 0.012s -─ReflectiveTactics.unify_abstract_cbv_in 3.9% 4.9% 1 0.280s -─Glue.refine_to_reflective_glue' ------- 0.0% 4.2% 1 0.236s -─Glue.zrange_to_reflective ------------- 0.1% 3.3% 1 0.188s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.052s -─prove_interp_compile_correct ---------- 0.0% 2.7% 1 0.152s -─clear (var_list) ---------------------- 2.7% 2.7% 91 0.028s -─rewrite ?EtaInterp.InterpExprEta ------ 2.5% 2.5% 1 0.140s -─ClearAll.clear_all -------------------- 0.4% 2.5% 7 0.036s -─Glue.zrange_to_reflective_goal -------- 2.0% 2.4% 1 0.136s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively_gen --------------- 0.0% 100.0% 1 5.680s - ├─ReflectiveTactics.do_reflective_pipel 0.0% 95.8% 1 5.444s - │└ReflectiveTactics.solve_side_conditio 0.4% 95.6% 1 5.428s - │ ├─ReflectiveTactics.do_reify -------- 46.0% 61.7% 1 3.504s - │ │ ├─Reify_rhs_gen ------------------- 0.7% 8.3% 1 0.472s - │ │ │└prove_interp_compile_correct ---- 0.0% 2.7% 1 0.152s - │ │ │└rewrite ?EtaInterp.InterpExprEta 2.5% 2.5% 1 0.140s - │ │ └─eexact -------------------------- 7.2% 7.2% 131 0.012s - │ ├─UnifyAbstractReflexivity.unify_tran 22.9% 28.4% 7 0.372s - │ │ ├─ClearAll.clear_all -------------- 0.4% 2.5% 7 0.036s - │ │ │└clear (var_list) ---------------- 2.1% 2.1% 70 0.028s - │ │ └─unify (constr) (constr) --------- 2.3% 2.3% 5 0.044s - │ └─ReflectiveTactics.unify_abstract_cb 3.9% 4.9% 1 0.280s - └─Glue.refine_to_reflective_glue' ----- 0.0% 4.2% 1 0.236s - └Glue.zrange_to_reflective ----------- 0.1% 3.3% 1 0.188s - └Glue.zrange_to_reflective_goal ------ 2.0% 2.4% 1 0.136s - - *) -Time Defined. (* Finished transaction in 3.607 secs (3.607u,0.s) (successful) *) + Set Ltac Profiling. + Time synthesize_freeze (). + Show Ltac Profile. +Time Defined. diff --git a/src/Specific/IntegrationTestSub.v b/src/Specific/IntegrationTestSub.v index c40041a1c..99999c9ae 100644 --- a/src/Specific/IntegrationTestSub.v +++ b/src/Specific/IntegrationTestSub.v @@ -1,63 +1,12 @@ -Require Import Crypto.Specific.X25519.C64.ReificationTypes. -Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest. -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 Import Crypto.Specific.X25519.C64.Synthesis. (* TODO : change this to field once field isomorphism happens *) Definition sub : { sub : feBW -> feBW -> feBW | forall a b, phiBW (sub a b) = F.sub (phiBW a) (phiBW b) }. Proof. - start_preglue. - do_rewrite_with_2sig_add_carry sub_sig carry_sig; cbv_runtime. - all:fin_preglue. - (* jgross start here! *) - (*Set Ltac Profiling.*) - Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *) - (*Show Ltac Profile.*) - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s - *) -Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *) + Set Ltac Profiling. + Time synthesize_sub (). + Show Ltac Profile. +Time Defined. diff --git a/src/Specific/IntegrationTestTemporaryMiscCommon.v b/src/Specific/IntegrationTestTemporaryMiscCommon.v index 083e82207..41bef884c 100644 --- a/src/Specific/IntegrationTestTemporaryMiscCommon.v +++ b/src/Specific/IntegrationTestTemporaryMiscCommon.v @@ -171,7 +171,8 @@ 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 cbv beta iota delta [proj1_sig f_sig] in 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 _ := diff --git a/src/Specific/LadderstepSynthesisFramework.v b/src/Specific/LadderstepSynthesisFramework.v new file mode 100644 index 000000000..d6afb31eb --- /dev/null +++ b/src/Specific/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/ReificationTypes.v b/src/Specific/ReificationTypes.v index cc705689b..3a160e04d 100644 --- a/src/Specific/ReificationTypes.v +++ b/src/Specific/ReificationTypes.v @@ -139,7 +139,7 @@ Ltac pose_phiBW feBW m wt phiBW := ltac:(exact (fun x : feBW => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x))) phiBW. -Ltac get_ReificationTypes_package wt sz bounds m wt_nonneg upper_bound_of_exponent := +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 @@ -166,12 +166,12 @@ Ltac get_ReificationTypes_package wt sz bounds m wt_nonneg upper_bound_of_expone 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 bounds m wt_nonneg upper_bound_of_exponent := +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 bounds m wt_nonneg upper_bound_of_exponent in + let pkg := get_ReificationTypes_package wt sz m wt_nonneg upper_bound_of_exponent in exact pkg. Module Type ReificationTypesPrePackage. @@ -180,22 +180,28 @@ Module Type ReificationTypesPrePackage. End ReificationTypesPrePackage. Module MakeReificationTypes (RP : ReificationTypesPrePackage). - Definition ReificationTypes_package := RP.ReificationTypes_package. - Ltac reduce_proj x := - let RP_ReificationTypes_package := (eval cbv [ReificationTypes_package] in ReificationTypes_package) in - let v := (eval cbv [ReificationTypes_package RP_ReificationTypes_package] in x) in - exact v. + 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(" Notation %s := (ltac:(reduce_proj (let '(%s) := ReificationTypes_package in %s))) (only parsing)." % (i, terms, i)) + 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)) >> *) - Notation feZ := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feZ))) (only parsing). - Notation feW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feW))) (only parsing). - Notation feW_bounded := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feW_bounded))) (only parsing). - Notation feBW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feBW))) (only parsing). - Notation feBW_bounded := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in feBW_bounded))) (only parsing). - Notation phiW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in phiW))) (only parsing). - Notation phiBW := (ltac:(reduce_proj (let '(feZ, feW, feW_bounded, feBW, feBW_bounded, phiW, phiBW) := ReificationTypes_package in phiBW))) (only parsing). + 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 new file mode 100644 index 000000000..a09e2fd61 --- /dev/null +++ b/src/Specific/SynthesisFramework.v @@ -0,0 +1,104 @@ +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/ArithmeticSynthesisTest.v b/src/Specific/X25519/C32/ArithmeticSynthesisTest.v deleted file mode 100644 index c961afd69..000000000 --- a/src/Specific/X25519/C32/ArithmeticSynthesisTest.v +++ /dev/null @@ -1,252 +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.Specific.X25519.C32.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. -Local Notation tuple := Tuple.tuple. -Local Open Scope list_scope. -Local Open Scope Z_scope. -Local Coercion Z.of_nat : nat >-> Z. - -Module P := CurveParameters.FillCurveParameters Curve. - -Section Ops. - Local Infix "^" := tuple : type_scope. - - (* These definitions will need to be passed as Ltac arguments (or - cleverly inferred) when things are eventually automated *) - Definition sz : nat := P.compute P.sz. - Definition bitwidth : Z := P.compute P.bitwidth. - Definition s : Z := P.unfold P.s. (* don't want to compute, e.g., [2^255] *) - Definition c : list B.limb := P.compute P.c. - Definition carry_chain1 := P.compute P.carry_chain1. - Definition carry_chain2 := P.compute P.carry_chain2. - - Definition a24 := P.compute P.a24. - Definition coef_div_modulus : nat := P.compute P.coef_div_modulus. - (* These definitions are inferred from those above *) - Definition m := Eval vm_compute in Z.to_pos (s - Associational.eval c). (* modulus *) - Section wt. - Import QArith Qround. - Local Coercion QArith_base.inject_Z : Z >-> Q. - Definition wt (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i). - End wt. - Definition sz2 := Eval vm_compute in ((sz * 2) - 1)%nat. - Definition m_enc := - Eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c)). - Definition coef := (* subtraction coefficient *) - 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). - Definition coef_mod : mod_eq m (Positional.eval (n:=sz) wt coef) 0 := eq_refl. - Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed. - Lemma wt_nonzero i : wt i <> 0. - Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed. - Lemma wt_nonneg i : 0 <= wt i. - Proof. apply pow_ceil_mul_nat_nonneg; vm_decide. Qed. - Lemma wt_divides i : wt (S i) / wt i > 0. - Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed. - Lemma wt_divides' i : wt (S i) / wt i <> 0. - Proof. symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides. Qed. - Definition wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0 := wt_divides' i. - Definition wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0 := wt_divides' i. - - Local Ltac solve_constant_sig := - 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. - - Definition zero_sig : - { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 0%F}. - Proof. - solve_constant_sig. - Defined. - - Definition one_sig : - { one : Z^sz | Positional.Fdecode (m:=m) wt one = 1%F}. - Proof. - solve_constant_sig. - Defined. - - Definition a24_sig : - { a24t : Z^sz | Positional.Fdecode (m:=m) wt a24t = F.of_Z m a24 }. - Proof. - solve_constant_sig. - Defined. - - Definition add_sig : - { 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 }. - Proof. - 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. - Defined. - - Definition sub_sig : - {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}. - Proof. - 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. - Defined. - - Definition opp_sig : - {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)}. - Proof. - 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. - Defined. - - Definition mul_sig : - {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}. - Proof. - 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. - Defined. - - Definition square_sig : - {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}. - Proof. - 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. - Defined. - - (* Performs a full carry loop (as specified by carry_chain) *) - Definition carry_sig : - {carry : (Z^sz -> Z^sz)%type | - forall a : Z^sz, - let eval := Positional.Fdecode (m := m) wt in - eval (carry a) = eval a}. - Proof. - 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. - Defined. - - Section PreFreeze. - Lemma wt_pos i : wt i > 0. - Proof. eapply pow_ceil_mul_nat_pos; vm_decide. Qed. - - Lemma wt_multiples i : wt (S i) mod (wt i) = 0. - Proof. apply pow_ceil_mul_nat_multiples; vm_decide. Qed. - End PreFreeze. - - Hint Opaque freeze : uncps. - Hint Rewrite freeze_id : uncps. - - Definition freeze_sig : - {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}. - Proof. - 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. - Defined. - - Definition ring := - (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) - ). - -(* -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). -*) - -End Ops. diff --git a/src/Specific/X25519/C32/ReificationTypes.v b/src/Specific/X25519/C32/ReificationTypes.v deleted file mode 100644 index c5a9e0fd3..000000000 --- a/src/Specific/X25519/C32/ReificationTypes.v +++ /dev/null @@ -1,12 +0,0 @@ -Require Import Crypto.Specific.ReificationTypes. -Require Import Crypto.Specific.X25519.C32.ArithmeticSynthesisTest. - -Module RP <: ReificationTypesPrePackage. - Definition ReificationTypes_package' : { T : _ & T }. - Proof. make_ReificationTypes_package wt sz bounds m wt_nonneg P.upper_bound_of_exponent. Defined. - - Definition ReificationTypes_package - := Eval cbv [ReificationTypes_package' projT2] in projT2 ReificationTypes_package'. -End RP. - -Module Export ReificationTypes := MakeReificationTypes RP. diff --git a/src/Specific/X25519/C32/Synthesis.v b/src/Specific/X25519/C32/Synthesis.v new file mode 100644 index 000000000..f4068d043 --- /dev/null +++ b/src/Specific/X25519/C32/Synthesis.v @@ -0,0 +1,14 @@ +Require Import Crypto.Specific.SynthesisFramework. +Require Import Crypto.Specific.X25519.C32.CurveParameters. + +Module Import T := MakeSynthesisTactics Curve. + +Module P <: SynthesisPrePackage. + Definition Synthesis_package' : Synthesis_package'_Type. + Proof. make_synthesis_package (). Defined. + + Definition Synthesis_package + := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'. +End P. + +Module Export S := PackageSynthesis Curve P. diff --git a/src/Specific/X25519/C32/femul.v b/src/Specific/X25519/C32/femul.v index 9802a372e..81bf1f255 100644 --- a/src/Specific/X25519/C32/femul.v +++ b/src/Specific/X25519/C32/femul.v @@ -1,63 +1,12 @@ -Require Import Crypto.Specific.X25519.C32.ReificationTypes. -Require Import Crypto.Specific.X25519.C32.ArithmeticSynthesisTest. -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 Import Crypto.Specific.X25519.C32.Synthesis. (* TODO : change this to field once field isomorphism happens *) Definition mul : { mul : feBW -> feBW -> feBW | forall a b, phiBW (mul a b) = F.mul (phiBW a) (phiBW b) }. Proof. - start_preglue. - do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime. - all:fin_preglue. - (* jgross start here! *) - (*Set Ltac Profiling.*) - Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *) - (*Show Ltac Profile.*) - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s - *) -Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *) + Set Ltac Profiling. + Time synthesize_mul (). + Show Ltac Profile. +Time Defined. diff --git a/src/Specific/X25519/C32/fesquare.v b/src/Specific/X25519/C32/fesquare.v index ff1d0a566..3fa837bd2 100644 --- a/src/Specific/X25519/C32/fesquare.v +++ b/src/Specific/X25519/C32/fesquare.v @@ -1,63 +1,12 @@ -Require Import Crypto.Specific.X25519.C32.ReificationTypes. -Require Import Crypto.Specific.X25519.C32.ArithmeticSynthesisTest. -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 Import Crypto.Specific.X25519.C32.Synthesis. (* TODO : change this to field once field isomorphism happens *) Definition square : { square : feBW -> feBW | forall a, phiBW (square a) = F.mul (phiBW a) (phiBW a) }. Proof. - start_preglue. - do_rewrite_with_1sig_add_carry square_sig carry_sig; cbv_runtime. - all:fin_preglue. - (* jgross start here! *) - (*Set Ltac Profiling.*) - Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *) - (*Show Ltac Profile.*) - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s - *) -Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *) + Set Ltac Profiling. + Time synthesize_square (). + Show Ltac Profile. +Time Defined. diff --git a/src/Specific/X25519/C64/ArithmeticSynthesisTest.v b/src/Specific/X25519/C64/ArithmeticSynthesisTest.v deleted file mode 100644 index 6994e13be..000000000 --- a/src/Specific/X25519/C64/ArithmeticSynthesisTest.v +++ /dev/null @@ -1,252 +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.Specific.X25519.C64.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. -Local Notation tuple := Tuple.tuple. -Local Open Scope list_scope. -Local Open Scope Z_scope. -Local Coercion Z.of_nat : nat >-> Z. - -Module P := CurveParameters.FillCurveParameters Curve. - -Section Ops. - Local Infix "^" := tuple : type_scope. - - (* These definitions will need to be passed as Ltac arguments (or - cleverly inferred) when things are eventually automated *) - Definition sz : nat := P.compute P.sz. - Definition bitwidth : Z := P.compute P.bitwidth. - Definition s : Z := P.unfold P.s. (* don't want to compute, e.g., [2^255] *) - Definition c : list B.limb := P.compute P.c. - Definition carry_chain1 := P.compute P.carry_chain1. - Definition carry_chain2 := P.compute P.carry_chain2. - - Definition a24 := P.compute P.a24. - Definition coef_div_modulus : nat := P.compute P.coef_div_modulus. - (* These definitions are inferred from those above *) - Definition m := Eval vm_compute in Z.to_pos (s - Associational.eval c). (* modulus *) - Section wt. - Import QArith Qround. - Local Coercion QArith_base.inject_Z : Z >-> Q. - Definition wt (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i). - End wt. - Definition sz2 := Eval vm_compute in ((sz * 2) - 1)%nat. - Definition m_enc := - Eval vm_compute in (Positional.encode (modulo:=modulo) (div:=div) (n:=sz) wt (s-Associational.eval c)). - Definition coef := (* subtraction coefficient *) - 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). - Definition coef_mod : mod_eq m (Positional.eval (n:=sz) wt coef) 0 := eq_refl. - Lemma sz_nonzero : sz <> 0%nat. Proof. vm_decide. Qed. - Lemma wt_nonzero i : wt i <> 0. - Proof. eapply pow_ceil_mul_nat_nonzero; vm_decide. Qed. - Lemma wt_nonneg i : 0 <= wt i. - Proof. apply pow_ceil_mul_nat_nonneg; vm_decide. Qed. - Lemma wt_divides i : wt (S i) / wt i > 0. - Proof. apply pow_ceil_mul_nat_divide; vm_decide. Qed. - Lemma wt_divides' i : wt (S i) / wt i <> 0. - Proof. symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides. Qed. - Definition wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0 := wt_divides' i. - Definition wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0 := wt_divides' i. - - Local Ltac solve_constant_sig := - 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. - - Definition zero_sig : - { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 0%F}. - Proof. - solve_constant_sig. - Defined. - - Definition one_sig : - { one : Z^sz | Positional.Fdecode (m:=m) wt one = 1%F}. - Proof. - solve_constant_sig. - Defined. - - Definition a24_sig : - { a24t : Z^sz | Positional.Fdecode (m:=m) wt a24t = F.of_Z m a24 }. - Proof. - solve_constant_sig. - Defined. - - Definition add_sig : - { 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 }. - Proof. - 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. - Defined. - - Definition sub_sig : - {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}. - Proof. - 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. - Defined. - - Definition opp_sig : - {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)}. - Proof. - 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. - Defined. - - Definition mul_sig : - {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}. - Proof. - 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. - Defined. - - Definition square_sig : - {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}. - Proof. - 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. - Defined. - - (* Performs a full carry loop (as specified by carry_chain) *) - Definition carry_sig : - {carry : (Z^sz -> Z^sz)%type | - forall a : Z^sz, - let eval := Positional.Fdecode (m := m) wt in - eval (carry a) = eval a}. - Proof. - 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. - Defined. - - Section PreFreeze. - Lemma wt_pos i : wt i > 0. - Proof. eapply pow_ceil_mul_nat_pos; vm_decide. Qed. - - Lemma wt_multiples i : wt (S i) mod (wt i) = 0. - Proof. apply pow_ceil_mul_nat_multiples; vm_decide. Qed. - End PreFreeze. - - Hint Opaque freeze : uncps. - Hint Rewrite freeze_id : uncps. - - Definition freeze_sig : - {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}. - Proof. - 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. - Defined. - - Definition ring := - (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) - ). - -(* -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). -*) - -End Ops. diff --git a/src/Specific/X25519/C64/ReificationTypes.v b/src/Specific/X25519/C64/ReificationTypes.v deleted file mode 100644 index 0e999b2fc..000000000 --- a/src/Specific/X25519/C64/ReificationTypes.v +++ /dev/null @@ -1,12 +0,0 @@ -Require Import Crypto.Specific.ReificationTypes. -Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest. - -Module RP <: ReificationTypesPrePackage. - Definition ReificationTypes_package' : { T : _ & T }. - Proof. make_ReificationTypes_package wt sz bounds m wt_nonneg P.upper_bound_of_exponent. Defined. - - Definition ReificationTypes_package - := Eval cbv [ReificationTypes_package' projT2] in projT2 ReificationTypes_package'. -End RP. - -Module Export ReificationTypes := MakeReificationTypes RP. diff --git a/src/Specific/X25519/C64/Synthesis.v b/src/Specific/X25519/C64/Synthesis.v new file mode 100644 index 000000000..d77bb5cee --- /dev/null +++ b/src/Specific/X25519/C64/Synthesis.v @@ -0,0 +1,14 @@ +Require Import Crypto.Specific.SynthesisFramework. +Require Import Crypto.Specific.X25519.C64.CurveParameters. + +Module Import T := MakeSynthesisTactics Curve. + +Module P <: SynthesisPrePackage. + Definition Synthesis_package' : Synthesis_package'_Type. + Proof. make_synthesis_package (). Defined. + + Definition Synthesis_package + := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'. +End P. + +Module Export S := PackageSynthesis Curve P. diff --git a/src/Specific/X25519/C64/femul.v b/src/Specific/X25519/C64/femul.v index f0db6c937..1e015ddd9 100644 --- a/src/Specific/X25519/C64/femul.v +++ b/src/Specific/X25519/C64/femul.v @@ -1,63 +1,12 @@ -Require Import Crypto.Specific.X25519.C64.ReificationTypes. -Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest. -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 Import Crypto.Specific.X25519.C64.Synthesis. (* TODO : change this to field once field isomorphism happens *) Definition mul : { mul : feBW -> feBW -> feBW | forall a b, phiBW (mul a b) = F.mul (phiBW a) (phiBW b) }. Proof. - start_preglue. - do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime. - all:fin_preglue. - (* jgross start here! *) - (*Set Ltac Profiling.*) - Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *) - (*Show Ltac Profile.*) - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s - *) -Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *) + Set Ltac Profiling. + Time synthesize_mul (). + Show Ltac Profile. +Time Defined. diff --git a/src/Specific/X25519/C64/fesquare.v b/src/Specific/X25519/C64/fesquare.v index 6be0713b6..cfad2d111 100644 --- a/src/Specific/X25519/C64/fesquare.v +++ b/src/Specific/X25519/C64/fesquare.v @@ -1,63 +1,12 @@ -Require Import Crypto.Specific.X25519.C64.ReificationTypes. -Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest. -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 Import Crypto.Specific.X25519.C64.Synthesis. (* TODO : change this to field once field isomorphism happens *) Definition square : { square : feBW -> feBW | forall a, phiBW (square a) = F.mul (phiBW a) (phiBW a) }. Proof. - start_preglue. - do_rewrite_with_1sig_add_carry square_sig carry_sig; cbv_runtime. - all:fin_preglue. - (* jgross start here! *) - (*Set Ltac Profiling.*) - Time refine_reflectively_gen P.allowable_bit_widths default. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *) - (*Show Ltac Profile.*) - (* total time: 19.632s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s -─ReflectiveTactics.do_reflective_pipelin -0.0% 96.2% 1 18.884s -─ReflectiveTactics.solve_side_conditions 1.2% 96.1% 1 18.860s -─ReflectiveTactics.do_reify ------------ 27.7% 44.0% 1 8.640s -─ReflectiveTactics.abstract_vm_compute_r 12.3% 13.9% 2 2.024s -─ReflectiveTactics.abstract_vm_compute_r 8.9% 12.2% 2 1.576s -─Reify_rhs_gen ------------------------- 0.8% 11.7% 1 2.300s -─ReflectiveTactics.renamify_rhs -------- 10.4% 11.5% 1 2.260s -─ReflectiveTactics.abstract_rhs -------- 4.6% 5.8% 1 1.148s -─clear (var_list) ---------------------- 5.2% 5.2% 57 0.184s -─eexact -------------------------------- 4.1% 4.1% 68 0.028s -─prove_interp_compile_correct ---------- 0.0% 3.4% 1 0.664s -─ReflectiveTactics.abstract_cbv_interp_r 2.7% 3.3% 1 0.648s -─unify (constr) (constr) --------------- 3.2% 3.2% 6 0.248s -─rewrite ?EtaInterp.InterpExprEta ------ 3.1% 3.1% 1 0.612s -─ReflectiveTactics.abstract_cbv_rhs ---- 2.0% 2.7% 1 0.532s -─Glue.refine_to_reflective_glue -------- 0.0% 2.2% 1 0.436s -─rewrite H ----------------------------- 2.1% 2.1% 1 0.420s - - tactic local total calls max -────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─refine_reflectively ------------------- 0.0% 98.4% 1 19.320s - ├─ReflectiveTactics.do_reflective_pipel -0.0% 96.2% 1 18.884s - │└ReflectiveTactics.solve_side_conditio 1.2% 96.1% 1 18.860s - │ ├─ReflectiveTactics.do_reify -------- 27.7% 44.0% 1 8.640s - │ │ ├─Reify_rhs_gen ------------------- 0.8% 11.7% 1 2.300s - │ │ │ ├─prove_interp_compile_correct -- 0.0% 3.4% 1 0.664s - │ │ │ │└rewrite ?EtaInterp.InterpExprEt 3.1% 3.1% 1 0.612s - │ │ │ └─rewrite H --------------------- 2.1% 2.1% 1 0.420s - │ │ └─eexact -------------------------- 4.1% 4.1% 68 0.028s - │ ├─ReflectiveTactics.abstract_vm_compu 12.3% 13.9% 2 2.024s - │ ├─ReflectiveTactics.abstract_vm_compu 8.9% 12.2% 2 1.576s - │ ├─ReflectiveTactics.renamify_rhs ---- 10.4% 11.5% 1 2.260s - │ ├─ReflectiveTactics.abstract_rhs ---- 4.6% 5.8% 1 1.148s - │ ├─ReflectiveTactics.abstract_cbv_inte 2.7% 3.3% 1 0.648s - │ └─ReflectiveTactics.abstract_cbv_rhs 2.0% 2.7% 1 0.532s - └─Glue.refine_to_reflective_glue ------ 0.0% 2.2% 1 0.436s - *) -Time Defined. (* Finished transaction in 10.167 secs (10.123u,0.023s) (successful) *) + Set Ltac Profiling. + Time synthesize_square (). + Show Ltac Profile. +Time Defined. diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v index 0d7c33588..11238e0b2 100644 --- a/src/Specific/X25519/C64/ladderstep.v +++ b/src/Specific/X25519/C64/ladderstep.v @@ -1,74 +1,7 @@ -Require Import Coq.Classes.Morphisms. - -Require Import Crypto.Specific.X25519.C64.ReificationTypes. -Require Import Crypto.Specific.X25519.C64.ArithmeticSynthesisTest. Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Specific.IntegrationTestTemporaryMiscCommon. -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Require Import Crypto.Util.FixedWordSizes. -Require Import Coq.ZArith.BinIntDef. -Require Import Crypto.Curves.Montgomery.XZ. -Require Import Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift. -Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.LetIn. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Require Import Crypto.Util.Tactics.SetEvars. -Require Import Crypto.Util.Tactics.SubstEvars. -Require Import Crypto.Util.Tactics.ETransitivity. -Require Import Crypto.Util.Notations. - -(** TODO(jadep,andreser): Move to NewBaseSystemTest? *) -Definition FMxzladderstep := @M.donnaladderstep (F m) F.add F.sub F.mul. - -Section with_notations. - Local Infix "+" := (proj1_sig add_sig). - Local Notation "a * b" := (proj1_sig carry_sig (proj1_sig mul_sig a b)). - Local Notation "x ^ 2" := (proj1_sig carry_sig (proj1_sig square_sig x)). - Local Infix "-" := (proj1_sig sub_sig). - 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? *) -Definition Mxzladderstep_sig - : { 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 (eval a24) (eval x1) (Tuple.map (n:=2) eval Q) (Tuple.map (n:=2) eval Q') }. -Proof. - exists Mxzladderstep. - intros a24 x1 Q Q' eval. - cbv [Mxzladderstep FMxzladderstep M.donnaladderstep]. - destruct Q, Q'; cbv [map map' fst snd Let_In eval]. - repeat rewrite ?(proj2_sig add_sig), ?(proj2_sig mul_sig), ?(proj2_sig square_sig), ?(proj2_sig sub_sig), ?(proj2_sig carry_sig). - reflexivity. -Defined. +Require Import Crypto.Specific.LadderstepSynthesisFramework. +Require Import Crypto.Specific.X25519.C64.Synthesis. (* TODO : change this to field once field isomorphism happens *) Definition xzladderstep : @@ -81,35 +14,9 @@ Definition xzladderstep : -> feW_bounded (fst Q') /\ feW_bounded (snd Q') -> ((feW_bounded (fst (fst xz)) /\ feW_bounded (snd (fst xz))) /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz)))) - /\ Tuple.map (n:=2) (Tuple.map (n:=2) phiW) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phiW x1) (Tuple.map (n:=2) phiW Q) (Tuple.map (n:=2) phiW Q') }. + /\ Tuple.map (n:=2) (Tuple.map (n:=2) phiW) xz = FMxzladderstep (m:=m) (eval (proj1_sig a24_sig)) (phiW x1) (Tuple.map (n:=2) phiW Q) (Tuple.map (n:=2) phiW Q') }. Proof. - start_preglue. - unmap_map_tuple (). - do_rewrite_with_sig_1arg Mxzladderstep_sig. - cbv [Mxzladderstep M.xzladderstep a24_sig]; cbn [proj1_sig]. - do_set_sigs (). - cbv_runtime. - all:finish_conjoined_preglue (). - (* jgross start here! *) Set Ltac Profiling. - (* - Time Glue.refine_to_reflective_glue P.allowable_bit_widths. - Time ReflectiveTactics.refine_with_pipeline_correct default. - { Time ReflectiveTactics.do_reify. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_vm_compute_rhs_reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_renamify_rhs_reflexivity. } - { Time SubstLet.subst_let; clear; abstract vm_cast_no_check (eq_refl true). } - { Time SubstLet.subst_let; clear; vm_compute; reflexivity. } - { Time UnifyAbstractReflexivity.unify_abstract_compute_rhs_reflexivity. } - { Time ReflectiveTactics.unify_abstract_cbv_interp_rhs_reflexivity. } - { Time abstract ReflectiveTactics.handle_bounds_from_hyps. } - { Time abstract ReflectiveTactics.handle_boundedness_side_condition. } - *) - Time refine_reflectively_gen P.allowable_bit_widths default. + synthesize_xzladderstep (). Show Ltac Profile. Time Defined. diff --git a/src/Specific/X25519/C64/ladderstepDisplay.log b/src/Specific/X25519/C64/ladderstepDisplay.log index 4e22b729f..6fb2a27d6 100644 --- a/src/Specific/X25519/C64/ladderstepDisplay.log +++ b/src/Specific/X25519/C64/ladderstepDisplay.log @@ -1,4 +1,4 @@ -λ x x0 x1 x2 x3 : ReificationTypes.RP.feW, +λ x x0 x1 x2 x3 : Synthesis.P.feW, let (a, b) := Interp-η (λ var : Syntax.base_type → Type, λ '(x15, x16, x14, x12, x10, (x25, x26, x24, x22, x20, (x33, x34, x32, x30, x28)), (x43, x44, x42, x40, x38, (x51, x52, x50, x48, x46)))%core, @@ -367,4 +367,4 @@ let (a, b) := Interp-η (let (a0, b0) := a in (a0, b0), let (a0, b0) := b in (a0, b0))%core - : ReificationTypes.RP.feW → ReificationTypes.RP.feW → ReificationTypes.RP.feW → ReificationTypes.RP.feW → ReificationTypes.RP.feW → ReificationTypes.RP.feW * ReificationTypes.RP.feW * (ReificationTypes.RP.feW * ReificationTypes.RP.feW) + : Synthesis.P.feW → Synthesis.P.feW → Synthesis.P.feW → Synthesis.P.feW → Synthesis.P.feW → Synthesis.P.feW * Synthesis.P.feW * (Synthesis.P.feW * Synthesis.P.feW) |