src/crypto/poly1305/limbs.bend

bend-collections@1.0.0.0 · 128 lines · 19 definitions

1import Base
2
3# Arithmetic modulo p = 2^130 - 5 on little-endian lists of U32 limbs of
4# radix 2^8 (TweetNaCl's representation): a list [l0, l1, ...] stands for
5# l0 + 2^8 l1 + 2^16 l2 + ... . Limbs may exceed 8 bits between carry
6# passes; every operation below keeps them under 2^31 on the Poly1305 path
7# (proofs/crypto/poly1305/ bounds each step), so no U32 operation wraps.
8#
9# Constant time: every loop runs over public lengths; the only data-dependent
10# choice (the final conditional subtraction of p) is a mask select, with no
11# branch and no secret-dependent memory access. Bend has no timing model, so
12# this is a property of the code's shape, not a proved fact.
13
14# The first limb (0 for the empty list) and the rest.
15def hd0(xs: List<&2, U32>) -> U32:
16  match xs:
17    case Nil{}: 0
18    case x <> t: x
19
20def tl(xs: List<&2, U32>) -> List<&2, U32>:
21  match xs:
22    case Nil{}: Nil{}
23    case x <> t: t
24
25# Limb-wise sum (the shorter list is padded with zeros), no carries.
26def add(a: List<&2, U32>, b: List<&2, U32>) -> List<&2, U32>:
27  match a b:
28    case Nil{} _: b
29    case x <> at Nil{}: x <> at
30    case x <> at y <> bt: U32.add(x, y) <> add(at, bt)
31
32# Every limb times c, no carries.
33def scale(+c: U32, a: List<&2, U32>) -> List<&2, U32>:
34  match a:
35    case Nil{}: Nil{}
36    case x <> t: U32.mul(x, c) <> scale(c, t)
37
38# Schoolbook product, no carries: x r0 + 2^8 (x r1 + 2^8 (...)).
39def mul(+x: List<&2, U32>, r: List<&2, U32>) -> List<&2, U32>:
40  match r:
41    case Nil{}: Nil{}
42    case r0 <> rs: add(scale(r0, x), 0 <> mul(x, rs))
43
44def take(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
45  match n xs:
46    case 0n _: Nil{}
47    case 1n+k Nil{}: Nil{}
48    case 1n+k x <> rest: x <> take(k, rest)
49
50def skip(n: Nat, xs: List<&2, U32>) -> List<&2, U32>:
51  match n xs:
52    case 0n _: xs
53    case 1n+k Nil{}: Nil{}
54    case 1n+k x <> rest: skip(k, rest)
55
56# The first n limbs, padded with zeros to exactly n.
57def fit(n: Nat, +xs: List<&2, U32>) -> List<&2, U32>:
58  match n:
59    case 0n: Nil{}
60    case 1n+k: hd0(xs) <> fit(k, tl(xs))
61
62# 2^136 = 64 p + 320: limbs 17.. are folded onto limbs 0.. times 320.
63def fold(+z: List<&2, U32>) -> List<&2, U32>:
64  add(take(17n, z), scale(320, skip(17n, z)))
65
66# A carry pass over n limbs, each kept to 8 bits; the carry u and all limbs
67# from n on (one, on the Poly1305 path) are summed into the top limb.
68def carry(n: Nat, +ds: List<&2, U32>, u: U32) -> List<&2, U32>:
69  match n:
70    case 0n: [U32.add(u, hd0(ds))]
71    case 1n+k:
72      +s = U32.add(u, hd0(ds))
73      U32.and(s, 255) <> carry(k, tl(ds), U32.shrn(s, 8n))
74
75# Limb n (the top one) reduced to its low 2 bits, i.e. the value below 2^130
76# when n = 16; quot is the rest of limb n, the multiple of 2^130.
77def split(n: Nat, +xs: List<&2, U32>) -> List<&2, U32>:
78  match n:
79    case 0n: [U32.and(hd0(xs), 3)]
80    case 1n+k: hd0(xs) <> split(k, tl(xs))
81
82def quot(n: Nat, +xs: List<&2, U32>) -> U32:
83  match n:
84    case 0n: U32.shrn(hd0(xs), 2n)
85    case 1n+k: quot(k, tl(xs))
86
87# Partial reduction of 17 limbs: carry, then 2^130 q = p q + 5 q, so q is
88# folded back as 5 q on limb 0 and carried again. The result has limbs 0..15
89# below 2^8 and a value below 5 * 2^128 < 2p.
90def reduce(+d: List<&2, U32>) -> List<&2, U32>:
91  +t = carry(16n, d, 0)
92  carry(16n, add([U32.mul(quot(16n, t), 5)], split(16n, t)), 0)
93
94# One Poly1305 block: h = (h + c) r, partially reduced mod p.
95def block(+r: List<&2, U32>, h: List<&2, U32>, c: List<&2, U32>) -> List<&2, U32>:
96  reduce(fold(mul(add(h, c), r)))
97
98# a when m is all zeros, b when m is all ones.
99def pick(+m: U32, +a: U32, b: U32) -> U32:
100  U32.xor(a, U32.and(m, U32.xor(a, b)))
101
102def select(+m: U32, a: List<&2, U32>, b: List<&2, U32>) -> List<&2, U32>:
103  match a b:
104    case x <> at y <> bt: pick(m, x, y) <> select(m, at, bt)
105    case _ _: Nil{}
106
107# The low 16 limbs of h mod p, for h below 2p: g = h + 5 has bit 130 set
108# exactly when h >= p, and then its low 128 bits are those of h - p.
109def freeze(+h: List<&2, U32>) -> List<&2, U32>:
110  +g = carry(16n, add(h, [5]), 0)
111  +b = U32.shrn(hd0(skip(16n, g)), 2n)
112  select(U32.sub(0, b), take(16n, h), take(16n, g))
113
114# n bytes of the value of ds + u (mod 2^(8n)).
115def bytes(n: Nat, +ds: List<&2, U32>, u: U32) -> List<&2, U32>:
116  match n:
117    case 0n: Nil{}
118    case 1n+k:
119      +s = U32.add(u, hd0(ds))
120      U32.and(s, 255) <> bytes(k, tl(ds), U32.shrn(s, 8n))
121
122# The tag bytes: the low 128 bits of (h mod p) + s. (Entered through a match
123# on s, both arms the same: while s is unknown a proof's goal stays one call
124# instead of sixteen unfolded byte steps.)
125def fin(+h: List<&2, U32>, s: List<&2, U32>) -> List<&2, U32>:
126  match s:
127    case Nil{}: bytes(16n, add(freeze(h), Nil{}), 0)
128    case y <> ys: bytes(16n, add(freeze(h), y <> ys), 0)