diff options
Diffstat (limited to 'src/Specific/X2555/C128/CurveParameters.v')
| -rw-r--r-- | src/Specific/X2555/C128/CurveParameters.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Specific/X2555/C128/CurveParameters.v b/src/Specific/X2555/C128/CurveParameters.v index 40c57e8e0..bb4384cc2 100644 --- a/src/Specific/X2555/C128/CurveParameters.v +++ b/src/Specific/X2555/C128/CurveParameters.v @@ -14,7 +14,7 @@ Module Curve <: CurveParameters. Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat. Definition a24 : option Z := Some (121665 (* XXX TODO(andreser) FIXME? Is this right for this curve? *)). - Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *) + Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) Definition goldilocks : bool := false. @@ -27,6 +27,7 @@ Module Curve <: CurveParameters. Definition upper_bound_of_exponent : option (Z -> Z) := None. Definition allowable_bit_widths : option (list nat) := None. Definition freeze_extra_allowable_bit_widths : option (list nat) := None. + Definition modinv_fuel : option nat := None. Ltac extra_prove_mul_eq := idtac. Ltac extra_prove_square_eq := idtac. End Curve. |