blob: 5ff22d2f1f8889bd223237e3053c25f1b6861888 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
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.
Open Scope list_scope.
Open Scope Z_scope.
Notation limb := (Z * Z)%type.
Infix "^" := Tuple.tuple : type_scope.
End Notations.
Record CurveParameters :=
{
sz : nat;
base : Q;
bitwidth : Z;
s : Z;
c : list limb;
carry_chains
: option (list (list nat)) (* defaults to [seq 0 (pred sz) :: (0 :: 1 :: nil) :: nil] *);
a24 : option Z;
coef_div_modulus : option nat;
goldilocks : option bool; (* defaults to true iff the prime ([s-c]) is of the form [2²ᵏ - 2ᵏ - 1] *)
karatsuba : option bool; (* defaults to false, currently unused *)
montgomery : bool;
freeze : option bool; (* defaults to true iff [s = 2^(base * sz)] *)
ladderstep : bool;
mul_code : option (Z^sz -> Z^sz -> Z^sz);
square_code : option (Z^sz -> Z^sz);
upper_bound_of_exponent_tight
: option (Z -> Z) (* defaults to [fun exp => 2^exp + 2^(exp-3)] for non-montgomery, [fun exp => 2^exp - 1] for montgomery *);
upper_bound_of_exponent_loose
: option (Z -> Z) (* defaults to [3 * upper_bound_of_exponent_tight] for non-montgomery, [fun exp => 2^exp - 1] for montgomery *);
allowable_bit_widths
: option (list nat) (* defaults to [bitwidth :: 2*bitwidth :: nil] *);
freeze_extra_allowable_bit_widths
: option (list nat) (* defaults to [8 :: nil] *);
modinv_fuel : option nat
}.
Declare Reduction cbv_RawCurveParameters
:= cbv [sz
base
bitwidth
s
c
carry_chains
a24
coef_div_modulus
goldilocks
karatsuba
montgomery
freeze
ladderstep
mul_code
square_code
upper_bound_of_exponent_tight
upper_bound_of_exponent_loose
allowable_bit_widths
freeze_extra_allowable_bit_widths
modinv_fuel].
(*
Ltac extra_prove_mul_eq := idtac.
Ltac extra_prove_square_eq := idtac.
*)
|
