diff options
author | Jason Gross <jgross@mit.edu> | 2018-01-04 19:03:52 -0500 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2018-01-05 15:56:49 -0500 |
commit | 5a17101cde1b568b1864f0509e3cb352f3762cbc (patch) | |
tree | 4062eabe659ca7b810509e991efbf286f222e250 /src | |
parent | 8d465a7de3c0af6be9bc1f998cbeb43f6f4da7fe (diff) |
Permit `TWord 0`
This handles bullet 2 of #288
Diffstat (limited to 'src')
-rw-r--r-- | src/Specific/Framework/CurveParameters.v | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/src/Specific/Framework/CurveParameters.v b/src/Specific/Framework/CurveParameters.v index 3b31d9339..91d876372 100644 --- a/src/Specific/Framework/CurveParameters.v +++ b/src/Specific/Framework/CurveParameters.v @@ -91,11 +91,15 @@ Module Export CurveParameters. => instantiate (1:=square_code) end. - Local Notation list_8_if_not_exists ls := - (if existsb (Nat.eqb 8) ls + Local Notation list_n_if_not_exists n ls := + (if existsb (Nat.eqb n) ls then nil - else [8]%nat) + else [n]%nat) (only parsing). + Local Notation list_8_if_not_exists ls + := (list_n_if_not_exists 8%nat ls) (only parsing). + Local Notation list_1_if_not_exists ls + := (list_n_if_not_exists 1%nat ls) (only parsing). Definition fill_defaults_CurveParameters (CP : RawCurveParameters.CurveParameters) : CurveParameters @@ -120,7 +124,7 @@ Module Export CurveParameters. := defaulted (RawCurveParameters.allowable_bit_widths CP) ((if montgomery - then [8] + then [1; 8] else nil) ++ (Z.to_nat bitwidth :: 2*Z.to_nat bitwidth :: nil))%nat in let upper_bound_of_exponent_tight @@ -159,7 +163,8 @@ Module Export CurveParameters. freeze_allowable_bit_widths := defaulted (RawCurveParameters.freeze_extra_allowable_bit_widths CP) - (list_8_if_not_exists allowable_bit_widths) + ((list_1_if_not_exists allowable_bit_widths) + ++ (list_8_if_not_exists allowable_bit_widths)) ++ allowable_bit_widths; modinv_fuel := defaulted (RawCurveParameters.modinv_fuel CP) (Z.to_nat (Z.log2_up s)) |}. |