src/crypto/secp256k1/limbs.bend

bend-collections@1.0.0.0 · 223 lines · 34 definitions

1import Base
2
3# Arithmetic modulo m = 2^256 - c on little-endian lists of natural-number
4# limbs in radix 2^16 (secp256k1's p and n are both of this form, with
5# c = 2^32 + 977 and c < 2^129). A list [l0, l1, ...] stands for
6# l0 + 2^16 l1 + 2^32 l2 + ... ; a reduced element is 16 limbs, each below
7# 2^16, with value below m.
8#
9# Bend's native runtime holds a Nat in one machine word and checks it stays
10# below 2^48 (it aborts otherwise, it never wraps). The products of two
11# limbs are below 2^32, a column of the schoolbook product below 2^36, and
12# every other intermediate below 2^40, so no operation here comes near the
13# bound (proofs/crypto/secp256k1/ proves the values; the bounds are shown in
14# docs/CRYPTO_CONTRACTS.md).
15#
16# Only the constants 2, 255 and 256 appear: a 16-bit limb is split into two
17# bytes with div/mod 256 (which compile to shifts and masks), so the proof
18# checker, which keeps natural numbers in unary, never meets 2^16 as a
19# literal.
20#
21# The reduction follows the folding reductions of libsecp256k1
22# (secp256k1_fe_mul_inner, secp256k1_scalar_reduce_512) and of Fiat-Crypto's
23# "solinas" reduction: with 2^256 = m + c, the high part hi of
24# x = lo + 2^256 hi is folded as x == lo + c hi (mod m); a fixed number of
25# folds (3 for p, 4 for n) brings any product of two reduced elements below
26# 2^256, and one conditional subtraction of m (computed branch-free as
27# "add c and look at bit 256") gives the representative below m.
28#
29# No function branches on a limb value: selection is arithmetic
30# (b * x + (1 - b) * y with b in {0, 1}), every list has a fixed length,
31# and loops run over public counts. Bend has no timing model, so this is a
32# property of the code's shape, not a proved fact.
33
34# ---- 16-bit limbs from bytes ----
35
36# s mod 2^16 and s div 2^16
37def lo16(+s: Nat) -> Nat:
38  Nat.add(Nat.mod(s, 256n), Nat.mul(Nat.mod(Nat.div(s, 256n), 256n), 256n))
39
40def hi16(+s: Nat) -> Nat:
41  Nat.div(Nat.div(s, 256n), 256n)
42
43# 2^16 - 1 - x for x below 2^16
44def comp1(+x: Nat) -> Nat:
45  Nat.add(Nat.sub(255n, Nat.mod(x, 256n)), Nat.mul(Nat.sub(255n, Nat.div(x, 256n)), 256n))
46
47# ---- limb lists ----
48
49def hd0(xs: List<&2, Nat>) -> Nat:
50  match xs:
51    case Nil{}: 0n
52    case x <> t: x
53
54def tl(xs: List<&2, Nat>) -> List<&2, Nat>:
55  match xs:
56    case Nil{}: Nil{}
57    case x <> t: t
58
59# limb-wise sum; the longer tail is kept
60def add(xs: List<&2, Nat>, ys: List<&2, Nat>) -> List<&2, Nat>:
61  match xs ys:
62    case Nil{} _: ys
63    case x <> xt Nil{}: x <> xt
64    case x <> xt y <> yt: Nat.add(x, y) <> add(xt, yt)
65
66# every limb times a
67def scal(+a: Nat, ys: List<&2, Nat>) -> List<&2, Nat>:
68  match ys:
69    case Nil{}: Nil{}
70    case y <> yt: Nat.mul(y, a) <> scal(a, yt)
71
72# the schoolbook product without carries: conv(x :: xs, ys) = x ys + 2^16 conv(xs, ys)
73def conv(xs: List<&2, Nat>, +ys: List<&2, Nat>) -> List<&2, Nat>:
74  match xs:
75    case Nil{}: Nil{}
76    case x <> xt: add(scal(x, ys), 0n <> conv(xt, ys))
77
78def take(n: Nat, xs: List<&2, Nat>) -> List<&2, Nat>:
79  match n xs:
80    case 0n _: Nil{}
81    case 1n+k Nil{}: Nil{}
82    case 1n+k x <> t: x <> take(k, t)
83
84def drop(n: Nat, xs: List<&2, Nat>) -> List<&2, Nat>:
85  match n xs:
86    case 0n _: xs
87    case 1n+k Nil{}: Nil{}
88    case 1n+k x <> t: drop(k, t)
89
90# the value of the limbs (only ever of an empty list at run time: see carry)
91def horner(xs: List<&2, Nat>) -> Nat:
92  match xs:
93    case Nil{}: 0n
94    case x <> t: Nat.add(Nat.mul(Nat.mul(horner(t), 256n), 256n), x)
95
96# A carry pass: n limbs, each below 2^16, then one limb holding the carry u
97# out of them plus the value of whatever is left of xs past n limbs (on
98# every call below xs has at most n limbs, so that is the carry alone).
99# Every function here looks at its list before producing anything, so that
100# on a symbolic argument the proof checker stops at once.
101def carry(n: Nat, xs: List<&2, Nat>, u: Nat) -> List<&2, Nat>:
102  match n xs:
103    case 0n Nil{}: [u]
104    case 0n x <> t: [Nat.add(u, horner(x <> t))]
105    case 1n+k Nil{}:
106      +s = Nat.add(u, 0n)
107      lo16(s) <> carry(k, Nil{}, hi16(s))
108    case 1n+k x <> t:
109      +s = Nat.add(u, x)
110      lo16(s) <> carry(k, t, hi16(s))
111
112# every limb x becomes 2^16 - 1 - x
113def comp(xs: List<&2, Nat>) -> List<&2, Nat>:
114  match xs:
115    case Nil{}: Nil{}
116    case x <> t: comp1(x) <> comp(t)
117
118# b x + (1 - b) y, limb-wise, for b in {0, 1}
119def pick1(+b: Nat, +x: Nat, +y: Nat) -> Nat:
120  Nat.add(Nat.mul(x, b), Nat.mul(y, Nat.sub(1n, b)))
121
122def select(+b: Nat, xs: List<&2, Nat>, ys: List<&2, Nat>) -> List<&2, Nat>:
123  match xs ys:
124    case x <> xt y <> yt: pick1(b, x, y) <> select(b, xt, yt)
125    case _ _: Nil{}
126
127# ---- reduction modulo m = 2^256 - c ----
128
129# the normalized form of a value below 2^256: exactly 16 limbs below 2^16
130def norm16(xs: List<&2, Nat>) -> List<&2, Nat>:
131  take(16n, carry(32n, xs, 0n))
132
133# lo + c hi, for x = lo + 2^256 hi: congruent to x modulo m
134def fold(+c: List<&2, Nat>, +xs: List<&2, Nat>) -> List<&2, Nat>:
135  add(take(16n, xs), conv(drop(16n, xs), c))
136
137def rounds(k: Nat, +c: List<&2, Nat>, xs: List<&2, Nat>) -> List<&2, Nat>:
138  match k:
139    case 0n: xs
140    case 1n+j: rounds(j, c, carry(32n, fold(c, xs), 0n))
141
142# the part of a carried value above 2^256 (0 or 1 below)
143def top(xs: List<&2, Nat>) -> Nat:
144  horner(drop(16n, xs))
145
146# t (16 limbs, value below 2^256) mod m: t + c has bit 256 set exactly when
147# t >= m, and then its low 256 bits are t - m
148def canon(+c: List<&2, Nat>, +t: List<&2, Nat>) -> List<&2, Nat>:
149  +u = carry(32n, add(t, c), 0n)
150  select(top(u), take(16n, u), t)
151
152def reduce_go(+c: List<&2, Nat>, k: Nat, xs: List<&2, Nat>) -> List<&2, Nat>:
153  canon(c, take(16n, rounds(k, c, carry(32n, xs, 0n))))
154
155# x mod m for x below 2^512, in k folds (x is looked at first, so that the
156# proof checker keeps an unknown reduction folded)
157def reduce(+c: List<&2, Nat>, k: Nat, xs: List<&2, Nat>) -> List<&2, Nat>:
158  match xs:
159    case Nil{}: reduce_go(c, k, Nil{})
160    case x <> t: reduce_go(c, k, x <> t)
161
162# ---- negation and comparison modulo m, from c ----
163
164# m - b = (2^256 - 1 - (b + c)) + 1, for b < m (so b + c < 2^256); no
165# constant but c is ever formed
166def neg_raw(+c: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
167  add(comp(norm16(add(b, c))), [1n])
168
169# x < m, i.e. x + c < 2^256, for x of 16 limbs below 2^16
170def ltm(+c: List<&2, Nat>, x: List<&2, Nat>) -> Bool:
171  Nat.is_eq(top(carry(32n, add(x, c), 0n)), 0n)
172
173# ---- comparisons and bits ----
174
175def b2n(b: Bool) -> Nat:
176  match b:
177    case True{}: 1n
178    case False{}: 0n
179
180# 1 when the value of xs is below the value of ys plus br, else 0 (the
181# borrow out of xs - ys - br), for lists of the same length
182def borrow(xs: List<&2, Nat>, ys: List<&2, Nat>, br: Nat) -> Nat:
183  match xs ys:
184    case x <> xt y <> yt: borrow(xt, yt, b2n(Nat.is_lt(x, Nat.add(br, y))))
185    case _ _: br
186
187def lt(xs: List<&2, Nat>, ys: List<&2, Nat>) -> Bool:
188  Nat.is_eq(borrow(xs, ys, 0n), 1n)
189
190# OR of all limbs being nonzero, without an early exit
191def nonzero(xs: List<&2, Nat>, acc: Nat) -> Nat:
192  match xs:
193    case Nil{}: acc
194    case x <> t: nonzero(t, Nat.add(acc, x))
195
196def is_zero(xs: List<&2, Nat>) -> Bool:
197  Nat.is_eq(nonzero(xs, 0n), 0n)
198
199def diff(xs: List<&2, Nat>, ys: List<&2, Nat>, acc: Nat) -> Nat:
200  match xs ys:
201    case +x <> xt +y <> yt: diff(xt, yt, Nat.add(acc, Nat.add(Nat.sub(x, y), Nat.sub(y, x))))
202    case _ _: acc
203
204def eq(xs: List<&2, Nat>, ys: List<&2, Nat>) -> Bool:
205  Nat.is_eq(diff(xs, ys, 0n), 0n)
206
207# the k low bits of x, most significant first
208def bits_of(k: Nat, +x: Nat) -> List<&2, Nat>:
209  match k:
210    case 0n: Nil{}
211    case 1n+j: List.append(&2, Nat, bits_of(j, Nat.div(x, 2n)), [Nat.mod(x, 2n)])
212
213# every bit flipped: the bits of 2^k - 1 - x from those of x
214def cbits(bs: List<&2, Nat>) -> List<&2, Nat>:
215  match bs:
216    case Nil{}: Nil{}
217    case b <> t: Nat.sub(1n, b) <> cbits(t)
218
219# all bits of a limb list, most significant first (16 per limb)
220def bits(xs: List<&2, Nat>) -> List<&2, Nat>:
221  match xs:
222    case Nil{}: Nil{}
223    case x <> t: List.append(&2, Nat, bits(t), bits_of(16n, x))