diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-15 22:12:34 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-10-18 23:01:29 -0400 |
| commit | a17f3ea44a09638f0d78428290a96ecce613ad65 (patch) | |
| tree | b6e955a57aeff83534d68b3ea0a87f47a1dec302 /src/Specific | |
| parent | 8f8bcf29a8c53d18eb24619703fa6c5f324382d9 (diff) | |
Explicitly specify base
This allows it to be something other than log2(m)/sz.
After | File Name | Before || Change
-------------------------------------------------------------------------------------------
8m20.82s | Total | 8m37.82s || -0m17.00s
-------------------------------------------------------------------------------------------
1m59.42s | Specific/NISTP256/AMD64/femul | 2m19.09s || -0m19.67s
3m28.66s | Specific/X25519/C64/ladderstep | 3m28.02s || +0m00.63s
0m24.97s | Specific/X25519/C64/femul | 0m24.60s || +0m00.36s
0m24.08s | Specific/NISTP256/AMD64/fesub | 0m23.48s || +0m00.59s
0m22.00s | Specific/NISTP256/AMD64/feadd | 0m21.34s || +0m00.66s
0m20.34s | Specific/X25519/C64/freeze | 0m19.76s || +0m00.57s
0m19.85s | Specific/X25519/C64/fesquare | 0m19.93s || -0m00.07s
0m18.04s | Specific/NISTP256/AMD64/feopp | 0m17.69s || +0m00.34s
0m15.10s | Specific/NISTP256/AMD64/fenz | 0m15.37s || -0m00.26s
0m08.31s | Specific/NISTP256/AMD64/Synthesis | 0m08.24s || +0m00.07s
0m05.96s | Specific/X25519/C64/Synthesis | 0m06.25s || -0m00.29s
0m02.10s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m02.14s || -0m00.04s
0m01.00s | Specific/Framework/SynthesisFramework | 0m01.03s || -0m00.03s
0m00.97s | Specific/Framework/ArithmeticSynthesis/Base | 0m01.02s || -0m00.05s
0m00.89s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.84s || +0m00.05s
0m00.80s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m00.81s || -0m00.01s
0m00.79s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.80s || -0m00.01s
0m00.76s | Specific/Framework/MontgomeryReificationTypesPackage | 0m00.75s || +0m00.01s
0m00.74s | Specific/Framework/ReificationTypesPackage | 0m00.77s || -0m00.03s
0m00.74s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m00.74s || +0m00.00s
0m00.73s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m00.70s || +0m00.03s
0m00.72s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.68s || +0m00.03s
0m00.70s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.72s || -0m00.02s
0m00.70s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.77s || -0m00.07s
0m00.69s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.70s || -0m00.01s
0m00.42s | Specific/X25519/C64/CurveParameters | 0m00.38s || +0m00.03s
0m00.36s | Specific/Framework/CurveParameters | 0m00.32s || +0m00.03s
0m00.33s | Specific/Framework/RawCurveParameters | 0m00.29s || +0m00.04s
0m00.33s | Specific/Framework/CurveParametersPackage | 0m00.30s || +0m00.03s
0m00.32s | Specific/NISTP256/AMD64/CurveParameters | 0m00.30s || +0m00.02s
Diffstat (limited to 'src/Specific')
304 files changed, 475 insertions, 122 deletions
diff --git a/src/Specific/Framework/ArithmeticSynthesis/Base.v b/src/Specific/Framework/ArithmeticSynthesis/Base.v index 2bf9719f0..541069d94 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/Base.v +++ b/src/Specific/Framework/ArithmeticSynthesis/Base.v @@ -1,5 +1,7 @@ Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. Require Import Coq.Lists.List. Import ListNotations. +Require Import Coq.micromega.Lia. +Require Import Coq.QArith.QArith_base. Require Import Crypto.Arithmetic.Core. Import B. Require Import Crypto.Specific.Framework.CurveParameters. Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics. @@ -30,15 +32,17 @@ Section wt. Local Coercion QArith_base.inject_Z : Z >-> Q. Local Coercion Z.of_nat : nat >-> Z. Local Coercion Z.pos : positive >-> Z. - Definition wt_gen (m : positive) (sz : nat) (i:nat) : Z := 2^Qceiling((Z.log2_up m/sz)*i). + Definition wt_gen (base : Q) (i:nat) : Z := 2^Qceiling(base*i). End wt. Section gen. - Context (m : positive) + Context (base : Q) + (m : positive) (sz : nat) - (coef_div_modulus : nat). + (coef_div_modulus : nat) + (base_pos : (1 <= base)%Q). - Local Notation wt := (wt_gen m sz). + Local Notation wt := (wt_gen base). Definition sz2' := ((sz * 2) - 1)%nat. @@ -50,69 +54,62 @@ Section gen. Lemma sz2'_nonzero (sz_nonzero : sz <> 0%nat) : sz2' <> 0%nat. - Proof. clear -sz_nonzero; cbv [sz2']; omega. Qed. + Proof using Type. clear -sz_nonzero; cbv [sz2']; omega. Qed. Local Ltac Q_cbv := - cbv [wt_gen Qround.Qceiling QArith_base.Qmult QArith_base.Qdiv QArith_base.inject_Z QArith_base.Qden QArith_base.Qnum QArith_base.Qopp Qround.Qfloor QArith_base.Qinv QArith_base.Qle Z.of_nat]. + cbv [wt_gen Qround.Qceiling QArith_base.Qmult QArith_base.Qdiv QArith_base.inject_Z QArith_base.Qden QArith_base.Qnum QArith_base.Qopp Qround.Qfloor QArith_base.Qinv QArith_base.Qle QArith_base.Qeq Z.of_nat] in *. Lemma wt_gen0_1 : wt 0 = 1. - Proof. + Proof using Type. Q_cbv; simpl. autorewrite with zsimplify_const; reflexivity. Qed. Lemma wt_gen_nonzero : forall i, wt i <> 0. - Proof. + Proof using base_pos. eapply pow_ceil_mul_nat_nonzero; [ omega | ]. - destruct sz; Q_cbv; - autorewrite with zsimplify_const; [ omega | ]. - apply Z.log2_up_nonneg. + destruct base; Q_cbv; lia. Qed. Lemma wt_gen_nonneg : forall i, 0 <= wt i. - Proof. apply pow_ceil_mul_nat_nonneg; omega. Qed. + Proof using Type. apply pow_ceil_mul_nat_nonneg; omega. Qed. Lemma wt_gen_pos : forall i, wt i > 0. - Proof. + Proof using base_pos. intro i; pose proof (wt_gen_nonzero i); pose proof (wt_gen_nonneg i). omega. Qed. Lemma wt_gen_multiples : forall i, wt (S i) mod (wt i) = 0. - Proof. - apply pow_ceil_mul_nat_multiples. - destruct sz; Q_cbv; autorewrite with zsimplify_const; - auto using Z.log2_up_nonneg, Z.le_refl. + Proof using base_pos. + apply pow_ceil_mul_nat_multiples; destruct base; Q_cbv; lia. Qed. Section divides. - Context (sz_nonzero : sz <> 0%nat) - (sz_small : Z.of_nat sz <= Z.log2_up (Z.pos m)). - Lemma wt_gen_divides : forall i, wt (S i) / wt i > 0. - Proof. + Proof using base_pos. apply pow_ceil_mul_nat_divide; [ omega | ]. - destruct sz; Q_cbv; autorewrite with zsimplify_const; [ congruence | ]. - rewrite Pos.mul_1_l; assumption. + destruct base; Q_cbv; lia. Qed. + Lemma wt_gen_divides' : forall i, wt (S i) / wt i <> 0. - Proof. + Proof using base_pos. symmetry; apply Z.lt_neq, Z.gt_lt_iff, wt_gen_divides; assumption. Qed. Lemma wt_gen_div_bound : forall i, wt (S i) / wt i <= wt 1. - Proof. + Proof using base_pos. intro; etransitivity. eapply pow_ceil_mul_nat_divide_upperbound; [ omega | ]. - all:destruct sz; Q_cbv; autorewrite with zsimplify_const; + all:destruct base; Q_cbv; autorewrite with zsimplify_const; rewrite ?Pos.mul_1_l, ?Pos.mul_1_r; try assumption; omega. Qed. Lemma wt_gen_divides_chain carry_chain : forall i (H:In i carry_chain), wt (S i) / wt i <> 0. - Proof. intros i ?; apply wt_gen_divides'; assumption. Qed. + Proof using base_pos. intros i ?; apply wt_gen_divides'; assumption. Qed. Lemma wt_gen_divides_chains carry_chains @@ -123,7 +120,7 @@ Section gen. (fun carry_chain => forall i (H:In i carry_chain), wt (S i) / wt i <> 0) carry_chains). - Proof. + Proof using base_pos. induction carry_chains as [|carry_chain carry_chains IHcarry_chains]; constructor; eauto using wt_gen_divides_chain. Qed. @@ -137,9 +134,8 @@ Section gen. end) (Positional.zeros sz) coef_div_modulus. Lemma coef_mod' - (sz_le_log2_m : Z.of_nat sz <= Z.log2_up (Z.pos m)) : mod_eq m (Positional.eval (n:=sz) wt coef') 0. - Proof. + Proof using base_pos. cbv [coef' m_enc']. remember (Positional.zeros sz) as v eqn:Hv. assert (Hv' : mod_eq m (Positional.eval wt v) 0) @@ -163,8 +159,8 @@ Section gen. Qed. End gen. -Ltac pose_wt m sz wt := - let v := (eval cbv [wt_gen] in (wt_gen m sz)) in +Ltac pose_wt base wt := + let v := (eval cbv [wt_gen] in (wt_gen base)) in cache_term v wt. Ltac pose_sz2 sz sz2 := @@ -193,24 +189,31 @@ Ltac pose_sz_le_log2_m sz m sz_le_log2_m := ltac:(vm_decide_no_check) sz_le_log2_m. +Ltac pose_base_pos base base_pos := + cache_proof_with_type_by + ((1 <= base)%Q) + ltac:(vm_decide_no_check) + base_pos. + Ltac pose_m_correct m s c m_correct := cache_proof_with_type_by (Z.pos m = s - Associational.eval c) ltac:(vm_decide_no_check) m_correct. -Ltac pose_m_enc sz m m_enc := - let v := (eval vm_compute in (m_enc' m sz)) in +Ltac pose_m_enc base m sz m_enc := + let v := (eval vm_compute in (m_enc' base m sz)) in let v := (eval compute in v) in (* compute away the type arguments *) cache_term v m_enc. -Ltac pose_coef sz m coef_div_modulus coef := (* subtraction coefficient *) - let v := (eval vm_compute in (coef' m sz coef_div_modulus)) in + +Ltac pose_coef base m sz coef_div_modulus coef := (* subtraction coefficient *) + let v := (eval vm_compute in (coef' base m sz coef_div_modulus)) in cache_term v coef. -Ltac pose_coef_mod sz wt m coef coef_div_modulus sz_le_log2_m coef_mod := +Ltac pose_coef_mod wt coef base m sz coef_div_modulus base_pos coef_mod := cache_proof_with_type_by (mod_eq m (Positional.eval (n:=sz) wt coef) 0) - ltac:(vm_cast_no_check (coef_mod' m sz coef_div_modulus sz_le_log2_m)) + ltac:(vm_cast_no_check (coef_mod' base m sz coef_div_modulus base_pos)) coef_mod. Ltac pose_sz_nonzero sz sz_nonzero := cache_proof_with_type_by @@ -238,6 +241,7 @@ Ltac pose_wt_divides' wt wt_divides wt_divides' := (forall i, wt (S i) / wt i <> 0) ltac:(apply wt_gen_divides'; vm_decide_no_check) wt_divides'. + Ltac pose_wt_divides_chains wt carry_chains wt_divides_chains := let T := (eval cbv [carry_chains List.fold_right List.map] in (List.fold_right @@ -249,7 +253,7 @@ Ltac pose_wt_divides_chains wt carry_chains wt_divides_chains := carry_chains))) in cache_proof_with_type_by T - ltac:(refine (@wt_gen_divides_chains _ _ _ _ carry_chains); vm_decide_no_check) + ltac:(refine (@wt_gen_divides_chains _ _ carry_chains); vm_decide_no_check) wt_divides_chains. Ltac pose_wt_pos wt wt_pos := diff --git a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v index d5b4e567c..80e032fb8 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v +++ b/src/Specific/Framework/ArithmeticSynthesis/BasePackage.v @@ -5,7 +5,7 @@ Require Import Crypto.Specific.Framework.Packages. Require Import Crypto.Util.TagList. Module TAG. - Inductive tags := r | m | wt | sz2 | half_sz | half_sz_nonzero | s_nonzero | sz_le_log2_m | m_correct | m_enc | coef | coef_mod | sz_nonzero | wt_nonzero | wt_nonneg | wt_divides | wt_divides' | wt_divides_chains | wt_pos | wt_multiples | c_small | m_enc_bounded | m_correct_wt. + Inductive tags := r | m | wt | sz2 | half_sz | half_sz_nonzero | s_nonzero | sz_le_log2_m | base_pos | m_correct | m_enc | coef | coef_mod | sz_nonzero | wt_nonzero | wt_nonneg | wt_divides | wt_divides' | wt_divides_chains | wt_pos | wt_multiples | c_small | m_enc_bounded | m_correct_wt. End TAG. Ltac add_r pkg := @@ -22,10 +22,9 @@ Ltac add_m pkg := Tag.update pkg TAG.m m. Ltac add_wt pkg := - let m := Tag.get pkg TAG.m in - let sz := Tag.get pkg TAG.sz in + let base := Tag.get pkg TAG.base in let wt := fresh "wt" in - let wt := pose_wt m sz wt in + let wt := pose_wt base wt in Tag.update pkg TAG.wt wt. Ltac add_sz2 pkg := @@ -59,6 +58,12 @@ Ltac add_sz_le_log2_m pkg := let sz_le_log2_m := pose_sz_le_log2_m sz m sz_le_log2_m in Tag.update pkg TAG.sz_le_log2_m sz_le_log2_m. +Ltac add_base_pos pkg := + let base := Tag.get pkg TAG.base in + let base_pos := fresh "base_pos" in + let base_pos := pose_base_pos base base_pos in + Tag.update pkg TAG.base_pos base_pos. + Ltac add_m_correct pkg := let m := Tag.get pkg TAG.m in let s := Tag.get pkg TAG.s in @@ -68,29 +73,32 @@ Ltac add_m_correct pkg := Tag.update pkg TAG.m_correct m_correct. Ltac add_m_enc pkg := - let sz := Tag.get pkg TAG.sz in + let base := Tag.get pkg TAG.base in let m := Tag.get pkg TAG.m in + let sz := Tag.get pkg TAG.sz in let m_enc := fresh "m_enc" in - let m_enc := pose_m_enc sz m m_enc in + let m_enc := pose_m_enc base m sz m_enc in Tag.update pkg TAG.m_enc m_enc. Ltac add_coef pkg := - let sz := Tag.get pkg TAG.sz in + let base := Tag.get pkg TAG.base in let m := Tag.get pkg TAG.m in + let sz := Tag.get pkg TAG.sz in let coef_div_modulus := Tag.get pkg TAG.coef_div_modulus in let coef := fresh "coef" in - let coef := pose_coef sz m coef_div_modulus coef in + let coef := pose_coef base m sz coef_div_modulus coef in Tag.update pkg TAG.coef coef. Ltac add_coef_mod pkg := - let sz := Tag.get pkg TAG.sz in let wt := Tag.get pkg TAG.wt in - let m := Tag.get pkg TAG.m in let coef := Tag.get pkg TAG.coef in + let base := Tag.get pkg TAG.base in + let m := Tag.get pkg TAG.m in + let sz := Tag.get pkg TAG.sz in let coef_div_modulus := Tag.get pkg TAG.coef_div_modulus in - let sz_le_log2_m := Tag.get pkg TAG.sz_le_log2_m in + let base_pos := Tag.get pkg TAG.base_pos in let coef_mod := fresh "coef_mod" in - let coef_mod := pose_coef_mod sz wt m coef coef_div_modulus sz_le_log2_m coef_mod in + let coef_mod := pose_coef_mod wt coef base m sz coef_div_modulus base_pos coef_mod in Tag.update pkg TAG.coef_mod coef_mod. Ltac add_sz_nonzero pkg := @@ -177,6 +185,7 @@ Ltac add_Base_package pkg := let pkg := add_half_sz_nonzero pkg in let pkg := add_s_nonzero pkg in let pkg := add_sz_le_log2_m pkg in + let pkg := add_base_pos pkg in let pkg := add_m_correct pkg in let pkg := add_m_enc pkg in let pkg := add_coef pkg in @@ -214,6 +223,8 @@ Module MakeBasePackage (PKG : PrePackage). Notation s_nonzero := (ltac:(let v := get_s_nonzero () in exact v)) (only parsing). Ltac get_sz_le_log2_m _ := get TAG.sz_le_log2_m. Notation sz_le_log2_m := (ltac:(let v := get_sz_le_log2_m () in exact v)) (only parsing). + Ltac get_base_pos _ := get TAG.base_pos. + Notation base_pos := (ltac:(let v := get_base_pos () in exact v)) (only parsing). Ltac get_m_correct _ := get TAG.m_correct. Notation m_correct := (ltac:(let v := get_m_correct () in exact v)) (only parsing). Ltac get_m_enc _ := get TAG.m_enc. diff --git a/src/Specific/Framework/ArithmeticSynthesis/Defaults.v b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v index 42c49f46d..36e02bb0e 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/Defaults.v +++ b/src/Specific/Framework/ArithmeticSynthesis/Defaults.v @@ -1,4 +1,5 @@ Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. +Require Import Coq.QArith.QArith_base. Require Import Coq.Lists.List. Import ListNotations. Require Import Crypto.Arithmetic.CoreUnfolder. Require Import Crypto.Arithmetic.Core. Import B. @@ -38,8 +39,8 @@ Local Ltac solve_constant_local_sig := | [ |- { c : Z^?sz | Positional.Fdecode (m:=?M) ?wt c = ?v } ] => (exists (Positional.encode (n:=sz) (modulo:=modulo) (div:=div) wt (F.to_Z (m:=M) v))); lazymatch goal with - | [ sz_nonzero : sz <> 0%nat, sz_le_log2_m : Z.of_nat sz <= Z.log2_up (Z.pos M) |- _ ] - => clear -sz_nonzero sz_le_log2_m + | [ sz_nonzero : sz <> 0%nat, base_pos : (1 <= _)%Q |- _ ] + => clear -base_pos sz_nonzero end end; abstract ( @@ -50,6 +51,7 @@ Local Ltac solve_constant_local_sig := Section gen. Context (m : positive) + (base : Q) (sz : nat) (s : Z) (c : list limb) @@ -59,12 +61,13 @@ Section gen. (square_code : option (Z^sz -> Z^sz)) (sz_nonzero : sz <> 0%nat) (s_nonzero : s <> 0) + (base_pos : (1 <= base)%Q) (sz_le_log2_m : Z.of_nat sz <= Z.log2_up (Z.pos m)). - Local Notation wt := (wt_gen m sz). + Local Notation wt := (wt_gen base). Local Notation sz2 := (sz2' sz). - Local Notation wt_divides' := (wt_gen_divides' m sz sz_nonzero sz_le_log2_m). - Local Notation wt_nonzero := (wt_gen_nonzero m sz). + Local Notation wt_divides' := (wt_gen_divides' base base_pos). + Local Notation wt_nonzero := (wt_gen_nonzero base base_pos). (* side condition needs cbv [Positional.mul_cps Positional.reduce_cps]. *) Context (mul_code_correct @@ -99,9 +102,9 @@ Section gen. Proof. let a := fresh "a" in eexists; cbv beta zeta; intros a. - pose proof (wt_gen0_1 m sz). + pose proof (wt_gen0_1 base). pose proof wt_nonzero; pose proof div_mod. - pose proof (wt_gen_divides_chains m sz sz_nonzero sz_le_log2_m carry_chains). + pose proof (wt_gen_divides_chains base base_pos carry_chains). pose proof wt_divides'. let x := constr:(chained_carries' sz wt s c a carry_chains) in presolve_op_F constr:(wt) x; @@ -148,7 +151,7 @@ Section gen. Proof. eexists; cbv beta zeta; intros a b. pose proof wt_nonzero. - pose proof (wt_gen0_1 m sz). + pose proof (wt_gen0_1 base). let x := constr:( Positional.add_cps (n := sz) wt a b id) in presolve_op_F constr:(wt) x; @@ -166,7 +169,7 @@ Section gen. let b := fresh "b" in eexists; cbv beta zeta; intros a b. pose proof wt_nonzero. - pose proof (wt_gen0_1 m sz). + pose proof (wt_gen0_1 base). let x := constr:( Positional.sub_cps (n:=sz) (coef := coef) wt a b id) in presolve_op_F constr:(wt) x; @@ -182,7 +185,7 @@ Section gen. Proof. eexists; cbv beta zeta; intros a. pose proof wt_nonzero. - pose proof (wt_gen0_1 m sz). + pose proof (wt_gen0_1 base). let x := constr:( Positional.opp_cps (n:=sz) (coef := coef) wt a id) in presolve_op_F constr:(wt) x; @@ -198,7 +201,7 @@ Section gen. Proof. eexists; cbv beta zeta; intros a b. pose proof wt_nonzero. - pose proof (wt_gen0_1 m sz). + pose proof (wt_gen0_1 base). pose proof (sz2'_nonzero sz sz_nonzero). let x := constr:( Positional.mul_cps (n:=sz) (m:=sz2) wt a b @@ -224,7 +227,7 @@ Section gen. Proof. eexists; cbv beta zeta; intros a. pose proof wt_nonzero. - pose proof (wt_gen0_1 m sz). + pose proof (wt_gen0_1 base). pose proof (sz2'_nonzero sz sz_nonzero). let x := constr:( Positional.mul_cps (n:=sz) (m:=sz2) wt a a @@ -263,7 +266,7 @@ Section gen. (Positional.Fdecode_Fencode_id (sz_nonzero := sz_nonzero) (div_mod := div_mod) - wt (wt_gen0_1 m sz) wt_nonzero wt_divides') + wt (wt_gen0_1 base) wt_nonzero wt_divides') (Positional.eq_Feq_iff wt) _ _ _); lazymatch goal with @@ -324,25 +327,25 @@ Ltac cache_sig_with_type_by_existing_sig ty existing_sig id := ltac:(fun _ => cbv [carry_sig' constant_sig' zero_sig' one_sig' add_sig' sub_sig' mul_sig' square_sig' opp_sig']) ty existing_sig id. -Ltac pose_carry_sig sz m wt s c carry_chains carry_sig := +Ltac pose_carry_sig wt m base sz s c carry_chains carry_sig := cache_sig_with_type_by_existing_sig {carry : (Z^sz -> Z^sz)%type | forall a : Z^sz, let eval := Positional.Fdecode (m := m) wt in eval (carry a) = eval a} - (carry_sig' m sz s c carry_chains) + (carry_sig' m base sz s c carry_chains) carry_sig. -Ltac pose_zero_sig sz m wt sz_nonzero sz_le_log2_m zero_sig := +Ltac pose_zero_sig wt m base sz sz_nonzero base_pos zero_sig := cache_vm_sig_with_type { zero : Z^sz | Positional.Fdecode (m:=m) wt zero = 0%F} - (zero_sig' m sz sz_nonzero sz_le_log2_m) + (zero_sig' m base sz sz_nonzero base_pos) zero_sig. -Ltac pose_one_sig sz m wt sz_nonzero sz_le_log2_m one_sig := +Ltac pose_one_sig wt m base sz sz_nonzero base_pos one_sig := cache_vm_sig_with_type { one : Z^sz | Positional.Fdecode (m:=m) wt one = 1%F} - (one_sig' m sz sz_nonzero sz_le_log2_m) + (one_sig' m base sz sz_nonzero base_pos) one_sig. Ltac pose_a24_sig sz m wt a24 a24_sig := @@ -351,49 +354,49 @@ Ltac pose_a24_sig sz m wt a24 a24_sig := solve_constant_sig a24_sig. -Ltac pose_add_sig sz m wt sz_nonzero add_sig := +Ltac pose_add_sig wt m base sz add_sig := cache_sig_with_type_by_existing_sig { add : (Z^sz -> Z^sz -> Z^sz)%type | forall a b : Z^sz, let eval := Positional.Fdecode (m:=m) wt in eval (add a b) = (eval a + eval b)%F } - (add_sig' m sz sz_nonzero) + (add_sig' m base sz) add_sig. -Ltac pose_sub_sig sz m wt coef sub_sig := +Ltac pose_sub_sig wt m base sz coef sub_sig := cache_sig_with_type_by_existing_sig {sub : (Z^sz -> Z^sz -> Z^sz)%type | forall a b : Z^sz, let eval := Positional.Fdecode (m:=m) wt in eval (sub a b) = (eval a - eval b)%F} - (sub_sig' m sz coef) + (sub_sig' m base sz coef) sub_sig. -Ltac pose_opp_sig sz m wt coef opp_sig := +Ltac pose_opp_sig wt m base sz coef opp_sig := cache_sig_with_type_by_existing_sig {opp : (Z^sz -> Z^sz)%type | forall a : Z^sz, let eval := Positional.Fdecode (m := m) wt in eval (opp a) = F.opp (eval a)} - (opp_sig' m sz coef) + (opp_sig' m base sz coef) opp_sig. -Ltac pose_mul_sig sz m wt s c mul_code sz_nonzero s_nonzero mul_code_correct mul_sig := +Ltac pose_mul_sig wt m base sz s c mul_code sz_nonzero s_nonzero base_pos mul_code_correct mul_sig := cache_sig_with_type_by_existing_sig {mul : (Z^sz -> Z^sz -> Z^sz)%type | forall a b : Z^sz, let eval := Positional.Fdecode (m := m) wt in eval (mul a b) = (eval a * eval b)%F} - (mul_sig' m sz s c mul_code sz_nonzero s_nonzero mul_code_correct) + (mul_sig' m base sz s c mul_code sz_nonzero s_nonzero base_pos mul_code_correct) mul_sig. -Ltac pose_square_sig sz m wt s c square_code sz_nonzero s_nonzero square_code_correct square_sig := +Ltac pose_square_sig wt m base sz s c square_code sz_nonzero s_nonzero base_pos square_code_correct square_sig := cache_sig_with_type_by_existing_sig {square : (Z^sz -> Z^sz)%type | forall a : Z^sz, let eval := Positional.Fdecode (m := m) wt in eval (square a) = (eval a * eval a)%F} - (square_sig' m sz s c square_code sz_nonzero s_nonzero square_code_correct) + (square_sig' m base sz s c square_code sz_nonzero s_nonzero base_pos square_code_correct) square_sig. Ltac pose_ring sz m wt wt_divides' sz_nonzero wt_nonzero zero_sig one_sig opp_sig add_sig sub_sig mul_sig ring := diff --git a/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v b/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v index 4a037f34a..10d6e42ed 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v +++ b/src/Specific/Framework/ArithmeticSynthesis/DefaultsPackage.v @@ -39,38 +39,41 @@ Ltac add_carry_sig pkg := Tag.update_by_tac_if_not_exists pkg TAG.carry_sig - ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + ltac:(fun _ => let wt := Tag.get pkg TAG.wt in let m := Tag.get pkg TAG.m in - let wt := Tag.get pkg TAG.wt in + let base := Tag.get pkg TAG.base in + let sz := Tag.get pkg TAG.sz in let s := Tag.get pkg TAG.s in let c := Tag.get pkg TAG.c in let carry_chains := Tag.get pkg TAG.carry_chains in let carry_sig := fresh "carry_sig" in - let carry_sig := pose_carry_sig sz m wt s c carry_chains carry_sig in + let carry_sig := pose_carry_sig wt m base sz s c carry_chains carry_sig in constr:(carry_sig)). Ltac add_zero_sig pkg := Tag.update_by_tac_if_not_exists pkg TAG.zero_sig - ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + ltac:(fun _ => let wt := Tag.get pkg TAG.wt in let m := Tag.get pkg TAG.m in - let wt := Tag.get pkg TAG.wt in + let base := Tag.get pkg TAG.base in + let sz := Tag.get pkg TAG.sz in let sz_nonzero := Tag.get pkg TAG.sz_nonzero in - let sz_le_log2_m := Tag.get pkg TAG.sz_le_log2_m in + let base_pos := Tag.get pkg TAG.base_pos in let zero_sig := fresh "zero_sig" in - let zero_sig := pose_zero_sig sz m wt sz_nonzero sz_le_log2_m zero_sig in + let zero_sig := pose_zero_sig wt m base sz sz_nonzero base_pos zero_sig in constr:(zero_sig)). Ltac add_one_sig pkg := Tag.update_by_tac_if_not_exists pkg TAG.one_sig - ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + ltac:(fun _ => let wt := Tag.get pkg TAG.wt in let m := Tag.get pkg TAG.m in - let wt := Tag.get pkg TAG.wt in + let base := Tag.get pkg TAG.base in + let sz := Tag.get pkg TAG.sz in let sz_nonzero := Tag.get pkg TAG.sz_nonzero in - let sz_le_log2_m := Tag.get pkg TAG.sz_le_log2_m in + let base_pos := Tag.get pkg TAG.base_pos in let one_sig := fresh "one_sig" in - let one_sig := pose_one_sig sz m wt sz_nonzero sz_le_log2_m one_sig in + let one_sig := pose_one_sig wt m base sz sz_nonzero base_pos one_sig in constr:(one_sig)). Ltac add_a24_sig pkg := Tag.update_by_tac_if_not_exists @@ -87,66 +90,72 @@ Ltac add_add_sig pkg := Tag.update_by_tac_if_not_exists pkg TAG.add_sig - ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + ltac:(fun _ => let wt := Tag.get pkg TAG.wt in let m := Tag.get pkg TAG.m in - let wt := Tag.get pkg TAG.wt in - let sz_nonzero := Tag.get pkg TAG.sz_nonzero in + let base := Tag.get pkg TAG.base in + let sz := Tag.get pkg TAG.sz in let add_sig := fresh "add_sig" in - let add_sig := pose_add_sig sz m wt sz_nonzero add_sig in + let add_sig := pose_add_sig wt m base sz add_sig in constr:(add_sig)). Ltac add_sub_sig pkg := Tag.update_by_tac_if_not_exists pkg TAG.sub_sig - ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + ltac:(fun _ => let wt := Tag.get pkg TAG.wt in let m := Tag.get pkg TAG.m in - let wt := Tag.get pkg TAG.wt in + let base := Tag.get pkg TAG.base in + let sz := Tag.get pkg TAG.sz in let coef := Tag.get pkg TAG.coef in let sub_sig := fresh "sub_sig" in - let sub_sig := pose_sub_sig sz m wt coef sub_sig in + let sub_sig := pose_sub_sig wt m base sz coef sub_sig in constr:(sub_sig)). Ltac add_opp_sig pkg := Tag.update_by_tac_if_not_exists pkg TAG.opp_sig - ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + ltac:(fun _ => let wt := Tag.get pkg TAG.wt in let m := Tag.get pkg TAG.m in - let wt := Tag.get pkg TAG.wt in + let base := Tag.get pkg TAG.base in + let sz := Tag.get pkg TAG.sz in let coef := Tag.get pkg TAG.coef in let opp_sig := fresh "opp_sig" in - let opp_sig := pose_opp_sig sz m wt coef opp_sig in + let opp_sig := pose_opp_sig wt m base sz coef opp_sig in constr:(opp_sig)). Ltac add_mul_sig pkg := Tag.update_by_tac_if_not_exists pkg TAG.mul_sig - ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + ltac:(fun _ => let wt := Tag.get pkg TAG.wt in let m := Tag.get pkg TAG.m in - let wt := Tag.get pkg TAG.wt in + let base := Tag.get pkg TAG.base in + let sz := Tag.get pkg TAG.sz in let s := Tag.get pkg TAG.s in let c := Tag.get pkg TAG.c in let mul_code := Tag.get pkg TAG.mul_code in let sz_nonzero := Tag.get pkg TAG.sz_nonzero in let s_nonzero := Tag.get pkg TAG.s_nonzero in + let base_pos := Tag.get pkg TAG.base_pos in let mul_code_correct := Tag.get pkg TAG.mul_code_correct in let mul_sig := fresh "mul_sig" in - let mul_sig := pose_mul_sig sz m wt s c mul_code sz_nonzero s_nonzero mul_code_correct mul_sig in + let mul_sig := pose_mul_sig wt m base sz s c mul_code sz_nonzero s_nonzero base_pos mul_code_correct mul_sig in constr:(mul_sig)). Ltac add_square_sig pkg := Tag.update_by_tac_if_not_exists pkg TAG.square_sig - ltac:(fun _ => let sz := Tag.get pkg TAG.sz in + ltac:(fun _ => let wt := Tag.get pkg TAG.wt in let m := Tag.get pkg TAG.m in - let wt := Tag.get pkg TAG.wt in + let base := Tag.get pkg TAG.base in + let sz := Tag.get pkg TAG.sz in let s := Tag.get pkg TAG.s in let c := Tag.get pkg TAG.c in let square_code := Tag.get pkg TAG.square_code in let sz_nonzero := Tag.get pkg TAG.sz_nonzero in let s_nonzero := Tag.get pkg TAG.s_nonzero in + let base_pos := Tag.get pkg TAG.base_pos in let square_code_correct := Tag.get pkg TAG.square_code_correct in let square_sig := fresh "square_sig" in - let square_sig := pose_square_sig sz m wt s c square_code sz_nonzero s_nonzero square_code_correct square_sig in + let square_sig := pose_square_sig wt m base sz s c square_code sz_nonzero s_nonzero base_pos square_code_correct square_sig in constr:(square_sig)). Ltac add_ring pkg := Tag.update_by_tac_if_not_exists diff --git a/src/Specific/Framework/ArithmeticSynthesis/Freeze.v b/src/Specific/Framework/ArithmeticSynthesis/Freeze.v index a32f9e220..44d284d8e 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/Freeze.v +++ b/src/Specific/Framework/ArithmeticSynthesis/Freeze.v @@ -1,4 +1,5 @@ Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef. +Require Import Coq.QArith.QArith_base. Require Import Coq.Lists.List. Import ListNotations. Require Import Crypto.Arithmetic.CoreUnfolder. Require Import Crypto.Arithmetic.Saturated.CoreUnfolder. @@ -26,17 +27,18 @@ Ltac freeze_preunfold := Section gen. Context (m : positive) + (base : Q) (sz : nat) (c : list limb) (bitwidth : Z) (m_enc : Z^sz) - (sz_nonzero : sz <> 0%nat) - (sz_le_log2_m : Z.of_nat sz <= Z.log2_up (Z.pos m)). + (base_pos : (1 <= base)%Q) + (sz_nonzero : sz <> 0%nat). - Local Notation wt := (wt_gen m sz). + Local Notation wt := (wt_gen base). Local Notation sz2 := (sz2' sz). - Local Notation wt_divides' := (wt_gen_divides' m sz sz_nonzero sz_le_log2_m). - Local Notation wt_nonzero := (wt_gen_nonzero m sz). + Local Notation wt_divides' := (wt_gen_divides' base base_pos). + Local Notation wt_nonzero := (wt_gen_nonzero base base_pos). Context (c_small : 0 < Associational.eval c < wt sz) (m_enc_bounded : Tuple.map (BinInt.Z.land (Z.ones bitwidth)) m_enc = m_enc) @@ -51,12 +53,11 @@ Section gen. eval (freeze a) = eval a }. Proof. eexists; cbv beta zeta; (intros a ?). - pose proof wt_nonzero; pose proof (wt_gen_pos m sz). - pose proof (wt_gen0_1 m sz). - pose proof div_mod; pose proof (wt_gen_divides m sz sz_nonzero sz_le_log2_m). - pose proof (wt_gen_multiples m sz). + pose proof wt_nonzero; pose proof (wt_gen_pos base base_pos). + pose proof (wt_gen0_1 base). + pose proof div_mod; pose proof (wt_gen_divides base base_pos). + pose proof (wt_gen_multiples base base_pos). pose proof div_correct; pose proof modulo_correct. - pose proof (wt_gen_divides_chain m sz sz_nonzero sz_le_log2_m). let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in presolve_op_F constr:(wt) x; [ autorewrite with pattern_runtime; reflexivity | ]. @@ -65,7 +66,7 @@ Section gen. Defined. End gen. -Ltac pose_freeze_sig wt m sz c bitwidth m_enc sz_nonzero sz_le_log2_m freeze_sig := +Ltac pose_freeze_sig wt m base sz c bitwidth m_enc base_pos sz_nonzero freeze_sig := cache_sig_with_type_by_existing_sig_helper ltac:(fun _ => cbv [freeze_sig']) {freeze : (Z^sz -> Z^sz)%type | @@ -73,5 +74,5 @@ Ltac pose_freeze_sig wt m sz c bitwidth m_enc sz_nonzero sz_le_log2_m freeze_sig (0 <= Positional.eval wt a < 2 * Z.pos m)-> let eval := Positional.Fdecode (m := m) wt in eval (freeze a) = eval a} - (freeze_sig' m sz c bitwidth m_enc sz_nonzero sz_le_log2_m) + (freeze_sig' m base sz c bitwidth m_enc base_pos sz_nonzero) freeze_sig. diff --git a/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v index 885bfde09..1a4b405b6 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v +++ b/src/Specific/Framework/ArithmeticSynthesis/FreezePackage.v @@ -15,14 +15,15 @@ Ltac add_freeze_sig pkg := TAG.freeze_sig ltac:(fun _ => let wt := Tag.get pkg TAG.wt in let m := Tag.get pkg TAG.m in + let base := Tag.get pkg TAG.base in let sz := Tag.get pkg TAG.sz in let c := Tag.get pkg TAG.c in let bitwidth := Tag.get pkg TAG.bitwidth in let m_enc := Tag.get pkg TAG.m_enc in + let base_pos := Tag.get pkg TAG.base_pos in let sz_nonzero := Tag.get pkg TAG.sz_nonzero in - let sz_le_log2_m := Tag.get pkg TAG.sz_le_log2_m in let freeze_sig := fresh "freeze_sig" in - let freeze_sig := pose_freeze_sig wt m sz c bitwidth m_enc sz_nonzero sz_le_log2_m freeze_sig in + let freeze_sig := pose_freeze_sig wt m base sz c bitwidth m_enc base_pos sz_nonzero freeze_sig in constr:(freeze_sig)). Ltac add_Freeze_package pkg := let pkg := add_freeze_sig pkg in diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v index 8911dccfc..f8d245a67 100644 --- a/src/Specific/Framework/CurveParameters.v +++ b/src/Specific/Framework/CurveParameters.v @@ -11,7 +11,7 @@ Local Set Primitive Projections. Module Export Notations := RawCurveParameters.Notations. 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 | mul_code | square_code. + Inductive tags := CP | sz | base | bitwidth | s | c | carry_chains | a24 | coef_div_modulus | goldilocks | montgomery | upper_bound_of_exponent | allowable_bit_widths | freeze_allowable_bit_widths | modinv_fuel | mul_code | square_code. End TAG. Module Export CurveParameters. @@ -32,6 +32,7 @@ Module Export CurveParameters. Record CurveParameters := { sz : nat; + base : Q; bitwidth : Z; s : Z; c : list limb; @@ -52,6 +53,7 @@ Module Export CurveParameters. Declare Reduction cbv_CurveParameters := cbv [sz + base bitwidth s c @@ -90,6 +92,7 @@ Module Export 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 s := RawCurveParameters.s CP in @@ -109,6 +112,7 @@ Module Export CurveParameters. {| sz := sz; + base := base; bitwidth := bitwidth; s := s; c := c; @@ -146,6 +150,7 @@ Module Export CurveParameters. lazymatch v with | ({| sz := ?sz'; + base := ?base'; bitwidth := ?bitwidth'; s := ?s'; c := ?c'; @@ -162,6 +167,7 @@ Module Export CurveParameters. 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 @@ -171,6 +177,7 @@ Module Export CurveParameters. let modinv_fuel' := do_compute modinv_fuel' in constr:({| sz := sz'; + base := base'; bitwidth := bitwidth'; s := s'; c := c'; @@ -194,6 +201,8 @@ Module Export CurveParameters. 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 := @@ -226,6 +235,12 @@ Module Export CurveParameters. 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 @@ -317,6 +332,7 @@ Module Export CurveParameters. 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 diff --git a/src/Specific/Framework/CurveParametersPackage.v b/src/Specific/Framework/CurveParametersPackage.v index 75ef1f7e7..458c1d4ea 100644 --- a/src/Specific/Framework/CurveParametersPackage.v +++ b/src/Specific/Framework/CurveParametersPackage.v @@ -23,6 +23,8 @@ Ltac if_montgomery pkg tac_true tac_false arg := Module MakeCurveParametersPackage (PKG : PrePackage). Module Import MakeCurveParametersPackageInternal := MakePackageBase PKG. + Ltac get_base _ := get TAG.base. + Notation base := (ltac:(let v := get_base () in exact v)) (only parsing). Ltac get_sz _ := get TAG.sz. Notation sz := (ltac:(let v := get_sz () in exact v)) (only parsing). Ltac get_bitwidth _ := get TAG.bitwidth. diff --git a/src/Specific/Framework/RawCurveParameters.v b/src/Specific/Framework/RawCurveParameters.v index 8adff1f69..b84089eaf 100644 --- a/src/Specific/Framework/RawCurveParameters.v +++ b/src/Specific/Framework/RawCurveParameters.v @@ -1,9 +1,12 @@ +Require Export Coq.QArith.QArith_base. Require Export Coq.ZArith.BinInt. Require Export Coq.Lists.List. Require Export Crypto.Util.ZUtil.Notations. Require Crypto.Util.Tuple. Local Set Primitive Projections. +Coercion QArith_base.inject_Z : Z >-> Q. +Coercion Z.of_nat : nat >-> Z. Module Export Notations. (* import/export tracking *) Export ListNotations. @@ -18,6 +21,7 @@ End Notations. Record CurveParameters := { sz : nat; + base : Q; bitwidth : Z; s : Z; c : list limb; @@ -42,6 +46,7 @@ Record CurveParameters := Declare Reduction cbv_RawCurveParameters := cbv [sz + base bitwidth s c diff --git a/src/Specific/Framework/make_curve.py b/src/Specific/Framework/make_curve.py index 70b88069d..516b67868 100755 --- a/src/Specific/Framework/make_curve.py +++ b/src/Specific/Framework/make_curve.py @@ -1,6 +1,7 @@ #!/usr/bin/env python from __future__ import with_statement import json, sys, os, math, re, shutil, io +from fractions import Fraction def compute_bitwidth(base): return 2**int(math.ceil(math.log(base, 2))) @@ -11,6 +12,10 @@ def default_carry_chains(sz): 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) +def reformat_base(base): + if '.' not in base: return base + int_part, frac_part = base.split('.') + return int_part + ' + ' + str(Fraction('.' + frac_part)) def compute_c(modulus_str): base, exp, rest = re.match(r'\s*'.join(('^', '(2)', r'\^', '([0-9]+)', r'([0-9\^ +\*-]*)$')), modulus_str).groups() if rest.strip() == '': return [] @@ -193,6 +198,7 @@ def make_curve_parameters(parameters): assert(all(ch in '0123456789^+- ' for ch in parameters['modulus'])) modulus = eval(parameters['modulus'].replace('^', '**')) base = float(parameters['base']) + replacements['reformatted_base'] = reformat_base(parameters['base']) replacements['bitwidth'] = parameters.get('bitwidth', str(compute_bitwidth(base))) bitwidth = int(replacements['bitwidth']) replacements['sz'] = parameters.get('sz', str(compute_sz(modulus, base))) @@ -242,6 +248,7 @@ Base: %(base)s Definition curve : CurveParameters := {| sz := %(sz)s%%nat; + base := %(reformatted_base)s; bitwidth := %(bitwidth)s; s := %(s)s; c := %(c)s; diff --git a/src/Specific/NISTP256/AMD128/CurveParameters.v b/src/Specific/NISTP256/AMD128/CurveParameters.v index 56d452941..09716c9f9 100644 --- a/src/Specific/NISTP256/AMD128/CurveParameters.v +++ b/src/Specific/NISTP256/AMD128/CurveParameters.v @@ -9,6 +9,7 @@ Base: 128 Definition curve : CurveParameters := {| sz := 2%nat; + base := 128; bitwidth := 128; s := 2^256; c := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]; diff --git a/src/Specific/NISTP256/AMD64/CurveParameters.v b/src/Specific/NISTP256/AMD64/CurveParameters.v index e90ffe113..f51ae2d4a 100644 --- a/src/Specific/NISTP256/AMD64/CurveParameters.v +++ b/src/Specific/NISTP256/AMD64/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 4%nat; + base := 64; bitwidth := 64; s := 2^256; c := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]; diff --git a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v index 7302294b8..3ba857263 100644 --- a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v +++ b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v @@ -9,6 +9,7 @@ Base: 56 Definition curve : CurveParameters := {| sz := 8%nat; + base := 56; bitwidth := 64; s := 2^448; c := [(1, 1); (2^224, 1)]; diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v index f112bc2ac..b921edf2c 100644 --- a/src/Specific/X25519/C32/CurveParameters.v +++ b/src/Specific/X25519/C32/CurveParameters.v @@ -9,6 +9,7 @@ Base: 25.5 Definition curve : CurveParameters := {| sz := 10%nat; + base := 25 + 1/2; bitwidth := 32; s := 2^255; c := [(1, 19)]; diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v index 0a727968f..1bcc5a633 100644 --- a/src/Specific/X25519/C64/CurveParameters.v +++ b/src/Specific/X25519/C64/CurveParameters.v @@ -9,6 +9,7 @@ Base: 51 Definition curve : CurveParameters := {| sz := 5%nat; + base := 51; bitwidth := 64; s := 2^255; c := [(1, 19)]; diff --git a/src/Specific/X2555/C128/CurveParameters.v b/src/Specific/X2555/C128/CurveParameters.v index f3ae4511b..6b00917ce 100644 --- a/src/Specific/X2555/C128/CurveParameters.v +++ b/src/Specific/X2555/C128/CurveParameters.v @@ -9,6 +9,7 @@ Base: 130 Definition curve : CurveParameters := {| sz := 3%nat; + base := 130; bitwidth := 128; s := 2^255; c := [(1, 5)]; diff --git a/src/Specific/montgomery32_2e127m1/CurveParameters.v b/src/Specific/montgomery32_2e127m1/CurveParameters.v index 7271e7450..6136ed227 100644 --- a/src/Specific/montgomery32_2e127m1/CurveParameters.v +++ b/src/Specific/montgomery32_2e127m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 3%nat; + base := 32; bitwidth := 32; s := 2^127; c := [(1, 1)]; diff --git a/src/Specific/montgomery32_2e129m25/CurveParameters.v b/src/Specific/montgomery32_2e129m25/CurveParameters.v index f2b9c9a3a..e0264fe37 100644 --- a/src/Specific/montgomery32_2e129m25/CurveParameters.v +++ b/src/Specific/montgomery32_2e129m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 4%nat; + base := 32; bitwidth := 32; s := 2^129; c := [(1, 25)]; diff --git a/src/Specific/montgomery32_2e130m5/CurveParameters.v b/src/Specific/montgomery32_2e130m5/CurveParameters.v index ed897050d..ceb6b7a5f 100644 --- a/src/Specific/montgomery32_2e130m5/CurveParameters.v +++ b/src/Specific/montgomery32_2e130m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 4%nat; + base := 32; bitwidth := 32; s := 2^130; c := [(1, 5)]; diff --git a/src/Specific/montgomery32_2e137m13/CurveParameters.v b/src/Specific/montgomery32_2e137m13/CurveParameters.v index c62b2000a..31d502cba 100644 --- a/src/Specific/montgomery32_2e137m13/CurveParameters.v +++ b/src/Specific/montgomery32_2e137m13/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 4%nat; + base := 32; bitwidth := 32; s := 2^137; c := [(1, 13)]; diff --git a/src/Specific/montgomery32_2e140m27/CurveParameters.v b/src/Specific/montgomery32_2e140m27/CurveParameters.v index 1d68c4a9d..8d7400d1d 100644 --- a/src/Specific/montgomery32_2e140m27/CurveParameters.v +++ b/src/Specific/montgomery32_2e140m27/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 4%nat; + base := 32; bitwidth := 32; s := 2^140; c := [(1, 27)]; diff --git a/src/Specific/montgomery32_2e141m9/CurveParameters.v b/src/Specific/montgomery32_2e141m9/CurveParameters.v index fc7caae4a..7aba5803b 100644 --- a/src/Specific/montgomery32_2e141m9/CurveParameters.v +++ b/src/Specific/montgomery32_2e141m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 4%nat; + base := 32; bitwidth := 32; s := 2^141; c := [(1, 9)]; diff --git a/src/Specific/montgomery32_2e150m3/CurveParameters.v b/src/Specific/montgomery32_2e150m3/CurveParameters.v index 451ede6b0..df1bd424f 100644 --- a/src/Specific/montgomery32_2e150m3/CurveParameters.v +++ b/src/Specific/montgomery32_2e150m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 4%nat; + base := 32; bitwidth := 32; s := 2^150; c := [(1, 3)]; diff --git a/src/Specific/montgomery32_2e150m5/CurveParameters.v b/src/Specific/montgomery32_2e150m5/CurveParameters.v index 769ffc313..12c8f87a4 100644 --- a/src/Specific/montgomery32_2e150m5/CurveParameters.v +++ b/src/Specific/montgomery32_2e150m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 4%nat; + base := 32; bitwidth := 32; s := 2^150; c := [(1, 5)]; diff --git a/src/Specific/montgomery32_2e152m17/CurveParameters.v b/src/Specific/montgomery32_2e152m17/CurveParameters.v index 181ebf561..a0c5cf694 100644 --- a/src/Specific/montgomery32_2e152m17/CurveParameters.v +++ b/src/Specific/montgomery32_2e152m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 4%nat; + base := 32; bitwidth := 32; s := 2^152; c := [(1, 17)]; diff --git a/src/Specific/montgomery32_2e158m15/CurveParameters.v b/src/Specific/montgomery32_2e158m15/CurveParameters.v index fdae2b541..0f5113951 100644 --- a/src/Specific/montgomery32_2e158m15/CurveParameters.v +++ b/src/Specific/montgomery32_2e158m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 4%nat; + base := 32; bitwidth := 32; s := 2^158; c := [(1, 15)]; diff --git a/src/Specific/montgomery32_2e165m25/CurveParameters.v b/src/Specific/montgomery32_2e165m25/CurveParameters.v index bee8e76a5..7025f5e42 100644 --- a/src/Specific/montgomery32_2e165m25/CurveParameters.v +++ b/src/Specific/montgomery32_2e165m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 5%nat; + base := 32; bitwidth := 32; s := 2^165; c := [(1, 25)]; diff --git a/src/Specific/montgomery32_2e166m5/CurveParameters.v b/src/Specific/montgomery32_2e166m5/CurveParameters.v index 8b47d73a3..0b3c6a6cd 100644 --- a/src/Specific/montgomery32_2e166m5/CurveParameters.v +++ b/src/Specific/montgomery32_2e166m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 5%nat; + base := 32; bitwidth := 32; s := 2^166; c := [(1, 5)]; diff --git a/src/Specific/montgomery32_2e171m19/CurveParameters.v b/src/Specific/montgomery32_2e171m19/CurveParameters.v index cb63b57ec..c36112bef 100644 --- a/src/Specific/montgomery32_2e171m19/CurveParameters.v +++ b/src/Specific/montgomery32_2e171m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 5%nat; + base := 32; bitwidth := 32; s := 2^171; c := [(1, 19)]; diff --git a/src/Specific/montgomery32_2e174m17/CurveParameters.v b/src/Specific/montgomery32_2e174m17/CurveParameters.v index 8f3460538..4d5c2d9f7 100644 --- a/src/Specific/montgomery32_2e174m17/CurveParameters.v +++ b/src/Specific/montgomery32_2e174m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 5%nat; + base := 32; bitwidth := 32; s := 2^174; c := [(1, 17)]; diff --git a/src/Specific/montgomery32_2e174m3/CurveParameters.v b/src/Specific/montgomery32_2e174m3/CurveParameters.v index 9a29393f4..086388838 100644 --- a/src/Specific/montgomery32_2e174m3/CurveParameters.v +++ b/src/Specific/montgomery32_2e174m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 5%nat; + base := 32; bitwidth := 32; s := 2^174; c := [(1, 3)]; diff --git a/src/Specific/montgomery32_2e189m25/CurveParameters.v b/src/Specific/montgomery32_2e189m25/CurveParameters.v index 6c6ebcbbe..c8989d6b3 100644 --- a/src/Specific/montgomery32_2e189m25/CurveParameters.v +++ b/src/Specific/montgomery32_2e189m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 5%nat; + base := 32; bitwidth := 32; s := 2^189; c := [(1, 25)]; diff --git a/src/Specific/montgomery32_2e190m11/CurveParameters.v b/src/Specific/montgomery32_2e190m11/CurveParameters.v index 1ef83cdcf..f93d3067a 100644 --- a/src/Specific/montgomery32_2e190m11/CurveParameters.v +++ b/src/Specific/montgomery32_2e190m11/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 5%nat; + base := 32; bitwidth := 32; s := 2^190; c := [(1, 11)]; diff --git a/src/Specific/montgomery32_2e191m19/CurveParameters.v b/src/Specific/montgomery32_2e191m19/CurveParameters.v index ff8992522..9e8e487fe 100644 --- a/src/Specific/montgomery32_2e191m19/CurveParameters.v +++ b/src/Specific/montgomery32_2e191m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 5%nat; + base := 32; bitwidth := 32; s := 2^191; c := [(1, 19)]; diff --git a/src/Specific/montgomery32_2e192m2e64m1/CurveParameters.v b/src/Specific/montgomery32_2e192m2e64m1/CurveParameters.v index 5d6da4b0d..cc1bba8d2 100644 --- a/src/Specific/montgomery32_2e192m2e64m1/CurveParameters.v +++ b/src/Specific/montgomery32_2e192m2e64m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 6%nat; + base := 32; bitwidth := 32; s := 2^192; c := [(1, 1); (2^64, 1)]; diff --git a/src/Specific/montgomery32_2e194m33/CurveParameters.v b/src/Specific/montgomery32_2e194m33/CurveParameters.v index 6a108e7ef..2a035de9f 100644 --- a/src/Specific/montgomery32_2e194m33/CurveParameters.v +++ b/src/Specific/montgomery32_2e194m33/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 6%nat; + base := 32; bitwidth := 32; s := 2^194; c := [(1, 33)]; diff --git a/src/Specific/montgomery32_2e196m15/CurveParameters.v b/src/Specific/montgomery32_2e196m15/CurveParameters.v index 60ec23119..cbd4fa1ca 100644 --- a/src/Specific/montgomery32_2e196m15/CurveParameters.v +++ b/src/Specific/montgomery32_2e196m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 6%nat; + base := 32; bitwidth := 32; s := 2^196; c := [(1, 15)]; diff --git a/src/Specific/montgomery32_2e198m17/CurveParameters.v b/src/Specific/montgomery32_2e198m17/CurveParameters.v index 585f66369..6a25f2758 100644 --- a/src/Specific/montgomery32_2e198m17/CurveParameters.v +++ b/src/Specific/montgomery32_2e198m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 6%nat; + base := 32; bitwidth := 32; s := 2^198; c := [(1, 17)]; diff --git a/src/Specific/montgomery32_2e206m5/CurveParameters.v b/src/Specific/montgomery32_2e206m5/CurveParameters.v index 5cc00a290..088ed05e0 100644 --- a/src/Specific/montgomery32_2e206m5/CurveParameters.v +++ b/src/Specific/montgomery32_2e206m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 6%nat; + base := 32; bitwidth := 32; s := 2^206; c := [(1, 5)]; diff --git a/src/Specific/montgomery32_2e212m29/CurveParameters.v b/src/Specific/montgomery32_2e212m29/CurveParameters.v index 8e339a959..a6bca7a82 100644 --- a/src/Specific/montgomery32_2e212m29/CurveParameters.v +++ b/src/Specific/montgomery32_2e212m29/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 6%nat; + base := 32; bitwidth := 32; s := 2^212; c := [(1, 29)]; diff --git a/src/Specific/montgomery32_2e213m3/CurveParameters.v b/src/Specific/montgomery32_2e213m3/CurveParameters.v index 5523cd0df..a471ab852 100644 --- a/src/Specific/montgomery32_2e213m3/CurveParameters.v +++ b/src/Specific/montgomery32_2e213m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 6%nat; + base := 32; bitwidth := 32; s := 2^213; c := [(1, 3)]; diff --git a/src/Specific/montgomery32_2e216m2e108m1/CurveParameters.v b/src/Specific/montgomery32_2e216m2e108m1/CurveParameters.v index cd5b5032c..a695673e7 100644 --- a/src/Specific/montgomery32_2e216m2e108m1/CurveParameters.v +++ b/src/Specific/montgomery32_2e216m2e108m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 6%nat; + base := 32; bitwidth := 32; s := 2^216; c := [(1, 1); (2^108, 1)]; diff --git a/src/Specific/montgomery32_2e221m3/CurveParameters.v b/src/Specific/montgomery32_2e221m3/CurveParameters.v index d215fbf7b..6a77d7443 100644 --- a/src/Specific/montgomery32_2e221m3/CurveParameters.v +++ b/src/Specific/montgomery32_2e221m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 6%nat; + base := 32; bitwidth := 32; s := 2^221; c := [(1, 3)]; diff --git a/src/Specific/montgomery32_2e222m117/CurveParameters.v b/src/Specific/montgomery32_2e222m117/CurveParameters.v index 428082e5b..c0b8d466c 100644 --- a/src/Specific/montgomery32_2e222m117/CurveParameters.v +++ b/src/Specific/montgomery32_2e222m117/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 6%nat; + base := 32; bitwidth := 32; s := 2^222; c := [(1, 117)]; diff --git a/src/Specific/montgomery32_2e224m2e96p1/CurveParameters.v b/src/Specific/montgomery32_2e224m2e96p1/CurveParameters.v index 5c45f02a0..efb1444d7 100644 --- a/src/Specific/montgomery32_2e224m2e96p1/CurveParameters.v +++ b/src/Specific/montgomery32_2e224m2e96p1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 7%nat; + base := 32; bitwidth := 32; s := 2^224; c := [(1, -1); (2^96, 1)]; diff --git a/src/Specific/montgomery32_2e226m5/CurveParameters.v b/src/Specific/montgomery32_2e226m5/CurveParameters.v index ceabbead1..bd36e92f8 100644 --- a/src/Specific/montgomery32_2e226m5/CurveParameters.v +++ b/src/Specific/montgomery32_2e226m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 7%nat; + base := 32; bitwidth := 32; s := 2^226; c := [(1, 5)]; diff --git a/src/Specific/montgomery32_2e230m27/CurveParameters.v b/src/Specific/montgomery32_2e230m27/CurveParameters.v index a04d83038..8cd75df4e 100644 --- a/src/Specific/montgomery32_2e230m27/CurveParameters.v +++ b/src/Specific/montgomery32_2e230m27/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 7%nat; + base := 32; bitwidth := 32; s := 2^230; c := [(1, 27)]; diff --git a/src/Specific/montgomery32_2e235m15/CurveParameters.v b/src/Specific/montgomery32_2e235m15/CurveParameters.v index 2edc8e3d0..3fa85530e 100644 --- a/src/Specific/montgomery32_2e235m15/CurveParameters.v +++ b/src/Specific/montgomery32_2e235m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 7%nat; + base := 32; bitwidth := 32; s := 2^235; c := [(1, 15)]; diff --git a/src/Specific/montgomery32_2e243m9/CurveParameters.v b/src/Specific/montgomery32_2e243m9/CurveParameters.v index 5da1e367e..c51a03964 100644 --- a/src/Specific/montgomery32_2e243m9/CurveParameters.v +++ b/src/Specific/montgomery32_2e243m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 7%nat; + base := 32; bitwidth := 32; s := 2^243; c := [(1, 9)]; diff --git a/src/Specific/montgomery32_2e251m9/CurveParameters.v b/src/Specific/montgomery32_2e251m9/CurveParameters.v index 98df66c25..b566f38e9 100644 --- a/src/Specific/montgomery32_2e251m9/CurveParameters.v +++ b/src/Specific/montgomery32_2e251m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 7%nat; + base := 32; bitwidth := 32; s := 2^251; c := [(1, 9)]; diff --git a/src/Specific/montgomery32_2e255m19/CurveParameters.v b/src/Specific/montgomery32_2e255m19/CurveParameters.v index 3a1b97c23..0a3e03d08 100644 --- a/src/Specific/montgomery32_2e255m19/CurveParameters.v +++ b/src/Specific/montgomery32_2e255m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 7%nat; + base := 32; bitwidth := 32; s := 2^255; c := [(1, 19)]; diff --git a/src/Specific/montgomery32_2e255m2e4m2e1m1/CurveParameters.v b/src/Specific/montgomery32_2e255m2e4m2e1m1/CurveParameters.v index 94f04957c..60fbf139e 100644 --- a/src/Specific/montgomery32_2e255m2e4m2e1m1/CurveParameters.v +++ b/src/Specific/montgomery32_2e255m2e4m2e1m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 7%nat; + base := 32; bitwidth := 32; s := 2^255; c := [(1, 1); (2^1, 1); (2^4, 1)]; diff --git a/src/Specific/montgomery32_2e255m765/CurveParameters.v b/src/Specific/montgomery32_2e255m765/CurveParameters.v index f48cc3b27..3d0a72d1e 100644 --- a/src/Specific/montgomery32_2e255m765/CurveParameters.v +++ b/src/Specific/montgomery32_2e255m765/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 7%nat; + base := 32; bitwidth := 32; s := 2^255; c := [(1, 765)]; diff --git a/src/Specific/montgomery32_2e256m189/CurveParameters.v b/src/Specific/montgomery32_2e256m189/CurveParameters.v index 6b09dfc0a..efce7b2d0 100644 --- a/src/Specific/montgomery32_2e256m189/CurveParameters.v +++ b/src/Specific/montgomery32_2e256m189/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 8%nat; + base := 32; bitwidth := 32; s := 2^256; c := [(1, 189)]; diff --git a/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1/CurveParameters.v b/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1/CurveParameters.v index b4890ac5d..d5020f25f 100644 --- a/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1/CurveParameters.v +++ b/src/Specific/montgomery32_2e256m2e224p2e192p2e96m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 8%nat; + base := 32; bitwidth := 32; s := 2^256; c := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]; diff --git a/src/Specific/montgomery32_2e256m2e32m977/CurveParameters.v b/src/Specific/montgomery32_2e256m2e32m977/CurveParameters.v index ab9b0aa47..6488a90b8 100644 --- a/src/Specific/montgomery32_2e256m2e32m977/CurveParameters.v +++ b/src/Specific/montgomery32_2e256m2e32m977/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 8%nat; + base := 32; bitwidth := 32; s := 2^256; c := [(1, 977); (2^32, 1)]; diff --git a/src/Specific/montgomery32_2e266m3/CurveParameters.v b/src/Specific/montgomery32_2e266m3/CurveParameters.v index 711290679..f44e38151 100644 --- a/src/Specific/montgomery32_2e266m3/CurveParameters.v +++ b/src/Specific/montgomery32_2e266m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 8%nat; + base := 32; bitwidth := 32; s := 2^266; c := [(1, 3)]; diff --git a/src/Specific/montgomery32_2e285m9/CurveParameters.v b/src/Specific/montgomery32_2e285m9/CurveParameters.v index 8cef52c40..1f89bdf96 100644 --- a/src/Specific/montgomery32_2e285m9/CurveParameters.v +++ b/src/Specific/montgomery32_2e285m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 8%nat; + base := 32; bitwidth := 32; s := 2^285; c := [(1, 9)]; diff --git a/src/Specific/montgomery32_2e291m19/CurveParameters.v b/src/Specific/montgomery32_2e291m19/CurveParameters.v index a1915ad1f..f26d12d8f 100644 --- a/src/Specific/montgomery32_2e291m19/CurveParameters.v +++ b/src/Specific/montgomery32_2e291m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 9%nat; + base := 32; bitwidth := 32; s := 2^291; c := [(1, 19)]; diff --git a/src/Specific/montgomery32_2e321m9/CurveParameters.v b/src/Specific/montgomery32_2e321m9/CurveParameters.v index ca875b403..67708c2ea 100644 --- a/src/Specific/montgomery32_2e321m9/CurveParameters.v +++ b/src/Specific/montgomery32_2e321m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 10%nat; + base := 32; bitwidth := 32; s := 2^321; c := [(1, 9)]; diff --git a/src/Specific/montgomery32_2e322m2e161m1/CurveParameters.v b/src/Specific/montgomery32_2e322m2e161m1/CurveParameters.v index de1c8a49d..85f5f62eb 100644 --- a/src/Specific/montgomery32_2e322m2e161m1/CurveParameters.v +++ b/src/Specific/montgomery32_2e322m2e161m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 10%nat; + base := 32; bitwidth := 32; s := 2^322; c := [(1, 1); (2^161, 1)]; diff --git a/src/Specific/montgomery32_2e336m17/CurveParameters.v b/src/Specific/montgomery32_2e336m17/CurveParameters.v index 7bfffe26a..18912be80 100644 --- a/src/Specific/montgomery32_2e336m17/CurveParameters.v +++ b/src/Specific/montgomery32_2e336m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 10%nat; + base := 32; bitwidth := 32; s := 2^336; c := [(1, 17)]; diff --git a/src/Specific/montgomery32_2e336m3/CurveParameters.v b/src/Specific/montgomery32_2e336m3/CurveParameters.v index 088bad85f..074daa69f 100644 --- a/src/Specific/montgomery32_2e336m3/CurveParameters.v +++ b/src/Specific/montgomery32_2e336m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 10%nat; + base := 32; bitwidth := 32; s := 2^336; c := [(1, 3)]; diff --git a/src/Specific/montgomery32_2e338m15/CurveParameters.v b/src/Specific/montgomery32_2e338m15/CurveParameters.v index bce7f19d1..e67a76c36 100644 --- a/src/Specific/montgomery32_2e338m15/CurveParameters.v +++ b/src/Specific/montgomery32_2e338m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 10%nat; + base := 32; bitwidth := 32; s := 2^338; c := [(1, 15)]; diff --git a/src/Specific/montgomery32_2e369m25/CurveParameters.v b/src/Specific/montgomery32_2e369m25/CurveParameters.v index 79800d48d..ee4541b67 100644 --- a/src/Specific/montgomery32_2e369m25/CurveParameters.v +++ b/src/Specific/montgomery32_2e369m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 11%nat; + base := 32; bitwidth := 32; s := 2^369; c := [(1, 25)]; diff --git a/src/Specific/montgomery32_2e379m19/CurveParameters.v b/src/Specific/montgomery32_2e379m19/CurveParameters.v index 9d34f2833..1a6df497b 100644 --- a/src/Specific/montgomery32_2e379m19/CurveParameters.v +++ b/src/Specific/montgomery32_2e379m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 11%nat; + base := 32; bitwidth := 32; s := 2^379; c := [(1, 19)]; diff --git a/src/Specific/montgomery32_2e382m105/CurveParameters.v b/src/Specific/montgomery32_2e382m105/CurveParameters.v index 5327d1bb5..909604998 100644 --- a/src/Specific/montgomery32_2e382m105/CurveParameters.v +++ b/src/Specific/montgomery32_2e382m105/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 11%nat; + base := 32; bitwidth := 32; s := 2^382; c := [(1, 105)]; diff --git a/src/Specific/montgomery32_2e383m187/CurveParameters.v b/src/Specific/montgomery32_2e383m187/CurveParameters.v index bfc4359ce..b72d17dd6 100644 --- a/src/Specific/montgomery32_2e383m187/CurveParameters.v +++ b/src/Specific/montgomery32_2e383m187/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 11%nat; + base := 32; bitwidth := 32; s := 2^383; c := [(1, 187)]; diff --git a/src/Specific/montgomery32_2e383m31/CurveParameters.v b/src/Specific/montgomery32_2e383m31/CurveParameters.v index ed045577e..aebd3d049 100644 --- a/src/Specific/montgomery32_2e383m31/CurveParameters.v +++ b/src/Specific/montgomery32_2e383m31/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 11%nat; + base := 32; bitwidth := 32; s := 2^383; c := [(1, 31)]; diff --git a/src/Specific/montgomery32_2e383m421/CurveParameters.v b/src/Specific/montgomery32_2e383m421/CurveParameters.v index 0de06aac7..f566ed3be 100644 --- a/src/Specific/montgomery32_2e383m421/CurveParameters.v +++ b/src/Specific/montgomery32_2e383m421/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 11%nat; + base := 32; bitwidth := 32; s := 2^383; c := [(1, 421)]; diff --git a/src/Specific/montgomery32_2e384m2e128m2e96p2e32m1/CurveParameters.v b/src/Specific/montgomery32_2e384m2e128m2e96p2e32m1/CurveParameters.v index c32d23e79..bdc2529a7 100644 --- a/src/Specific/montgomery32_2e384m2e128m2e96p2e32m1/CurveParameters.v +++ b/src/Specific/montgomery32_2e384m2e128m2e96p2e32m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 12%nat; + base := 32; bitwidth := 32; s := 2^384; c := [(1, 1); (2^32, -1); (2^96, 1); (2^128, 1)]; diff --git a/src/Specific/montgomery32_2e384m317/CurveParameters.v b/src/Specific/montgomery32_2e384m317/CurveParameters.v index d4acdd325..2779e0b42 100644 --- a/src/Specific/montgomery32_2e384m317/CurveParameters.v +++ b/src/Specific/montgomery32_2e384m317/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 12%nat; + base := 32; bitwidth := 32; s := 2^384; c := [(1, 317)]; diff --git a/src/Specific/montgomery32_2e389m21/CurveParameters.v b/src/Specific/montgomery32_2e389m21/CurveParameters.v index a88b76ebe..210aa7fba 100644 --- a/src/Specific/montgomery32_2e389m21/CurveParameters.v +++ b/src/Specific/montgomery32_2e389m21/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 12%nat; + base := 32; bitwidth := 32; s := 2^389; c := [(1, 21)]; diff --git a/src/Specific/montgomery32_2e401m31/CurveParameters.v b/src/Specific/montgomery32_2e401m31/CurveParameters.v index 5e093ad31..f4e7012c7 100644 --- a/src/Specific/montgomery32_2e401m31/CurveParameters.v +++ b/src/Specific/montgomery32_2e401m31/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 12%nat; + base := 32; bitwidth := 32; s := 2^401; c := [(1, 31)]; diff --git a/src/Specific/montgomery32_2e413m21/CurveParameters.v b/src/Specific/montgomery32_2e413m21/CurveParameters.v index 13fb130c8..532d6f952 100644 --- a/src/Specific/montgomery32_2e413m21/CurveParameters.v +++ b/src/Specific/montgomery32_2e413m21/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 12%nat; + base := 32; bitwidth := 32; s := 2^413; c := [(1, 21)]; diff --git a/src/Specific/montgomery32_2e414m17/CurveParameters.v b/src/Specific/montgomery32_2e414m17/CurveParameters.v index 4b26d0d91..a798c53fb 100644 --- a/src/Specific/montgomery32_2e414m17/CurveParameters.v +++ b/src/Specific/montgomery32_2e414m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 12%nat; + base := 32; bitwidth := 32; s := 2^414; c := [(1, 17)]; diff --git a/src/Specific/montgomery32_2e416m2e208m1/CurveParameters.v b/src/Specific/montgomery32_2e416m2e208m1/CurveParameters.v index d5b057244..f0984b4d4 100644 --- a/src/Specific/montgomery32_2e416m2e208m1/CurveParameters.v +++ b/src/Specific/montgomery32_2e416m2e208m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 13%nat; + base := 32; bitwidth := 32; s := 2^416; c := [(1, 1); (2^208, 1)]; diff --git a/src/Specific/montgomery32_2e444m17/CurveParameters.v b/src/Specific/montgomery32_2e444m17/CurveParameters.v index 95e6cc326..e30dc6ee2 100644 --- a/src/Specific/montgomery32_2e444m17/CurveParameters.v +++ b/src/Specific/montgomery32_2e444m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 13%nat; + base := 32; bitwidth := 32; s := 2^444; c := [(1, 17)]; diff --git a/src/Specific/montgomery32_2e448m2e224m1/CurveParameters.v b/src/Specific/montgomery32_2e448m2e224m1/CurveParameters.v index 879dbb487..ba1a6d6c4 100644 --- a/src/Specific/montgomery32_2e448m2e224m1/CurveParameters.v +++ b/src/Specific/montgomery32_2e448m2e224m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 14%nat; + base := 32; bitwidth := 32; s := 2^448; c := [(1, 1); (2^224, 1)]; diff --git a/src/Specific/montgomery32_2e450m2e225m1/CurveParameters.v b/src/Specific/montgomery32_2e450m2e225m1/CurveParameters.v index 8b74751e6..2ce8dbb80 100644 --- a/src/Specific/montgomery32_2e450m2e225m1/CurveParameters.v +++ b/src/Specific/montgomery32_2e450m2e225m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 14%nat; + base := 32; bitwidth := 32; s := 2^450; c := [(1, 1); (2^225, 1)]; diff --git a/src/Specific/montgomery32_2e452m3/CurveParameters.v b/src/Specific/montgomery32_2e452m3/CurveParameters.v index 47e836c87..bfac593c2 100644 --- a/src/Specific/montgomery32_2e452m3/CurveParameters.v +++ b/src/Specific/montgomery32_2e452m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 14%nat; + base := 32; bitwidth := 32; s := 2^452; c := [(1, 3)]; diff --git a/src/Specific/montgomery32_2e468m17/CurveParameters.v b/src/Specific/montgomery32_2e468m17/CurveParameters.v index 6a0bd617f..1ff5d433d 100644 --- a/src/Specific/montgomery32_2e468m17/CurveParameters.v +++ b/src/Specific/montgomery32_2e468m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 14%nat; + base := 32; bitwidth := 32; s := 2^468; c := [(1, 17)]; diff --git a/src/Specific/montgomery32_2e480m2e240m1/CurveParameters.v b/src/Specific/montgomery32_2e480m2e240m1/CurveParameters.v index 19d73fb20..e4073b6a0 100644 --- a/src/Specific/montgomery32_2e480m2e240m1/CurveParameters.v +++ b/src/Specific/montgomery32_2e480m2e240m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 15%nat; + base := 32; bitwidth := 32; s := 2^480; c := [(1, 1); (2^240, 1)]; diff --git a/src/Specific/montgomery32_2e488m17/CurveParameters.v b/src/Specific/montgomery32_2e488m17/CurveParameters.v index 614698a5d..a392806d2 100644 --- a/src/Specific/montgomery32_2e488m17/CurveParameters.v +++ b/src/Specific/montgomery32_2e488m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 15%nat; + base := 32; bitwidth := 32; s := 2^488; c := [(1, 17)]; diff --git a/src/Specific/montgomery32_2e489m21/CurveParameters.v b/src/Specific/montgomery32_2e489m21/CurveParameters.v index 01ba9b36b..7aa49d3c8 100644 --- a/src/Specific/montgomery32_2e489m21/CurveParameters.v +++ b/src/Specific/montgomery32_2e489m21/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 15%nat; + base := 32; bitwidth := 32; s := 2^489; c := [(1, 21)]; diff --git a/src/Specific/montgomery32_2e495m31/CurveParameters.v b/src/Specific/montgomery32_2e495m31/CurveParameters.v index fd3ae4973..d366176e4 100644 --- a/src/Specific/montgomery32_2e495m31/CurveParameters.v +++ b/src/Specific/montgomery32_2e495m31/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 15%nat; + base := 32; bitwidth := 32; s := 2^495; c := [(1, 31)]; diff --git a/src/Specific/montgomery32_2e511m187/CurveParameters.v b/src/Specific/montgomery32_2e511m187/CurveParameters.v index 5d2d59011..e60e97107 100644 --- a/src/Specific/montgomery32_2e511m187/CurveParameters.v +++ b/src/Specific/montgomery32_2e511m187/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 15%nat; + base := 32; bitwidth := 32; s := 2^511; c := [(1, 187)]; diff --git a/src/Specific/montgomery32_2e511m481/CurveParameters.v b/src/Specific/montgomery32_2e511m481/CurveParameters.v index a2a0ac8c6..edafe1df8 100644 --- a/src/Specific/montgomery32_2e511m481/CurveParameters.v +++ b/src/Specific/montgomery32_2e511m481/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 15%nat; + base := 32; bitwidth := 32; s := 2^511; c := [(1, 481)]; diff --git a/src/Specific/montgomery32_2e512m569/CurveParameters.v b/src/Specific/montgomery32_2e512m569/CurveParameters.v index e3b227d14..2dfb70de2 100644 --- a/src/Specific/montgomery32_2e512m569/CurveParameters.v +++ b/src/Specific/montgomery32_2e512m569/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 16%nat; + base := 32; bitwidth := 32; s := 2^512; c := [(1, 569)]; diff --git a/src/Specific/montgomery32_2e521m1/CurveParameters.v b/src/Specific/montgomery32_2e521m1/CurveParameters.v index 89dd148d5..1fc41b51e 100644 --- a/src/Specific/montgomery32_2e521m1/CurveParameters.v +++ b/src/Specific/montgomery32_2e521m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 16%nat; + base := 32; bitwidth := 32; s := 2^521; c := [(1, 1)]; diff --git a/src/Specific/montgomery64_2e127m1/CurveParameters.v b/src/Specific/montgomery64_2e127m1/CurveParameters.v index 47370182c..3cff26742 100644 --- a/src/Specific/montgomery64_2e127m1/CurveParameters.v +++ b/src/Specific/montgomery64_2e127m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 1%nat; + base := 64; bitwidth := 64; s := 2^127; c := [(1, 1)]; diff --git a/src/Specific/montgomery64_2e129m25/CurveParameters.v b/src/Specific/montgomery64_2e129m25/CurveParameters.v index c46f63358..da08712b9 100644 --- a/src/Specific/montgomery64_2e129m25/CurveParameters.v +++ b/src/Specific/montgomery64_2e129m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^129; c := [(1, 25)]; diff --git a/src/Specific/montgomery64_2e130m5/CurveParameters.v b/src/Specific/montgomery64_2e130m5/CurveParameters.v index 74d880860..3cbce9b48 100644 --- a/src/Specific/montgomery64_2e130m5/CurveParameters.v +++ b/src/Specific/montgomery64_2e130m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^130; c := [(1, 5)]; diff --git a/src/Specific/montgomery64_2e137m13/CurveParameters.v b/src/Specific/montgomery64_2e137m13/CurveParameters.v index ce06e0307..33aa6f0d3 100644 --- a/src/Specific/montgomery64_2e137m13/CurveParameters.v +++ b/src/Specific/montgomery64_2e137m13/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^137; c := [(1, 13)]; diff --git a/src/Specific/montgomery64_2e140m27/CurveParameters.v b/src/Specific/montgomery64_2e140m27/CurveParameters.v index d587823e5..695e6b715 100644 --- a/src/Specific/montgomery64_2e140m27/CurveParameters.v +++ b/src/Specific/montgomery64_2e140m27/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^140; c := [(1, 27)]; diff --git a/src/Specific/montgomery64_2e141m9/CurveParameters.v b/src/Specific/montgomery64_2e141m9/CurveParameters.v index 545052531..7995a342c 100644 --- a/src/Specific/montgomery64_2e141m9/CurveParameters.v +++ b/src/Specific/montgomery64_2e141m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^141; c := [(1, 9)]; diff --git a/src/Specific/montgomery64_2e150m3/CurveParameters.v b/src/Specific/montgomery64_2e150m3/CurveParameters.v index 937bbd064..50d5f8712 100644 --- a/src/Specific/montgomery64_2e150m3/CurveParameters.v +++ b/src/Specific/montgomery64_2e150m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^150; c := [(1, 3)]; diff --git a/src/Specific/montgomery64_2e150m5/CurveParameters.v b/src/Specific/montgomery64_2e150m5/CurveParameters.v index 7e817fdcb..52fa3e568 100644 --- a/src/Specific/montgomery64_2e150m5/CurveParameters.v +++ b/src/Specific/montgomery64_2e150m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^150; c := [(1, 5)]; diff --git a/src/Specific/montgomery64_2e152m17/CurveParameters.v b/src/Specific/montgomery64_2e152m17/CurveParameters.v index d80db4404..b1a43d05e 100644 --- a/src/Specific/montgomery64_2e152m17/CurveParameters.v +++ b/src/Specific/montgomery64_2e152m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^152; c := [(1, 17)]; diff --git a/src/Specific/montgomery64_2e158m15/CurveParameters.v b/src/Specific/montgomery64_2e158m15/CurveParameters.v index 7b673cf4c..9ac621b75 100644 --- a/src/Specific/montgomery64_2e158m15/CurveParameters.v +++ b/src/Specific/montgomery64_2e158m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^158; c := [(1, 15)]; diff --git a/src/Specific/montgomery64_2e165m25/CurveParameters.v b/src/Specific/montgomery64_2e165m25/CurveParameters.v index 4cf2e2634..7367f1917 100644 --- a/src/Specific/montgomery64_2e165m25/CurveParameters.v +++ b/src/Specific/montgomery64_2e165m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^165; c := [(1, 25)]; diff --git a/src/Specific/montgomery64_2e166m5/CurveParameters.v b/src/Specific/montgomery64_2e166m5/CurveParameters.v index cded4a72b..e4eb3863a 100644 --- a/src/Specific/montgomery64_2e166m5/CurveParameters.v +++ b/src/Specific/montgomery64_2e166m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^166; c := [(1, 5)]; diff --git a/src/Specific/montgomery64_2e171m19/CurveParameters.v b/src/Specific/montgomery64_2e171m19/CurveParameters.v index b0058cd54..12a53ed35 100644 --- a/src/Specific/montgomery64_2e171m19/CurveParameters.v +++ b/src/Specific/montgomery64_2e171m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^171; c := [(1, 19)]; diff --git a/src/Specific/montgomery64_2e174m17/CurveParameters.v b/src/Specific/montgomery64_2e174m17/CurveParameters.v index 211d241b3..a642cc5f9 100644 --- a/src/Specific/montgomery64_2e174m17/CurveParameters.v +++ b/src/Specific/montgomery64_2e174m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^174; c := [(1, 17)]; diff --git a/src/Specific/montgomery64_2e174m3/CurveParameters.v b/src/Specific/montgomery64_2e174m3/CurveParameters.v index babe5e156..c7cfe5599 100644 --- a/src/Specific/montgomery64_2e174m3/CurveParameters.v +++ b/src/Specific/montgomery64_2e174m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^174; c := [(1, 3)]; diff --git a/src/Specific/montgomery64_2e189m25/CurveParameters.v b/src/Specific/montgomery64_2e189m25/CurveParameters.v index b8db361c3..cc2f90097 100644 --- a/src/Specific/montgomery64_2e189m25/CurveParameters.v +++ b/src/Specific/montgomery64_2e189m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^189; c := [(1, 25)]; diff --git a/src/Specific/montgomery64_2e190m11/CurveParameters.v b/src/Specific/montgomery64_2e190m11/CurveParameters.v index 1d67492a9..2f12f5ada 100644 --- a/src/Specific/montgomery64_2e190m11/CurveParameters.v +++ b/src/Specific/montgomery64_2e190m11/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^190; c := [(1, 11)]; diff --git a/src/Specific/montgomery64_2e191m19/CurveParameters.v b/src/Specific/montgomery64_2e191m19/CurveParameters.v index 0b1f0d8d6..f598649f4 100644 --- a/src/Specific/montgomery64_2e191m19/CurveParameters.v +++ b/src/Specific/montgomery64_2e191m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 2%nat; + base := 64; bitwidth := 64; s := 2^191; c := [(1, 19)]; diff --git a/src/Specific/montgomery64_2e192m2e64m1/CurveParameters.v b/src/Specific/montgomery64_2e192m2e64m1/CurveParameters.v index 0b6aa57a5..274e7a06d 100644 --- a/src/Specific/montgomery64_2e192m2e64m1/CurveParameters.v +++ b/src/Specific/montgomery64_2e192m2e64m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^192; c := [(1, 1); (2^64, 1)]; diff --git a/src/Specific/montgomery64_2e194m33/CurveParameters.v b/src/Specific/montgomery64_2e194m33/CurveParameters.v index 85cf391dc..1ee1f898c 100644 --- a/src/Specific/montgomery64_2e194m33/CurveParameters.v +++ b/src/Specific/montgomery64_2e194m33/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^194; c := [(1, 33)]; diff --git a/src/Specific/montgomery64_2e196m15/CurveParameters.v b/src/Specific/montgomery64_2e196m15/CurveParameters.v index 3e600aaff..dd98299e3 100644 --- a/src/Specific/montgomery64_2e196m15/CurveParameters.v +++ b/src/Specific/montgomery64_2e196m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^196; c := [(1, 15)]; diff --git a/src/Specific/montgomery64_2e198m17/CurveParameters.v b/src/Specific/montgomery64_2e198m17/CurveParameters.v index 3f7528bc5..b4c22eee4 100644 --- a/src/Specific/montgomery64_2e198m17/CurveParameters.v +++ b/src/Specific/montgomery64_2e198m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^198; c := [(1, 17)]; diff --git a/src/Specific/montgomery64_2e206m5/CurveParameters.v b/src/Specific/montgomery64_2e206m5/CurveParameters.v index f1f8c44e5..0e9f3ce8f 100644 --- a/src/Specific/montgomery64_2e206m5/CurveParameters.v +++ b/src/Specific/montgomery64_2e206m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^206; c := [(1, 5)]; diff --git a/src/Specific/montgomery64_2e212m29/CurveParameters.v b/src/Specific/montgomery64_2e212m29/CurveParameters.v index c51c61c23..917d26e1d 100644 --- a/src/Specific/montgomery64_2e212m29/CurveParameters.v +++ b/src/Specific/montgomery64_2e212m29/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^212; c := [(1, 29)]; diff --git a/src/Specific/montgomery64_2e213m3/CurveParameters.v b/src/Specific/montgomery64_2e213m3/CurveParameters.v index beedf7554..2b8116172 100644 --- a/src/Specific/montgomery64_2e213m3/CurveParameters.v +++ b/src/Specific/montgomery64_2e213m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^213; c := [(1, 3)]; diff --git a/src/Specific/montgomery64_2e216m2e108m1/CurveParameters.v b/src/Specific/montgomery64_2e216m2e108m1/CurveParameters.v index de17a43f9..87eea5950 100644 --- a/src/Specific/montgomery64_2e216m2e108m1/CurveParameters.v +++ b/src/Specific/montgomery64_2e216m2e108m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^216; c := [(1, 1); (2^108, 1)]; diff --git a/src/Specific/montgomery64_2e221m3/CurveParameters.v b/src/Specific/montgomery64_2e221m3/CurveParameters.v index 1b05f2b5e..07eb471a4 100644 --- a/src/Specific/montgomery64_2e221m3/CurveParameters.v +++ b/src/Specific/montgomery64_2e221m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^221; c := [(1, 3)]; diff --git a/src/Specific/montgomery64_2e222m117/CurveParameters.v b/src/Specific/montgomery64_2e222m117/CurveParameters.v index e91895555..12197d8c1 100644 --- a/src/Specific/montgomery64_2e222m117/CurveParameters.v +++ b/src/Specific/montgomery64_2e222m117/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^222; c := [(1, 117)]; diff --git a/src/Specific/montgomery64_2e224m2e96p1/CurveParameters.v b/src/Specific/montgomery64_2e224m2e96p1/CurveParameters.v index b75df72ab..a67a6fa82 100644 --- a/src/Specific/montgomery64_2e224m2e96p1/CurveParameters.v +++ b/src/Specific/montgomery64_2e224m2e96p1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^224; c := [(1, -1); (2^96, 1)]; diff --git a/src/Specific/montgomery64_2e226m5/CurveParameters.v b/src/Specific/montgomery64_2e226m5/CurveParameters.v index 0cf8281f3..1d44e7e4d 100644 --- a/src/Specific/montgomery64_2e226m5/CurveParameters.v +++ b/src/Specific/montgomery64_2e226m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^226; c := [(1, 5)]; diff --git a/src/Specific/montgomery64_2e230m27/CurveParameters.v b/src/Specific/montgomery64_2e230m27/CurveParameters.v index f65113c47..4ab77e91b 100644 --- a/src/Specific/montgomery64_2e230m27/CurveParameters.v +++ b/src/Specific/montgomery64_2e230m27/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^230; c := [(1, 27)]; diff --git a/src/Specific/montgomery64_2e235m15/CurveParameters.v b/src/Specific/montgomery64_2e235m15/CurveParameters.v index f4f01625c..fbedeca2c 100644 --- a/src/Specific/montgomery64_2e235m15/CurveParameters.v +++ b/src/Specific/montgomery64_2e235m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^235; c := [(1, 15)]; diff --git a/src/Specific/montgomery64_2e243m9/CurveParameters.v b/src/Specific/montgomery64_2e243m9/CurveParameters.v index cdc1b8e6b..e8b538f70 100644 --- a/src/Specific/montgomery64_2e243m9/CurveParameters.v +++ b/src/Specific/montgomery64_2e243m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^243; c := [(1, 9)]; diff --git a/src/Specific/montgomery64_2e251m9/CurveParameters.v b/src/Specific/montgomery64_2e251m9/CurveParameters.v index ce7f5f766..09e295c46 100644 --- a/src/Specific/montgomery64_2e251m9/CurveParameters.v +++ b/src/Specific/montgomery64_2e251m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^251; c := [(1, 9)]; diff --git a/src/Specific/montgomery64_2e255m19/CurveParameters.v b/src/Specific/montgomery64_2e255m19/CurveParameters.v index 574297de5..0f1bd8d29 100644 --- a/src/Specific/montgomery64_2e255m19/CurveParameters.v +++ b/src/Specific/montgomery64_2e255m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^255; c := [(1, 19)]; diff --git a/src/Specific/montgomery64_2e255m2e4m2e1m1/CurveParameters.v b/src/Specific/montgomery64_2e255m2e4m2e1m1/CurveParameters.v index a58f6c71c..1a8b1666a 100644 --- a/src/Specific/montgomery64_2e255m2e4m2e1m1/CurveParameters.v +++ b/src/Specific/montgomery64_2e255m2e4m2e1m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^255; c := [(1, 1); (2^1, 1); (2^4, 1)]; diff --git a/src/Specific/montgomery64_2e255m765/CurveParameters.v b/src/Specific/montgomery64_2e255m765/CurveParameters.v index 728175495..4b2cff902 100644 --- a/src/Specific/montgomery64_2e255m765/CurveParameters.v +++ b/src/Specific/montgomery64_2e255m765/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 3%nat; + base := 64; bitwidth := 64; s := 2^255; c := [(1, 765)]; diff --git a/src/Specific/montgomery64_2e256m189/CurveParameters.v b/src/Specific/montgomery64_2e256m189/CurveParameters.v index 32f422e49..45e0e606f 100644 --- a/src/Specific/montgomery64_2e256m189/CurveParameters.v +++ b/src/Specific/montgomery64_2e256m189/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 4%nat; + base := 64; bitwidth := 64; s := 2^256; c := [(1, 189)]; diff --git a/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1/CurveParameters.v b/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1/CurveParameters.v index 35a36d4b5..ded104af1 100644 --- a/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1/CurveParameters.v +++ b/src/Specific/montgomery64_2e256m2e224p2e192p2e96m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 4%nat; + base := 64; bitwidth := 64; s := 2^256; c := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]; diff --git a/src/Specific/montgomery64_2e256m2e32m977/CurveParameters.v b/src/Specific/montgomery64_2e256m2e32m977/CurveParameters.v index 33b48b76d..9c065e667 100644 --- a/src/Specific/montgomery64_2e256m2e32m977/CurveParameters.v +++ b/src/Specific/montgomery64_2e256m2e32m977/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 4%nat; + base := 64; bitwidth := 64; s := 2^256; c := [(1, 977); (2^32, 1)]; diff --git a/src/Specific/montgomery64_2e266m3/CurveParameters.v b/src/Specific/montgomery64_2e266m3/CurveParameters.v index 0b2f50766..86e248078 100644 --- a/src/Specific/montgomery64_2e266m3/CurveParameters.v +++ b/src/Specific/montgomery64_2e266m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 4%nat; + base := 64; bitwidth := 64; s := 2^266; c := [(1, 3)]; diff --git a/src/Specific/montgomery64_2e285m9/CurveParameters.v b/src/Specific/montgomery64_2e285m9/CurveParameters.v index d275f876f..d64a049db 100644 --- a/src/Specific/montgomery64_2e285m9/CurveParameters.v +++ b/src/Specific/montgomery64_2e285m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 4%nat; + base := 64; bitwidth := 64; s := 2^285; c := [(1, 9)]; diff --git a/src/Specific/montgomery64_2e291m19/CurveParameters.v b/src/Specific/montgomery64_2e291m19/CurveParameters.v index 7b1a56c04..a7c8b8582 100644 --- a/src/Specific/montgomery64_2e291m19/CurveParameters.v +++ b/src/Specific/montgomery64_2e291m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 4%nat; + base := 64; bitwidth := 64; s := 2^291; c := [(1, 19)]; diff --git a/src/Specific/montgomery64_2e321m9/CurveParameters.v b/src/Specific/montgomery64_2e321m9/CurveParameters.v index e10a581e8..80b72e6a1 100644 --- a/src/Specific/montgomery64_2e321m9/CurveParameters.v +++ b/src/Specific/montgomery64_2e321m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 5%nat; + base := 64; bitwidth := 64; s := 2^321; c := [(1, 9)]; diff --git a/src/Specific/montgomery64_2e322m2e161m1/CurveParameters.v b/src/Specific/montgomery64_2e322m2e161m1/CurveParameters.v index 473c9ebae..af412b089 100644 --- a/src/Specific/montgomery64_2e322m2e161m1/CurveParameters.v +++ b/src/Specific/montgomery64_2e322m2e161m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 5%nat; + base := 64; bitwidth := 64; s := 2^322; c := [(1, 1); (2^161, 1)]; diff --git a/src/Specific/montgomery64_2e336m17/CurveParameters.v b/src/Specific/montgomery64_2e336m17/CurveParameters.v index b1f2674dc..6fcd45813 100644 --- a/src/Specific/montgomery64_2e336m17/CurveParameters.v +++ b/src/Specific/montgomery64_2e336m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 5%nat; + base := 64; bitwidth := 64; s := 2^336; c := [(1, 17)]; diff --git a/src/Specific/montgomery64_2e336m3/CurveParameters.v b/src/Specific/montgomery64_2e336m3/CurveParameters.v index 6e476d776..357ec07d3 100644 --- a/src/Specific/montgomery64_2e336m3/CurveParameters.v +++ b/src/Specific/montgomery64_2e336m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 5%nat; + base := 64; bitwidth := 64; s := 2^336; c := [(1, 3)]; diff --git a/src/Specific/montgomery64_2e338m15/CurveParameters.v b/src/Specific/montgomery64_2e338m15/CurveParameters.v index c3129ebc2..2469355f3 100644 --- a/src/Specific/montgomery64_2e338m15/CurveParameters.v +++ b/src/Specific/montgomery64_2e338m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 5%nat; + base := 64; bitwidth := 64; s := 2^338; c := [(1, 15)]; diff --git a/src/Specific/montgomery64_2e369m25/CurveParameters.v b/src/Specific/montgomery64_2e369m25/CurveParameters.v index d6a9b3a32..68e2ddf13 100644 --- a/src/Specific/montgomery64_2e369m25/CurveParameters.v +++ b/src/Specific/montgomery64_2e369m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 5%nat; + base := 64; bitwidth := 64; s := 2^369; c := [(1, 25)]; diff --git a/src/Specific/montgomery64_2e379m19/CurveParameters.v b/src/Specific/montgomery64_2e379m19/CurveParameters.v index de21ec61e..7ccff7ae7 100644 --- a/src/Specific/montgomery64_2e379m19/CurveParameters.v +++ b/src/Specific/montgomery64_2e379m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 5%nat; + base := 64; bitwidth := 64; s := 2^379; c := [(1, 19)]; diff --git a/src/Specific/montgomery64_2e382m105/CurveParameters.v b/src/Specific/montgomery64_2e382m105/CurveParameters.v index 4f77a2081..2a3a3b6cc 100644 --- a/src/Specific/montgomery64_2e382m105/CurveParameters.v +++ b/src/Specific/montgomery64_2e382m105/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 5%nat; + base := 64; bitwidth := 64; s := 2^382; c := [(1, 105)]; diff --git a/src/Specific/montgomery64_2e383m187/CurveParameters.v b/src/Specific/montgomery64_2e383m187/CurveParameters.v index 50a96b2e2..11296b9cb 100644 --- a/src/Specific/montgomery64_2e383m187/CurveParameters.v +++ b/src/Specific/montgomery64_2e383m187/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 5%nat; + base := 64; bitwidth := 64; s := 2^383; c := [(1, 187)]; diff --git a/src/Specific/montgomery64_2e383m31/CurveParameters.v b/src/Specific/montgomery64_2e383m31/CurveParameters.v index 355da2cc8..7e8a4f6ed 100644 --- a/src/Specific/montgomery64_2e383m31/CurveParameters.v +++ b/src/Specific/montgomery64_2e383m31/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 5%nat; + base := 64; bitwidth := 64; s := 2^383; c := [(1, 31)]; diff --git a/src/Specific/montgomery64_2e383m421/CurveParameters.v b/src/Specific/montgomery64_2e383m421/CurveParameters.v index c0bd5fe64..5b2ac43b4 100644 --- a/src/Specific/montgomery64_2e383m421/CurveParameters.v +++ b/src/Specific/montgomery64_2e383m421/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 5%nat; + base := 64; bitwidth := 64; s := 2^383; c := [(1, 421)]; diff --git a/src/Specific/montgomery64_2e384m2e128m2e96p2e32m1/CurveParameters.v b/src/Specific/montgomery64_2e384m2e128m2e96p2e32m1/CurveParameters.v index 8b29e6620..790302664 100644 --- a/src/Specific/montgomery64_2e384m2e128m2e96p2e32m1/CurveParameters.v +++ b/src/Specific/montgomery64_2e384m2e128m2e96p2e32m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 6%nat; + base := 64; bitwidth := 64; s := 2^384; c := [(1, 1); (2^32, -1); (2^96, 1); (2^128, 1)]; diff --git a/src/Specific/montgomery64_2e384m317/CurveParameters.v b/src/Specific/montgomery64_2e384m317/CurveParameters.v index a43f2fdc0..189e04497 100644 --- a/src/Specific/montgomery64_2e384m317/CurveParameters.v +++ b/src/Specific/montgomery64_2e384m317/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 6%nat; + base := 64; bitwidth := 64; s := 2^384; c := [(1, 317)]; diff --git a/src/Specific/montgomery64_2e389m21/CurveParameters.v b/src/Specific/montgomery64_2e389m21/CurveParameters.v index 0a01b5ee7..cafb3e08b 100644 --- a/src/Specific/montgomery64_2e389m21/CurveParameters.v +++ b/src/Specific/montgomery64_2e389m21/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 6%nat; + base := 64; bitwidth := 64; s := 2^389; c := [(1, 21)]; diff --git a/src/Specific/montgomery64_2e401m31/CurveParameters.v b/src/Specific/montgomery64_2e401m31/CurveParameters.v index 8b8cb1387..90ea36075 100644 --- a/src/Specific/montgomery64_2e401m31/CurveParameters.v +++ b/src/Specific/montgomery64_2e401m31/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 6%nat; + base := 64; bitwidth := 64; s := 2^401; c := [(1, 31)]; diff --git a/src/Specific/montgomery64_2e413m21/CurveParameters.v b/src/Specific/montgomery64_2e413m21/CurveParameters.v index 138026294..a4799b1ec 100644 --- a/src/Specific/montgomery64_2e413m21/CurveParameters.v +++ b/src/Specific/montgomery64_2e413m21/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 6%nat; + base := 64; bitwidth := 64; s := 2^413; c := [(1, 21)]; diff --git a/src/Specific/montgomery64_2e414m17/CurveParameters.v b/src/Specific/montgomery64_2e414m17/CurveParameters.v index 8739048a2..0527b15c5 100644 --- a/src/Specific/montgomery64_2e414m17/CurveParameters.v +++ b/src/Specific/montgomery64_2e414m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 6%nat; + base := 64; bitwidth := 64; s := 2^414; c := [(1, 17)]; diff --git a/src/Specific/montgomery64_2e416m2e208m1/CurveParameters.v b/src/Specific/montgomery64_2e416m2e208m1/CurveParameters.v index 7c1f436a2..67bccbc64 100644 --- a/src/Specific/montgomery64_2e416m2e208m1/CurveParameters.v +++ b/src/Specific/montgomery64_2e416m2e208m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 6%nat; + base := 64; bitwidth := 64; s := 2^416; c := [(1, 1); (2^208, 1)]; diff --git a/src/Specific/montgomery64_2e444m17/CurveParameters.v b/src/Specific/montgomery64_2e444m17/CurveParameters.v index d747364ac..6000dfa9b 100644 --- a/src/Specific/montgomery64_2e444m17/CurveParameters.v +++ b/src/Specific/montgomery64_2e444m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 6%nat; + base := 64; bitwidth := 64; s := 2^444; c := [(1, 17)]; diff --git a/src/Specific/montgomery64_2e448m2e224m1/CurveParameters.v b/src/Specific/montgomery64_2e448m2e224m1/CurveParameters.v index 7b7b3e65c..d0871f963 100644 --- a/src/Specific/montgomery64_2e448m2e224m1/CurveParameters.v +++ b/src/Specific/montgomery64_2e448m2e224m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 7%nat; + base := 64; bitwidth := 64; s := 2^448; c := [(1, 1); (2^224, 1)]; diff --git a/src/Specific/montgomery64_2e450m2e225m1/CurveParameters.v b/src/Specific/montgomery64_2e450m2e225m1/CurveParameters.v index 50082723f..1bded1301 100644 --- a/src/Specific/montgomery64_2e450m2e225m1/CurveParameters.v +++ b/src/Specific/montgomery64_2e450m2e225m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 7%nat; + base := 64; bitwidth := 64; s := 2^450; c := [(1, 1); (2^225, 1)]; diff --git a/src/Specific/montgomery64_2e452m3/CurveParameters.v b/src/Specific/montgomery64_2e452m3/CurveParameters.v index 91b59fc14..206b538a4 100644 --- a/src/Specific/montgomery64_2e452m3/CurveParameters.v +++ b/src/Specific/montgomery64_2e452m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 7%nat; + base := 64; bitwidth := 64; s := 2^452; c := [(1, 3)]; diff --git a/src/Specific/montgomery64_2e468m17/CurveParameters.v b/src/Specific/montgomery64_2e468m17/CurveParameters.v index bb4b44300..2881d2193 100644 --- a/src/Specific/montgomery64_2e468m17/CurveParameters.v +++ b/src/Specific/montgomery64_2e468m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 7%nat; + base := 64; bitwidth := 64; s := 2^468; c := [(1, 17)]; diff --git a/src/Specific/montgomery64_2e480m2e240m1/CurveParameters.v b/src/Specific/montgomery64_2e480m2e240m1/CurveParameters.v index 2253d41e9..24c2d43cb 100644 --- a/src/Specific/montgomery64_2e480m2e240m1/CurveParameters.v +++ b/src/Specific/montgomery64_2e480m2e240m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 7%nat; + base := 64; bitwidth := 64; s := 2^480; c := [(1, 1); (2^240, 1)]; diff --git a/src/Specific/montgomery64_2e488m17/CurveParameters.v b/src/Specific/montgomery64_2e488m17/CurveParameters.v index cf9e878f3..bec557569 100644 --- a/src/Specific/montgomery64_2e488m17/CurveParameters.v +++ b/src/Specific/montgomery64_2e488m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 7%nat; + base := 64; bitwidth := 64; s := 2^488; c := [(1, 17)]; diff --git a/src/Specific/montgomery64_2e489m21/CurveParameters.v b/src/Specific/montgomery64_2e489m21/CurveParameters.v index 492fb558a..a54a56a6f 100644 --- a/src/Specific/montgomery64_2e489m21/CurveParameters.v +++ b/src/Specific/montgomery64_2e489m21/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 7%nat; + base := 64; bitwidth := 64; s := 2^489; c := [(1, 21)]; diff --git a/src/Specific/montgomery64_2e495m31/CurveParameters.v b/src/Specific/montgomery64_2e495m31/CurveParameters.v index 223a60eae..724f4d062 100644 --- a/src/Specific/montgomery64_2e495m31/CurveParameters.v +++ b/src/Specific/montgomery64_2e495m31/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 7%nat; + base := 64; bitwidth := 64; s := 2^495; c := [(1, 31)]; diff --git a/src/Specific/montgomery64_2e511m187/CurveParameters.v b/src/Specific/montgomery64_2e511m187/CurveParameters.v index 67ebc276e..01ddf626d 100644 --- a/src/Specific/montgomery64_2e511m187/CurveParameters.v +++ b/src/Specific/montgomery64_2e511m187/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 7%nat; + base := 64; bitwidth := 64; s := 2^511; c := [(1, 187)]; diff --git a/src/Specific/montgomery64_2e511m481/CurveParameters.v b/src/Specific/montgomery64_2e511m481/CurveParameters.v index d989ba385..9b39c3362 100644 --- a/src/Specific/montgomery64_2e511m481/CurveParameters.v +++ b/src/Specific/montgomery64_2e511m481/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 7%nat; + base := 64; bitwidth := 64; s := 2^511; c := [(1, 481)]; diff --git a/src/Specific/montgomery64_2e512m569/CurveParameters.v b/src/Specific/montgomery64_2e512m569/CurveParameters.v index 13caf487e..6cc21b0e5 100644 --- a/src/Specific/montgomery64_2e512m569/CurveParameters.v +++ b/src/Specific/montgomery64_2e512m569/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 8%nat; + base := 64; bitwidth := 64; s := 2^512; c := [(1, 569)]; diff --git a/src/Specific/montgomery64_2e521m1/CurveParameters.v b/src/Specific/montgomery64_2e521m1/CurveParameters.v index bdb86dec8..5f50e8117 100644 --- a/src/Specific/montgomery64_2e521m1/CurveParameters.v +++ b/src/Specific/montgomery64_2e521m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 64 Definition curve : CurveParameters := {| sz := 8%nat; + base := 64; bitwidth := 64; s := 2^521; c := [(1, 1)]; diff --git a/src/Specific/solinas32_2e127m1/CurveParameters.v b/src/Specific/solinas32_2e127m1/CurveParameters.v index a3aeb5dad..88a440104 100644 --- a/src/Specific/solinas32_2e127m1/CurveParameters.v +++ b/src/Specific/solinas32_2e127m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 21 Definition curve : CurveParameters := {| sz := 6%nat; + base := 21; bitwidth := 32; s := 2^127; c := [(1, 1)]; diff --git a/src/Specific/solinas32_2e129m25/CurveParameters.v b/src/Specific/solinas32_2e129m25/CurveParameters.v index 1e1f480b2..751d88025 100644 --- a/src/Specific/solinas32_2e129m25/CurveParameters.v +++ b/src/Specific/solinas32_2e129m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 21 Definition curve : CurveParameters := {| sz := 6%nat; + base := 21; bitwidth := 32; s := 2^129; c := [(1, 25)]; diff --git a/src/Specific/solinas32_2e130m5/CurveParameters.v b/src/Specific/solinas32_2e130m5/CurveParameters.v index 30dbf2e00..e0a411f19 100644 --- a/src/Specific/solinas32_2e130m5/CurveParameters.v +++ b/src/Specific/solinas32_2e130m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 16 Definition curve : CurveParameters := {| sz := 8%nat; + base := 16; bitwidth := 32; s := 2^130; c := [(1, 5)]; diff --git a/src/Specific/solinas32_2e137m13/CurveParameters.v b/src/Specific/solinas32_2e137m13/CurveParameters.v index 13a61ff27..32edba1bf 100644 --- a/src/Specific/solinas32_2e137m13/CurveParameters.v +++ b/src/Specific/solinas32_2e137m13/CurveParameters.v @@ -9,6 +9,7 @@ Base: 17 Definition curve : CurveParameters := {| sz := 8%nat; + base := 17; bitwidth := 32; s := 2^137; c := [(1, 13)]; diff --git a/src/Specific/solinas32_2e140m27/CurveParameters.v b/src/Specific/solinas32_2e140m27/CurveParameters.v index 7704604d7..ff2a817c9 100644 --- a/src/Specific/solinas32_2e140m27/CurveParameters.v +++ b/src/Specific/solinas32_2e140m27/CurveParameters.v @@ -9,6 +9,7 @@ Base: 20 Definition curve : CurveParameters := {| sz := 7%nat; + base := 20; bitwidth := 32; s := 2^140; c := [(1, 27)]; diff --git a/src/Specific/solinas32_2e141m9/CurveParameters.v b/src/Specific/solinas32_2e141m9/CurveParameters.v index 443201dc7..c7cdb8630 100644 --- a/src/Specific/solinas32_2e141m9/CurveParameters.v +++ b/src/Specific/solinas32_2e141m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 20 Definition curve : CurveParameters := {| sz := 7%nat; + base := 20; bitwidth := 32; s := 2^141; c := [(1, 9)]; diff --git a/src/Specific/solinas32_2e150m3/CurveParameters.v b/src/Specific/solinas32_2e150m3/CurveParameters.v index 70f68572c..2ed5af242 100644 --- a/src/Specific/solinas32_2e150m3/CurveParameters.v +++ b/src/Specific/solinas32_2e150m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 25 Definition curve : CurveParameters := {| sz := 6%nat; + base := 25; bitwidth := 32; s := 2^150; c := [(1, 3)]; diff --git a/src/Specific/solinas32_2e150m5/CurveParameters.v b/src/Specific/solinas32_2e150m5/CurveParameters.v index 5f65326ff..fe8170e46 100644 --- a/src/Specific/solinas32_2e150m5/CurveParameters.v +++ b/src/Specific/solinas32_2e150m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 15 Definition curve : CurveParameters := {| sz := 10%nat; + base := 15; bitwidth := 32; s := 2^150; c := [(1, 5)]; diff --git a/src/Specific/solinas32_2e152m17/CurveParameters.v b/src/Specific/solinas32_2e152m17/CurveParameters.v index 162c9a176..846416f46 100644 --- a/src/Specific/solinas32_2e152m17/CurveParameters.v +++ b/src/Specific/solinas32_2e152m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 19 Definition curve : CurveParameters := {| sz := 8%nat; + base := 19; bitwidth := 32; s := 2^152; c := [(1, 17)]; diff --git a/src/Specific/solinas32_2e158m15/CurveParameters.v b/src/Specific/solinas32_2e158m15/CurveParameters.v index aac81cfc9..ba0ee328f 100644 --- a/src/Specific/solinas32_2e158m15/CurveParameters.v +++ b/src/Specific/solinas32_2e158m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 13 Definition curve : CurveParameters := {| sz := 12%nat; + base := 13; bitwidth := 32; s := 2^158; c := [(1, 15)]; diff --git a/src/Specific/solinas32_2e165m25/CurveParameters.v b/src/Specific/solinas32_2e165m25/CurveParameters.v index 36c61dad1..ee2bd7088 100644 --- a/src/Specific/solinas32_2e165m25/CurveParameters.v +++ b/src/Specific/solinas32_2e165m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 18 Definition curve : CurveParameters := {| sz := 9%nat; + base := 18; bitwidth := 32; s := 2^165; c := [(1, 25)]; diff --git a/src/Specific/solinas32_2e166m5/CurveParameters.v b/src/Specific/solinas32_2e166m5/CurveParameters.v index e95606dcb..3cd6d3959 100644 --- a/src/Specific/solinas32_2e166m5/CurveParameters.v +++ b/src/Specific/solinas32_2e166m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 15 Definition curve : CurveParameters := {| sz := 11%nat; + base := 15; bitwidth := 32; s := 2^166; c := [(1, 5)]; diff --git a/src/Specific/solinas32_2e171m19/CurveParameters.v b/src/Specific/solinas32_2e171m19/CurveParameters.v index 121c79854..99b98f018 100644 --- a/src/Specific/solinas32_2e171m19/CurveParameters.v +++ b/src/Specific/solinas32_2e171m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 19 Definition curve : CurveParameters := {| sz := 9%nat; + base := 19; bitwidth := 32; s := 2^171; c := [(1, 19)]; diff --git a/src/Specific/solinas32_2e174m17/CurveParameters.v b/src/Specific/solinas32_2e174m17/CurveParameters.v index bb4d5900d..6df8a62b1 100644 --- a/src/Specific/solinas32_2e174m17/CurveParameters.v +++ b/src/Specific/solinas32_2e174m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 19 Definition curve : CurveParameters := {| sz := 9%nat; + base := 19; bitwidth := 32; s := 2^174; c := [(1, 17)]; diff --git a/src/Specific/solinas32_2e174m3/CurveParameters.v b/src/Specific/solinas32_2e174m3/CurveParameters.v index 544b44105..6cf82b368 100644 --- a/src/Specific/solinas32_2e174m3/CurveParameters.v +++ b/src/Specific/solinas32_2e174m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 19 Definition curve : CurveParameters := {| sz := 9%nat; + base := 19; bitwidth := 32; s := 2^174; c := [(1, 3)]; diff --git a/src/Specific/solinas32_2e189m25/CurveParameters.v b/src/Specific/solinas32_2e189m25/CurveParameters.v index b0856234b..1aac16970 100644 --- a/src/Specific/solinas32_2e189m25/CurveParameters.v +++ b/src/Specific/solinas32_2e189m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 21 Definition curve : CurveParameters := {| sz := 9%nat; + base := 21; bitwidth := 32; s := 2^189; c := [(1, 25)]; diff --git a/src/Specific/solinas32_2e190m11/CurveParameters.v b/src/Specific/solinas32_2e190m11/CurveParameters.v index d2d4bf8f6..36dac4f68 100644 --- a/src/Specific/solinas32_2e190m11/CurveParameters.v +++ b/src/Specific/solinas32_2e190m11/CurveParameters.v @@ -9,6 +9,7 @@ Base: 21 Definition curve : CurveParameters := {| sz := 9%nat; + base := 21; bitwidth := 32; s := 2^190; c := [(1, 11)]; diff --git a/src/Specific/solinas32_2e191m19/CurveParameters.v b/src/Specific/solinas32_2e191m19/CurveParameters.v index 9736c3d90..cf183ae40 100644 --- a/src/Specific/solinas32_2e191m19/CurveParameters.v +++ b/src/Specific/solinas32_2e191m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 19 Definition curve : CurveParameters := {| sz := 10%nat; + base := 19; bitwidth := 32; s := 2^191; c := [(1, 19)]; diff --git a/src/Specific/solinas32_2e192m2e64m1/CurveParameters.v b/src/Specific/solinas32_2e192m2e64m1/CurveParameters.v index 0d40d5e8f..637a7628f 100644 --- a/src/Specific/solinas32_2e192m2e64m1/CurveParameters.v +++ b/src/Specific/solinas32_2e192m2e64m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 24 Definition curve : CurveParameters := {| sz := 8%nat; + base := 24; bitwidth := 32; s := 2^192; c := [(1, 1); (2^64, 1)]; diff --git a/src/Specific/solinas32_2e194m33/CurveParameters.v b/src/Specific/solinas32_2e194m33/CurveParameters.v index ac714a6de..7b82a6d88 100644 --- a/src/Specific/solinas32_2e194m33/CurveParameters.v +++ b/src/Specific/solinas32_2e194m33/CurveParameters.v @@ -9,6 +9,7 @@ Base: 16 Definition curve : CurveParameters := {| sz := 12%nat; + base := 16; bitwidth := 32; s := 2^194; c := [(1, 33)]; diff --git a/src/Specific/solinas32_2e196m15/CurveParameters.v b/src/Specific/solinas32_2e196m15/CurveParameters.v index 5f1ca68b8..1bbe7a4b8 100644 --- a/src/Specific/solinas32_2e196m15/CurveParameters.v +++ b/src/Specific/solinas32_2e196m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 24 Definition curve : CurveParameters := {| sz := 8%nat; + base := 24; bitwidth := 32; s := 2^196; c := [(1, 15)]; diff --git a/src/Specific/solinas32_2e198m17/CurveParameters.v b/src/Specific/solinas32_2e198m17/CurveParameters.v index 613beefd0..79185d696 100644 --- a/src/Specific/solinas32_2e198m17/CurveParameters.v +++ b/src/Specific/solinas32_2e198m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 22 Definition curve : CurveParameters := {| sz := 9%nat; + base := 22; bitwidth := 32; s := 2^198; c := [(1, 17)]; diff --git a/src/Specific/solinas32_2e206m5/CurveParameters.v b/src/Specific/solinas32_2e206m5/CurveParameters.v index 04d6be18a..07f9d3f4c 100644 --- a/src/Specific/solinas32_2e206m5/CurveParameters.v +++ b/src/Specific/solinas32_2e206m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 17 Definition curve : CurveParameters := {| sz := 12%nat; + base := 17; bitwidth := 32; s := 2^206; c := [(1, 5)]; diff --git a/src/Specific/solinas32_2e212m29/CurveParameters.v b/src/Specific/solinas32_2e212m29/CurveParameters.v index fd99bbe99..fe09da328 100644 --- a/src/Specific/solinas32_2e212m29/CurveParameters.v +++ b/src/Specific/solinas32_2e212m29/CurveParameters.v @@ -9,6 +9,7 @@ Base: 21 Definition curve : CurveParameters := {| sz := 10%nat; + base := 21; bitwidth := 32; s := 2^212; c := [(1, 29)]; diff --git a/src/Specific/solinas32_2e213m3/CurveParameters.v b/src/Specific/solinas32_2e213m3/CurveParameters.v index ea06c10d9..693c68174 100644 --- a/src/Specific/solinas32_2e213m3/CurveParameters.v +++ b/src/Specific/solinas32_2e213m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 14 Definition curve : CurveParameters := {| sz := 15%nat; + base := 14; bitwidth := 32; s := 2^213; c := [(1, 3)]; diff --git a/src/Specific/solinas32_2e216m2e108m1/CurveParameters.v b/src/Specific/solinas32_2e216m2e108m1/CurveParameters.v index 594e4ca55..ba0dcf76e 100644 --- a/src/Specific/solinas32_2e216m2e108m1/CurveParameters.v +++ b/src/Specific/solinas32_2e216m2e108m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 27 Definition curve : CurveParameters := {| sz := 8%nat; + base := 27; bitwidth := 32; s := 2^216; c := [(1, 1); (2^108, 1)]; diff --git a/src/Specific/solinas32_2e221m3/CurveParameters.v b/src/Specific/solinas32_2e221m3/CurveParameters.v index ade81eefc..8577ba6df 100644 --- a/src/Specific/solinas32_2e221m3/CurveParameters.v +++ b/src/Specific/solinas32_2e221m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 22 Definition curve : CurveParameters := {| sz := 10%nat; + base := 22; bitwidth := 32; s := 2^221; c := [(1, 3)]; diff --git a/src/Specific/solinas32_2e222m117/CurveParameters.v b/src/Specific/solinas32_2e222m117/CurveParameters.v index add4aaab2..37ac18bee 100644 --- a/src/Specific/solinas32_2e222m117/CurveParameters.v +++ b/src/Specific/solinas32_2e222m117/CurveParameters.v @@ -9,6 +9,7 @@ Base: 22 Definition curve : CurveParameters := {| sz := 10%nat; + base := 22; bitwidth := 32; s := 2^222; c := [(1, 117)]; diff --git a/src/Specific/solinas32_2e224m2e96p1/CurveParameters.v b/src/Specific/solinas32_2e224m2e96p1/CurveParameters.v index ace0603b4..1b39c9806 100644 --- a/src/Specific/solinas32_2e224m2e96p1/CurveParameters.v +++ b/src/Specific/solinas32_2e224m2e96p1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 28 Definition curve : CurveParameters := {| sz := 8%nat; + base := 28; bitwidth := 32; s := 2^224; c := [(1, -1); (2^96, 1)]; diff --git a/src/Specific/solinas32_2e226m5/CurveParameters.v b/src/Specific/solinas32_2e226m5/CurveParameters.v index 96417aa62..4db734035 100644 --- a/src/Specific/solinas32_2e226m5/CurveParameters.v +++ b/src/Specific/solinas32_2e226m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 25 Definition curve : CurveParameters := {| sz := 9%nat; + base := 25; bitwidth := 32; s := 2^226; c := [(1, 5)]; diff --git a/src/Specific/solinas32_2e230m27/CurveParameters.v b/src/Specific/solinas32_2e230m27/CurveParameters.v index e5be42277..bc7f75394 100644 --- a/src/Specific/solinas32_2e230m27/CurveParameters.v +++ b/src/Specific/solinas32_2e230m27/CurveParameters.v @@ -9,6 +9,7 @@ Base: 23 Definition curve : CurveParameters := {| sz := 10%nat; + base := 23; bitwidth := 32; s := 2^230; c := [(1, 27)]; diff --git a/src/Specific/solinas32_2e235m15/CurveParameters.v b/src/Specific/solinas32_2e235m15/CurveParameters.v index 43a282935..4bc71e156 100644 --- a/src/Specific/solinas32_2e235m15/CurveParameters.v +++ b/src/Specific/solinas32_2e235m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 23 Definition curve : CurveParameters := {| sz := 10%nat; + base := 23; bitwidth := 32; s := 2^235; c := [(1, 15)]; diff --git a/src/Specific/solinas32_2e243m9/CurveParameters.v b/src/Specific/solinas32_2e243m9/CurveParameters.v index 07cae3d4b..e71d50e3a 100644 --- a/src/Specific/solinas32_2e243m9/CurveParameters.v +++ b/src/Specific/solinas32_2e243m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 22 Definition curve : CurveParameters := {| sz := 11%nat; + base := 22; bitwidth := 32; s := 2^243; c := [(1, 9)]; diff --git a/src/Specific/solinas32_2e251m9/CurveParameters.v b/src/Specific/solinas32_2e251m9/CurveParameters.v index e15731335..257923486 100644 --- a/src/Specific/solinas32_2e251m9/CurveParameters.v +++ b/src/Specific/solinas32_2e251m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 25 Definition curve : CurveParameters := {| sz := 10%nat; + base := 25; bitwidth := 32; s := 2^251; c := [(1, 9)]; diff --git a/src/Specific/solinas32_2e255m19/CurveParameters.v b/src/Specific/solinas32_2e255m19/CurveParameters.v index c573e5a8d..13ab57fb6 100644 --- a/src/Specific/solinas32_2e255m19/CurveParameters.v +++ b/src/Specific/solinas32_2e255m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 21 Definition curve : CurveParameters := {| sz := 12%nat; + base := 21; bitwidth := 32; s := 2^255; c := [(1, 19)]; diff --git a/src/Specific/solinas32_2e255m2e4m2e1m1/CurveParameters.v b/src/Specific/solinas32_2e255m2e4m2e1m1/CurveParameters.v index 3e10b2177..9506e6f5b 100644 --- a/src/Specific/solinas32_2e255m2e4m2e1m1/CurveParameters.v +++ b/src/Specific/solinas32_2e255m2e4m2e1m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 28 Definition curve : CurveParameters := {| sz := 9%nat; + base := 28; bitwidth := 32; s := 2^255; c := [(1, 1); (2^1, 1); (2^4, 1)]; diff --git a/src/Specific/solinas32_2e255m765/CurveParameters.v b/src/Specific/solinas32_2e255m765/CurveParameters.v index 268c5ff7c..898e743f0 100644 --- a/src/Specific/solinas32_2e255m765/CurveParameters.v +++ b/src/Specific/solinas32_2e255m765/CurveParameters.v @@ -9,6 +9,7 @@ Base: 17 Definition curve : CurveParameters := {| sz := 15%nat; + base := 17; bitwidth := 32; s := 2^255; c := [(1, 765)]; diff --git a/src/Specific/solinas32_2e256m189/CurveParameters.v b/src/Specific/solinas32_2e256m189/CurveParameters.v index 5d7ef9fd4..9323a1385 100644 --- a/src/Specific/solinas32_2e256m189/CurveParameters.v +++ b/src/Specific/solinas32_2e256m189/CurveParameters.v @@ -9,6 +9,7 @@ Base: 21 Definition curve : CurveParameters := {| sz := 12%nat; + base := 21; bitwidth := 32; s := 2^256; c := [(1, 189)]; diff --git a/src/Specific/solinas32_2e256m2e224p2e192p2e96m1/CurveParameters.v b/src/Specific/solinas32_2e256m2e224p2e192p2e96m1/CurveParameters.v index e9433584a..05eb83f42 100644 --- a/src/Specific/solinas32_2e256m2e224p2e192p2e96m1/CurveParameters.v +++ b/src/Specific/solinas32_2e256m2e224p2e192p2e96m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 21 Definition curve : CurveParameters := {| sz := 12%nat; + base := 21; bitwidth := 32; s := 2^256; c := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]; diff --git a/src/Specific/solinas32_2e256m2e32m977/CurveParameters.v b/src/Specific/solinas32_2e256m2e32m977/CurveParameters.v index 088b65e8c..e708379b5 100644 --- a/src/Specific/solinas32_2e256m2e32m977/CurveParameters.v +++ b/src/Specific/solinas32_2e256m2e32m977/CurveParameters.v @@ -9,6 +9,7 @@ Base: 17 Definition curve : CurveParameters := {| sz := 15%nat; + base := 17; bitwidth := 32; s := 2^256; c := [(1, 977); (2^32, 1)]; diff --git a/src/Specific/solinas32_2e266m3/CurveParameters.v b/src/Specific/solinas32_2e266m3/CurveParameters.v index fe4026d1a..a11f58861 100644 --- a/src/Specific/solinas32_2e266m3/CurveParameters.v +++ b/src/Specific/solinas32_2e266m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 22 Definition curve : CurveParameters := {| sz := 12%nat; + base := 22; bitwidth := 32; s := 2^266; c := [(1, 3)]; diff --git a/src/Specific/solinas32_2e285m9/CurveParameters.v b/src/Specific/solinas32_2e285m9/CurveParameters.v index f969bd7d9..c27410c3a 100644 --- a/src/Specific/solinas32_2e285m9/CurveParameters.v +++ b/src/Specific/solinas32_2e285m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 19 Definition curve : CurveParameters := {| sz := 15%nat; + base := 19; bitwidth := 32; s := 2^285; c := [(1, 9)]; diff --git a/src/Specific/solinas32_2e291m19/CurveParameters.v b/src/Specific/solinas32_2e291m19/CurveParameters.v index 90ab80cf8..16ebd3202 100644 --- a/src/Specific/solinas32_2e291m19/CurveParameters.v +++ b/src/Specific/solinas32_2e291m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 24 Definition curve : CurveParameters := {| sz := 12%nat; + base := 24; bitwidth := 32; s := 2^291; c := [(1, 19)]; diff --git a/src/Specific/solinas32_2e321m9/CurveParameters.v b/src/Specific/solinas32_2e321m9/CurveParameters.v index edc1f33f3..82d6f50d3 100644 --- a/src/Specific/solinas32_2e321m9/CurveParameters.v +++ b/src/Specific/solinas32_2e321m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 20 Definition curve : CurveParameters := {| sz := 16%nat; + base := 20; bitwidth := 32; s := 2^321; c := [(1, 9)]; diff --git a/src/Specific/solinas32_2e322m2e161m1/CurveParameters.v b/src/Specific/solinas32_2e322m2e161m1/CurveParameters.v index 72aebc8bb..3665be7ea 100644 --- a/src/Specific/solinas32_2e322m2e161m1/CurveParameters.v +++ b/src/Specific/solinas32_2e322m2e161m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 23 Definition curve : CurveParameters := {| sz := 14%nat; + base := 23; bitwidth := 32; s := 2^322; c := [(1, 1); (2^161, 1)]; diff --git a/src/Specific/solinas32_2e336m17/CurveParameters.v b/src/Specific/solinas32_2e336m17/CurveParameters.v index c1b6bdb75..2b85734fb 100644 --- a/src/Specific/solinas32_2e336m17/CurveParameters.v +++ b/src/Specific/solinas32_2e336m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 24 Definition curve : CurveParameters := {| sz := 14%nat; + base := 24; bitwidth := 32; s := 2^336; c := [(1, 17)]; diff --git a/src/Specific/solinas32_2e336m3/CurveParameters.v b/src/Specific/solinas32_2e336m3/CurveParameters.v index fb888dece..4a66a5dee 100644 --- a/src/Specific/solinas32_2e336m3/CurveParameters.v +++ b/src/Specific/solinas32_2e336m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 24 Definition curve : CurveParameters := {| sz := 14%nat; + base := 24; bitwidth := 32; s := 2^336; c := [(1, 3)]; diff --git a/src/Specific/solinas32_2e338m15/CurveParameters.v b/src/Specific/solinas32_2e338m15/CurveParameters.v index 090c2507d..bf960a8cd 100644 --- a/src/Specific/solinas32_2e338m15/CurveParameters.v +++ b/src/Specific/solinas32_2e338m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 24 Definition curve : CurveParameters := {| sz := 14%nat; + base := 24; bitwidth := 32; s := 2^338; c := [(1, 15)]; diff --git a/src/Specific/solinas32_2e369m25/CurveParameters.v b/src/Specific/solinas32_2e369m25/CurveParameters.v index 5e3cf4a01..e2d2792a1 100644 --- a/src/Specific/solinas32_2e369m25/CurveParameters.v +++ b/src/Specific/solinas32_2e369m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 23 Definition curve : CurveParameters := {| sz := 16%nat; + base := 23; bitwidth := 32; s := 2^369; c := [(1, 25)]; diff --git a/src/Specific/solinas32_2e379m19/CurveParameters.v b/src/Specific/solinas32_2e379m19/CurveParameters.v index 317295beb..597eb60c8 100644 --- a/src/Specific/solinas32_2e379m19/CurveParameters.v +++ b/src/Specific/solinas32_2e379m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 21 Definition curve : CurveParameters := {| sz := 18%nat; + base := 21; bitwidth := 32; s := 2^379; c := [(1, 19)]; diff --git a/src/Specific/solinas32_2e382m105/CurveParameters.v b/src/Specific/solinas32_2e382m105/CurveParameters.v index e7359580e..fc8d8de2f 100644 --- a/src/Specific/solinas32_2e382m105/CurveParameters.v +++ b/src/Specific/solinas32_2e382m105/CurveParameters.v @@ -9,6 +9,7 @@ Base: 19 Definition curve : CurveParameters := {| sz := 20%nat; + base := 19; bitwidth := 32; s := 2^382; c := [(1, 105)]; diff --git a/src/Specific/solinas32_2e384m2e128m2e96p2e32m1/CurveParameters.v b/src/Specific/solinas32_2e384m2e128m2e96p2e32m1/CurveParameters.v index b29950df3..665b52900 100644 --- a/src/Specific/solinas32_2e384m2e128m2e96p2e32m1/CurveParameters.v +++ b/src/Specific/solinas32_2e384m2e128m2e96p2e32m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 24 Definition curve : CurveParameters := {| sz := 16%nat; + base := 24; bitwidth := 32; s := 2^384; c := [(1, 1); (2^32, -1); (2^96, 1); (2^128, 1)]; diff --git a/src/Specific/solinas32_2e384m317/CurveParameters.v b/src/Specific/solinas32_2e384m317/CurveParameters.v index 2d9bf6263..bd88da389 100644 --- a/src/Specific/solinas32_2e384m317/CurveParameters.v +++ b/src/Specific/solinas32_2e384m317/CurveParameters.v @@ -9,6 +9,7 @@ Base: 21 Definition curve : CurveParameters := {| sz := 18%nat; + base := 21; bitwidth := 32; s := 2^384; c := [(1, 317)]; diff --git a/src/Specific/solinas32_2e401m31/CurveParameters.v b/src/Specific/solinas32_2e401m31/CurveParameters.v index 3fea51421..b0e9112f4 100644 --- a/src/Specific/solinas32_2e401m31/CurveParameters.v +++ b/src/Specific/solinas32_2e401m31/CurveParameters.v @@ -9,6 +9,7 @@ Base: 25 Definition curve : CurveParameters := {| sz := 16%nat; + base := 25; bitwidth := 32; s := 2^401; c := [(1, 31)]; diff --git a/src/Specific/solinas32_2e413m21/CurveParameters.v b/src/Specific/solinas32_2e413m21/CurveParameters.v index 4b3a212e3..8d245211d 100644 --- a/src/Specific/solinas32_2e413m21/CurveParameters.v +++ b/src/Specific/solinas32_2e413m21/CurveParameters.v @@ -9,6 +9,7 @@ Base: 7 Definition curve : CurveParameters := {| sz := 59%nat; + base := 7; bitwidth := 32; s := 2^413; c := [(1, 21)]; diff --git a/src/Specific/solinas32_2e414m17/CurveParameters.v b/src/Specific/solinas32_2e414m17/CurveParameters.v index da96fb060..803e45369 100644 --- a/src/Specific/solinas32_2e414m17/CurveParameters.v +++ b/src/Specific/solinas32_2e414m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 23 Definition curve : CurveParameters := {| sz := 18%nat; + base := 23; bitwidth := 32; s := 2^414; c := [(1, 17)]; diff --git a/src/Specific/solinas32_2e416m2e208m1/CurveParameters.v b/src/Specific/solinas32_2e416m2e208m1/CurveParameters.v index 6295a0867..b8347211e 100644 --- a/src/Specific/solinas32_2e416m2e208m1/CurveParameters.v +++ b/src/Specific/solinas32_2e416m2e208m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 26 Definition curve : CurveParameters := {| sz := 16%nat; + base := 26; bitwidth := 32; s := 2^416; c := [(1, 1); (2^208, 1)]; diff --git a/src/Specific/solinas32_2e444m17/CurveParameters.v b/src/Specific/solinas32_2e444m17/CurveParameters.v index 0bc85cf21..45727d7b0 100644 --- a/src/Specific/solinas32_2e444m17/CurveParameters.v +++ b/src/Specific/solinas32_2e444m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 22 Definition curve : CurveParameters := {| sz := 20%nat; + base := 22; bitwidth := 32; s := 2^444; c := [(1, 17)]; diff --git a/src/Specific/solinas32_2e448m2e224m1/CurveParameters.v b/src/Specific/solinas32_2e448m2e224m1/CurveParameters.v index 3b8d4e8ee..11bb6b4e2 100644 --- a/src/Specific/solinas32_2e448m2e224m1/CurveParameters.v +++ b/src/Specific/solinas32_2e448m2e224m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 28 Definition curve : CurveParameters := {| sz := 16%nat; + base := 28; bitwidth := 32; s := 2^448; c := [(1, 1); (2^224, 1)]; diff --git a/src/Specific/solinas32_2e450m2e225m1/CurveParameters.v b/src/Specific/solinas32_2e450m2e225m1/CurveParameters.v index f7216034e..eb7e3f444 100644 --- a/src/Specific/solinas32_2e450m2e225m1/CurveParameters.v +++ b/src/Specific/solinas32_2e450m2e225m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 28 Definition curve : CurveParameters := {| sz := 16%nat; + base := 28; bitwidth := 32; s := 2^450; c := [(1, 1); (2^225, 1)]; diff --git a/src/Specific/solinas32_2e452m3/CurveParameters.v b/src/Specific/solinas32_2e452m3/CurveParameters.v index bf185327f..e87f46107 100644 --- a/src/Specific/solinas32_2e452m3/CurveParameters.v +++ b/src/Specific/solinas32_2e452m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 25 Definition curve : CurveParameters := {| sz := 18%nat; + base := 25; bitwidth := 32; s := 2^452; c := [(1, 3)]; diff --git a/src/Specific/solinas32_2e468m17/CurveParameters.v b/src/Specific/solinas32_2e468m17/CurveParameters.v index 0e05fc82f..e44d7b682 100644 --- a/src/Specific/solinas32_2e468m17/CurveParameters.v +++ b/src/Specific/solinas32_2e468m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 19 Definition curve : CurveParameters := {| sz := 24%nat; + base := 19; bitwidth := 32; s := 2^468; c := [(1, 17)]; diff --git a/src/Specific/solinas32_2e480m2e240m1/CurveParameters.v b/src/Specific/solinas32_2e480m2e240m1/CurveParameters.v index 45051abd7..3c9b6dc39 100644 --- a/src/Specific/solinas32_2e480m2e240m1/CurveParameters.v +++ b/src/Specific/solinas32_2e480m2e240m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 30 Definition curve : CurveParameters := {| sz := 16%nat; + base := 30; bitwidth := 32; s := 2^480; c := [(1, 1); (2^240, 1)]; diff --git a/src/Specific/solinas32_2e488m17/CurveParameters.v b/src/Specific/solinas32_2e488m17/CurveParameters.v index 9c4a57305..910254a3d 100644 --- a/src/Specific/solinas32_2e488m17/CurveParameters.v +++ b/src/Specific/solinas32_2e488m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 20 Definition curve : CurveParameters := {| sz := 24%nat; + base := 20; bitwidth := 32; s := 2^488; c := [(1, 17)]; diff --git a/src/Specific/solinas32_2e489m21/CurveParameters.v b/src/Specific/solinas32_2e489m21/CurveParameters.v index 465fcdf01..5e42cf526 100644 --- a/src/Specific/solinas32_2e489m21/CurveParameters.v +++ b/src/Specific/solinas32_2e489m21/CurveParameters.v @@ -9,6 +9,7 @@ Base: 18 Definition curve : CurveParameters := {| sz := 27%nat; + base := 18; bitwidth := 32; s := 2^489; c := [(1, 21)]; diff --git a/src/Specific/solinas32_2e495m31/CurveParameters.v b/src/Specific/solinas32_2e495m31/CurveParameters.v index ea520666f..2f2b48858 100644 --- a/src/Specific/solinas32_2e495m31/CurveParameters.v +++ b/src/Specific/solinas32_2e495m31/CurveParameters.v @@ -9,6 +9,7 @@ Base: 22 Definition curve : CurveParameters := {| sz := 22%nat; + base := 22; bitwidth := 32; s := 2^495; c := [(1, 31)]; diff --git a/src/Specific/solinas32_2e511m187/CurveParameters.v b/src/Specific/solinas32_2e511m187/CurveParameters.v index c5bce978f..c6afd0f11 100644 --- a/src/Specific/solinas32_2e511m187/CurveParameters.v +++ b/src/Specific/solinas32_2e511m187/CurveParameters.v @@ -9,6 +9,7 @@ Base: 18 Definition curve : CurveParameters := {| sz := 28%nat; + base := 18; bitwidth := 32; s := 2^511; c := [(1, 187)]; diff --git a/src/Specific/solinas32_2e511m481/CurveParameters.v b/src/Specific/solinas32_2e511m481/CurveParameters.v index 839b27383..de877ff5b 100644 --- a/src/Specific/solinas32_2e511m481/CurveParameters.v +++ b/src/Specific/solinas32_2e511m481/CurveParameters.v @@ -9,6 +9,7 @@ Base: 18 Definition curve : CurveParameters := {| sz := 28%nat; + base := 18; bitwidth := 32; s := 2^511; c := [(1, 481)]; diff --git a/src/Specific/solinas32_2e512m569/CurveParameters.v b/src/Specific/solinas32_2e512m569/CurveParameters.v index 5e3245006..bc0433f2c 100644 --- a/src/Specific/solinas32_2e512m569/CurveParameters.v +++ b/src/Specific/solinas32_2e512m569/CurveParameters.v @@ -9,6 +9,7 @@ Base: 17 Definition curve : CurveParameters := {| sz := 30%nat; + base := 17; bitwidth := 32; s := 2^512; c := [(1, 569)]; diff --git a/src/Specific/solinas32_2e521m1/CurveParameters.v b/src/Specific/solinas32_2e521m1/CurveParameters.v index 6bd17770f..e5a6dfa8a 100644 --- a/src/Specific/solinas32_2e521m1/CurveParameters.v +++ b/src/Specific/solinas32_2e521m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 26 Definition curve : CurveParameters := {| sz := 20%nat; + base := 26; bitwidth := 32; s := 2^521; c := [(1, 1)]; diff --git a/src/Specific/solinas64_2e127m1/CurveParameters.v b/src/Specific/solinas64_2e127m1/CurveParameters.v index 8af535441..585295358 100644 --- a/src/Specific/solinas64_2e127m1/CurveParameters.v +++ b/src/Specific/solinas64_2e127m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 42 Definition curve : CurveParameters := {| sz := 3%nat; + base := 42; bitwidth := 64; s := 2^127; c := [(1, 1)]; diff --git a/src/Specific/solinas64_2e129m25/CurveParameters.v b/src/Specific/solinas64_2e129m25/CurveParameters.v index 7f4e537a8..832c97c99 100644 --- a/src/Specific/solinas64_2e129m25/CurveParameters.v +++ b/src/Specific/solinas64_2e129m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 4%nat; + base := 32; bitwidth := 64; s := 2^129; c := [(1, 25)]; diff --git a/src/Specific/solinas64_2e130m5/CurveParameters.v b/src/Specific/solinas64_2e130m5/CurveParameters.v index bb1ca71ec..b1ede3d74 100644 --- a/src/Specific/solinas64_2e130m5/CurveParameters.v +++ b/src/Specific/solinas64_2e130m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 4%nat; + base := 32; bitwidth := 64; s := 2^130; c := [(1, 5)]; diff --git a/src/Specific/solinas64_2e137m13/CurveParameters.v b/src/Specific/solinas64_2e137m13/CurveParameters.v index 6692e0d94..97f952285 100644 --- a/src/Specific/solinas64_2e137m13/CurveParameters.v +++ b/src/Specific/solinas64_2e137m13/CurveParameters.v @@ -9,6 +9,7 @@ Base: 34 Definition curve : CurveParameters := {| sz := 4%nat; + base := 34; bitwidth := 64; s := 2^137; c := [(1, 13)]; diff --git a/src/Specific/solinas64_2e140m27/CurveParameters.v b/src/Specific/solinas64_2e140m27/CurveParameters.v index b202655ba..1fa077d48 100644 --- a/src/Specific/solinas64_2e140m27/CurveParameters.v +++ b/src/Specific/solinas64_2e140m27/CurveParameters.v @@ -9,6 +9,7 @@ Base: 35 Definition curve : CurveParameters := {| sz := 4%nat; + base := 35; bitwidth := 64; s := 2^140; c := [(1, 27)]; diff --git a/src/Specific/solinas64_2e141m9/CurveParameters.v b/src/Specific/solinas64_2e141m9/CurveParameters.v index c8ba55e0c..42a59b213 100644 --- a/src/Specific/solinas64_2e141m9/CurveParameters.v +++ b/src/Specific/solinas64_2e141m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 35 Definition curve : CurveParameters := {| sz := 4%nat; + base := 35; bitwidth := 64; s := 2^141; c := [(1, 9)]; diff --git a/src/Specific/solinas64_2e150m3/CurveParameters.v b/src/Specific/solinas64_2e150m3/CurveParameters.v index 5f26d8bd0..263868b60 100644 --- a/src/Specific/solinas64_2e150m3/CurveParameters.v +++ b/src/Specific/solinas64_2e150m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 37 Definition curve : CurveParameters := {| sz := 4%nat; + base := 37; bitwidth := 64; s := 2^150; c := [(1, 3)]; diff --git a/src/Specific/solinas64_2e150m5/CurveParameters.v b/src/Specific/solinas64_2e150m5/CurveParameters.v index 2746bcc0a..967425999 100644 --- a/src/Specific/solinas64_2e150m5/CurveParameters.v +++ b/src/Specific/solinas64_2e150m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 37 Definition curve : CurveParameters := {| sz := 4%nat; + base := 37; bitwidth := 64; s := 2^150; c := [(1, 5)]; diff --git a/src/Specific/solinas64_2e152m17/CurveParameters.v b/src/Specific/solinas64_2e152m17/CurveParameters.v index 44bd56245..2ff237959 100644 --- a/src/Specific/solinas64_2e152m17/CurveParameters.v +++ b/src/Specific/solinas64_2e152m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 38 Definition curve : CurveParameters := {| sz := 4%nat; + base := 38; bitwidth := 64; s := 2^152; c := [(1, 17)]; diff --git a/src/Specific/solinas64_2e158m15/CurveParameters.v b/src/Specific/solinas64_2e158m15/CurveParameters.v index 53e537787..1fa028164 100644 --- a/src/Specific/solinas64_2e158m15/CurveParameters.v +++ b/src/Specific/solinas64_2e158m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 39 Definition curve : CurveParameters := {| sz := 4%nat; + base := 39; bitwidth := 64; s := 2^158; c := [(1, 15)]; diff --git a/src/Specific/solinas64_2e165m25/CurveParameters.v b/src/Specific/solinas64_2e165m25/CurveParameters.v index 02fed3fb8..c89b7b5d7 100644 --- a/src/Specific/solinas64_2e165m25/CurveParameters.v +++ b/src/Specific/solinas64_2e165m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 41 Definition curve : CurveParameters := {| sz := 4%nat; + base := 41; bitwidth := 64; s := 2^165; c := [(1, 25)]; diff --git a/src/Specific/solinas64_2e166m5/CurveParameters.v b/src/Specific/solinas64_2e166m5/CurveParameters.v index a67ae8cbf..beb1332fe 100644 --- a/src/Specific/solinas64_2e166m5/CurveParameters.v +++ b/src/Specific/solinas64_2e166m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 41 Definition curve : CurveParameters := {| sz := 4%nat; + base := 41; bitwidth := 64; s := 2^166; c := [(1, 5)]; diff --git a/src/Specific/solinas64_2e171m19/CurveParameters.v b/src/Specific/solinas64_2e171m19/CurveParameters.v index d6798ba7c..6b885508b 100644 --- a/src/Specific/solinas64_2e171m19/CurveParameters.v +++ b/src/Specific/solinas64_2e171m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 34 Definition curve : CurveParameters := {| sz := 5%nat; + base := 34; bitwidth := 64; s := 2^171; c := [(1, 19)]; diff --git a/src/Specific/solinas64_2e174m17/CurveParameters.v b/src/Specific/solinas64_2e174m17/CurveParameters.v index cf37cd033..79fc4445d 100644 --- a/src/Specific/solinas64_2e174m17/CurveParameters.v +++ b/src/Specific/solinas64_2e174m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 43 Definition curve : CurveParameters := {| sz := 4%nat; + base := 43; bitwidth := 64; s := 2^174; c := [(1, 17)]; diff --git a/src/Specific/solinas64_2e174m3/CurveParameters.v b/src/Specific/solinas64_2e174m3/CurveParameters.v index d0c91efc6..74521ff93 100644 --- a/src/Specific/solinas64_2e174m3/CurveParameters.v +++ b/src/Specific/solinas64_2e174m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 43 Definition curve : CurveParameters := {| sz := 4%nat; + base := 43; bitwidth := 64; s := 2^174; c := [(1, 3)]; diff --git a/src/Specific/solinas64_2e189m25/CurveParameters.v b/src/Specific/solinas64_2e189m25/CurveParameters.v index 082da31cb..a79eb839e 100644 --- a/src/Specific/solinas64_2e189m25/CurveParameters.v +++ b/src/Specific/solinas64_2e189m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 31 Definition curve : CurveParameters := {| sz := 6%nat; + base := 31; bitwidth := 64; s := 2^189; c := [(1, 25)]; diff --git a/src/Specific/solinas64_2e190m11/CurveParameters.v b/src/Specific/solinas64_2e190m11/CurveParameters.v index 82d0e9712..fff8cf373 100644 --- a/src/Specific/solinas64_2e190m11/CurveParameters.v +++ b/src/Specific/solinas64_2e190m11/CurveParameters.v @@ -9,6 +9,7 @@ Base: 38 Definition curve : CurveParameters := {| sz := 5%nat; + base := 38; bitwidth := 64; s := 2^190; c := [(1, 11)]; diff --git a/src/Specific/solinas64_2e191m19/CurveParameters.v b/src/Specific/solinas64_2e191m19/CurveParameters.v index 9d7333943..680cd5a1e 100644 --- a/src/Specific/solinas64_2e191m19/CurveParameters.v +++ b/src/Specific/solinas64_2e191m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 38 Definition curve : CurveParameters := {| sz := 5%nat; + base := 38; bitwidth := 64; s := 2^191; c := [(1, 19)]; diff --git a/src/Specific/solinas64_2e192m2e64m1/CurveParameters.v b/src/Specific/solinas64_2e192m2e64m1/CurveParameters.v index 9505f7190..5b497fc51 100644 --- a/src/Specific/solinas64_2e192m2e64m1/CurveParameters.v +++ b/src/Specific/solinas64_2e192m2e64m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 48 Definition curve : CurveParameters := {| sz := 4%nat; + base := 48; bitwidth := 64; s := 2^192; c := [(1, 1); (2^64, 1)]; diff --git a/src/Specific/solinas64_2e194m33/CurveParameters.v b/src/Specific/solinas64_2e194m33/CurveParameters.v index c0d42734b..6ae7ab953 100644 --- a/src/Specific/solinas64_2e194m33/CurveParameters.v +++ b/src/Specific/solinas64_2e194m33/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 6%nat; + base := 32; bitwidth := 64; s := 2^194; c := [(1, 33)]; diff --git a/src/Specific/solinas64_2e196m15/CurveParameters.v b/src/Specific/solinas64_2e196m15/CurveParameters.v index 465198151..920939b0b 100644 --- a/src/Specific/solinas64_2e196m15/CurveParameters.v +++ b/src/Specific/solinas64_2e196m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 39 Definition curve : CurveParameters := {| sz := 5%nat; + base := 39; bitwidth := 64; s := 2^196; c := [(1, 15)]; diff --git a/src/Specific/solinas64_2e198m17/CurveParameters.v b/src/Specific/solinas64_2e198m17/CurveParameters.v index 2a5a102d0..689c9cf14 100644 --- a/src/Specific/solinas64_2e198m17/CurveParameters.v +++ b/src/Specific/solinas64_2e198m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 33 Definition curve : CurveParameters := {| sz := 6%nat; + base := 33; bitwidth := 64; s := 2^198; c := [(1, 17)]; diff --git a/src/Specific/solinas64_2e206m5/CurveParameters.v b/src/Specific/solinas64_2e206m5/CurveParameters.v index 23248bbc1..40d0bf636 100644 --- a/src/Specific/solinas64_2e206m5/CurveParameters.v +++ b/src/Specific/solinas64_2e206m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 41 Definition curve : CurveParameters := {| sz := 5%nat; + base := 41; bitwidth := 64; s := 2^206; c := [(1, 5)]; diff --git a/src/Specific/solinas64_2e212m29/CurveParameters.v b/src/Specific/solinas64_2e212m29/CurveParameters.v index 81e47c234..93575351f 100644 --- a/src/Specific/solinas64_2e212m29/CurveParameters.v +++ b/src/Specific/solinas64_2e212m29/CurveParameters.v @@ -9,6 +9,7 @@ Base: 35 Definition curve : CurveParameters := {| sz := 6%nat; + base := 35; bitwidth := 64; s := 2^212; c := [(1, 29)]; diff --git a/src/Specific/solinas64_2e213m3/CurveParameters.v b/src/Specific/solinas64_2e213m3/CurveParameters.v index 0219e4f79..4aaa1b85a 100644 --- a/src/Specific/solinas64_2e213m3/CurveParameters.v +++ b/src/Specific/solinas64_2e213m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 35 Definition curve : CurveParameters := {| sz := 6%nat; + base := 35; bitwidth := 64; s := 2^213; c := [(1, 3)]; diff --git a/src/Specific/solinas64_2e216m2e108m1/CurveParameters.v b/src/Specific/solinas64_2e216m2e108m1/CurveParameters.v index 266c44e73..c6e24e21e 100644 --- a/src/Specific/solinas64_2e216m2e108m1/CurveParameters.v +++ b/src/Specific/solinas64_2e216m2e108m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 43 Definition curve : CurveParameters := {| sz := 5%nat; + base := 43; bitwidth := 64; s := 2^216; c := [(1, 1); (2^108, 1)]; diff --git a/src/Specific/solinas64_2e221m3/CurveParameters.v b/src/Specific/solinas64_2e221m3/CurveParameters.v index a7d90d497..29c5a2813 100644 --- a/src/Specific/solinas64_2e221m3/CurveParameters.v +++ b/src/Specific/solinas64_2e221m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 44 Definition curve : CurveParameters := {| sz := 5%nat; + base := 44; bitwidth := 64; s := 2^221; c := [(1, 3)]; diff --git a/src/Specific/solinas64_2e222m117/CurveParameters.v b/src/Specific/solinas64_2e222m117/CurveParameters.v index e4d3701ae..8eb74563a 100644 --- a/src/Specific/solinas64_2e222m117/CurveParameters.v +++ b/src/Specific/solinas64_2e222m117/CurveParameters.v @@ -9,6 +9,7 @@ Base: 37 Definition curve : CurveParameters := {| sz := 6%nat; + base := 37; bitwidth := 64; s := 2^222; c := [(1, 117)]; diff --git a/src/Specific/solinas64_2e224m2e96p1/CurveParameters.v b/src/Specific/solinas64_2e224m2e96p1/CurveParameters.v index 6c35c0027..b76b2879f 100644 --- a/src/Specific/solinas64_2e224m2e96p1/CurveParameters.v +++ b/src/Specific/solinas64_2e224m2e96p1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 37 Definition curve : CurveParameters := {| sz := 6%nat; + base := 37; bitwidth := 64; s := 2^224; c := [(1, -1); (2^96, 1)]; diff --git a/src/Specific/solinas64_2e226m5/CurveParameters.v b/src/Specific/solinas64_2e226m5/CurveParameters.v index 840ad51e4..6f4306093 100644 --- a/src/Specific/solinas64_2e226m5/CurveParameters.v +++ b/src/Specific/solinas64_2e226m5/CurveParameters.v @@ -9,6 +9,7 @@ Base: 45 Definition curve : CurveParameters := {| sz := 5%nat; + base := 45; bitwidth := 64; s := 2^226; c := [(1, 5)]; diff --git a/src/Specific/solinas64_2e230m27/CurveParameters.v b/src/Specific/solinas64_2e230m27/CurveParameters.v index b2529f018..2b909f1bb 100644 --- a/src/Specific/solinas64_2e230m27/CurveParameters.v +++ b/src/Specific/solinas64_2e230m27/CurveParameters.v @@ -9,6 +9,7 @@ Base: 46 Definition curve : CurveParameters := {| sz := 5%nat; + base := 46; bitwidth := 64; s := 2^230; c := [(1, 27)]; diff --git a/src/Specific/solinas64_2e235m15/CurveParameters.v b/src/Specific/solinas64_2e235m15/CurveParameters.v index 4a1e49247..dec843f24 100644 --- a/src/Specific/solinas64_2e235m15/CurveParameters.v +++ b/src/Specific/solinas64_2e235m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 47 Definition curve : CurveParameters := {| sz := 5%nat; + base := 47; bitwidth := 64; s := 2^235; c := [(1, 15)]; diff --git a/src/Specific/solinas64_2e243m9/CurveParameters.v b/src/Specific/solinas64_2e243m9/CurveParameters.v index 1dc4e1640..c8dce3b16 100644 --- a/src/Specific/solinas64_2e243m9/CurveParameters.v +++ b/src/Specific/solinas64_2e243m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 40 Definition curve : CurveParameters := {| sz := 6%nat; + base := 40; bitwidth := 64; s := 2^243; c := [(1, 9)]; diff --git a/src/Specific/solinas64_2e251m9/CurveParameters.v b/src/Specific/solinas64_2e251m9/CurveParameters.v index 52ba2f753..023041b13 100644 --- a/src/Specific/solinas64_2e251m9/CurveParameters.v +++ b/src/Specific/solinas64_2e251m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 25 Definition curve : CurveParameters := {| sz := 10%nat; + base := 25; bitwidth := 64; s := 2^251; c := [(1, 9)]; diff --git a/src/Specific/solinas64_2e255m19/CurveParameters.v b/src/Specific/solinas64_2e255m19/CurveParameters.v index f113a3dcc..03964ea0c 100644 --- a/src/Specific/solinas64_2e255m19/CurveParameters.v +++ b/src/Specific/solinas64_2e255m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 42 Definition curve : CurveParameters := {| sz := 6%nat; + base := 42; bitwidth := 64; s := 2^255; c := [(1, 19)]; diff --git a/src/Specific/solinas64_2e255m2e4m2e1m1/CurveParameters.v b/src/Specific/solinas64_2e255m2e4m2e1m1/CurveParameters.v index a27a0ba4b..5c2747c0b 100644 --- a/src/Specific/solinas64_2e255m2e4m2e1m1/CurveParameters.v +++ b/src/Specific/solinas64_2e255m2e4m2e1m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 51 Definition curve : CurveParameters := {| sz := 5%nat; + base := 51; bitwidth := 64; s := 2^255; c := [(1, 1); (2^1, 1); (2^4, 1)]; diff --git a/src/Specific/solinas64_2e255m765/CurveParameters.v b/src/Specific/solinas64_2e255m765/CurveParameters.v index 83a63703d..2d1c2199b 100644 --- a/src/Specific/solinas64_2e255m765/CurveParameters.v +++ b/src/Specific/solinas64_2e255m765/CurveParameters.v @@ -9,6 +9,7 @@ Base: 42 Definition curve : CurveParameters := {| sz := 6%nat; + base := 42; bitwidth := 64; s := 2^255; c := [(1, 765)]; diff --git a/src/Specific/solinas64_2e256m189/CurveParameters.v b/src/Specific/solinas64_2e256m189/CurveParameters.v index 3e25722d7..f9d9b9c06 100644 --- a/src/Specific/solinas64_2e256m189/CurveParameters.v +++ b/src/Specific/solinas64_2e256m189/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 8%nat; + base := 32; bitwidth := 64; s := 2^256; c := [(1, 189)]; diff --git a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1/CurveParameters.v b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1/CurveParameters.v index 108b9aeaa..a169dfe68 100644 --- a/src/Specific/solinas64_2e256m2e224p2e192p2e96m1/CurveParameters.v +++ b/src/Specific/solinas64_2e256m2e224p2e192p2e96m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 51 Definition curve : CurveParameters := {| sz := 5%nat; + base := 51; bitwidth := 64; s := 2^256; c := [(1, 1); (2^96, -1); (2^192, -1); (2^224, 1)]; diff --git a/src/Specific/solinas64_2e256m2e32m977/CurveParameters.v b/src/Specific/solinas64_2e256m2e32m977/CurveParameters.v index 1a10fc18b..d2fb79b54 100644 --- a/src/Specific/solinas64_2e256m2e32m977/CurveParameters.v +++ b/src/Specific/solinas64_2e256m2e32m977/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 8%nat; + base := 32; bitwidth := 64; s := 2^256; c := [(1, 977); (2^32, 1)]; diff --git a/src/Specific/solinas64_2e266m3/CurveParameters.v b/src/Specific/solinas64_2e266m3/CurveParameters.v index 6215265f4..abd42c2e9 100644 --- a/src/Specific/solinas64_2e266m3/CurveParameters.v +++ b/src/Specific/solinas64_2e266m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 44 Definition curve : CurveParameters := {| sz := 6%nat; + base := 44; bitwidth := 64; s := 2^266; c := [(1, 3)]; diff --git a/src/Specific/solinas64_2e285m9/CurveParameters.v b/src/Specific/solinas64_2e285m9/CurveParameters.v index 20f884c12..52ba8173d 100644 --- a/src/Specific/solinas64_2e285m9/CurveParameters.v +++ b/src/Specific/solinas64_2e285m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 47 Definition curve : CurveParameters := {| sz := 6%nat; + base := 47; bitwidth := 64; s := 2^285; c := [(1, 9)]; diff --git a/src/Specific/solinas64_2e291m19/CurveParameters.v b/src/Specific/solinas64_2e291m19/CurveParameters.v index 59feda840..bb41bc110 100644 --- a/src/Specific/solinas64_2e291m19/CurveParameters.v +++ b/src/Specific/solinas64_2e291m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 48 Definition curve : CurveParameters := {| sz := 6%nat; + base := 48; bitwidth := 64; s := 2^291; c := [(1, 19)]; diff --git a/src/Specific/solinas64_2e321m9/CurveParameters.v b/src/Specific/solinas64_2e321m9/CurveParameters.v index 8112879f0..3014703cf 100644 --- a/src/Specific/solinas64_2e321m9/CurveParameters.v +++ b/src/Specific/solinas64_2e321m9/CurveParameters.v @@ -9,6 +9,7 @@ Base: 40 Definition curve : CurveParameters := {| sz := 8%nat; + base := 40; bitwidth := 64; s := 2^321; c := [(1, 9)]; diff --git a/src/Specific/solinas64_2e322m2e161m1/CurveParameters.v b/src/Specific/solinas64_2e322m2e161m1/CurveParameters.v index b6a2c0947..ba1442980 100644 --- a/src/Specific/solinas64_2e322m2e161m1/CurveParameters.v +++ b/src/Specific/solinas64_2e322m2e161m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 46 Definition curve : CurveParameters := {| sz := 7%nat; + base := 46; bitwidth := 64; s := 2^322; c := [(1, 1); (2^161, 1)]; diff --git a/src/Specific/solinas64_2e336m17/CurveParameters.v b/src/Specific/solinas64_2e336m17/CurveParameters.v index 3de0c9ac7..ea471461d 100644 --- a/src/Specific/solinas64_2e336m17/CurveParameters.v +++ b/src/Specific/solinas64_2e336m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 48 Definition curve : CurveParameters := {| sz := 7%nat; + base := 48; bitwidth := 64; s := 2^336; c := [(1, 17)]; diff --git a/src/Specific/solinas64_2e336m3/CurveParameters.v b/src/Specific/solinas64_2e336m3/CurveParameters.v index e0c5109e5..cc3eff42c 100644 --- a/src/Specific/solinas64_2e336m3/CurveParameters.v +++ b/src/Specific/solinas64_2e336m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 48 Definition curve : CurveParameters := {| sz := 7%nat; + base := 48; bitwidth := 64; s := 2^336; c := [(1, 3)]; diff --git a/src/Specific/solinas64_2e338m15/CurveParameters.v b/src/Specific/solinas64_2e338m15/CurveParameters.v index 5fdb17750..7aec1cf59 100644 --- a/src/Specific/solinas64_2e338m15/CurveParameters.v +++ b/src/Specific/solinas64_2e338m15/CurveParameters.v @@ -9,6 +9,7 @@ Base: 42 Definition curve : CurveParameters := {| sz := 8%nat; + base := 42; bitwidth := 64; s := 2^338; c := [(1, 15)]; diff --git a/src/Specific/solinas64_2e369m25/CurveParameters.v b/src/Specific/solinas64_2e369m25/CurveParameters.v index 13b0f66df..c321b0364 100644 --- a/src/Specific/solinas64_2e369m25/CurveParameters.v +++ b/src/Specific/solinas64_2e369m25/CurveParameters.v @@ -9,6 +9,7 @@ Base: 46 Definition curve : CurveParameters := {| sz := 8%nat; + base := 46; bitwidth := 64; s := 2^369; c := [(1, 25)]; diff --git a/src/Specific/solinas64_2e379m19/CurveParameters.v b/src/Specific/solinas64_2e379m19/CurveParameters.v index 1981adcf5..ee053dea7 100644 --- a/src/Specific/solinas64_2e379m19/CurveParameters.v +++ b/src/Specific/solinas64_2e379m19/CurveParameters.v @@ -9,6 +9,7 @@ Base: 42 Definition curve : CurveParameters := {| sz := 9%nat; + base := 42; bitwidth := 64; s := 2^379; c := [(1, 19)]; diff --git a/src/Specific/solinas64_2e382m105/CurveParameters.v b/src/Specific/solinas64_2e382m105/CurveParameters.v index 4dff15b2a..661b261b3 100644 --- a/src/Specific/solinas64_2e382m105/CurveParameters.v +++ b/src/Specific/solinas64_2e382m105/CurveParameters.v @@ -9,6 +9,7 @@ Base: 38 Definition curve : CurveParameters := {| sz := 10%nat; + base := 38; bitwidth := 64; s := 2^382; c := [(1, 105)]; diff --git a/src/Specific/solinas64_2e384m2e128m2e96p2e32m1/CurveParameters.v b/src/Specific/solinas64_2e384m2e128m2e96p2e32m1/CurveParameters.v index 23733bdf6..11d2ce031 100644 --- a/src/Specific/solinas64_2e384m2e128m2e96p2e32m1/CurveParameters.v +++ b/src/Specific/solinas64_2e384m2e128m2e96p2e32m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 48 Definition curve : CurveParameters := {| sz := 8%nat; + base := 48; bitwidth := 64; s := 2^384; c := [(1, 1); (2^32, -1); (2^96, 1); (2^128, 1)]; diff --git a/src/Specific/solinas64_2e384m317/CurveParameters.v b/src/Specific/solinas64_2e384m317/CurveParameters.v index 3947edf8b..37ec17f42 100644 --- a/src/Specific/solinas64_2e384m317/CurveParameters.v +++ b/src/Specific/solinas64_2e384m317/CurveParameters.v @@ -9,6 +9,7 @@ Base: 48 Definition curve : CurveParameters := {| sz := 8%nat; + base := 48; bitwidth := 64; s := 2^384; c := [(1, 317)]; diff --git a/src/Specific/solinas64_2e401m31/CurveParameters.v b/src/Specific/solinas64_2e401m31/CurveParameters.v index fd79bcc09..4ef1e1a1e 100644 --- a/src/Specific/solinas64_2e401m31/CurveParameters.v +++ b/src/Specific/solinas64_2e401m31/CurveParameters.v @@ -9,6 +9,7 @@ Base: 50 Definition curve : CurveParameters := {| sz := 8%nat; + base := 50; bitwidth := 64; s := 2^401; c := [(1, 31)]; diff --git a/src/Specific/solinas64_2e413m21/CurveParameters.v b/src/Specific/solinas64_2e413m21/CurveParameters.v index bbf20f65a..dcb5b3771 100644 --- a/src/Specific/solinas64_2e413m21/CurveParameters.v +++ b/src/Specific/solinas64_2e413m21/CurveParameters.v @@ -9,6 +9,7 @@ Base: 29 Definition curve : CurveParameters := {| sz := 14%nat; + base := 29; bitwidth := 64; s := 2^413; c := [(1, 21)]; diff --git a/src/Specific/solinas64_2e414m17/CurveParameters.v b/src/Specific/solinas64_2e414m17/CurveParameters.v index 2dcf746df..8152e2881 100644 --- a/src/Specific/solinas64_2e414m17/CurveParameters.v +++ b/src/Specific/solinas64_2e414m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 46 Definition curve : CurveParameters := {| sz := 9%nat; + base := 46; bitwidth := 64; s := 2^414; c := [(1, 17)]; diff --git a/src/Specific/solinas64_2e416m2e208m1/CurveParameters.v b/src/Specific/solinas64_2e416m2e208m1/CurveParameters.v index 8280b7471..f9a5233df 100644 --- a/src/Specific/solinas64_2e416m2e208m1/CurveParameters.v +++ b/src/Specific/solinas64_2e416m2e208m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 52 Definition curve : CurveParameters := {| sz := 8%nat; + base := 52; bitwidth := 64; s := 2^416; c := [(1, 1); (2^208, 1)]; diff --git a/src/Specific/solinas64_2e444m17/CurveParameters.v b/src/Specific/solinas64_2e444m17/CurveParameters.v index df70cc9e0..99fa3f6b9 100644 --- a/src/Specific/solinas64_2e444m17/CurveParameters.v +++ b/src/Specific/solinas64_2e444m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 49 Definition curve : CurveParameters := {| sz := 9%nat; + base := 49; bitwidth := 64; s := 2^444; c := [(1, 17)]; diff --git a/src/Specific/solinas64_2e448m2e224m1/CurveParameters.v b/src/Specific/solinas64_2e448m2e224m1/CurveParameters.v index e28b2bf32..112ca94f1 100644 --- a/src/Specific/solinas64_2e448m2e224m1/CurveParameters.v +++ b/src/Specific/solinas64_2e448m2e224m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 56 Definition curve : CurveParameters := {| sz := 8%nat; + base := 56; bitwidth := 64; s := 2^448; c := [(1, 1); (2^224, 1)]; diff --git a/src/Specific/solinas64_2e450m2e225m1/CurveParameters.v b/src/Specific/solinas64_2e450m2e225m1/CurveParameters.v index e6fff2de0..8cd2a090a 100644 --- a/src/Specific/solinas64_2e450m2e225m1/CurveParameters.v +++ b/src/Specific/solinas64_2e450m2e225m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 50 Definition curve : CurveParameters := {| sz := 9%nat; + base := 50; bitwidth := 64; s := 2^450; c := [(1, 1); (2^225, 1)]; diff --git a/src/Specific/solinas64_2e452m3/CurveParameters.v b/src/Specific/solinas64_2e452m3/CurveParameters.v index 4f7a8cda9..f081f9745 100644 --- a/src/Specific/solinas64_2e452m3/CurveParameters.v +++ b/src/Specific/solinas64_2e452m3/CurveParameters.v @@ -9,6 +9,7 @@ Base: 45 Definition curve : CurveParameters := {| sz := 10%nat; + base := 45; bitwidth := 64; s := 2^452; c := [(1, 3)]; diff --git a/src/Specific/solinas64_2e468m17/CurveParameters.v b/src/Specific/solinas64_2e468m17/CurveParameters.v index 7a7086cf9..f82ed7f10 100644 --- a/src/Specific/solinas64_2e468m17/CurveParameters.v +++ b/src/Specific/solinas64_2e468m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 52 Definition curve : CurveParameters := {| sz := 9%nat; + base := 52; bitwidth := 64; s := 2^468; c := [(1, 17)]; diff --git a/src/Specific/solinas64_2e480m2e240m1/CurveParameters.v b/src/Specific/solinas64_2e480m2e240m1/CurveParameters.v index b3051d75e..cd5cb85c4 100644 --- a/src/Specific/solinas64_2e480m2e240m1/CurveParameters.v +++ b/src/Specific/solinas64_2e480m2e240m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 53 Definition curve : CurveParameters := {| sz := 9%nat; + base := 53; bitwidth := 64; s := 2^480; c := [(1, 1); (2^240, 1)]; diff --git a/src/Specific/solinas64_2e488m17/CurveParameters.v b/src/Specific/solinas64_2e488m17/CurveParameters.v index b2837cdbf..5244d6754 100644 --- a/src/Specific/solinas64_2e488m17/CurveParameters.v +++ b/src/Specific/solinas64_2e488m17/CurveParameters.v @@ -9,6 +9,7 @@ Base: 30 Definition curve : CurveParameters := {| sz := 16%nat; + base := 30; bitwidth := 64; s := 2^488; c := [(1, 17)]; diff --git a/src/Specific/solinas64_2e489m21/CurveParameters.v b/src/Specific/solinas64_2e489m21/CurveParameters.v index 8c842d205..e8980fda5 100644 --- a/src/Specific/solinas64_2e489m21/CurveParameters.v +++ b/src/Specific/solinas64_2e489m21/CurveParameters.v @@ -9,6 +9,7 @@ Base: 27 Definition curve : CurveParameters := {| sz := 18%nat; + base := 27; bitwidth := 64; s := 2^489; c := [(1, 21)]; diff --git a/src/Specific/solinas64_2e495m31/CurveParameters.v b/src/Specific/solinas64_2e495m31/CurveParameters.v index 0f461ac6c..29d85256a 100644 --- a/src/Specific/solinas64_2e495m31/CurveParameters.v +++ b/src/Specific/solinas64_2e495m31/CurveParameters.v @@ -9,6 +9,7 @@ Base: 49 Definition curve : CurveParameters := {| sz := 10%nat; + base := 49; bitwidth := 64; s := 2^495; c := [(1, 31)]; diff --git a/src/Specific/solinas64_2e511m187/CurveParameters.v b/src/Specific/solinas64_2e511m187/CurveParameters.v index 102905ed1..36c85b4db 100644 --- a/src/Specific/solinas64_2e511m187/CurveParameters.v +++ b/src/Specific/solinas64_2e511m187/CurveParameters.v @@ -9,6 +9,7 @@ Base: 36 Definition curve : CurveParameters := {| sz := 14%nat; + base := 36; bitwidth := 64; s := 2^511; c := [(1, 187)]; diff --git a/src/Specific/solinas64_2e511m481/CurveParameters.v b/src/Specific/solinas64_2e511m481/CurveParameters.v index ac65d991d..5252e1dda 100644 --- a/src/Specific/solinas64_2e511m481/CurveParameters.v +++ b/src/Specific/solinas64_2e511m481/CurveParameters.v @@ -9,6 +9,7 @@ Base: 36 Definition curve : CurveParameters := {| sz := 14%nat; + base := 36; bitwidth := 64; s := 2^511; c := [(1, 481)]; diff --git a/src/Specific/solinas64_2e512m569/CurveParameters.v b/src/Specific/solinas64_2e512m569/CurveParameters.v index 6a7620320..91ab7fcce 100644 --- a/src/Specific/solinas64_2e512m569/CurveParameters.v +++ b/src/Specific/solinas64_2e512m569/CurveParameters.v @@ -9,6 +9,7 @@ Base: 32 Definition curve : CurveParameters := {| sz := 16%nat; + base := 32; bitwidth := 64; s := 2^512; c := [(1, 569)]; diff --git a/src/Specific/solinas64_2e521m1/CurveParameters.v b/src/Specific/solinas64_2e521m1/CurveParameters.v index 33dd15c4a..0aa20d83b 100644 --- a/src/Specific/solinas64_2e521m1/CurveParameters.v +++ b/src/Specific/solinas64_2e521m1/CurveParameters.v @@ -9,6 +9,7 @@ Base: 52 Definition curve : CurveParameters := {| sz := 10%nat; + base := 52; bitwidth := 64; s := 2^521; c := [(1, 1)]; |