diff options
20 files changed, 670 insertions, 730 deletions
diff --git a/.gitignore b/.gitignore index 191e360a7..b2acd253d 100644 --- a/.gitignore +++ b/.gitignore @@ -61,6 +61,8 @@ src/Specific/X25519/C32/measure src/Specific/X25519/C32/test src/Specific/X2555/C128/ladderstep.c src/Specific/X2555/C128/ladderstep.h +src/Specific/X2448/Karatsuba/C64/femul.c +src/Specific/X2448/Karatsuba/C64/femul.h third_party/openssl-curve25519/measure third_party/openssl-nistp256c64/measure third_party/openssl-nistz256-adx/measure @@ -61,7 +61,7 @@ SPECIAL_VOFILES := src/Specific/%Display.vo UNMADE_VOFILES := # add files to this list to prevent them from being built as final # targets by the "lite" target -LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo src/Specific/Karatsuba.vo src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.vo src/Specific/X25519/C64/ladderstep.vo src/Specific/X25519/C32/%.vo +LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo src/Specific/X2448/Karatsuba/C64/Synthesis.vo src/Specific/NISTP256/AMD64/IntegrationTestMontgomeryP256.vo src/Specific/X25519/C64/ladderstep.vo src/Specific/X25519/C32/%.vo REGULAR_VOFILES := $(filter-out $(SPECIAL_VOFILES),$(VOFILES)) CURVES_PROOFS_PRE_VOFILES := $(filter src/Curves/%Proofs.vo,$(REGULAR_VOFILES)) NO_CURVES_PROOFS_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo diff --git a/_CoqProject b/_CoqProject index e141313b6..e2619d54b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -228,9 +228,6 @@ src/Spec/MontgomeryCurve.v src/Spec/MxDH.v src/Spec/WeierstrassCurve.v src/Spec/Test/X25519.v -src/Specific/ArithmeticSynthesisTest130.v -src/Specific/IntegrationTestKaratsubaMul.v -src/Specific/IntegrationTestKaratsubaMulDisplay.v src/Specific/IntegrationTestMontgomeryP256_128.v src/Specific/IntegrationTestMontgomeryP256_128Display.v src/Specific/IntegrationTestMontgomeryP256_128_Add.v @@ -241,7 +238,6 @@ src/Specific/IntegrationTestMontgomeryP256_128_Opp.v src/Specific/IntegrationTestMontgomeryP256_128_OppDisplay.v src/Specific/IntegrationTestMontgomeryP256_128_Sub.v src/Specific/IntegrationTestMontgomeryP256_128_SubDisplay.v -src/Specific/Karatsuba.v src/Specific/MontgomeryP256_128.v src/Specific/Framework/ArithmeticSynthesisFramework.v src/Specific/Framework/CurveParameters.v @@ -265,6 +261,10 @@ 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/X2448/Karatsuba/C64/CurveParameters.v +src/Specific/X2448/Karatsuba/C64/Synthesis.v +src/Specific/X2448/Karatsuba/C64/femul.v +src/Specific/X2448/Karatsuba/C64/femulDisplay.v src/Specific/X25519/C32/CurveParameters.v src/Specific/X25519/C32/Synthesis.v src/Specific/X25519/C32/femul.v diff --git a/src/Specific/ArithmeticSynthesisTest130.v b/src/Specific/ArithmeticSynthesisTest130.v deleted file mode 100644 index e9e40df19..000000000 --- a/src/Specific/ArithmeticSynthesisTest130.v +++ /dev/null @@ -1,224 +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.Util.Decidable. -Require Import Crypto.Util.LetIn Crypto.Util.ZUtil. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Crypto.Util.Tuple. -Local Notation tuple := Tuple.tuple. -Local Open Scope list_scope. -Local Open Scope Z_scope. -Local Coercion Z.of_nat : nat >-> Z. - -(*** -Modulus : 2^255-5 -Base: 130 -***) -Section Ops51. - 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 := 3%nat. - Definition s : Z := 2^255. - Definition c : list B.limb := [(1, 5)]. - Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *) - Definition carry_chain1 := Eval vm_compute in (seq 0 (pred sz)). - Definition carry_chain2 := ([0;1])%nat. - Definition a24 := 121665%Z. (* XXX TODO(andreser) FIXME? Is this right for this curve? *) - - (* These definitions are inferred from those above *) - Definition m := Eval vm_compute in Z.to_pos (s - Associational.eval c). (* modulus *) - Definition wt := fun i : nat => - let si := Z.log2 s * i in - 2 ^ ((si/sz) + (if dec ((si/sz)*sz=si) then 0 else 1)). - Definition sz2 := Eval vm_compute in ((sz * 2) - 1)%nat. - Definition coef := (* subtraction coefficient *) - Eval vm_compute in - ( let p := Positional.encode - (modulo:=modulo) (div:=div) (n:=sz) - wt (s-Associational.eval c) in - (fix addp (acc: Z^sz) (ctr : nat) : Z^sz := - match ctr with - | O => acc - | S n => addp (Positional.add_cps wt acc p 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. - apply Z.pow_nonzero; zero_bounds; try break_match; vm_decide. - Qed. - - Lemma wt_divides_chain1 i (H:In i carry_chain1) : wt (S i) / wt i <> 0. - Proof. - cbv [In carry_chain1] in H. - repeat match goal with H : _ \/ _ |- _ => destruct H end; - try (exfalso; assumption); subst; try vm_decide. - Qed. - Lemma wt_divides_chain2 i (H:In i carry_chain2) : wt (S i) / wt i <> 0. - Proof. - cbv [In carry_chain2] in H. - repeat match goal with H : _ \/ _ |- _ => destruct H end; - try (exfalso; assumption); subst; try vm_decide. - Qed. - Lemma wt_divides_full i : wt (S i) / wt i <> 0. - Proof. - cbv [wt]. - match goal with |- _ ^ ?x / _ ^ ?y <> _ => assert (0 <= y <= x) end. - { rewrite Nat2Z.inj_succ. - split; try break_match; ring_simplify; - repeat match goal with - | _ => apply Z.div_le_mono; try vm_decide; [ ] - | _ => apply Z.mul_le_mono_nonneg_l; try vm_decide; [ ] - | _ => apply Z.add_le_mono; try vm_decide; [ ] - | |- ?x <= ?y + 1 => assert (x <= y); [|omega] - | |- ?x + 1 <= ?y => rewrite <- Z.div_add by vm_decide - | _ => progress zero_bounds - | _ => progress ring_simplify - | _ => vm_decide - end. } - break_match; rewrite <-Z.pow_sub_r by omega; - apply Z.pow_nonzero; omega. - Qed. - - 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. reflexivity. - - (* rough breakdown of synthesis time *) - (* 1.2s for side conditions -- should improve significantly when [chained_carries] gets a correctness lemma *) - (* basesystem_partial_evaluation_RHS (primarily vm_compute): 1.8s, which gets re-computed during defined *) - - (* doing [cbv -[Let_In runtime_add runtime_mul]] took 37s *) - - Defined. (* 3s *) - - (* 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. - - Definition ring_51 := - (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_full) - (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 Ops51. diff --git a/src/Specific/CurveParameters/x25519_c64.json b/src/Specific/CurveParameters/x25519_c64.json index 45f27b535..d65187d05 100644 --- a/src/Specific/CurveParameters/x25519_c64.json +++ b/src/Specific/CurveParameters/x25519_c64.json @@ -4,8 +4,7 @@ "a24" : "121665", "sz" : "5", "bitwidth" : "64", - "carry_chain1" : "default", - "carry_chain2" : ["0", "1"], + "carry_chains" : ["default", ["0", "1"]], "coef_div_modulus" : "2", "operations" : ["femul", "fesquare", "freeze", "ladderstep"], "extra_files" : ["X25519_C64/scalarmult.c"], diff --git a/src/Specific/Framework/ArithmeticSynthesisFramework.v b/src/Specific/Framework/ArithmeticSynthesisFramework.v index 77624ed41..342c759fe 100644 --- a/src/Specific/Framework/ArithmeticSynthesisFramework.v +++ b/src/Specific/Framework/ArithmeticSynthesisFramework.v @@ -6,8 +6,11 @@ Require Import Crypto.Arithmetic.Saturated.Freeze. Require Crypto.Specific.Framework.CurveParameters. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.LetIn Crypto.Util.ZUtil. +Require Import Crypto.Arithmetic.Karatsuba. Require Import Crypto.Util.Tactics.BreakMatch. Require Crypto.Util.Tuple. +Require Import Crypto.Util.IdfunWithAlt. +Require Import Crypto.Util.Tactics.VM. Require Import Crypto.Util.QUtil. Require Import Crypto.Util.Tactics.PoseTermWithName. @@ -58,12 +61,9 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete (list B.limb) ltac:(let v := P.do_compute P.c in exact v) c. - Ltac pose_carry_chain1 carry_chain1 := - let v := P.do_compute P.carry_chain1 in - cache_term v carry_chain1. - Ltac pose_carry_chain2 carry_chain2 := - let v := P.do_compute P.carry_chain2 in - cache_term v carry_chain2. + Ltac pose_carry_chains carry_chains := + let v := P.do_compute P.carry_chains in + cache_term v carry_chains. Ltac pose_a24 a24 := let v := P.do_compute P.a24 in @@ -73,6 +73,11 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete nat ltac:(let v := P.do_compute P.coef_div_modulus in exact v) coef_div_modulus. + Ltac pose_goldilocks goldilocks := + cache_term_with_type_by + bool + ltac:(let v := P.do_compute P.goldilocks in exact v) + goldilocks. (* These definitions are inferred from those above *) Ltac pose_m s c m := (* modulus *) let v := (eval vm_compute in (Z.to_pos (s - Associational.eval c))) in @@ -130,16 +135,25 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete (forall i, wt (S i) / wt i <> 0) ltac:(symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_divides) wt_divides'. - Ltac pose_wt_divides_chain1 wt carry_chain1 wt_divides' wt_divides_chain1 := - cache_term_with_type_by - (forall i (H:In i carry_chain1), wt (S i) / wt i <> 0) - ltac:(let i := fresh "i" in intros i ?; exact (wt_divides' i)) - wt_divides_chain1. - Ltac pose_wt_divides_chain2 wt carry_chain2 wt_divides' wt_divides_chain2 := + Ltac helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chain := cache_term_with_type_by - (forall i (H:In i carry_chain2), wt (S i) / wt i <> 0) + (forall i (H:In i carry_chain), wt (S i) / wt i <> 0) ltac:(let i := fresh "i" in intros i ?; exact (wt_divides' i)) - wt_divides_chain2. + wt_divides_chain. + Ltac pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains := + lazymatch carry_chains with + | ?carry_chain :: nil + => helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chains + | ?carry_chain :: ?carry_chains + => let wt_divides_chains := fresh wt_divides_chains in + let wt_divides_chain := fresh wt_divides_chains in + let wt_divides_chain := helper_pose_wt_divides_chain wt carry_chain wt_divides' wt_divides_chain in + let wt_divides_chains := pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains in + constr:((wt_divides_chain, wt_divides_chains)) + end. + Ltac pose_wt_divides_chains wt carry_chains wt_divides' wt_divides_chains := + let carry_chains := (eval cbv delta [carry_chains] in carry_chains) in + pose_wt_divides_chains' wt carry_chains wt_divides' wt_divides_chains. Local Ltac solve_constant_sig := idtac; @@ -215,6 +229,99 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete solve_op_F wt x; reflexivity) opp_sig. + Ltac pose_half_sz sz half_sz := + let v := (eval compute in (sz / 2)%nat) in + cache_term v half_sz. + Ltac pose_half_sz_nonzero half_sz half_sz_nonzero := + cache_proof_with_type_by + (half_sz <> 0%nat) + ltac:(cbv; congruence) + half_sz_nonzero. + + Ltac basesystem_partial_evaluation_RHS := + let t0 := (match goal with + | |- _ _ ?t => t + end) in + let t := + eval + cbv + delta [Positional.to_associational_cps Positional.to_associational + Positional.eval Positional.zeros Positional.add_to_nth_cps + Positional.add_to_nth Positional.place_cps Positional.place + Positional.from_associational_cps Positional.from_associational + Positional.carry_cps Positional.carry + Positional.chained_carries_cps Positional.chained_carries + Positional.sub_cps Positional.sub Positional.split_cps + Positional.scmul_cps Positional.unbalanced_sub_cps + Positional.negate_snd_cps Positional.add_cps Positional.opp_cps + Associational.eval Associational.multerm Associational.mul_cps + Associational.mul Associational.split_cps Associational.split + Associational.reduce_cps Associational.reduce + Associational.carryterm_cps Associational.carryterm + Associational.carry_cps Associational.carry + Associational.negate_snd_cps Associational.negate_snd div modulo + id_tuple_with_alt id_tuple'_with_alt + ] + in t0 + in + let t := eval pattern @runtime_mul in t in + let t := (match t with + | ?t _ => t + end) in + let t := eval pattern @runtime_add in t in + let t := (match t with + | ?t _ => t + end) in + let t := eval pattern @runtime_opp in t in + let t := (match t with + | ?t _ => t + end) in + let t := eval pattern @runtime_shr in t in + let t := (match t with + | ?t _ => t + end) in + let t := eval pattern @runtime_and in t in + let t := (match t with + | ?t _ => t + end) in + let t := eval pattern @Let_In in t in + let t := (match t with + | ?t _ => t + end) in + let t := eval pattern @id_with_alt in t in + let t := (match t with + | ?t _ => t + end) in + let t1 := fresh "t1" in + pose (t1 := t); + transitivity + (t1 (@id_with_alt) (@Let_In) (@runtime_and) (@runtime_shr) (@runtime_opp) (@runtime_add) + (@runtime_mul)); + [ replace_with_vm_compute t1; clear t1 | reflexivity ]. + + (** XXX TODO(jadep) FIXME: Is sqrt(s) the right thing to pass to goldilocks_mul_cps (the original code hard-coded 2^224 *) + Ltac pose_sqrt_s s sqrt_s := + let v := (eval vm_compute in (Z.log2 s / 2)) in + cache_term (2^v) sqrt_s. + + Ltac pose_goldilocks_mul_sig goldilocks sz wt s c half_sz sqrt_s goldilocks_mul_sig := + lazymatch eval compute in goldilocks with + | true + => cache_term_with_type_by + {mul : (Z^sz -> Z^sz -> Z^sz)%type | + forall a b : Z^sz, + mul a b = goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt sqrt_s a b (fun ab => Positional.reduce_cps (n:=sz) wt s c ab id)} + ltac:(eexists; cbv beta zeta; intros; + cbv [goldilocks_mul_cps]; + repeat autounfold; + basesystem_partial_evaluation_RHS; + do_replace_match_with_destructuring_match_in_goal; + reflexivity) + goldilocks_mul_sig + | false + => goldilocks_mul_sig + end. + Ltac pose_mul_sig sz m wt s c sz2 wt_nonzero mul_sig := cache_term_with_type_by {mul : (Z^sz -> Z^sz -> Z^sz)%type | @@ -235,6 +342,41 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring) mul_sig. + Ltac pose_mul_sig_from_goldilocks_mul_sig sz m wt s c half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig := + cache_term_with_type_by + {mul : (Z^sz -> Z^sz -> Z^sz)%type | + forall a b : Z^sz, + let eval := Positional.Fdecode (m := m) wt in + Positional.Fdecode (m := m) wt (mul a b) = (eval a * eval b)%F} + ltac:(idtac; + let a := fresh "a" in + let b := fresh "b" in + eexists; cbv beta zeta; intros a b; + pose proof wt_nonzero; + let x := constr:( + goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt sqrt_s a b (fun ab => Positional.reduce_cps (n:=sz) wt s c ab id)) in + F_mod_eq; + transitivity (Positional.eval wt x); repeat autounfold; + + [ + | autorewrite with uncps push_id push_basesystem_eval; + apply goldilocks_mul_correct; try assumption; cbv; congruence ]; + cbv [mod_eq]; apply f_equal2; + [ | reflexivity ]; + apply f_equal; + etransitivity; [|apply (proj2_sig goldilocks_mul_sig)]; + cbv [proj1_sig goldilocks_mul_sig]; + reflexivity) + mul_sig. + + Ltac pose_mul_sig_full goldilocks sz m wt s c sz2 half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig := + lazymatch eval compute in goldilocks with + | true + => pose_mul_sig_from_goldilocks_mul_sig sz m wt s c half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig + | false + => pose_mul_sig sz m wt s c sz2 wt_nonzero mul_sig + end. + Ltac pose_square_sig sz m wt s c sz2 wt_nonzero square_sig := cache_term_with_type_by {square : (Z^sz -> Z^sz)%type | @@ -254,8 +396,51 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete break_match; cbv [Let_In runtime_mul runtime_add]; repeat apply (f_equal2 pair); rewrite ?Z.shiftl_mul_pow2 by omega; ring) square_sig. + Ltac pose_square_sig_from_mul_sig sz m wt mul_sig square_sig := + cache_term_with_type_by + {square : (Z^sz -> Z^sz)%type | + forall a : Z^sz, + let eval := Positional.Fdecode (m := m) wt in + Positional.Fdecode (m := m) wt (square a) = (eval a * eval a)%F} + ltac:(idtac; + let a := fresh "a" in + eexists; cbv beta zeta; intros a; + rewrite <-(proj2_sig mul_sig); + apply f_equal; + cbv [proj1_sig mul_sig]; + reflexivity) + square_sig. + + Ltac pose_square_sig_full goldilocks sz m wt s c sz2 wt_nonzero mul_sig square_sig := + lazymatch eval compute in goldilocks with + | true + => pose_square_sig_from_mul_sig sz m wt mul_sig square_sig + | false + => pose_square_sig sz m wt s c sz2 wt_nonzero square_sig + end. + + Ltac pose_proof_tuple ls := + lazymatch ls with + | pair ?x ?y => pose_proof_tuple x; pose_proof_tuple y + | ?ls => pose proof ls + end. + + Ltac make_chained_carries_cps' sz wt s c a carry_chains := + lazymatch carry_chains with + | ?carry_chain :: nil + => constr:(Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain id) + | ?carry_chain :: ?carry_chains + => let r := fresh "r" in + let r' := fresh r in + constr:(Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt a carry_chain + (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r + (fun r' => ltac:(let v := make_chained_carries_cps' sz wt s c r' carry_chains in exact v)))) + end. + Ltac make_chained_carries_cps sz wt s c a carry_chains := + let carry_chains := (eval cbv delta [carry_chains] in carry_chains) in + make_chained_carries_cps' sz wt s c a carry_chains. (* Performs a full carry loop (as specified by carry_chain) *) - Ltac pose_carry_sig sz m wt s c carry_chain1 carry_chain2 wt_nonzero wt_divides_chain1 wt_divides_chain2 carry_sig := + Ltac pose_carry_sig sz m wt s c carry_chains wt_nonzero wt_divides_chains carry_sig := cache_term_with_type_by {carry : (Z^sz -> Z^sz)%type | forall a : Z^sz, @@ -264,15 +449,9 @@ Module MakeArithmeticSynthesisTestTactics (Curve : CurveParameters.CurveParamete ltac:(idtac; let a := fresh "a" in eexists; cbv beta zeta; intros a; - pose proof wt_nonzero; pose proof wt_divides_chain1; - pose proof div_mod; pose proof wt_divides_chain2; - let x := constr:( - Positional.chained_carries_cps - (n:=sz) (div:=div)(modulo:=modulo) wt a carry_chain1 - (fun r => Positional.carry_reduce_cps - (n:=sz) (div:=div) (modulo:=modulo) wt s c r - (fun rrr => Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt rrr carry_chain2 id - ))) in + pose proof wt_nonzero; pose proof div_mod; + pose_proof_tuple wt_divides_chains; + let x := make_chained_carries_cps sz wt s c a carry_chains in solve_op_F wt x; reflexivity) carry_sig. @@ -409,10 +588,10 @@ print('End MakeArithmeticSynthesisTest.') let bitwidth := fresh "bitwidth" in let s := fresh "s" in let c := fresh "c" in - let carry_chain1 := fresh "carry_chain1" in - let carry_chain2 := fresh "carry_chain2" in + let carry_chains := fresh "carry_chains" in let a24 := fresh "a24" in let coef_div_modulus := fresh "coef_div_modulus" in + let goldilocks := fresh "goldilocks" in let m := fresh "m" in let wt := fresh "wt" in let sz2 := fresh "sz2" in @@ -424,14 +603,17 @@ print('End MakeArithmeticSynthesisTest.') let wt_nonneg := fresh "wt_nonneg" in let wt_divides := fresh "wt_divides" in let wt_divides' := fresh "wt_divides'" in - let wt_divides_chain1 := fresh "wt_divides_chain1" in - let wt_divides_chain2 := fresh "wt_divides_chain2" in + let wt_divides_chains := fresh "wt_divides_chains" in let zero_sig := fresh "zero_sig" in let one_sig := fresh "one_sig" in let a24_sig := fresh "a24_sig" in let add_sig := fresh "add_sig" in let sub_sig := fresh "sub_sig" in let opp_sig := fresh "opp_sig" in + let half_sz := fresh "half_sz" in + let half_sz_nonzero := fresh "half_sz_nonzero" in + let sqrt_s := fresh "sqrt_s" in + let goldilocks_mul_sig := fresh "goldilocks_mul_sig" in let mul_sig := fresh "mul_sig" in let square_sig := fresh "square_sig" in let carry_sig := fresh "carry_sig" in @@ -443,10 +625,10 @@ print('End MakeArithmeticSynthesisTest.') let bitwidth := pose_bitwidth bitwidth in let s := pose_s s in let c := pose_c c in - let carry_chain1 := pose_carry_chain1 carry_chain1 in - let carry_chain2 := pose_carry_chain2 carry_chain2 in + let carry_chains := pose_carry_chains carry_chains in let a24 := pose_a24 a24 in let coef_div_modulus := pose_coef_div_modulus coef_div_modulus in + let goldilocks := pose_goldilocks goldilocks in let m := pose_m s c m in let wt := pose_wt m sz wt in let sz2 := pose_sz2 sz sz2 in @@ -458,22 +640,25 @@ print('End MakeArithmeticSynthesisTest.') let wt_nonneg := pose_wt_nonneg wt wt_nonneg in let wt_divides := pose_wt_divides wt wt_divides in let wt_divides' := pose_wt_divides' wt wt_divides wt_divides' in - let wt_divides_chain1 := pose_wt_divides_chain1 wt carry_chain1 wt_divides' wt_divides_chain1 in - let wt_divides_chain2 := pose_wt_divides_chain2 wt carry_chain2 wt_divides' wt_divides_chain2 in + let wt_divides_chains := pose_wt_divides_chains wt carry_chains wt_divides' wt_divides_chains in let zero_sig := pose_zero_sig sz m wt zero_sig in let one_sig := pose_one_sig sz m wt one_sig in let a24_sig := pose_a24_sig sz m wt a24 a24_sig in let add_sig := pose_add_sig sz m wt wt_nonzero add_sig in let sub_sig := pose_sub_sig sz m wt wt_nonzero coef sub_sig in let opp_sig := pose_opp_sig sz m wt wt_nonzero coef opp_sig in - let mul_sig := pose_mul_sig sz m wt s c sz2 wt_nonzero mul_sig in - let square_sig := pose_square_sig sz m wt s c sz2 wt_nonzero square_sig in - let carry_sig := pose_carry_sig sz m wt s c carry_chain1 carry_chain2 wt_nonzero wt_divides_chain1 wt_divides_chain2 carry_sig in + let half_sz := pose_half_sz sz half_sz in + let half_sz_nonzero := pose_half_sz_nonzero half_sz half_sz_nonzero in + let sqrt_s := pose_sqrt_s s sqrt_s in + let goldilocks_mul_sig := pose_goldilocks_mul_sig goldilocks sz wt s c half_sz sqrt_s goldilocks_mul_sig in + let mul_sig := pose_mul_sig_full goldilocks sz m wt s c sz2 half_sz sqrt_s goldilocks_mul_sig wt_nonzero mul_sig in + let square_sig := pose_square_sig_full goldilocks sz m wt s c sz2 wt_nonzero mul_sig square_sig in + let carry_sig := pose_carry_sig sz m wt s c carry_chains wt_nonzero wt_divides_chains carry_sig in let wt_pos := pose_wt_pos wt wt_pos in let wt_multiples := pose_wt_multiples wt wt_multiples in let freeze_sig := pose_freeze_sig sz m wt c m_enc bitwidth wt_nonzero wt_pos wt_divides wt_multiples freeze_sig in let ring := pose_ring sz m wt wt_divides' sz_nonzero wt_nonzero zero_sig one_sig opp_sig add_sig sub_sig mul_sig ring in - constr:((sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring)). + constr:((sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring)). Ltac make_ArithmeticSynthesis_package _ := lazymatch goal with @@ -494,72 +679,76 @@ Module MakeArithmeticSynthesisTest (AP : ArithmeticSynthesisPrePackage). Ltac AS_reduce_proj x := eval cbv beta iota zeta in x. - Ltac get_sz _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz). + Ltac get_sz _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz). Notation sz := (ltac:(let v := get_sz () in exact v)) (only parsing). - Ltac get_bitwidth _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in bitwidth). + Ltac get_bitwidth _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in bitwidth). Notation bitwidth := (ltac:(let v := get_bitwidth () in exact v)) (only parsing). - Ltac get_s _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in s). + Ltac get_s _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in s). Notation s := (ltac:(let v := get_s () in exact v)) (only parsing). - Ltac get_c _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in c). + Ltac get_c _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in c). Notation c := (ltac:(let v := get_c () in exact v)) (only parsing). - Ltac get_carry_chain1 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_chain1). - Notation carry_chain1 := (ltac:(let v := get_carry_chain1 () in exact v)) (only parsing). - Ltac get_carry_chain2 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_chain2). - Notation carry_chain2 := (ltac:(let v := get_carry_chain2 () in exact v)) (only parsing). - Ltac get_a24 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in a24). + Ltac get_carry_chains _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_chains). + Notation carry_chains := (ltac:(let v := get_carry_chains () in exact v)) (only parsing). + Ltac get_a24 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in a24). Notation a24 := (ltac:(let v := get_a24 () in exact v)) (only parsing). - Ltac get_coef_div_modulus _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef_div_modulus). + Ltac get_coef_div_modulus _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef_div_modulus). Notation coef_div_modulus := (ltac:(let v := get_coef_div_modulus () in exact v)) (only parsing). - Ltac get_m _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in m). + Ltac get_goldilocks _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in goldilocks). + Notation goldilocks := (ltac:(let v := get_goldilocks () in exact v)) (only parsing). + Ltac get_m _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in m). Notation m := (ltac:(let v := get_m () in exact v)) (only parsing). - Ltac get_wt _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt). + Ltac get_wt _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt). Notation wt := (ltac:(let v := get_wt () in exact v)) (only parsing). - Ltac get_sz2 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz2). + Ltac get_sz2 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz2). Notation sz2 := (ltac:(let v := get_sz2 () in exact v)) (only parsing). - Ltac get_m_enc _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in m_enc). + Ltac get_m_enc _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in m_enc). Notation m_enc := (ltac:(let v := get_m_enc () in exact v)) (only parsing). - Ltac get_coef _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef). + Ltac get_coef _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef). Notation coef := (ltac:(let v := get_coef () in exact v)) (only parsing). - Ltac get_coef_mod _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef_mod). + Ltac get_coef_mod _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in coef_mod). Notation coef_mod := (ltac:(let v := get_coef_mod () in exact v)) (only parsing). - Ltac get_sz_nonzero _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz_nonzero). + Ltac get_sz_nonzero _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sz_nonzero). Notation sz_nonzero := (ltac:(let v := get_sz_nonzero () in exact v)) (only parsing). - Ltac get_wt_nonzero _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_nonzero). + Ltac get_wt_nonzero _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_nonzero). Notation wt_nonzero := (ltac:(let v := get_wt_nonzero () in exact v)) (only parsing). - Ltac get_wt_nonneg _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_nonneg). + Ltac get_wt_nonneg _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_nonneg). Notation wt_nonneg := (ltac:(let v := get_wt_nonneg () in exact v)) (only parsing). - Ltac get_wt_divides _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides). + Ltac get_wt_divides _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides). Notation wt_divides := (ltac:(let v := get_wt_divides () in exact v)) (only parsing). - Ltac get_wt_divides' _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides'). + Ltac get_wt_divides' _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides'). Notation wt_divides' := (ltac:(let v := get_wt_divides' () in exact v)) (only parsing). - Ltac get_wt_divides_chain1 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides_chain1). - Notation wt_divides_chain1 := (ltac:(let v := get_wt_divides_chain1 () in exact v)) (only parsing). - Ltac get_wt_divides_chain2 _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides_chain2). - Notation wt_divides_chain2 := (ltac:(let v := get_wt_divides_chain2 () in exact v)) (only parsing). - Ltac get_zero_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in zero_sig). + Ltac get_wt_divides_chains _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_divides_chains). + Notation wt_divides_chains := (ltac:(let v := get_wt_divides_chains () in exact v)) (only parsing). + Ltac get_zero_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in zero_sig). Notation zero_sig := (ltac:(let v := get_zero_sig () in exact v)) (only parsing). - Ltac get_one_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in one_sig). + Ltac get_one_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in one_sig). Notation one_sig := (ltac:(let v := get_one_sig () in exact v)) (only parsing). - Ltac get_a24_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in a24_sig). + Ltac get_a24_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in a24_sig). Notation a24_sig := (ltac:(let v := get_a24_sig () in exact v)) (only parsing). - Ltac get_add_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in add_sig). + Ltac get_add_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in add_sig). Notation add_sig := (ltac:(let v := get_add_sig () in exact v)) (only parsing). - Ltac get_sub_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sub_sig). + Ltac get_sub_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sub_sig). Notation sub_sig := (ltac:(let v := get_sub_sig () in exact v)) (only parsing). - Ltac get_opp_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in opp_sig). + Ltac get_opp_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in opp_sig). Notation opp_sig := (ltac:(let v := get_opp_sig () in exact v)) (only parsing). - Ltac get_mul_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in mul_sig). + Ltac get_half_sz _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in half_sz). + Notation half_sz := (ltac:(let v := get_half_sz () in exact v)) (only parsing). + Ltac get_half_sz_nonzero _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in half_sz_nonzero). + Notation half_sz_nonzero := (ltac:(let v := get_half_sz_nonzero () in exact v)) (only parsing). + Ltac get_sqrt_s _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in sqrt_s). + Notation sqrt_s := (ltac:(let v := get_sqrt_s () in exact v)) (only parsing). + Ltac get_mul_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in mul_sig). Notation mul_sig := (ltac:(let v := get_mul_sig () in exact v)) (only parsing). - Ltac get_square_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in square_sig). + Ltac get_square_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in square_sig). Notation square_sig := (ltac:(let v := get_square_sig () in exact v)) (only parsing). - Ltac get_carry_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_sig). + Ltac get_carry_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in carry_sig). Notation carry_sig := (ltac:(let v := get_carry_sig () in exact v)) (only parsing). - Ltac get_wt_pos _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_pos). + Ltac get_wt_pos _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_pos). Notation wt_pos := (ltac:(let v := get_wt_pos () in exact v)) (only parsing). - Ltac get_wt_multiples _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_multiples). + Ltac get_wt_multiples _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in wt_multiples). Notation wt_multiples := (ltac:(let v := get_wt_multiples () in exact v)) (only parsing). - Ltac get_freeze_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in freeze_sig). + Ltac get_freeze_sig _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in freeze_sig). Notation freeze_sig := (ltac:(let v := get_freeze_sig () in exact v)) (only parsing). - Ltac get_ring _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chain1, carry_chain2, a24, coef_div_modulus, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chain1, wt_divides_chain2, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in ring). + Ltac get_ring _ := let pkg := get_MakeArithmeticSynthesisTest_package () in AS_reduce_proj (let '(sz, bitwidth, s, c, carry_chains, a24, coef_div_modulus, goldilocks, m, wt, sz2, m_enc, coef, coef_mod, sz_nonzero, wt_nonzero, wt_nonneg, wt_divides, wt_divides', wt_divides_chains, zero_sig, one_sig, a24_sig, add_sig, sub_sig, opp_sig, half_sz, half_sz_nonzero, sqrt_s, mul_sig, square_sig, carry_sig, wt_pos, wt_multiples, freeze_sig, ring) := pkg in ring). Notation ring := (ltac:(let v := get_ring () in exact v)) (only parsing). End MakeArithmeticSynthesisTest. diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v index aa679a4d3..2d0bf5152 100644 --- a/src/Specific/Framework/CurveParameters.v +++ b/src/Specific/Framework/CurveParameters.v @@ -20,13 +20,13 @@ Module Type CurveParameters. Parameter bitwidth : Z. Parameter s : Z. Parameter c : list limb. - Parameter carry_chain1 - : option (list nat). (* defaults to [seq 0 (pred sz)] *) - Parameter carry_chain2 - : option (list nat). (* defaults to [0 :: 1 :: nil] *) - Parameter a24 : Z. + Parameter carry_chains + : option (list (list nat)). (* defaults to [seq 0 (pred sz) :: (0 :: 1 :: nil) :: nil] *) + Parameter a24 : option Z. Parameter coef_div_modulus : nat. + Parameter goldilocks : bool. + Parameter mul_code : option (Z^sz -> Z^sz -> Z^sz). Parameter square_code : option (Z^sz -> Z^sz). Parameter upper_bound_of_exponent @@ -54,11 +54,12 @@ Module FillCurveParameters (P : CurveParameters). Definition bitwidth := P.bitwidth. Definition s := P.s. Definition c := P.c. - Definition carry_chain1 := defaulted P.carry_chain1 (seq 0 (pred sz)). - Definition carry_chain2 := defaulted P.carry_chain2 (0 :: 1 :: nil)%nat. - Definition a24 := P.a24. + Definition carry_chains := defaulted P.carry_chains [seq 0 (pred sz); [0; 1]]%nat. + Definition a24 := defaulted P.a24 0. Definition coef_div_modulus := P.coef_div_modulus. + Definition goldilocks := P.goldilocks. + Ltac default_mul := lazymatch (eval hnf in P.mul_code) with | None => reflexivity @@ -85,10 +86,10 @@ Module FillCurveParameters (P : CurveParameters). let P_bitwidth := P.bitwidth in let P_s := P.s in let P_c := P.c in - let P_carry_chain1 := P.carry_chain1 in - let P_carry_chain2 := P.carry_chain2 in + let P_carry_chains := P.carry_chains in let P_a24 := P.a24 in let P_coef_div_modulus := P.coef_div_modulus in + let P_goldilocks := P.goldilocks in let P_mul_code := P.mul_code in let P_square_code := P.square_code in let P_upper_bound_of_exponent := P.upper_bound_of_exponent in @@ -96,8 +97,8 @@ Module FillCurveParameters (P : CurveParameters). let P_freeze_extra_allowable_bit_widths := P.freeze_extra_allowable_bit_widths in let v' := (eval cbv [id List.app - sz bitwidth s c carry_chain1 carry_chain2 a24 coef_div_modulus - P_sz P_bitwidth P_s P_c P_carry_chain1 P_carry_chain2 P_a24 P_coef_div_modulus + sz bitwidth s c carry_chains a24 coef_div_modulus goldilocks + P_sz P_bitwidth P_s P_c P_carry_chains P_a24 P_coef_div_modulus P_goldilocks P_mul_code P_square_code upper_bound_of_exponent allowable_bit_widths freeze_allowable_bit_widths P_upper_bound_of_exponent P_allowable_bit_widths P_freeze_extra_allowable_bit_widths diff --git a/src/Specific/Framework/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v index c30024181..9c80efaa0 100644 --- a/src/Specific/Framework/SynthesisFramework.v +++ b/src/Specific/Framework/SynthesisFramework.v @@ -18,10 +18,14 @@ Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters). 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) + | (?sz, ?bitwidth, ?s, ?c, ?carry_chains, ?a24, ?coef_div_modulus, ?goldilocks, ?m, ?wt, ?sz2, ?m_enc, ?coef, ?coef_mod, ?sz_nonzero, ?wt_nonzero, ?wt_nonneg, ?wt_divides, ?wt_divides', ?wt_divides_chains, ?zero_sig, ?one_sig, ?a24_sig, ?add_sig, ?sub_sig, ?opp_sig, ?half_sz, ?half_sz_nonzero, ?sqrt_s, ?mul_sig, ?square_sig, ?carry_sig, ?wt_pos, ?wt_multiples, ?freeze_sig, ?ring) => 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)) + | _ => let dummy := match goal with + | _ => fail "Did you update get_ArithmeticSynthesis_package but forget to update get_synthesis_package?" + end in + constr:(I : I) end. Ltac make_synthesis_package _ := lazymatch goal with diff --git a/src/Specific/Framework/make_curve.py b/src/Specific/Framework/make_curve.py index b530a72ee..6c155efb9 100755 --- a/src/Specific/Framework/make_curve.py +++ b/src/Specific/Framework/make_curve.py @@ -6,9 +6,8 @@ def compute_bitwidth(base): return 2**int(math.ceil(math.log(base, 2))) def compute_sz(modulus, base): return 1 + int(math.ceil(math.log(modulus, 2) / base)) -def default_carry_chain(cc): - assert(cc == 'carry_chain1') - return 'Some (seq 0 (pred sz))' +def default_carry_chains(): + return ('seq 0 (pred sz)', '[0; 1]') def compute_s(modulus_str): base, exp, rest = re.match(r'\s*'.join(('^', '(2)', r'\^', '([0-9]+)', '([0-9^ +-]*)$')), modulus_str).groups() return '%s^%s' % (base, exp) @@ -132,7 +131,23 @@ def format_c_code(header, code, numargs, sz, indent=' ', closing_indent=' ret += '\n%s)' % closing_indent return ret +def nested_list_to_string(v): + if isinstance(v, str) or isinstance(v, int) or isinstance(v, unicode): + return str(v) + elif isinstance(v, list): + return '[%s]' % '; '.join(map(nested_list_to_string, v)) + else: + print('ERROR: Invalid type in nested_list_to_string: %s' % str(type(v))) + assert(False) + def make_curve_parameters(parameters): + def fix_option(term): + if not isinstance(term, str) and not isinstance(term, unicode): + return term + if term[:len('Some ')] != 'Some ' and term != 'None': + if ' ' in term: return 'Some (%s)' % term + return 'Some %s' % term + return term replacements = dict(parameters) assert(all(ch in '0123456789^+- ' for ch in parameters['modulus'])) modulus = eval(parameters['modulus'].replace('^', '**')) @@ -141,17 +156,16 @@ def make_curve_parameters(parameters): bitwidth = int(replacements['bitwidth']) replacements['sz'] = parameters.get('sz', str(compute_sz(modulus, base))) sz = int(replacements['sz']) - for cc in ('carry_chain1', 'carry_chain2'): - if cc in replacements.keys() and isinstance(replacements[cc], list): - replacements[cc] = 'Some [%s]%%nat' % '; '.join(map(str, replacements[cc])) - elif replacements[cc] == 'default': - replacements[cc] = default_carry_chain(cc) - elif isinstance(replacements[cc], str): - if replacements[cc][:len('Some ')] != 'Some ' and replacements[cc][:len('None')] != 'None': - if ' ' in replacements[cc]: replacements[cc] = '(%s)' % replacements[cc] - replacements[cc] = 'Some %s' % replacements[cc] - elif cc not in replacements.keys(): - replacements[cc] = 'None' + replacements['a24'] = fix_option(parameters.get('a24', 'None')) + replacements['carry_chains'] = fix_option(parameters.get('carry_chains', 'None')) + if isinstance(replacements['carry_chains'], list): + defaults = default_carry_chains() + replacements['carry_chains'] \ + = ('Some %s%%nat' + % nested_list_to_string([(v if v != 'default' else defaults[i]) + for i, v in enumerate(replacements['carry_chains'])])) + elif replacements['carry_chains'] == 'default': + replacements['carry_chains'] = 'Some %s%%nat' % nested_list_to_string(default_carry_chains()) replacements['s'] = parameters.get('s', compute_s(parameters['modulus'])) replacements['c'] = parameters.get('c', compute_c(parameters['modulus'])) if isinstance(replacements['c'], list): @@ -164,6 +178,9 @@ def make_curve_parameters(parameters): for k in ('upper_bound_of_exponent', 'allowable_bit_widths', 'freeze_extra_allowable_bit_widths'): if k not in replacements.keys(): replacements[k] = 'None' + for k in ('goldilocks', ): + if k not in replacements.keys(): + replacements[k] = 'false' for k in ('extra_prove_mul_eq', 'extra_prove_square_eq'): if k not in replacements.keys(): replacements[k] = 'idtac' @@ -180,12 +197,13 @@ Module Curve <: CurveParameters. Definition bitwidth : Z := %(bitwidth)s. Definition s : Z := %(s)s. Definition c : list limb := %(c)s. - Definition carry_chain1 : option (list nat) := Eval vm_compute in %(carry_chain1)s. - Definition carry_chain2 : option (list nat) := Eval vm_compute in %(carry_chain2)s. + Definition carry_chains : option (list (list nat)) := Eval vm_compute in %(carry_chains)s. - Definition a24 : Z := %(a24)s. + Definition a24 : option Z := %(a24)s. Definition coef_div_modulus : nat := %(coef_div_modulus)s%%nat. (* add %(coef_div_modulus)s*modulus before subtracting *) + Definition goldilocks : bool := %(goldilocks)s. + Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) := %(mul)s. diff --git a/src/Specific/IntegrationTestKaratsubaMul.v b/src/Specific/IntegrationTestKaratsubaMul.v deleted file mode 100644 index 8474a05c9..000000000 --- a/src/Specific/IntegrationTestKaratsubaMul.v +++ /dev/null @@ -1,58 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Local Open Scope Z_scope. - -Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Util.FixedWordSizes. -Require Import Crypto.Specific.Karatsuba. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Tactics.MoveLetIn. -Import ListNotations. - -Require Import Crypto.Specific.Framework.IntegrationTestTemporaryMiscCommon. - -Require Import Crypto.Compilers.Z.Bounds.Pipeline. - -Section BoundedField25p5. - Local Coercion Z.of_nat : nat >-> Z. - - Let limb_widths := Eval vm_compute in (List.map (fun i => Z.log2 (wt (S i) / wt i)) (seq 0 sz)). - Let length_lw := Eval compute in List.length limb_widths. - - Local Notation b_of exp := {| lower := 0 ; upper := 2^exp + 2^(exp-3) |}%Z (only parsing). (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *) - (* The definition [bounds_exp] is a tuple-version of the - limb-widths, which are the [exp] argument in [b_of] above, i.e., - the approximate base-2 exponent of the bounds on the limb in that - position. *) - Let bounds_exp : Tuple.tuple Z length_lw - := Eval compute in - Tuple.from_list length_lw limb_widths eq_refl. - Let bounds : Tuple.tuple zrange length_lw - := Eval compute in - Tuple.map (fun e => b_of e) bounds_exp. - - Let lgbitwidth := Eval compute in (Z.to_nat (Z.log2_up (List.fold_right Z.max 0 limb_widths))). - Let bitwidth := Eval compute in (2^lgbitwidth)%nat. - Let feZ : Type := tuple Z sz. - Let feW : Type := tuple (wordT lgbitwidth) sz. - Let feBW : Type := BoundedWord sz bitwidth bounds. - Let phi : feBW -> F m := - fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x). - - (* TODO : change this to field once field isomorphism happens *) - Definition mul : - { mul : feBW -> feBW -> feBW - | forall a b, phi (mul a b) = F.mul (phi a) (phi 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. - (*Show Ltac Profile.*) - Time Defined. - -End BoundedField25p5. diff --git a/src/Specific/Karatsuba.v b/src/Specific/Karatsuba.v deleted file mode 100644 index eaefd0493..000000000 --- a/src/Specific/Karatsuba.v +++ /dev/null @@ -1,327 +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.Saturated.Core. -Require Import Crypto.Arithmetic.Saturated.Freeze. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.LetIn Crypto.Util.ZUtil. -Require Import Crypto.Arithmetic.Karatsuba. -Require Crypto.Util.Tuple. -Require Import Crypto.Util.IdfunWithAlt. -Require Import Crypto.Util.QUtil. -Require Import Crypto.Util.Tactics.VM. -Local Notation tuple := Tuple.tuple. -Local Open Scope list_scope. -Local Open Scope Z_scope. -Local Coercion Z.of_nat : nat >-> Z. - -(*** -Modulus : 2^448-2^224-1 -Base: 56 -***) -Section Ops51. - 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 := 8%nat. - Definition bitwidth := 64. - Definition s : Z := 2^448. - Definition c : list B.limb := [(1, 1); (2^224, 1)]. - Definition carry_chain1 := [3;7]%nat. - Definition carry_chain2 := [0;4;1;5;2;6;3;7]%nat. - Definition carry_chain3 := [4;0]%nat. - - Definition coef_div_modulus : nat := 2. (* add 2*modulus before subtracting *) - (* 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_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. - Definition wt_divides_chain3 i (H:In i carry_chain3) : 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 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. - 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. - 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. - 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 half_sz : nat := Eval compute in (sz / 2). - Lemma half_sz_nonzero : half_sz <> 0%nat. Proof. cbv; congruence. Qed. - -Ltac basesystem_partial_evaluation_RHS := - let t0 := (match goal with - | |- _ _ ?t => t - end) in - let t := - eval - cbv - delta [Positional.to_associational_cps Positional.to_associational - Positional.eval Positional.zeros Positional.add_to_nth_cps - Positional.add_to_nth Positional.place_cps Positional.place - Positional.from_associational_cps Positional.from_associational - Positional.carry_cps Positional.carry - Positional.chained_carries_cps Positional.chained_carries - Positional.sub_cps Positional.sub Positional.split_cps - Positional.scmul_cps Positional.unbalanced_sub_cps - Positional.negate_snd_cps Positional.add_cps Positional.opp_cps - Associational.eval Associational.multerm Associational.mul_cps - Associational.mul Associational.split_cps Associational.split - Associational.reduce_cps Associational.reduce - Associational.carryterm_cps Associational.carryterm - Associational.carry_cps Associational.carry - Associational.negate_snd_cps Associational.negate_snd div modulo - id_tuple_with_alt id_tuple'_with_alt - ] - in t0 - in - let t := eval pattern @runtime_mul in t in - let t := (match t with - | ?t _ => t - end) in - let t := eval pattern @runtime_add in t in - let t := (match t with - | ?t _ => t - end) in - let t := eval pattern @runtime_opp in t in - let t := (match t with - | ?t _ => t - end) in - let t := eval pattern @runtime_shr in t in - let t := (match t with - | ?t _ => t - end) in - let t := eval pattern @runtime_and in t in - let t := (match t with - | ?t _ => t - end) in - let t := eval pattern @Let_In in t in - let t := (match t with - | ?t _ => t - end) in - let t := eval pattern @id_with_alt in t in - let t := (match t with - | ?t _ => t - end) in - let t1 := fresh "t1" in - pose (t1 := t); - transitivity - (t1 (@id_with_alt) (@Let_In) (@runtime_and) (@runtime_shr) (@runtime_opp) (@runtime_add) - (@runtime_mul)); - [ replace_with_vm_compute t1; clear t1 | reflexivity ]. - - Definition goldilocks_mul_sig : - {mul : (Z^sz -> Z^sz -> Z^sz)%type | - forall a b : Z^sz, - mul a b = goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt (2 ^ 224) a b (fun ab => Positional.reduce_cps (n:=sz) wt s c ab id)}. - Proof. - eexists; cbv beta zeta; intros. - cbv [goldilocks_mul_cps]. - repeat autounfold. - basesystem_partial_evaluation_RHS. - do_replace_match_with_destructuring_match_in_goal. - 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 - Positional.Fdecode (m := m) wt (mul a b) = (eval a * eval b)%F}. - Proof. - eexists; cbv beta zeta; intros. - pose proof wt_nonzero. - let x := constr:( - goldilocks_mul_cps (n:=half_sz) (n2:=sz) wt (2^224) a b (fun ab => Positional.reduce_cps (n:=sz) wt s c ab id)) in - F_mod_eq; - transitivity (Positional.eval wt x); repeat autounfold; - - [ - | autorewrite with uncps push_id push_basesystem_eval; - apply goldilocks_mul_correct; try assumption; cbv; congruence ]. - cbv [mod_eq]; apply f_equal2; - [ | reflexivity ]. apply f_equal. - etransitivity; [|apply (proj2_sig (goldilocks_mul_sig))]. - cbv [proj1_sig goldilocks_mul_sig]. - reflexivity. - Defined. - - Definition square_sig : - {square : (Z^sz -> Z^sz)%type | - forall a : Z^sz, - let eval := Positional.Fdecode (m := m) wt in - Positional.Fdecode (m := m) wt (square a) = (eval a * eval a)%F}. - Proof. - eexists; cbv beta zeta; intros. - rewrite <-(proj2_sig mul_sig). - apply f_equal. - cbv [proj1_sig mul_sig]. - reflexivity. - 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. - pose proof wt_nonzero. pose proof wt_divides_chain1. - pose proof div_mod. pose proof wt_divides_chain2. - pose proof wt_divides_chain3. - 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 r => Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt r carry_chain2 - (fun r => Positional.carry_reduce_cps (n:=sz) (div:=div) (modulo:=modulo) wt s c r - (fun r => Positional.chained_carries_cps (n:=sz) (div:=div) (modulo:=modulo) wt r carry_chain3 id - ))))) in - solve_op_F wt x. reflexivity. - Defined. - - (* [freeze] preconditions *) - 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. - 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. - 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_56 := - (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 Ops51. diff --git a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v new file mode 100644 index 000000000..aa8fd5614 --- /dev/null +++ b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v @@ -0,0 +1,32 @@ +Require Import Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Util.LetIn. + +(*** +Modulus : 2^448-2^224-1 +Base: 56 +***) + +Module Curve <: CurveParameters. + Definition sz : nat := 8%nat. + Definition bitwidth : Z := 64. + Definition s : Z := 2^448. + Definition c : list limb := [(1, 1); (2^224, 1)]. + Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [[3; 7]; [0; 4; 1; 5; 2; 6; 3; 7]; [4; 0]]%nat. + + Definition a24 : option Z := None. + Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *) + + Definition goldilocks : bool := true. + + Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) + := None. + + Definition square_code : option (Z^sz -> Z^sz) + := None. + + Definition upper_bound_of_exponent : option (Z -> Z) := None. + Definition allowable_bit_widths : option (list nat) := None. + Definition freeze_extra_allowable_bit_widths : option (list nat) := None. + Ltac extra_prove_mul_eq := idtac. + Ltac extra_prove_square_eq := idtac. +End Curve. diff --git a/src/Specific/X2448/Karatsuba/C64/Synthesis.v b/src/Specific/X2448/Karatsuba/C64/Synthesis.v new file mode 100644 index 000000000..8ea8aa5c9 --- /dev/null +++ b/src/Specific/X2448/Karatsuba/C64/Synthesis.v @@ -0,0 +1,14 @@ +Require Import Crypto.Specific.Framework.SynthesisFramework. +Require Import Crypto.Specific.X2448.Karatsuba.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/X2448/Karatsuba/C64/femul.v b/src/Specific/X2448/Karatsuba/C64/femul.v new file mode 100644 index 000000000..2f890a88f --- /dev/null +++ b/src/Specific/X2448/Karatsuba/C64/femul.v @@ -0,0 +1,12 @@ +Require Import Crypto.Arithmetic.PrimeFieldTheorems. +Require Import Crypto.Specific.X2448.Karatsuba.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. + Set Ltac Profiling. + Time synthesize_mul (). + Show Ltac Profile. +Time Defined. diff --git a/src/Specific/X2448/Karatsuba/C64/femulDisplay.log b/src/Specific/X2448/Karatsuba/C64/femulDisplay.log new file mode 100644 index 000000000..17db6102d --- /dev/null +++ b/src/Specific/X2448/Karatsuba/C64/femulDisplay.log @@ -0,0 +1,61 @@ +λ x x0 : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64, +Interp-η +(λ var : Syntax.base_type → Type, + λ '(x16, x17, x15, x13, x11, x9, x7, x5, (x30, x31, x29, x27, x25, x23, x21, x19))%core, + uint128_t x32 = (uint128_t) (x11 + x16) * (x25 + x30) - (uint128_t) x11 * x25; + uint128_t x33 = (uint128_t) (x9 + x17) * (x25 + x30) + (uint128_t) (x11 + x16) * (x23 + x31) - ((uint128_t) x9 * x25 + (uint128_t) x11 * x23); + uint128_t x34 = (uint128_t) (x7 + x15) * (x25 + x30) + ((uint128_t) (x9 + x17) * (x23 + x31) + (uint128_t) (x11 + x16) * (x21 + x29)) - ((uint128_t) x7 * x25 + ((uint128_t) x9 * x23 + (uint128_t) x11 * x21)); + uint128_t x35 = (uint128_t) (x5 + x13) * (x25 + x30) + ((uint128_t) (x7 + x15) * (x23 + x31) + ((uint128_t) (x9 + x17) * (x21 + x29) + (uint128_t) (x11 + x16) * (x19 + x27))) - ((uint128_t) x5 * x25 + ((uint128_t) x7 * x23 + ((uint128_t) x9 * x21 + (uint128_t) x11 * x19))); + uint128_t x36 = (uint128_t) (x5 + x13) * (x23 + x31) + ((uint128_t) (x7 + x15) * (x21 + x29) + (uint128_t) (x9 + x17) * (x19 + x27)) - ((uint128_t) x5 * x23 + ((uint128_t) x7 * x21 + (uint128_t) x9 * x19)); + uint128_t x37 = (uint128_t) (x5 + x13) * (x21 + x29) + (uint128_t) (x7 + x15) * (x19 + x27) - ((uint128_t) x5 * x21 + (uint128_t) x7 * x19); + uint128_t x38 = (uint128_t) (x5 + x13) * (x19 + x27) - (uint128_t) x5 * x19; + uint128_t x39 = (uint128_t) x11 * x25 + (uint128_t) x16 * x30 + x36 + x32; + uint128_t x40 = (uint128_t) x9 * x25 + (uint128_t) x11 * x23 + ((uint128_t) x17 * x30 + (uint128_t) x16 * x31) + x37 + x33; + uint128_t x41 = (uint128_t) x7 * x25 + ((uint128_t) x9 * x23 + (uint128_t) x11 * x21) + ((uint128_t) x15 * x30 + ((uint128_t) x17 * x31 + (uint128_t) x16 * x29)) + x38 + x34; + uint128_t x42 = (uint128_t) x5 * x25 + ((uint128_t) x7 * x23 + ((uint128_t) x9 * x21 + (uint128_t) x11 * x19)) + ((uint128_t) x13 * x30 + ((uint128_t) x15 * x31 + ((uint128_t) x17 * x29 + (uint128_t) x16 * x27))); + uint128_t x43 = (uint128_t) x5 * x23 + ((uint128_t) x7 * x21 + (uint128_t) x9 * x19) + ((uint128_t) x13 * x31 + ((uint128_t) x15 * x29 + (uint128_t) x17 * x27)) + x32; + uint128_t x44 = (uint128_t) x5 * x21 + (uint128_t) x7 * x19 + ((uint128_t) x13 * x29 + (uint128_t) x15 * x27) + x33; + uint128_t x45 = (uint128_t) x5 * x19 + (uint128_t) x13 * x27 + x34; + uint64_t x46 = (uint64_t) (x42 >> 0x38); + uint64_t x47 = (uint64_t) x42 & 0xffffffffffffff; + uint64_t x48 = (uint64_t) (x35 >> 0x38); + uint64_t x49 = (uint64_t) x35 & 0xffffffffffffff; + uint128_t x50 = (uint128_t) 0x100000000000000 * x48 + x49; + uint64_t x51 = (uint64_t) (x50 >> 0x38); + uint64_t x52 = (uint64_t) x50 & 0xffffffffffffff; + uint128_t x53 = x45 + x51; + uint64_t x54 = (uint64_t) (x53 >> 0x38); + uint64_t x55 = (uint64_t) x53 & 0xffffffffffffff; + uint128_t x56 = x46 + x41 + x51; + uint64_t x57 = (uint64_t) (x56 >> 0x38); + uint64_t x58 = (uint64_t) x56 & 0xffffffffffffff; + uint128_t x59 = x54 + x44; + uint64_t x60 = (uint64_t) (x59 >> 0x38); + uint64_t x61 = (uint64_t) x59 & 0xffffffffffffff; + uint128_t x62 = x57 + x40; + uint64_t x63 = (uint64_t) (x62 >> 0x38); + uint64_t x64 = (uint64_t) x62 & 0xffffffffffffff; + uint128_t x65 = x60 + x43; + uint64_t x66 = (uint64_t) (x65 >> 0x38); + uint64_t x67 = (uint64_t) x65 & 0xffffffffffffff; + uint128_t x68 = x63 + x39; + uint64_t x69 = (uint64_t) (x68 >> 0x38); + uint64_t x70 = (uint64_t) x68 & 0xffffffffffffff; + uint64_t x71 = x66 + x47; + uint64_t x72 = x71 >> 0x38; + uint64_t x73 = x71 & 0xffffffffffffff; + uint64_t x74 = x69 + x52; + uint64_t x75 = x74 >> 0x38; + uint64_t x76 = x74 & 0xffffffffffffff; + uint64_t x77 = 0x100000000000000 * x75 + x76; + uint64_t x78 = x77 >> 0x38; + uint64_t x79 = x77 & 0xffffffffffffff; + uint64_t x80 = x72 + x58 + x78; + uint64_t x81 = x80 >> 0x38; + uint64_t x82 = x80 & 0xffffffffffffff; + uint64_t x83 = x55 + x78; + uint64_t x84 = x83 >> 0x38; + uint64_t x85 = x83 & 0xffffffffffffff; + return (Return x79, Return x70, x81 + x64, Return x82, Return x73, Return x67, x84 + x61, Return x85)) +(x, x0)%core + : word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → word64 * word64 * word64 * word64 * word64 * word64 * word64 * word64 → ReturnType (uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t * uint64_t) diff --git a/src/Specific/IntegrationTestKaratsubaMulDisplay.v b/src/Specific/X2448/Karatsuba/C64/femulDisplay.v index 7649ca88b..15877076f 100644 --- a/src/Specific/IntegrationTestKaratsubaMulDisplay.v +++ b/src/Specific/X2448/Karatsuba/C64/femulDisplay.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.IntegrationTestKaratsubaMul. +Require Import Crypto.Specific.X2448.Karatsuba.C64.femul. Require Import Crypto.Specific.Framework.IntegrationTestDisplayCommon. Check display mul. diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v index c8c7cb04f..e8a46ea9e 100644 --- a/src/Specific/X25519/C32/CurveParameters.v +++ b/src/Specific/X25519/C32/CurveParameters.v @@ -11,12 +11,13 @@ Module Curve <: CurveParameters. Definition bitwidth : Z := 32. Definition s : Z := 2^255. Definition c : list limb := [(1, 19)]. - Definition carry_chain1 : option (list nat) := Eval vm_compute in Some (seq 0 (pred sz)). - Definition carry_chain2 : option (list nat) := Eval vm_compute in Some [0; 1]%nat. + Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat. - Definition a24 : Z := 121665. + Definition a24 : option Z := Some 121665. Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *) + Definition goldilocks : bool := false. + Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) := Some (fun a b => (* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *) diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v index 9a543b569..54c578a08 100644 --- a/src/Specific/X25519/C64/CurveParameters.v +++ b/src/Specific/X25519/C64/CurveParameters.v @@ -11,12 +11,13 @@ Module Curve <: CurveParameters. Definition bitwidth : Z := 64. Definition s : Z := 2^255. Definition c : list limb := [(1, 19)]. - Definition carry_chain1 : option (list nat) := Eval vm_compute in Some (seq 0 (pred sz)). - Definition carry_chain2 : option (list nat) := Eval vm_compute in Some [0; 1]%nat. + Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat. - Definition a24 : Z := 121665. + Definition a24 : option Z := Some 121665. Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *) + Definition goldilocks : bool := false. + Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) := Some (fun a b => (* Micro-optimized form from curve25519-donna-c64 by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *) diff --git a/src/Specific/X2555/C128/CurveParameters.v b/src/Specific/X2555/C128/CurveParameters.v index a0a0dc027..40c57e8e0 100644 --- a/src/Specific/X2555/C128/CurveParameters.v +++ b/src/Specific/X2555/C128/CurveParameters.v @@ -11,12 +11,13 @@ Module Curve <: CurveParameters. Definition bitwidth : Z := 128. Definition s : Z := 2^255. Definition c : list limb := [(1, 5)]. - Definition carry_chain1 : option (list nat) := Eval vm_compute in Some (seq 0 (pred sz)). - Definition carry_chain2 : option (list nat) := Eval vm_compute in Some [0; 1]%nat. + Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat. - Definition a24 : Z := 121665 (* XXX TODO(andreser) FIXME? Is this right for this curve? *). + Definition a24 : option Z := Some (121665 (* XXX TODO(andreser) FIXME? Is this right for this curve? *)). Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *) + Definition goldilocks : bool := false. + Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) := None. diff --git a/src/Specific/X2555/C128/ladderstepDisplay.log b/src/Specific/X2555/C128/ladderstepDisplay.log new file mode 100644 index 000000000..d6c2ec14d --- /dev/null +++ b/src/Specific/X2555/C128/ladderstepDisplay.log @@ -0,0 +1,214 @@ +λ x x0 x1 x2 x3 : Synthesis.P.feW, +let (a, b) := Interp-η +(λ var : Syntax.base_type → Type, + λ '(x11, x12, x10, (x17, x18, x16, (x21, x22, x20)), (x27, x28, x26, (x31, x32, x30)))%core, + uint128_t x33 = x17 + x21; + uint128_t x34 = x18 + x22; + uint128_t x35 = x16 + x20; + uint128_t x36 = 0x3ffffffffffffffffffffeL + x17 - x21; + uint128_t x37 = 0x3ffffffffffffffffffffeL + x18 - x22; + uint128_t x38 = 0x3ffffffffffffffffffff6L + x16 - x20; + uint128_t x39 = x27 + x31; + uint128_t x40 = x28 + x32; + uint128_t x41 = x26 + x30; + uint128_t x42 = 0x3ffffffffffffffffffffeL + x27 - x31; + uint128_t x43 = 0x3ffffffffffffffffffffeL + x28 - x32; + uint128_t x44 = 0x3ffffffffffffffffffff6L + x26 - x30; + uint256_t x45 = (uint256_t) x41 * x36 + ((uint256_t) x40 * x37 + (uint256_t) x39 * x38); + uint256_t x46 = (uint256_t) x41 * x37 + (uint256_t) x40 * x38 + 0x5 * ((uint256_t) x39 * x36); + uint256_t x47 = (uint256_t) x41 * x38 + 0x5 * ((uint256_t) x40 * x36 + (uint256_t) x39 * x37); + uint128_t x48 = (uint128_t) (x47 >> 0x55); + uint128_t x49 = (uint128_t) x47 & 0x1fffffffffffffffffffffL; + uint256_t x50 = x48 + x46; + uint128_t x51 = (uint128_t) (x50 >> 0x55); + uint128_t x52 = (uint128_t) x50 & 0x1fffffffffffffffffffffL; + uint256_t x53 = x51 + x45; + uint128_t x54 = (uint128_t) (x53 >> 0x55); + uint128_t x55 = (uint128_t) x53 & 0x1fffffffffffffffffffffL; + uint128_t x56 = x49 + 0x5 * x54; + uint128_t x57 = x56 >> 0x55; + uint128_t x58 = x56 & 0x1fffffffffffffffffffffL; + uint128_t x59 = x57 + x52; + uint128_t x60 = x59 >> 0x55; + uint128_t x61 = x59 & 0x1fffffffffffffffffffffL; + uint128_t x62 = x60 + x55; + uint256_t x63 = (uint256_t) x35 * x42 + ((uint256_t) x34 * x43 + (uint256_t) x33 * x44); + uint256_t x64 = (uint256_t) x35 * x43 + (uint256_t) x34 * x44 + 0x5 * ((uint256_t) x33 * x42); + uint256_t x65 = (uint256_t) x35 * x44 + 0x5 * ((uint256_t) x34 * x42 + (uint256_t) x33 * x43); + uint128_t x66 = (uint128_t) (x65 >> 0x55); + uint128_t x67 = (uint128_t) x65 & 0x1fffffffffffffffffffffL; + uint256_t x68 = x66 + x64; + uint128_t x69 = (uint128_t) (x68 >> 0x55); + uint128_t x70 = (uint128_t) x68 & 0x1fffffffffffffffffffffL; + uint256_t x71 = x69 + x63; + uint128_t x72 = (uint128_t) (x71 >> 0x55); + uint128_t x73 = (uint128_t) x71 & 0x1fffffffffffffffffffffL; + uint128_t x74 = x67 + 0x5 * x72; + uint128_t x75 = x74 >> 0x55; + uint128_t x76 = x74 & 0x1fffffffffffffffffffffL; + uint128_t x77 = x75 + x70; + uint128_t x78 = x77 >> 0x55; + uint128_t x79 = x77 & 0x1fffffffffffffffffffffL; + uint128_t x80 = x78 + x73; + uint128_t x81 = x62 + x80; + uint128_t x82 = x61 + x79; + uint128_t x83 = x58 + x76; + uint128_t x84 = 0x3ffffffffffffffffffffeL + x62 - x80; + uint128_t x85 = 0x3ffffffffffffffffffffeL + x61 - x79; + uint128_t x86 = 0x3ffffffffffffffffffff6L + x58 - x76; + uint256_t x87 = (uint256_t) x83 * x81 + ((uint256_t) x82 * x82 + (uint256_t) x81 * x83); + uint256_t x88 = (uint256_t) x83 * x82 + (uint256_t) x82 * x83 + 0x5 * ((uint256_t) x81 * x81); + uint256_t x89 = (uint256_t) x83 * x83 + 0x5 * ((uint256_t) x82 * x81 + (uint256_t) x81 * x82); + uint128_t x90 = (uint128_t) (x89 >> 0x55); + uint128_t x91 = (uint128_t) x89 & 0x1fffffffffffffffffffffL; + uint256_t x92 = x90 + x88; + uint128_t x93 = (uint128_t) (x92 >> 0x55); + uint128_t x94 = (uint128_t) x92 & 0x1fffffffffffffffffffffL; + uint256_t x95 = x93 + x87; + uint128_t x96 = (uint128_t) (x95 >> 0x55); + uint128_t x97 = (uint128_t) x95 & 0x1fffffffffffffffffffffL; + uint128_t x98 = x91 + 0x5 * x96; + uint128_t x99 = x98 >> 0x55; + uint128_t x100 = x98 & 0x1fffffffffffffffffffffL; + uint128_t x101 = x99 + x94; + uint128_t x102 = x101 >> 0x55; + uint128_t x103 = x101 & 0x1fffffffffffffffffffffL; + uint128_t x104 = x102 + x97; + uint256_t x105 = (uint256_t) x86 * x84 + ((uint256_t) x85 * x85 + (uint256_t) x84 * x86); + uint256_t x106 = (uint256_t) x86 * x85 + (uint256_t) x85 * x86 + 0x5 * ((uint256_t) x84 * x84); + uint256_t x107 = (uint256_t) x86 * x86 + 0x5 * ((uint256_t) x85 * x84 + (uint256_t) x84 * x85); + uint128_t x108 = (uint128_t) (x107 >> 0x55); + uint128_t x109 = (uint128_t) x107 & 0x1fffffffffffffffffffffL; + uint256_t x110 = x108 + x106; + uint128_t x111 = (uint128_t) (x110 >> 0x55); + uint128_t x112 = (uint128_t) x110 & 0x1fffffffffffffffffffffL; + uint256_t x113 = x111 + x105; + uint128_t x114 = (uint128_t) (x113 >> 0x55); + uint128_t x115 = (uint128_t) x113 & 0x1fffffffffffffffffffffL; + uint128_t x116 = x109 + 0x5 * x114; + uint128_t x117 = x116 >> 0x55; + uint128_t x118 = x116 & 0x1fffffffffffffffffffffL; + uint128_t x119 = x117 + x112; + uint128_t x120 = x119 >> 0x55; + uint128_t x121 = x119 & 0x1fffffffffffffffffffffL; + uint128_t x122 = x120 + x115; + uint256_t x123 = (uint256_t) x118 * x11 + ((uint256_t) x121 * x12 + (uint256_t) x122 * x10); + uint256_t x124 = (uint256_t) x118 * x12 + (uint256_t) x121 * x10 + 0x5 * ((uint256_t) x122 * x11); + uint256_t x125 = (uint256_t) x118 * x10 + 0x5 * ((uint256_t) x121 * x11 + (uint256_t) x122 * x12); + uint128_t x126 = (uint128_t) (x125 >> 0x55); + uint128_t x127 = (uint128_t) x125 & 0x1fffffffffffffffffffffL; + uint256_t x128 = x126 + x124; + uint128_t x129 = (uint128_t) (x128 >> 0x55); + uint128_t x130 = (uint128_t) x128 & 0x1fffffffffffffffffffffL; + uint256_t x131 = x129 + x123; + uint128_t x132 = (uint128_t) (x131 >> 0x55); + uint128_t x133 = (uint128_t) x131 & 0x1fffffffffffffffffffffL; + uint128_t x134 = x127 + 0x5 * x132; + uint128_t x135 = x134 >> 0x55; + uint128_t x136 = x134 & 0x1fffffffffffffffffffffL; + uint128_t x137 = x135 + x130; + uint128_t x138 = x137 >> 0x55; + uint128_t x139 = x137 & 0x1fffffffffffffffffffffL; + uint128_t x140 = x138 + x133; + uint256_t x141 = (uint256_t) x35 * x33 + ((uint256_t) x34 * x34 + (uint256_t) x33 * x35); + uint256_t x142 = (uint256_t) x35 * x34 + (uint256_t) x34 * x35 + 0x5 * ((uint256_t) x33 * x33); + uint256_t x143 = (uint256_t) x35 * x35 + 0x5 * ((uint256_t) x34 * x33 + (uint256_t) x33 * x34); + uint128_t x144 = (uint128_t) (x143 >> 0x55); + uint128_t x145 = (uint128_t) x143 & 0x1fffffffffffffffffffffL; + uint256_t x146 = x144 + x142; + uint128_t x147 = (uint128_t) (x146 >> 0x55); + uint128_t x148 = (uint128_t) x146 & 0x1fffffffffffffffffffffL; + uint256_t x149 = x147 + x141; + uint128_t x150 = (uint128_t) (x149 >> 0x55); + uint128_t x151 = (uint128_t) x149 & 0x1fffffffffffffffffffffL; + uint128_t x152 = x145 + 0x5 * x150; + uint128_t x153 = x152 >> 0x55; + uint128_t x154 = x152 & 0x1fffffffffffffffffffffL; + uint128_t x155 = x153 + x148; + uint128_t x156 = x155 >> 0x55; + uint128_t x157 = x155 & 0x1fffffffffffffffffffffL; + uint128_t x158 = x156 + x151; + uint256_t x159 = (uint256_t) x38 * x36 + ((uint256_t) x37 * x37 + (uint256_t) x36 * x38); + uint256_t x160 = (uint256_t) x38 * x37 + (uint256_t) x37 * x38 + 0x5 * ((uint256_t) x36 * x36); + uint256_t x161 = (uint256_t) x38 * x38 + 0x5 * ((uint256_t) x37 * x36 + (uint256_t) x36 * x37); + uint128_t x162 = (uint128_t) (x161 >> 0x55); + uint128_t x163 = (uint128_t) x161 & 0x1fffffffffffffffffffffL; + uint256_t x164 = x162 + x160; + uint128_t x165 = (uint128_t) (x164 >> 0x55); + uint128_t x166 = (uint128_t) x164 & 0x1fffffffffffffffffffffL; + uint256_t x167 = x165 + x159; + uint128_t x168 = (uint128_t) (x167 >> 0x55); + uint128_t x169 = (uint128_t) x167 & 0x1fffffffffffffffffffffL; + uint128_t x170 = x163 + 0x5 * x168; + uint128_t x171 = x170 >> 0x55; + uint128_t x172 = x170 & 0x1fffffffffffffffffffffL; + uint128_t x173 = x171 + x166; + uint128_t x174 = x173 >> 0x55; + uint128_t x175 = x173 & 0x1fffffffffffffffffffffL; + uint128_t x176 = x174 + x169; + uint256_t x177 = (uint256_t) x154 * x176 + ((uint256_t) x157 * x175 + (uint256_t) x158 * x172); + uint256_t x178 = (uint256_t) x154 * x175 + (uint256_t) x157 * x172 + 0x5 * ((uint256_t) x158 * x176); + uint256_t x179 = (uint256_t) x154 * x172 + 0x5 * ((uint256_t) x157 * x176 + (uint256_t) x158 * x175); + uint128_t x180 = (uint128_t) (x179 >> 0x55); + uint128_t x181 = (uint128_t) x179 & 0x1fffffffffffffffffffffL; + uint256_t x182 = x180 + x178; + uint128_t x183 = (uint128_t) (x182 >> 0x55); + uint128_t x184 = (uint128_t) x182 & 0x1fffffffffffffffffffffL; + uint256_t x185 = x183 + x177; + uint128_t x186 = (uint128_t) (x185 >> 0x55); + uint128_t x187 = (uint128_t) x185 & 0x1fffffffffffffffffffffL; + uint128_t x188 = x181 + 0x5 * x186; + uint128_t x189 = x188 >> 0x55; + uint128_t x190 = x188 & 0x1fffffffffffffffffffffL; + uint128_t x191 = x189 + x184; + uint128_t x192 = x191 >> 0x55; + uint128_t x193 = x191 & 0x1fffffffffffffffffffffL; + uint128_t x194 = x192 + x187; + uint128_t x195 = 0x3ffffffffffffffffffffeL + x158 - x176; + uint128_t x196 = 0x3ffffffffffffffffffffeL + x157 - x175; + uint128_t x197 = 0x3ffffffffffffffffffff6L + x154 - x172; + uint128_t x198 = x195 * 0x1db41; + uint128_t x199 = x196 * 0x1db41; + uint128_t x200 = x197 * 0x1db41; + uint128_t x201 = x200 >> 0x55; + uint128_t x202 = x200 & 0x1fffffffffffffffffffffL; + uint128_t x203 = x201 + x199; + uint128_t x204 = x203 >> 0x55; + uint128_t x205 = x203 & 0x1fffffffffffffffffffffL; + uint128_t x206 = x204 + x198; + uint128_t x207 = x206 >> 0x55; + uint128_t x208 = x206 & 0x1fffffffffffffffffffffL; + uint128_t x209 = x202 + 0x5 * x207; + uint128_t x210 = x209 >> 0x55; + uint128_t x211 = x209 & 0x1fffffffffffffffffffffL; + uint128_t x212 = x210 + x205; + uint128_t x213 = x212 >> 0x55; + uint128_t x214 = x212 & 0x1fffffffffffffffffffffL; + uint128_t x215 = x213 + x208; + uint128_t x216 = x215 + x158; + uint128_t x217 = x214 + x157; + uint128_t x218 = x211 + x154; + uint256_t x219 = (uint256_t) x197 * x216 + ((uint256_t) x196 * x217 + (uint256_t) x195 * x218); + uint256_t x220 = (uint256_t) x197 * x217 + (uint256_t) x196 * x218 + 0x5 * ((uint256_t) x195 * x216); + uint256_t x221 = (uint256_t) x197 * x218 + 0x5 * ((uint256_t) x196 * x216 + (uint256_t) x195 * x217); + uint128_t x222 = (uint128_t) (x221 >> 0x55); + uint128_t x223 = (uint128_t) x221 & 0x1fffffffffffffffffffffL; + uint256_t x224 = x222 + x220; + uint128_t x225 = (uint128_t) (x224 >> 0x55); + uint128_t x226 = (uint128_t) x224 & 0x1fffffffffffffffffffffL; + uint256_t x227 = x225 + x219; + uint128_t x228 = (uint128_t) (x227 >> 0x55); + uint128_t x229 = (uint128_t) x227 & 0x1fffffffffffffffffffffL; + uint128_t x230 = x223 + 0x5 * x228; + uint128_t x231 = x230 >> 0x55; + uint128_t x232 = x230 & 0x1fffffffffffffffffffffL; + uint128_t x233 = x231 + x226; + uint128_t x234 = x233 >> 0x55; + uint128_t x235 = x233 & 0x1fffffffffffffffffffffL; + uint128_t x236 = x234 + x229; + return (Return x194, Return x193, Return x190, (Return x236, Return x235, Return x232), (Return x104, Return x103, Return x100, (Return x140, Return x139, Return x136)))) +(x, (x0, x1), (x2, x3))%core in +(let (a0, b0) := a in +(a0, b0), let (a0, b0) := b in +(a0, b0))%core + : 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) |