src/crypto/secp256k1/field.bend

bend-collections@1.0.0.0 · 137 lines · 29 definitions

1import Base
2import bend-collections@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
3
4# GF(p), p = 2^256 - 2^32 - 977 (SEC 2 section 2.4.1), on 16 limbs of
5# radix 2^16 (src/crypto/secp256k1/limbs.bend). Every operation takes and
6# returns reduced elements: exactly 16 limbs below 2^16, value below p.
7# The contract is spec/crypto/secp256k1/field.bend; the proofs are in
8# proofs/crypto/secp256k1/.
9#
10# Inversion and square root are exponentiations by the public exponents
11# p - 2 (Fermat) and (p + 1) / 4 (p = 3 mod 4), square-and-multiply over
12# the exponent's bits: the branch is on the public exponent, never on the
13# base.
14
15# 2^256 - p = 2^32 + 977
16def c() -> List<&2, Nat>:
17  [977n, 0n, 1n]
18
19def reduce(xs: List<&2, Nat>) -> List<&2, Nat>:
20  L.reduce(c(), 3n, xs)
21
22def small(+k: Nat) -> List<&2, Nat>:
23  L.norm16([k])
24
25def zero() -> List<&2, Nat>:
26  small(0n)
27
28def one() -> List<&2, Nat>:
29  small(1n)
30
31# The operations look at their first argument first (and are the *_u
32# forms then), so that on unknown arguments the proof checker keeps them
33# folded instead of unfolding the reduction.
34
35def add_u(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
36  reduce(L.add(a, b))
37
38def add_b(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
39  match b:
40    case Nil{}: add_u(a, Nil{})
41    case y <> u: add_u(a, y <> u)
42
43def add(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
44  match a:
45    case Nil{}: add_b(Nil{}, b)
46    case x <> t: add_b(x <> t, b)
47
48# a - b = a + (p - b); the first argument is looked at first, so that a
49# constant b is never unfolded while a is unknown
50def sub(a: List<&2, Nat>, +b: List<&2, Nat>) -> List<&2, Nat>:
51  match a:
52    case Nil{}: reduce(L.neg_raw(c(), b))
53    case x <> t: reduce(L.add(x <> t, L.neg_raw(c(), b)))
54
55def neg_u(a: List<&2, Nat>) -> List<&2, Nat>:
56  reduce(L.neg_raw(c(), a))
57
58# (one argument: nothing to look at first)
59def neg(a: List<&2, Nat>) -> List<&2, Nat>:
60  neg_u(a)
61
62def mul_u(a: List<&2, Nat>, +b: List<&2, Nat>) -> List<&2, Nat>:
63  reduce(L.conv(a, b))
64
65def mul_b(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
66  match b:
67    case Nil{}: mul_u(a, Nil{})
68    case y <> u: mul_u(a, y <> u)
69
70def mul(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
71  match a:
72    case Nil{}: mul_b(Nil{}, b)
73    case x <> t: mul_b(x <> t, b)
74
75def sq(+a: List<&2, Nat>) -> List<&2, Nat>:
76  mul(a, a)
77
78# x^e for the exponent e given by its bits, most significant first
79def pow_step(b: Nat, +x: List<&2, Nat>, +s: List<&2, Nat>) -> List<&2, Nat>:
80  match b:
81    case 0n: s
82    case 1n+k: mul(s, x)
83
84def pow_go(+x: List<&2, Nat>, bits: List<&2, Nat>, +acc: List<&2, Nat>) -> List<&2, Nat>:
85  match bits:
86    case Nil{}: acc
87    case b <> t: pow_go(x, t, pow_step(b, x, sq(acc)))
88
89# x is looked at first, so that on an unknown x nothing is unfolded
90def pow(x: List<&2, Nat>, bits: List<&2, Nat>, +acc: List<&2, Nat>) -> List<&2, Nat>:
91  match x:
92    case Nil{}: pow_go(Nil{}, bits, acc)
93    case +y <> +t: pow_go(y <> t, bits, acc)
94
95# the bits of p - 2 = 2^256 - 1 - (c + 1): those of c + 1, flipped
96def inv_bits() -> List<&2, Nat>:
97  L.cbits(L.bits(L.norm16([978n, 0n, 1n])))
98
99def init2(xs: List<&2, Nat>) -> List<&2, Nat>:
100  List.reverse(&2, Nat, L.drop(2n, List.reverse(&2, Nat, xs)))
101
102# the bits of (p + 1) / 4: p + 1 = 2^256 - 1 - (c - 2), without its last two bits
103def sqrt_bits() -> List<&2, Nat>:
104  init2(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))))
105
106# a^(p - 2): the inverse of a nonzero a, 0 for 0
107def inv(+a: List<&2, Nat>) -> List<&2, Nat>:
108  pow(a, inv_bits(), one())
109
110# a^((p + 1) / 4): a square root of a when a is a square (p = 3 mod 4)
111def sqrt(+a: List<&2, Nat>) -> List<&2, Nat>:
112  pow(a, sqrt_bits(), one())
113
114def is_zero(a: List<&2, Nat>) -> Bool:
115  L.is_zero(a)
116
117def eq_b(a: List<&2, Nat>, b: List<&2, Nat>) -> Bool:
118  match b:
119    case Nil{}: L.eq(a, Nil{})
120    case y <> u: L.eq(a, y <> u)
121
122def eq(a: List<&2, Nat>, b: List<&2, Nat>) -> Bool:
123  match a:
124    case Nil{}: eq_b(Nil{}, b)
125    case x <> t: eq_b(x <> t, b)
126
127# a mod 2 (the parity of the canonical representative)
128def parity(a: List<&2, Nat>) -> Nat:
129  Nat.mod(L.hd0(a), 2n)
130
131# a < p, for 16 limbs below 2^16
132def lt_p(a: List<&2, Nat>) -> Bool:
133  L.ltm(c(), a)
134
135# b ? x : y, branch-free, for b in {0, 1}
136def select(+b: Nat, x: List<&2, Nat>, y: List<&2, Nat>) -> List<&2, Nat>:
137  L.select(b, x, y)