aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--_CoqProject1
-rw-r--r--src/Specific/Framework/CurveParameters.v412
-rw-r--r--src/Specific/Framework/CurveParametersPackage.v8
-rw-r--r--src/Specific/Framework/RawCurveParameters.v63
-rw-r--r--src/Specific/Framework/SynthesisFramework.v53
-rwxr-xr-xsrc/Specific/Framework/make_curve.py62
-rw-r--r--src/Specific/NISTP256/AMD128/CurveParameters.v44
-rw-r--r--src/Specific/NISTP256/AMD128/Synthesis.v6
-rw-r--r--src/Specific/NISTP256/AMD64/CurveParameters.v44
-rw-r--r--src/Specific/NISTP256/AMD64/Synthesis.v6
-rw-r--r--src/Specific/X2448/Karatsuba/C64/CurveParameters.v44
-rw-r--r--src/Specific/X2448/Karatsuba/C64/Synthesis.v6
-rw-r--r--src/Specific/X25519/C32/CurveParameters.v48
-rw-r--r--src/Specific/X25519/C32/Synthesis.v6
-rw-r--r--src/Specific/X25519/C64/CurveParameters.v48
-rw-r--r--src/Specific/X25519/C64/Synthesis.v6
-rw-r--r--src/Specific/X2555/C128/CurveParameters.v44
-rw-r--r--src/Specific/X2555/C128/Synthesis.v6
18 files changed, 501 insertions, 406 deletions
diff --git a/_CoqProject b/_CoqProject
index d36554986..e505f6bb5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -236,6 +236,7 @@ src/Specific/Framework/IntegrationTestTemporaryMiscCommon.v
src/Specific/Framework/MontgomeryReificationTypes.v
src/Specific/Framework/MontgomeryReificationTypesPackage.v
src/Specific/Framework/Packages.v
+src/Specific/Framework/RawCurveParameters.v
src/Specific/Framework/ReificationTypes.v
src/Specific/Framework/ReificationTypesPackage.v
src/Specific/Framework/SynthesisFramework.v
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 09:49:54 +0000