diff options
Diffstat (limited to 'src/Specific')
-rw-r--r-- | src/Specific/Framework/CurveParameters.v | 412 | ||||
-rw-r--r-- | src/Specific/Framework/CurveParametersPackage.v | 8 | ||||
-rw-r--r-- | src/Specific/Framework/RawCurveParameters.v | 63 | ||||
-rw-r--r-- | src/Specific/Framework/SynthesisFramework.v | 53 | ||||
-rwxr-xr-x | src/Specific/Framework/make_curve.py | 62 | ||||
-rw-r--r-- | src/Specific/NISTP256/AMD128/CurveParameters.v | 44 | ||||
-rw-r--r-- | src/Specific/NISTP256/AMD128/Synthesis.v | 6 | ||||
-rw-r--r-- | src/Specific/NISTP256/AMD64/CurveParameters.v | 44 | ||||
-rw-r--r-- | src/Specific/NISTP256/AMD64/Synthesis.v | 6 | ||||
-rw-r--r-- | src/Specific/X2448/Karatsuba/C64/CurveParameters.v | 44 | ||||
-rw-r--r-- | src/Specific/X2448/Karatsuba/C64/Synthesis.v | 6 | ||||
-rw-r--r-- | src/Specific/X25519/C32/CurveParameters.v | 48 | ||||
-rw-r--r-- | src/Specific/X25519/C32/Synthesis.v | 6 | ||||
-rw-r--r-- | src/Specific/X25519/C64/CurveParameters.v | 48 | ||||
-rw-r--r-- | src/Specific/X25519/C64/Synthesis.v | 6 | ||||
-rw-r--r-- | src/Specific/X2555/C128/CurveParameters.v | 44 | ||||
-rw-r--r-- | src/Specific/X2555/C128/Synthesis.v | 6 |
17 files changed, 500 insertions, 406 deletions
diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v index 4aa255d11..ceac0fbcc 100644 --- a/src/Specific/Framework/CurveParameters.v +++ b/src/Specific/Framework/CurveParameters.v @@ -2,270 +2,302 @@ Require Export Coq.ZArith.BinInt. Require Export Coq.Lists.List. Require Export Crypto.Util.ZUtil.Notations. Require Import Crypto.Util.Tactics.CacheTerm. +Require Import Crypto.Specific.Framework.RawCurveParameters. Require Import Crypto.Util.TagList. Require Crypto.Util.Tuple. -Module Export Notations. - Export ListNotations. +Local Set Primitive Projections. - Open Scope list_scope. - Open Scope Z_scope. +Module Export Notations := RawCurveParameters.Notations. - Notation limb := (Z * Z)%type. - Infix "^" := Tuple.tuple : type_scope. -End Notations. - -(* These definitions will need to be passed as Ltac arguments (or - cleverly inferred) when things are eventually automated *) -Module Type CurveParameters. - Parameter sz : nat. - Parameter bitwidth : Z. - Parameter s : Z. - Parameter c : list limb. - Parameter carry_chains - : option (list (list nat)). (* defaults to [seq 0 (pred sz) :: (0 :: 1 :: nil) :: nil] *) - Parameter a24 : option Z. - Parameter coef_div_modulus : option nat. - - Parameter goldilocks : bool. - Parameter montgomery : bool. - - Parameter mul_code : option (Z^sz -> Z^sz -> Z^sz). - Parameter square_code : option (Z^sz -> Z^sz). - Parameter upper_bound_of_exponent - : option (Z -> Z). (* defaults to [fun exp => 2^exp + 2^(exp-3)] *) - Parameter allowable_bit_widths - : option (list nat). (* defaults to [bitwidth :: 2*bitwidth :: nil] *) - Parameter freeze_extra_allowable_bit_widths - : option (list nat). (* defaults to [8 :: nil] *) - Parameter modinv_fuel : option nat. - Ltac extra_prove_mul_eq := idtac. - Ltac extra_prove_square_eq := idtac. -End CurveParameters. - -Module TAG. - Inductive tags := sz | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | montgomery | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel. +Module TAG. (* namespacing *) + Inductive tags := CP | sz | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | montgomery | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel. End TAG. -Module FillCurveParameters (P : CurveParameters). - Local Notation defaulted opt_v default - := (match opt_v with - | Some v => v - | None => default - end). +Module Export CurveParameters. + Local Notation eval p := + (List.fold_right Z.add 0%Z (List.map (fun t => fst t * snd t) p)). + Ltac do_compute v := let v' := (eval vm_compute in v) in v'. Notation compute v := (ltac:(let v' := do_compute v in exact v')) (only parsing). - Definition sz := P.sz. - Definition bitwidth := P.bitwidth. - Definition s := P.s. - Definition c := P.c. - Definition carry_chains := defaulted P.carry_chains [seq 0 (pred sz); [0; 1]]%nat. - Definition a24 := defaulted P.a24 0. - Definition coef_div_modulus := defaulted P.coef_div_modulus 0%nat. + Local Notation defaulted opt_v default + := (match opt_v with + | Some v => v + | None => default + end) + (only parsing). + Record CurveParameters := + { + sz : nat; + bitwidth : Z; + s : Z; + c : list limb; + carry_chains : list (list nat); + a24 : Z; + coef_div_modulus : nat; - Definition goldilocks := P.goldilocks. - Definition montgomery := P.montgomery. + goldilocks : bool; + montgomery : bool; - Ltac default_mul := - lazymatch (eval hnf in P.mul_code) with + mul_code : option (Z^sz -> Z^sz -> Z^sz); + square_code : option (Z^sz -> Z^sz); + upper_bound_of_exponent : Z -> Z; + allowable_bit_widths : list nat; + freeze_allowable_bit_widths : list nat; + modinv_fuel : nat + }. + + Declare Reduction cbv_CurveParameters + := cbv [sz + bitwidth + s + c + carry_chains + a24 + coef_div_modulus + goldilocks + montgomery + mul_code + square_code + upper_bound_of_exponent + allowable_bit_widths + freeze_allowable_bit_widths + modinv_fuel]. + + Ltac default_mul CP := + lazymatch (eval hnf in (mul_code CP)) with | None => reflexivity | Some ?mul_code => instantiate (1:=mul_code) end. - Ltac default_square := - lazymatch (eval hnf in P.square_code) with + Ltac default_square CP := + lazymatch (eval hnf in (square_code CP)) with | None => reflexivity | Some ?square_code => instantiate (1:=square_code) end. - Definition upper_bound_of_exponent - := defaulted P.upper_bound_of_exponent - (if P.montgomery - then (fun exp => (2^exp - 1)%Z) - else (fun exp => (2^exp + 2^(exp-3))%Z)). Local Notation list_8_if_not_exists ls := (if existsb (Nat.eqb 8) ls then nil else [8]%nat) (only parsing). - Definition allowable_bit_widths - := defaulted - P.allowable_bit_widths - ((if P.montgomery - then [8] - else nil) - ++ (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil))%nat. - Definition freeze_allowable_bit_widths - := defaulted - P.freeze_extra_allowable_bit_widths - (list_8_if_not_exists allowable_bit_widths) - ++ allowable_bit_widths. - Definition modinv_fuel := defaulted P.modinv_fuel 10%nat. - (* hack around https://coq.inria.fr/bugs/show_bug.cgi?id=5764 *) - Ltac do_unfold v' := - let P_sz := P.sz in - let P_bitwidth := P.bitwidth in - let P_s := P.s in - let P_c := P.c in - let P_carry_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_montgomery := P.montgomery in - let P_mul_code := P.mul_code in - let P_square_code := P.square_code in - let P_upper_bound_of_exponent := P.upper_bound_of_exponent in - let P_allowable_bit_widths := P.allowable_bit_widths in - let P_freeze_extra_allowable_bit_widths := P.freeze_extra_allowable_bit_widths in - let P_modinv_fuel := P.modinv_fuel in - let v' := (eval cbv [id - List.app - sz bitwidth s c carry_chains a24 coef_div_modulus goldilocks montgomery modinv_fuel - P_sz P_bitwidth P_s P_c P_carry_chains P_a24 P_coef_div_modulus P_goldilocks P_montgomery P_modinv_fuel - P_mul_code P_square_code - upper_bound_of_exponent allowable_bit_widths freeze_allowable_bit_widths - P_upper_bound_of_exponent P_allowable_bit_widths P_freeze_extra_allowable_bit_widths - pred seq] - in v') in - v'. - Notation unfold v - := (ltac:(let v' := v in - let v' := do_unfold v' in - exact v')) - (only parsing). - Ltac extra_prove_mul_eq := P.extra_prove_mul_eq. - Ltac extra_prove_square_eq := P.extra_prove_square_eq. + Definition fill_defaults_CurveParameters (CP : RawCurveParameters.CurveParameters) + : CurveParameters + := Eval cbv_RawCurveParameters in + let sz := RawCurveParameters.sz CP in + let bitwidth := RawCurveParameters.bitwidth CP in + let montgomery := RawCurveParameters.montgomery CP in + let s := RawCurveParameters.s CP in + let c := RawCurveParameters.c CP in + let goldilocks := + defaulted + (RawCurveParameters.goldilocks CP) + (let k := Z.log2 s / 2 in + (s - eval c) =? (2^(2*k) - 2^k - 1)) in + let allowable_bit_widths + := defaulted + (RawCurveParameters.allowable_bit_widths CP) + ((if montgomery + then [8] + else nil) + ++ (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil))%nat in - Local Notation P_sz := sz. - Local Notation P_bitwidth := bitwidth. - Local Notation P_s := s. - Local Notation P_c := c. - Local Notation P_carry_chains := carry_chains. - Local Notation P_a24 := a24. - Local Notation P_coef_div_modulus := coef_div_modulus. - Local Notation P_goldilocks := goldilocks. - Local Notation P_montgomery := montgomery. - Local Notation P_upper_bound_of_exponent := upper_bound_of_exponent. - Local Notation P_allowable_bit_widths := allowable_bit_widths. - Local Notation P_freeze_allowable_bit_widths := freeze_allowable_bit_widths. - Local Notation P_modinv_fuel := modinv_fuel. + {| + sz := sz; + bitwidth := bitwidth; + s := s; + c := c; + carry_chains := defaulted (RawCurveParameters.carry_chains CP) [seq 0 (pred sz); [0; 1]]%nat; + a24 := defaulted (RawCurveParameters.a24 CP) 0; + coef_div_modulus := defaulted (RawCurveParameters.coef_div_modulus CP) 0%nat; - Ltac pose_sz sz := - cache_term_with_type_by - nat - ltac:(let v := do_compute P_sz in exact v) - sz. - Ltac pose_bitwidth bitwidth := - cache_term_with_type_by - Z - ltac:(let v := do_compute P_bitwidth in exact v) - bitwidth. - Ltac pose_s s := (* don't want to compute, e.g., [2^255] *) - cache_term_with_type_by - Z - ltac:(let v := do_unfold P_s in exact v) - s. - Ltac pose_c c := - cache_term_with_type_by - (list limb) - ltac:(let v := do_compute P_c in exact v) - c. - Ltac pose_carry_chains carry_chains := - let v := do_compute P_carry_chains in - cache_term v carry_chains. + goldilocks := goldilocks; + montgomery := montgomery; - Ltac pose_a24 a24 := - let v := do_compute P_a24 in - cache_term v a24. - Ltac pose_coef_div_modulus coef_div_modulus := - cache_term_with_type_by - nat - ltac:(let v := 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 := do_compute P_goldilocks in exact v) - goldilocks. - Ltac pose_montgomery montgomery := - cache_term_with_type_by - bool - ltac:(let v := do_compute P_montgomery in exact v) - montgomery. + mul_code := RawCurveParameters.mul_code CP; + square_code := RawCurveParameters.square_code CP; + upper_bound_of_exponent + := defaulted (RawCurveParameters.upper_bound_of_exponent CP) + (if montgomery + then (fun exp => (2^exp - 1)%Z) + else (fun exp => (2^exp + 2^(exp-3))%Z)); + allowable_bit_widths := allowable_bit_widths; + freeze_allowable_bit_widths + := defaulted + (RawCurveParameters.freeze_extra_allowable_bit_widths CP) + (list_8_if_not_exists allowable_bit_widths) + ++ allowable_bit_widths; + modinv_fuel := defaulted (RawCurveParameters.modinv_fuel CP) 10%nat + |}. - Ltac pose_modinv_fuel modinv_fuel := - cache_term_with_type_by - nat - ltac:(let v := do_compute P_modinv_fuel in exact v) - modinv_fuel. + Ltac get_fill_CurveParameters CP := + let CP := (eval hnf in CP) in + let v := (eval cbv [fill_defaults_CurveParameters] in + (fill_defaults_CurveParameters CP)) in + let v := (eval cbv_CurveParameters in v) in + let v := (eval cbv_RawCurveParameters in v) in + lazymatch v with + | ({| + sz := ?sz'; + bitwidth := ?bitwidth'; + s := ?s'; + c := ?c'; + carry_chains := ?carry_chains'; + a24 := ?a24'; + coef_div_modulus := ?coef_div_modulus'; + goldilocks := ?goldilocks'; + montgomery := ?montgomery'; + mul_code := ?mul_code'; + square_code := ?square_code'; + upper_bound_of_exponent := ?upper_bound_of_exponent'; + allowable_bit_widths := ?allowable_bit_widths'; + freeze_allowable_bit_widths := ?freeze_allowable_bit_widths'; + modinv_fuel := ?modinv_fuel' + |}) + => let sz' := do_compute sz' in + let bitwidth' := do_compute bitwidth' in + let carry_chains' := do_compute carry_chains' in + let goldilocks' := do_compute goldilocks' in + let montgomery' := do_compute montgomery' in + let allowable_bit_widths' := do_compute allowable_bit_widths' in + let freeze_allowable_bit_widths' := do_compute freeze_allowable_bit_widths' in + let modinv_fuel' := do_compute modinv_fuel' in + constr:({| + sz := sz'; + bitwidth := bitwidth'; + s := s'; + c := c'; + carry_chains := carry_chains'; + a24 := a24'; + coef_div_modulus := coef_div_modulus'; + goldilocks := goldilocks'; + montgomery := montgomery'; + mul_code := mul_code'; + square_code := square_code'; + upper_bound_of_exponent := upper_bound_of_exponent'; + allowable_bit_widths := allowable_bit_widths'; + freeze_allowable_bit_widths := freeze_allowable_bit_widths'; + modinv_fuel := modinv_fuel' + |}) + end. + (*existsb Nat.eqb List.app seq pred Z_add_red Z_sub_red Z_mul_red Z_div_red Z_pow_red Z_eqb_red + Z.to_nat Pos.to_nat Pos.iter_op Nat.add Nat.mul orb andb] in*) + Notation fill_CurveParameters CP := ltac:(let v := get_fill_CurveParameters CP in exact v) (only parsing). - Ltac pose_upper_bound_of_exponent upper_bound_of_exponent := - cache_term_with_type_by - (Z -> Z) - ltac:(let v := do_unfold P_upper_bound_of_exponent in exact v) - upper_bound_of_exponent. + Ltac internal_pose_of_CP CP proj id := + let P_proj := (eval cbv_CurveParameters in (proj CP)) in + cache_term P_proj id. + Ltac pose_sz CP sz := + internal_pose_of_CP CP CurveParameters.sz sz. + Ltac pose_bitwidth CP bitwidth := + internal_pose_of_CP CP CurveParameters.bitwidth bitwidth. + Ltac pose_s CP s := (* don't want to compute, e.g., [2^255] *) + internal_pose_of_CP CP CurveParameters.s s. + Ltac pose_c CP c := + internal_pose_of_CP CP CurveParameters.c c. + Ltac pose_carry_chains CP carry_chains := + internal_pose_of_CP CP CurveParameters.carry_chains carry_chains. + Ltac pose_a24 CP a24 := + internal_pose_of_CP CP CurveParameters.a24 a24. + Ltac pose_coef_div_modulus CP coef_div_modulus := + internal_pose_of_CP CP CurveParameters.coef_div_modulus coef_div_modulus. + Ltac pose_goldilocks CP goldilocks := + internal_pose_of_CP CP CurveParameters.goldilocks goldilocks. + Ltac pose_montgomery CP montgomery := + internal_pose_of_CP CP CurveParameters.montgomery montgomery. + Ltac pose_allowable_bit_widths CP allowable_bit_widths := + internal_pose_of_CP CP CurveParameters.allowable_bit_widths allowable_bit_widths. + Ltac pose_freeze_allowable_bit_widths CP freeze_allowable_bit_widths := + internal_pose_of_CP CP CurveParameters.freeze_allowable_bit_widths freeze_allowable_bit_widths. + Ltac pose_upper_bound_of_exponent CP upper_bound_of_exponent := + internal_pose_of_CP CP CurveParameters.upper_bound_of_exponent upper_bound_of_exponent. + Ltac pose_modinv_fuel CP modinv_fuel := + internal_pose_of_CP CP CurveParameters.modinv_fuel modinv_fuel. (* Everything below this line autogenerated by remake_packages.py *) Ltac add_sz pkg := + let CP := Tag.get pkg TAG.CP in let sz := fresh "sz" in - let sz := pose_sz sz in + let sz := pose_sz CP sz in Tag.update pkg TAG.sz sz. Ltac add_bitwidth pkg := + let CP := Tag.get pkg TAG.CP in let bitwidth := fresh "bitwidth" in - let bitwidth := pose_bitwidth bitwidth in + let bitwidth := pose_bitwidth CP bitwidth in Tag.update pkg TAG.bitwidth bitwidth. Ltac add_s pkg := + let CP := Tag.get pkg TAG.CP in let s := fresh "s" in - let s := pose_s s in + let s := pose_s CP s in Tag.update pkg TAG.s s. Ltac add_c pkg := + let CP := Tag.get pkg TAG.CP in let c := fresh "c" in - let c := pose_c c in + let c := pose_c CP c in Tag.update pkg TAG.c c. Ltac add_carry_chains pkg := + let CP := Tag.get pkg TAG.CP in let carry_chains := fresh "carry_chains" in - let carry_chains := pose_carry_chains carry_chains in + let carry_chains := pose_carry_chains CP carry_chains in Tag.update pkg TAG.carry_chains carry_chains. Ltac add_a24 pkg := + let CP := Tag.get pkg TAG.CP in let a24 := fresh "a24" in - let a24 := pose_a24 a24 in + let a24 := pose_a24 CP a24 in Tag.update pkg TAG.a24 a24. Ltac add_coef_div_modulus pkg := + let CP := Tag.get pkg TAG.CP in let coef_div_modulus := fresh "coef_div_modulus" in - let coef_div_modulus := pose_coef_div_modulus coef_div_modulus in + let coef_div_modulus := pose_coef_div_modulus CP coef_div_modulus in Tag.update pkg TAG.coef_div_modulus coef_div_modulus. Ltac add_goldilocks pkg := + let CP := Tag.get pkg TAG.CP in let goldilocks := fresh "goldilocks" in - let goldilocks := pose_goldilocks goldilocks in + let goldilocks := pose_goldilocks CP goldilocks in Tag.update pkg TAG.goldilocks goldilocks. Ltac add_montgomery pkg := + let CP := Tag.get pkg TAG.CP in let montgomery := fresh "montgomery" in - let montgomery := pose_montgomery montgomery in + let montgomery := pose_montgomery CP montgomery in Tag.update pkg TAG.montgomery montgomery. - Ltac add_modinv_fuel pkg := - let modinv_fuel := fresh "modinv_fuel" in - let modinv_fuel := pose_modinv_fuel modinv_fuel in - Tag.update pkg TAG.modinv_fuel modinv_fuel. + Ltac add_allowable_bit_widths pkg := + let CP := Tag.get pkg TAG.CP in + let allowable_bit_widths := fresh "allowable_bit_widths" in + let allowable_bit_widths := pose_allowable_bit_widths CP allowable_bit_widths in + Tag.update pkg TAG.allowable_bit_widths allowable_bit_widths. + + Ltac add_freeze_allowable_bit_widths pkg := + let CP := Tag.get pkg TAG.CP in + let freeze_allowable_bit_widths := fresh "freeze_allowable_bit_widths" in + let freeze_allowable_bit_widths := pose_freeze_allowable_bit_widths CP freeze_allowable_bit_widths in + Tag.update pkg TAG.freeze_allowable_bit_widths freeze_allowable_bit_widths. Ltac add_upper_bound_of_exponent pkg := + let CP := Tag.get pkg TAG.CP in let upper_bound_of_exponent := fresh "upper_bound_of_exponent" in - let upper_bound_of_exponent := pose_upper_bound_of_exponent upper_bound_of_exponent in + let upper_bound_of_exponent := pose_upper_bound_of_exponent CP upper_bound_of_exponent in Tag.update pkg TAG.upper_bound_of_exponent upper_bound_of_exponent. + Ltac add_modinv_fuel pkg := + let CP := Tag.get pkg TAG.CP in + let modinv_fuel := fresh "modinv_fuel" in + let modinv_fuel := pose_modinv_fuel CP modinv_fuel in + Tag.update pkg TAG.modinv_fuel modinv_fuel. + Ltac add_CurveParameters_package pkg := let pkg := add_sz pkg in let pkg := add_bitwidth pkg in @@ -276,7 +308,9 @@ Module FillCurveParameters (P : CurveParameters). let pkg := add_coef_div_modulus pkg in let pkg := add_goldilocks pkg in let pkg := add_montgomery pkg in - let pkg := add_modinv_fuel pkg in + let pkg := add_allowable_bit_widths pkg in + let pkg := add_freeze_allowable_bit_widths pkg in let pkg := add_upper_bound_of_exponent pkg in + let pkg := add_modinv_fuel pkg in Tag.strip_local pkg. -End FillCurveParameters.
\ No newline at end of file +End CurveParameters. diff --git a/src/Specific/Framework/CurveParametersPackage.v b/src/Specific/Framework/CurveParametersPackage.v index fbc937f7a..10b72f2ba 100644 --- a/src/Specific/Framework/CurveParametersPackage.v +++ b/src/Specific/Framework/CurveParametersPackage.v @@ -41,8 +41,12 @@ Module MakeCurveParametersPackage (PKG : PrePackage). Notation goldilocks := (ltac:(let v := get_goldilocks () in exact v)) (only parsing). Ltac get_montgomery _ := get TAG.montgomery. Notation montgomery := (ltac:(let v := get_montgomery () in exact v)) (only parsing). - Ltac get_modinv_fuel _ := get TAG.modinv_fuel. - Notation modinv_fuel := (ltac:(let v := get_modinv_fuel () in exact v)) (only parsing). + Ltac get_allowable_bit_widths _ := get TAG.allowable_bit_widths. + Notation allowable_bit_widths := (ltac:(let v := get_allowable_bit_widths () in exact v)) (only parsing). + Ltac get_freeze_allowable_bit_widths _ := get TAG.freeze_allowable_bit_widths. + Notation freeze_allowable_bit_widths := (ltac:(let v := get_freeze_allowable_bit_widths () in exact v)) (only parsing). Ltac get_upper_bound_of_exponent _ := get TAG.upper_bound_of_exponent. Notation upper_bound_of_exponent := (ltac:(let v := get_upper_bound_of_exponent () in exact v)) (only parsing). + Ltac get_modinv_fuel _ := get TAG.modinv_fuel. + Notation modinv_fuel := (ltac:(let v := get_modinv_fuel () in exact v)) (only parsing). End MakeCurveParametersPackage. diff --git a/src/Specific/Framework/RawCurveParameters.v b/src/Specific/Framework/RawCurveParameters.v new file mode 100644 index 000000000..8adff1f69 --- /dev/null +++ b/src/Specific/Framework/RawCurveParameters.v @@ -0,0 +1,63 @@ +Require Export Coq.ZArith.BinInt. +Require Export Coq.Lists.List. +Require Export Crypto.Util.ZUtil.Notations. +Require Crypto.Util.Tuple. + +Local Set Primitive Projections. + +Module Export Notations. (* import/export tracking *) + Export ListNotations. + + Open Scope list_scope. + Open Scope Z_scope. + + Notation limb := (Z * Z)%type. + Infix "^" := Tuple.tuple : type_scope. +End Notations. + +Record CurveParameters := + { + sz : nat; + bitwidth : Z; + s : Z; + c : list limb; + carry_chains + : option (list (list nat)) (* defaults to [seq 0 (pred sz) :: (0 :: 1 :: nil) :: nil] *); + a24 : option Z; + coef_div_modulus : option nat; + + goldilocks : option bool; (* defaults to true iff the prime ([s-c]) is of the form [2²ᵏ - 2ᵏ - 1] *) + montgomery : bool; + + mul_code : option (Z^sz -> Z^sz -> Z^sz); + square_code : option (Z^sz -> Z^sz); + upper_bound_of_exponent + : option (Z -> Z) (* defaults to [fun exp => 2^exp + 2^(exp-3)] for non-montgomery, [fun exp => 2^exp - 1] for montgomery *); + allowable_bit_widths + : option (list nat) (* defaults to [bitwidth :: 2*bitwidth :: nil] *); + freeze_extra_allowable_bit_widths + : option (list nat) (* defaults to [8 :: nil] *); + modinv_fuel : option nat + }. + +Declare Reduction cbv_RawCurveParameters + := cbv [sz + bitwidth + s + c + carry_chains + a24 + coef_div_modulus + goldilocks + montgomery + mul_code + square_code + upper_bound_of_exponent + allowable_bit_widths + freeze_extra_allowable_bit_widths + modinv_fuel]. + +(* +Ltac extra_prove_mul_eq := idtac. +Ltac extra_prove_square_eq := idtac. + *) diff --git a/src/Specific/Framework/SynthesisFramework.v b/src/Specific/Framework/SynthesisFramework.v index 01f91731e..9c930567e 100644 --- a/src/Specific/Framework/SynthesisFramework.v +++ b/src/Specific/Framework/SynthesisFramework.v @@ -27,15 +27,16 @@ Module Tag. Notation Context := Tag.Context (only parsing). End Tag. -Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters). - Module P := FillCurveParameters Curve. - - Ltac add_Synthesis_package pkg := - let P_default_mul _ := P.default_mul in - let P_extra_prove_mul_eq _ := P.extra_prove_mul_eq in - let P_default_square _ := P.default_square in - let P_extra_prove_square_eq _ := P.extra_prove_square_eq in - let pkg := P.add_CurveParameters_package pkg in +Module Export MakeSynthesisTactics. + Ltac add_Synthesis_package pkg curve extra_prove_mul_eq extra_prove_square_eq := + let CP := get_fill_CurveParameters curve in + let P_default_mul _ := default_mul CP in + let P_extra_prove_mul_eq := extra_prove_mul_eq in + let P_default_square _ := default_square CP in + let P_extra_prove_square_eq := extra_prove_square_eq in + let pkg := Tag.local_update pkg TAG.CP CP in + let pkg := add_CurveParameters_package pkg in + let pkg := Tag.strip_local pkg in let pkg := add_Base_package pkg in let pkg := add_ReificationTypes_package pkg in let pkg := add_Karatsuba_package pkg in @@ -49,18 +50,16 @@ Module MakeSynthesisTactics (Curve : CurveParameters.CurveParameters). let pkg := add_Ladderstep_package pkg in pkg. - Ltac get_Synthesis_package _ := + Ltac get_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq := let pkg := constr:(Tag.empty) in - add_Synthesis_package pkg. + add_Synthesis_package pkg curve extra_prove_mul_eq extra_prove_square_eq. - Ltac make_Synthesis_package _ := - let pkg := get_Synthesis_package () in + Ltac make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq := + let pkg := get_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq in exact pkg. End MakeSynthesisTactics. -Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePackage). - Module P := CurveParameters.FillCurveParameters Curve. - +Module PackageSynthesis (PKG : PrePackage). Module CP := MakeCurveParametersPackage PKG. Module BP := MakeBasePackage PKG. Module DP := MakeDefaultsPackage PKG. @@ -83,11 +82,12 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack Ltac synthesize_with_carry do_rewrite get_op_sig := let carry_sig := get_carry_sig () in let op_sig := get_op_sig () in + let allowable_bit_widths := get_allowable_bit_widths () in start_preglue; [ do_rewrite op_sig carry_sig; cbv_runtime | .. ]; fin_preglue; - refine_reflectively_gen P.allowable_bit_widths default. + refine_reflectively_gen allowable_bit_widths default. Ltac synthesize_2arg_with_carry get_op_sig := synthesize_with_carry do_rewrite_with_2sig_add_carry get_op_sig. Ltac synthesize_1arg_with_carry get_op_sig := @@ -97,6 +97,7 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack let phi := get_phi_for_preglue () in let op_sig := get_op_sig () in let op_bounded := get_op_bounded () in + let allowable_bit_widths := get_allowable_bit_widths () in let do_red _ := lazymatch (eval cbv [phi] in phi) with | (fun x => ?montgomery_to_F (?meval (?feBW_of_feBW_small _))) @@ -109,15 +110,17 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack | .. ]; fin_preglue; factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t; - refine_reflectively_gen P.allowable_bit_widths anf. + refine_reflectively_gen allowable_bit_widths anf. Ltac synthesize_2arg_choice get_op_sig get_op_bounded := - lazymatch (eval vm_compute in P.montgomery) with + let montgomery := get_montgomery () in + lazymatch (eval vm_compute in montgomery) with | true => synthesize_montgomery get_op_sig get_op_bounded | false => synthesize_2arg_with_carry get_op_sig end. Ltac synthesize_1arg_choice get_op_sig get_op_bounded := - lazymatch (eval vm_compute in P.montgomery) with + let montgomery := get_montgomery () in + lazymatch (eval vm_compute in montgomery) with | true => synthesize_montgomery get_op_sig get_op_bounded | false => synthesize_1arg_with_carry get_op_sig end. @@ -130,14 +133,16 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack Ltac synthesize_freeze _ := let freeze_sig := get_freeze_sig () in let feBW_bounded := get_feBW_bounded () in + let freeze_allowable_bit_widths := get_freeze_allowable_bit_widths () in start_preglue; [ do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime | .. ]; fin_preglue; - refine_reflectively_gen P.freeze_allowable_bit_widths anf. + refine_reflectively_gen freeze_allowable_bit_widths anf. Ltac synthesize_xzladderstep _ := let Mxzladderstep_sig := get_Mxzladderstep_sig () in let a24_sig := get_a24_sig () in + let allowable_bit_widths := get_allowable_bit_widths () in start_preglue; [ unmap_map_tuple (); do_rewrite_with_sig_1arg Mxzladderstep_sig; @@ -146,10 +151,10 @@ Module PackageSynthesis (Curve : CurveParameters.CurveParameters) (PKG : PrePack cbv_runtime | .. ]; finish_conjoined_preglue (); - refine_reflectively_gen P.allowable_bit_widths default. + refine_reflectively_gen allowable_bit_widths default. Ltac synthesize_nonzero _ := let op_sig := get_nonzero_sig () in + let allowable_bit_widths := get_allowable_bit_widths () in nonzero_preglue op_sig ltac:(fun _ => cbv_runtime); - refine_reflectively_gen P.allowable_bit_widths anf. - + refine_reflectively_gen allowable_bit_widths anf. End PackageSynthesis. diff --git a/src/Specific/Framework/make_curve.py b/src/Specific/Framework/make_curve.py index afed1243c..9bd260d4e 100755 --- a/src/Specific/Framework/make_curve.py +++ b/src/Specific/Framework/make_curve.py @@ -6,8 +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_chains(): - return ['seq 0 (pred sz)', '[0; 1]'] +def default_carry_chains(sz): + return ['seq 0 (pred %(sz)s)' % locals(), '[0; 1]'] def compute_s(modulus_str): base, exp, rest = re.match(r'\s*'.join(('^', '(2)', r'\^', '([0-9]+)', r'([0-9\^ +\*-]*)$')), modulus_str).groups() return '%s^%s' % (base, exp) @@ -33,6 +33,7 @@ def compute_c(modulus_str): # XXX FIXME: Is this the right way to extract c? return [('1', rest)] def compute_goldilocks(s, c): + # true if the prime is of the form 2^2k - 2^k - 1 ms = re.match(r'^2\^([0-9]+)$', s) if ms is None: return False two_k = int(ms.groups()[0]) @@ -194,13 +195,13 @@ def make_curve_parameters(parameters): 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() + defaults = default_carry_chains(replacements['sz']) 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'] in ('default', 'Some default'): - replacements['carry_chains'] = 'Some %s%%nat' % nested_list_to_string(default_carry_chains()) + replacements['carry_chains'] = 'Some %s%%nat' % nested_list_to_string(default_carry_chains(replacements['sz'])) replacements['s'] = parameters.get('s', compute_s(parameters['modulus'])) replacements['c'] = parameters.get('c', compute_c(parameters['modulus'])) replacements['goldilocks'] = parameters.get('goldilocks', compute_goldilocks(replacements['s'], replacements['c'])) @@ -214,7 +215,8 @@ def make_curve_parameters(parameters): ('allowable_bit_widths', '%nat'), ('freeze_extra_allowable_bit_widths', '%nat'), ('coef_div_modulus', '%nat'), - ('modinv_fuel', '%nat')): + ('modinv_fuel', '%nat'), + ('goldilocks', '')): replacements[k] = fix_option(nested_list_to_string(replacements.get(k, 'None')), scope_string=scope_string) for k in ('montgomery', ): if k not in replacements.keys(): @@ -224,7 +226,7 @@ def make_curve_parameters(parameters): for k in ('extra_prove_mul_eq', 'extra_prove_square_eq'): if k not in replacements.keys(): replacements[k] = 'idtac' - ret = r"""Require Import Crypto.Specific.Framework.CurveParameters. + ret = r"""Require Import Crypto.Specific.Framework.RawCurveParameters. Require Import Crypto.Util.LetIn. (*** @@ -232,32 +234,32 @@ Modulus : %(modulus)s Base: %(base)s ***) -Module Curve <: CurveParameters. - Definition sz : nat := %(sz)s%%nat. - Definition bitwidth : Z := %(bitwidth)s. - Definition s : Z := %(s)s. - Definition c : list limb := %(c)s. - Definition carry_chains : option (list (list nat)) := Eval vm_compute in %(carry_chains)s. +Definition curve : CurveParameters := + {| + sz := %(sz)s%%nat; + bitwidth := %(bitwidth)s; + s := %(s)s; + c := %(c)s; + carry_chains := %(carry_chains)s; - Definition a24 : option Z := %(a24)s. - Definition coef_div_modulus : option nat := %(coef_div_modulus)s. (* add %(coef_div_modulus_raw)s*modulus before subtracting *) + a24 := %(a24)s; + coef_div_modulus := %(coef_div_modulus)s; - Definition goldilocks : bool := %(goldilocks)s. - Definition montgomery : bool := %(montgomery)s. + goldilocks := %(goldilocks)s; + montgomery := %(montgomery)s; - Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) - := %(mul)s. + mul_code := %(mul)s; - Definition square_code : option (Z^sz -> Z^sz) - := %(square)s. + square_code := %(square)s; - Definition upper_bound_of_exponent : option (Z -> Z) := %(upper_bound_of_exponent)s. - Definition allowable_bit_widths : option (list nat) := %(allowable_bit_widths)s. - Definition freeze_extra_allowable_bit_widths : option (list nat) := %(freeze_extra_allowable_bit_widths)s. - Definition modinv_fuel : option nat := %(modinv_fuel)s. - Ltac extra_prove_mul_eq := %(extra_prove_mul_eq)s. - Ltac extra_prove_square_eq := %(extra_prove_square_eq)s. -End Curve. + upper_bound_of_exponent := %(upper_bound_of_exponent)s; + allowable_bit_widths := %(allowable_bit_widths)s; + freeze_extra_allowable_bit_widths := %(freeze_extra_allowable_bit_widths)s; + modinv_fuel := %(modinv_fuel)s + |}. + +Ltac extra_prove_mul_eq _ := %(extra_prove_mul_eq)s. +Ltac extra_prove_square_eq _ := %(extra_prove_square_eq)s. """ % replacements return ret @@ -265,14 +267,12 @@ def make_synthesis(prefix): return r"""Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import %s.CurveParameters. -Module Import T := MakeSynthesisTactics Curve. - Module P <: PrePackage. Definition package : Tag.Context. - Proof. make_Synthesis_package (). Defined. + Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined. End P. -Module Export S := PackageSynthesis Curve P. +Module Export S := PackageSynthesis P. """ % prefix def make_synthesized_arg(fearg, prefix, montgomery=False): diff --git a/src/Specific/NISTP256/AMD128/CurveParameters.v b/src/Specific/NISTP256/AMD128/CurveParameters.v index ea4865b08..56d452941 100644 --- a/src/Specific/NISTP256/AMD128/CurveParameters.v +++ b/src/Specific/NISTP256/AMD128/CurveParameters.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Specific.Framework.RawCurveParameters. Require Import Crypto.Util.LetIn. (*** @@ -6,29 +6,29 @@ Modulus : 2^256-2^224+2^192+2^96-1 Base: 128 ***) -Module Curve <: CurveParameters. - Definition sz : nat := 2%nat. - Definition bitwidth : Z := 128. - Definition s : Z := 2^256. - Definition c : list limb := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]. - Definition carry_chains : option (list (list nat)) := Eval vm_compute in None. +Definition curve : CurveParameters := + {| + sz := 2%nat; + bitwidth := 128; + s := 2^256; + c := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]; + carry_chains := None; - Definition a24 : option Z := None. - Definition coef_div_modulus : option nat := None. (* add 0*modulus before subtracting *) + a24 := None; + coef_div_modulus := None; - Definition goldilocks : bool := false. - Definition montgomery : bool := true. + goldilocks := Some false; + montgomery := true; - Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) - := None. + mul_code := None; - Definition square_code : option (Z^sz -> Z^sz) - := None. + square_code := 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. - Definition modinv_fuel : option nat := None. - Ltac extra_prove_mul_eq := idtac. - Ltac extra_prove_square_eq := idtac. -End Curve. + upper_bound_of_exponent := None; + allowable_bit_widths := None; + freeze_extra_allowable_bit_widths := None; + modinv_fuel := None + |}. + +Ltac extra_prove_mul_eq _ := idtac. +Ltac extra_prove_square_eq _ := idtac. diff --git a/src/Specific/NISTP256/AMD128/Synthesis.v b/src/Specific/NISTP256/AMD128/Synthesis.v index 3871666e1..4dffed20b 100644 --- a/src/Specific/NISTP256/AMD128/Synthesis.v +++ b/src/Specific/NISTP256/AMD128/Synthesis.v @@ -1,11 +1,9 @@ Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import Crypto.Specific.NISTP256.AMD128.CurveParameters. -Module Import T := MakeSynthesisTactics Curve. - Module P <: PrePackage. Definition package : Tag.Context. - Proof. make_Synthesis_package (). Defined. + Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined. End P. -Module Export S := PackageSynthesis Curve P. +Module Export S := PackageSynthesis P. diff --git a/src/Specific/NISTP256/AMD64/CurveParameters.v b/src/Specific/NISTP256/AMD64/CurveParameters.v index 01cac5db0..e90ffe113 100644 --- a/src/Specific/NISTP256/AMD64/CurveParameters.v +++ b/src/Specific/NISTP256/AMD64/CurveParameters.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Specific.Framework.RawCurveParameters. Require Import Crypto.Util.LetIn. (*** @@ -6,29 +6,29 @@ Modulus : 2^256-2^224+2^192+2^96-1 Base: 64 ***) -Module Curve <: CurveParameters. - Definition sz : nat := 4%nat. - Definition bitwidth : Z := 64. - Definition s : Z := 2^256. - Definition c : list limb := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]. - Definition carry_chains : option (list (list nat)) := Eval vm_compute in None. +Definition curve : CurveParameters := + {| + sz := 4%nat; + bitwidth := 64; + s := 2^256; + c := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]; + carry_chains := None; - Definition a24 : option Z := None. - Definition coef_div_modulus : option nat := None. (* add 0*modulus before subtracting *) + a24 := None; + coef_div_modulus := None; - Definition goldilocks : bool := false. - Definition montgomery : bool := true. + goldilocks := Some false; + montgomery := true; - Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) - := None. + mul_code := None; - Definition square_code : option (Z^sz -> Z^sz) - := None. + square_code := 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. - Definition modinv_fuel : option nat := None. - Ltac extra_prove_mul_eq := idtac. - Ltac extra_prove_square_eq := idtac. -End Curve. + upper_bound_of_exponent := None; + allowable_bit_widths := None; + freeze_extra_allowable_bit_widths := None; + modinv_fuel := None + |}. + +Ltac extra_prove_mul_eq _ := idtac. +Ltac extra_prove_square_eq _ := idtac. diff --git a/src/Specific/NISTP256/AMD64/Synthesis.v b/src/Specific/NISTP256/AMD64/Synthesis.v index ede40bb8c..5cd0686e1 100644 --- a/src/Specific/NISTP256/AMD64/Synthesis.v +++ b/src/Specific/NISTP256/AMD64/Synthesis.v @@ -1,11 +1,9 @@ Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import Crypto.Specific.NISTP256.AMD64.CurveParameters. -Module Import T := MakeSynthesisTactics Curve. - Module P <: PrePackage. Definition package : Tag.Context. - Proof. make_Synthesis_package (). Defined. + Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined. End P. -Module Export S := PackageSynthesis Curve P. +Module Export S := PackageSynthesis P. diff --git a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v index cc8393d9b..7302294b8 100644 --- a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v +++ b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Specific.Framework.RawCurveParameters. Require Import Crypto.Util.LetIn. (*** @@ -6,29 +6,29 @@ 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 curve : CurveParameters := + {| + sz := 8%nat; + bitwidth := 64; + s := 2^448; + c := [(1, 1); (2^224, 1)]; + carry_chains := Some [[3; 7]; [0; 4; 1; 5; 2; 6; 3; 7]; [4; 0]]%nat; - Definition a24 : option Z := None. - Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) + a24 := None; + coef_div_modulus := Some 2%nat; - Definition goldilocks : bool := true. - Definition montgomery : bool := false. + goldilocks := Some true; + montgomery := false; - Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) - := None. + mul_code := None; - Definition square_code : option (Z^sz -> Z^sz) - := None. + square_code := 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. - Definition modinv_fuel : option nat := None. - Ltac extra_prove_mul_eq := idtac. - Ltac extra_prove_square_eq := idtac. -End Curve. + upper_bound_of_exponent := None; + allowable_bit_widths := None; + freeze_extra_allowable_bit_widths := None; + modinv_fuel := None + |}. + +Ltac extra_prove_mul_eq _ := idtac. +Ltac extra_prove_square_eq _ := idtac. diff --git a/src/Specific/X2448/Karatsuba/C64/Synthesis.v b/src/Specific/X2448/Karatsuba/C64/Synthesis.v index 500671c90..4016ee71c 100644 --- a/src/Specific/X2448/Karatsuba/C64/Synthesis.v +++ b/src/Specific/X2448/Karatsuba/C64/Synthesis.v @@ -1,11 +1,9 @@ Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import Crypto.Specific.X2448.Karatsuba.C64.CurveParameters. -Module Import T := MakeSynthesisTactics Curve. - Module P <: PrePackage. Definition package : Tag.Context. - Proof. make_Synthesis_package (). Defined. + Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined. End P. -Module Export S := PackageSynthesis Curve P. +Module Export S := PackageSynthesis P. diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v index 55853a9c1..f112bc2ac 100644 --- a/src/Specific/X25519/C32/CurveParameters.v +++ b/src/Specific/X25519/C32/CurveParameters.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Specific.Framework.RawCurveParameters. Require Import Crypto.Util.LetIn. (*** @@ -6,21 +6,21 @@ Modulus : 2^255-19 Base: 25.5 ***) -Module Curve <: CurveParameters. - Definition sz : nat := 10%nat. - Definition bitwidth : Z := 32. - Definition s : Z := 2^255. - Definition c : list limb := [(1, 19)]. - Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat. +Definition curve : CurveParameters := + {| + sz := 10%nat; + bitwidth := 32; + s := 2^255; + c := [(1, 19)]; + carry_chains := Some [seq 0 (pred 10); [0; 1]]%nat; - Definition a24 : option Z := Some 121665. - Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) + a24 := Some 121665; + coef_div_modulus := Some 2%nat; - Definition goldilocks : bool := false. - Definition montgomery : bool := false. + goldilocks := Some false; + montgomery := false; - Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) - := Some (fun a b => + mul_code := 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>. *) let '(in9, in8, in7, in6, in5, in4, in3, in2, in1, in0) := a in let '(in29, in28, in27, in26, in25, in24, in23, in22, in21, in20) := b in @@ -152,10 +152,9 @@ Module Curve <: CurveParameters. dlet output0 := output0 + output10 << 1 in dlet output0 := output0 + output10 in (output9, output8, output7, output6, output5, output4, output3, output2, output1, output0) - ). + ); - Definition square_code : option (Z^sz -> Z^sz) - := Some (fun a => + square_code := Some (fun a => (* Micro-optimized form from curve25519-donna by Adam Langley (Google) and Daniel Bernstein. See <https://github.com/agl/curve25519-donna/blob/master/LICENSE.md>. *) let '(in9, in8, in7, in6, in5, in4, in3, in2, in1, in0) := a in dlet output0 := in0 * in0 in @@ -241,12 +240,13 @@ Module Curve <: CurveParameters. dlet output0 := output0 + output10 << 1 in dlet output0 := output0 + output10 in (output9, output8, output7, output6, output5, output4, output3, output2, output1, output0) - ). + ); - 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. - Definition modinv_fuel : option nat := None. - Ltac extra_prove_mul_eq := idtac. - Ltac extra_prove_square_eq := idtac. -End Curve. + upper_bound_of_exponent := None; + allowable_bit_widths := None; + freeze_extra_allowable_bit_widths := None; + modinv_fuel := None + |}. + +Ltac extra_prove_mul_eq _ := idtac. +Ltac extra_prove_square_eq _ := idtac. diff --git a/src/Specific/X25519/C32/Synthesis.v b/src/Specific/X25519/C32/Synthesis.v index 0b3336b20..0fc22f0a7 100644 --- a/src/Specific/X25519/C32/Synthesis.v +++ b/src/Specific/X25519/C32/Synthesis.v @@ -1,11 +1,9 @@ Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import Crypto.Specific.X25519.C32.CurveParameters. -Module Import T := MakeSynthesisTactics Curve. - Module P <: PrePackage. Definition package : Tag.Context. - Proof. make_Synthesis_package (). Defined. + Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined. End P. -Module Export S := PackageSynthesis Curve P. +Module Export S := PackageSynthesis P. diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v index 6d9666194..0a727968f 100644 --- a/src/Specific/X25519/C64/CurveParameters.v +++ b/src/Specific/X25519/C64/CurveParameters.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Specific.Framework.RawCurveParameters. Require Import Crypto.Util.LetIn. (*** @@ -6,21 +6,21 @@ Modulus : 2^255-19 Base: 51 ***) -Module Curve <: CurveParameters. - Definition sz : nat := 5%nat. - Definition bitwidth : Z := 64. - Definition s : Z := 2^255. - Definition c : list limb := [(1, 19)]. - Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat. +Definition curve : CurveParameters := + {| + sz := 5%nat; + bitwidth := 64; + s := 2^255; + c := [(1, 19)]; + carry_chains := Some [seq 0 (pred 5); [0; 1]]%nat; - Definition a24 : option Z := Some 121665. - Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) + a24 := Some 121665; + coef_div_modulus := Some 2%nat; - Definition goldilocks : bool := false. - Definition montgomery : bool := false. + goldilocks := Some false; + montgomery := false; - Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) - := Some (fun a b => + mul_code := 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>. *) let '(r4, r3, r2, r1, r0) := a in let '(s4, s3, s2, s1, s0) := b in @@ -40,10 +40,9 @@ Module Curve <: CurveParameters. dlet t2 := t2 + r4 * s3 + r3 * s4 in dlet t3 := t3 + r4 * s4 in (t4, t3, t2, t1, t0) - ). + ); - Definition square_code : option (Z^sz -> Z^sz) - := Some (fun a => + square_code := Some (fun a => (* 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>. *) let '(r4, r3, r2, r1, r0) := a in dlet d0 := r0 * 2 in @@ -58,12 +57,13 @@ Module Curve <: CurveParameters. dlet t3 := d0 * r3 + d1 * r2 + (r4 * (d419 )) in dlet t4 := d0 * r4 + d1 * r3 + (r2 * (r2 )) in (t4, t3, t2, t1, t0) - ). + ); - 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. - Definition modinv_fuel : option nat := None. - Ltac extra_prove_mul_eq := idtac. - Ltac extra_prove_square_eq := idtac. -End Curve. + upper_bound_of_exponent := None; + allowable_bit_widths := None; + freeze_extra_allowable_bit_widths := None; + modinv_fuel := None + |}. + +Ltac extra_prove_mul_eq _ := idtac. +Ltac extra_prove_square_eq _ := idtac. diff --git a/src/Specific/X25519/C64/Synthesis.v b/src/Specific/X25519/C64/Synthesis.v index 2ea78caba..b398e13d9 100644 --- a/src/Specific/X25519/C64/Synthesis.v +++ b/src/Specific/X25519/C64/Synthesis.v @@ -1,11 +1,9 @@ Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import Crypto.Specific.X25519.C64.CurveParameters. -Module Import T := MakeSynthesisTactics Curve. - Module P <: PrePackage. Definition package : Tag.Context. - Proof. make_Synthesis_package (). Defined. + Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined. End P. -Module Export S := PackageSynthesis Curve P. +Module Export S := PackageSynthesis P. diff --git a/src/Specific/X2555/C128/CurveParameters.v b/src/Specific/X2555/C128/CurveParameters.v index 46b56378b..f3ae4511b 100644 --- a/src/Specific/X2555/C128/CurveParameters.v +++ b/src/Specific/X2555/C128/CurveParameters.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Specific.Framework.RawCurveParameters. Require Import Crypto.Util.LetIn. (*** @@ -6,29 +6,29 @@ Modulus : 2^255-5 Base: 130 ***) -Module Curve <: CurveParameters. - Definition sz : nat := 3%nat. - Definition bitwidth : Z := 128. - Definition s : Z := 2^255. - Definition c : list limb := [(1, 5)]. - Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat. +Definition curve : CurveParameters := + {| + sz := 3%nat; + bitwidth := 128; + s := 2^255; + c := [(1, 5)]; + carry_chains := Some [seq 0 (pred 3); [0; 1]]%nat; - Definition a24 : option Z := Some (121665 (* XXX TODO(andreser) FIXME? Is this right for this curve? *)). - Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) + a24 := Some (121665 (* XXX TODO(andreser) FIXME? Is this right for this curve? *)); + coef_div_modulus := Some 2%nat; - Definition goldilocks : bool := false. - Definition montgomery : bool := false. + goldilocks := Some false; + montgomery := false; - Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) - := None. + mul_code := None; - Definition square_code : option (Z^sz -> Z^sz) - := None. + square_code := 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. - Definition modinv_fuel : option nat := None. - Ltac extra_prove_mul_eq := idtac. - Ltac extra_prove_square_eq := idtac. -End Curve. + upper_bound_of_exponent := None; + allowable_bit_widths := None; + freeze_extra_allowable_bit_widths := None; + modinv_fuel := None + |}. + +Ltac extra_prove_mul_eq _ := idtac. +Ltac extra_prove_square_eq _ := idtac. diff --git a/src/Specific/X2555/C128/Synthesis.v b/src/Specific/X2555/C128/Synthesis.v index 1fa3b4a6c..af7b8ae33 100644 --- a/src/Specific/X2555/C128/Synthesis.v +++ b/src/Specific/X2555/C128/Synthesis.v @@ -1,11 +1,9 @@ Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import Crypto.Specific.X2555.C128.CurveParameters. -Module Import T := MakeSynthesisTactics Curve. - Module P <: PrePackage. Definition package : Tag.Context. - Proof. make_Synthesis_package (). Defined. + Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined. End P. -Module Export S := PackageSynthesis Curve P. +Module Export S := PackageSynthesis P. |