diff options
Diffstat (limited to 'src/Specific/Framework/CurveParameters.v')
| -rw-r--r-- | src/Specific/Framework/CurveParameters.v | 425 |
1 files changed, 0 insertions, 425 deletions
diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v deleted file mode 100644 index 91d876372..000000000 --- a/src/Specific/Framework/CurveParameters.v +++ /dev/null @@ -1,425 +0,0 @@ -Require Import Coq.QArith.Qround. -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. - -Local Set Primitive Projections. - -Module Export Notations := RawCurveParameters.Notations. - -Module TAG. (* namespacing *) - Inductive tags := CP | sz | base | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | karatsuba | montgomery | freeze | ladderstep | upper_bound_of_exponent_tight | upper_bound_of_exponent_loose | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel | mul_code | square_code. -End TAG. - -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). - Local Notation defaulted opt_v default - := (match opt_v with - | Some v => v - | None => default - end) - (only parsing). - Record CurveParameters := - { - sz : nat; - base : Q; - bitwidth : Z; - s : Z; - c : list limb; - carry_chains : list (list nat); - a24 : option Z; - coef_div_modulus : nat; - - goldilocks : bool; - karatsuba : bool; - montgomery : bool; - freeze : bool; - ladderstep : bool; - - mul_code : option (Z^sz -> Z^sz -> Z^sz); - square_code : option (Z^sz -> Z^sz); - upper_bound_of_exponent_tight : Z -> Z; - upper_bound_of_exponent_loose : Z -> Z; - allowable_bit_widths : list nat; - freeze_allowable_bit_widths : list nat; - modinv_fuel : nat - }. - - Declare Reduction cbv_CurveParameters - := cbv [sz - base - bitwidth - s - c - carry_chains - a24 - coef_div_modulus - goldilocks - karatsuba - montgomery - freeze - ladderstep - mul_code - square_code - upper_bound_of_exponent_tight - upper_bound_of_exponent_loose - 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 CP := - lazymatch (eval hnf in (square_code CP)) with - | None => reflexivity - | Some ?square_code - => instantiate (1:=square_code) - end. - - Local Notation list_n_if_not_exists n ls := - (if existsb (Nat.eqb n) ls - then nil - else [n]%nat) - (only parsing). - Local Notation list_8_if_not_exists ls - := (list_n_if_not_exists 8%nat ls) (only parsing). - Local Notation list_1_if_not_exists ls - := (list_n_if_not_exists 1%nat ls) (only parsing). - - Definition fill_defaults_CurveParameters (CP : RawCurveParameters.CurveParameters) - : CurveParameters - := Eval cbv_RawCurveParameters in - let sz := RawCurveParameters.sz CP in - let base := RawCurveParameters.base CP in - let bitwidth := RawCurveParameters.bitwidth CP in - let montgomery := RawCurveParameters.montgomery CP in - let karatsuba := defaulted (RawCurveParameters.karatsuba CP) false in - let s := RawCurveParameters.s CP in - let c := RawCurveParameters.c CP in - let freeze - := defaulted - (RawCurveParameters.freeze CP) - (s =? 2^(Qceiling (base * sz))) 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 [1; 8] - else nil) - ++ (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil))%nat in - let upper_bound_of_exponent_tight - := defaulted (RawCurveParameters.upper_bound_of_exponent_tight CP) - (if montgomery - then (fun exp => (2^exp - 1)%Z) - else (fun exp => (2^exp + 2^(exp-3))%Z)) - (* max is [(0, 2^(exp+2) + 2^exp + 2^(exp-1) + 2^(exp-3) + 2^(exp-4) + 2^(exp-5) + 2^(exp-6) + 2^(exp-10) + 2^(exp-12) + 2^(exp-13) + 2^(exp-14) + 2^(exp-15) + 2^(exp-17) + 2^(exp-23) + 2^(exp-24))%Z] *) in - let upper_bound_of_exponent_loose - := defaulted (RawCurveParameters.upper_bound_of_exponent_loose CP) - (if montgomery - then (fun exp => (2^exp - 1)%Z) - else (fun exp => (3 * upper_bound_of_exponent_tight exp)%Z)) in - {| - sz := sz; - base := base; - bitwidth := bitwidth; - s := s; - c := c; - carry_chains := defaulted (RawCurveParameters.carry_chains CP) [seq 0 (pred sz); [0; 1]]%nat; - a24 := RawCurveParameters.a24 CP; - coef_div_modulus := defaulted (RawCurveParameters.coef_div_modulus CP) 0%nat; - - goldilocks := goldilocks; - karatsuba := karatsuba; - montgomery := montgomery; - freeze := freeze; - ladderstep := RawCurveParameters.ladderstep CP; - - mul_code := RawCurveParameters.mul_code CP; - square_code := RawCurveParameters.square_code CP; - upper_bound_of_exponent_tight := upper_bound_of_exponent_tight; - upper_bound_of_exponent_loose := upper_bound_of_exponent_loose; - - allowable_bit_widths := allowable_bit_widths; - freeze_allowable_bit_widths - := defaulted - (RawCurveParameters.freeze_extra_allowable_bit_widths CP) - ((list_1_if_not_exists allowable_bit_widths) - ++ (list_8_if_not_exists allowable_bit_widths)) - ++ allowable_bit_widths; - modinv_fuel := defaulted (RawCurveParameters.modinv_fuel CP) (Z.to_nat (Z.log2_up s)) - |}. - - 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'; - base := ?base'; - bitwidth := ?bitwidth'; - s := ?s'; - c := ?c'; - carry_chains := ?carry_chains'; - a24 := ?a24'; - coef_div_modulus := ?coef_div_modulus'; - goldilocks := ?goldilocks'; - karatsuba := ?karatsuba'; - montgomery := ?montgomery'; - freeze := ?freeze'; - ladderstep := ?ladderstep'; - mul_code := ?mul_code'; - square_code := ?square_code'; - upper_bound_of_exponent_tight := ?upper_bound_of_exponent_tight'; - upper_bound_of_exponent_loose := ?upper_bound_of_exponent_loose'; - 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 base' := do_compute base' in - let bitwidth' := do_compute bitwidth' in - let carry_chains' := do_compute carry_chains' in - let goldilocks' := do_compute goldilocks' in - let karatsuba' := do_compute karatsuba' in - let montgomery' := do_compute montgomery' in - let freeze' := do_compute freeze' in - let ladderstep' := do_compute ladderstep' 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'; - base := base'; - bitwidth := bitwidth'; - s := s'; - c := c'; - carry_chains := carry_chains'; - a24 := a24'; - coef_div_modulus := coef_div_modulus'; - goldilocks := goldilocks'; - karatsuba := karatsuba'; - montgomery := montgomery'; - freeze := freeze'; - ladderstep := ladderstep'; - mul_code := mul_code'; - square_code := square_code'; - upper_bound_of_exponent_tight := upper_bound_of_exponent_tight'; - upper_bound_of_exponent_loose := upper_bound_of_exponent_loose'; - allowable_bit_widths := allowable_bit_widths'; - freeze_allowable_bit_widths := freeze_allowable_bit_widths'; - modinv_fuel := modinv_fuel' - |}) - end. - Notation fill_CurveParameters CP := ltac:(let v := get_fill_CurveParameters CP in exact v) (only parsing). - - 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_base CP base := - internal_pose_of_CP CP CurveParameters.base base. - 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_karatsuba CP karatsuba := - internal_pose_of_CP CP CurveParameters.karatsuba karatsuba. - Ltac pose_montgomery CP montgomery := - internal_pose_of_CP CP CurveParameters.montgomery montgomery. - Ltac pose_freeze CP freeze := - internal_pose_of_CP CP CurveParameters.freeze freeze. - Ltac pose_ladderstep CP ladderstep := - internal_pose_of_CP CP CurveParameters.ladderstep ladderstep. - 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_tight CP upper_bound_of_exponent_tight := - internal_pose_of_CP CP CurveParameters.upper_bound_of_exponent_tight upper_bound_of_exponent_tight. - Ltac pose_upper_bound_of_exponent_loose CP upper_bound_of_exponent_loose := - internal_pose_of_CP CP CurveParameters.upper_bound_of_exponent_loose upper_bound_of_exponent_loose. - Ltac pose_modinv_fuel CP modinv_fuel := - internal_pose_of_CP CP CurveParameters.modinv_fuel modinv_fuel. - Ltac pose_mul_code CP mul_code := - internal_pose_of_CP CP CurveParameters.mul_code mul_code. - Ltac pose_square_code CP square_code := - internal_pose_of_CP CP CurveParameters.square_code square_code. - - (* Everything below this line autogenerated by remake_packages.py *) - Ltac add_base pkg := - let CP := Tag.get pkg TAG.CP in - let base := fresh "base" in - let base := pose_base CP base in - Tag.update pkg TAG.base base. - - Ltac add_sz pkg := - let CP := Tag.get pkg TAG.CP in - let sz := fresh "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 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 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 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 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 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 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 CP goldilocks in - Tag.update pkg TAG.goldilocks goldilocks. - - Ltac add_karatsuba pkg := - let CP := Tag.get pkg TAG.CP in - let karatsuba := fresh "karatsuba" in - let karatsuba := pose_karatsuba CP karatsuba in - Tag.update pkg TAG.karatsuba karatsuba. - - Ltac add_montgomery pkg := - let CP := Tag.get pkg TAG.CP in - let montgomery := fresh "montgomery" in - let montgomery := pose_montgomery CP montgomery in - Tag.update pkg TAG.montgomery montgomery. - - Ltac add_freeze pkg := - let CP := Tag.get pkg TAG.CP in - let freeze := fresh "freeze" in - let freeze := pose_freeze CP freeze in - Tag.update pkg TAG.freeze freeze. - - Ltac add_ladderstep pkg := - let CP := Tag.get pkg TAG.CP in - let ladderstep := fresh "ladderstep" in - let ladderstep := pose_ladderstep CP ladderstep in - Tag.update pkg TAG.ladderstep ladderstep. - - 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_tight pkg := - let CP := Tag.get pkg TAG.CP in - let upper_bound_of_exponent_tight := fresh "upper_bound_of_exponent_tight" in - let upper_bound_of_exponent_tight := pose_upper_bound_of_exponent_tight CP upper_bound_of_exponent_tight in - Tag.update pkg TAG.upper_bound_of_exponent_tight upper_bound_of_exponent_tight. - - Ltac add_upper_bound_of_exponent_loose pkg := - let CP := Tag.get pkg TAG.CP in - let upper_bound_of_exponent_loose := fresh "upper_bound_of_exponent_loose" in - let upper_bound_of_exponent_loose := pose_upper_bound_of_exponent_loose CP upper_bound_of_exponent_loose in - Tag.update pkg TAG.upper_bound_of_exponent_loose upper_bound_of_exponent_loose. - - 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_mul_code pkg := - let CP := Tag.get pkg TAG.CP in - let mul_code := fresh "mul_code" in - let mul_code := pose_mul_code CP mul_code in - Tag.update pkg TAG.mul_code mul_code. - - Ltac add_square_code pkg := - let CP := Tag.get pkg TAG.CP in - let square_code := fresh "square_code" in - let square_code := pose_square_code CP square_code in - Tag.update pkg TAG.square_code square_code. - - Ltac add_CurveParameters_package pkg := - let pkg := add_base pkg in - let pkg := add_sz pkg in - let pkg := add_bitwidth pkg in - let pkg := add_s pkg in - let pkg := add_c pkg in - let pkg := add_carry_chains pkg in - let pkg := add_a24 pkg in - let pkg := add_coef_div_modulus pkg in - let pkg := add_goldilocks pkg in - let pkg := add_karatsuba pkg in - let pkg := add_montgomery pkg in - let pkg := add_freeze pkg in - let pkg := add_ladderstep 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_tight pkg in - let pkg := add_upper_bound_of_exponent_loose pkg in - let pkg := add_modinv_fuel pkg in - let pkg := add_mul_code pkg in - let pkg := add_square_code pkg in - Tag.strip_subst_local pkg. -End CurveParameters. |