~/jendhub

spec/crypto/sha512.bend

bend-collections-laws-crypto@1.0.0.0 · 297 lines · 42 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T
3
4# Executable specification of SHA-512 (FIPS 180-4), byte oriented, written
5# from the standard in the shape of spec/crypto/sha.bend (SHA-256) and of
6# HACL*'s Spec.SHA2. Only the neutral records of src/crypto/sha512/types.bend
7# are shared with the implementation: a 64-bit word is T.W{hi, lo}, its two
8# 32-bit halves, most significant first, and the working state is T.H{a..h}.
9# No implementation function, table or padding is called.
10#
11# Bytes are U32 values; each contributes its low 8 bits (the byte convention
12# of the crypto modules: every byte < 256).
13
14# ---------------------------------------------------------------- 64-bit words
15
16# FIPS 180-4 section 3.2: x + y mod 2^64. The low halves add modulo 2^32; the
17# high halves add the carry out of the low half, which is 1 exactly when the
18# low sum wrapped below either addend.
19def add(a: T.Lane, b: T.Lane) -> T.Lane:
20  match a b:
21    case T.W{ah, +al} T.W{bh, bl}:
22      +lo = U32.add(al, bl)
23      T.W{U32.add(U32.add(ah, bh), Bool.to_u32(U32.is_lt(lo, al))), lo}
24
25def xor(a: T.Lane, b: T.Lane) -> T.Lane:
26  match a b:
27    case T.W{ah, al} T.W{bh, bl}:
28      T.W{U32.xor(ah, bh), U32.xor(al, bl)}
29
30def and(a: T.Lane, b: T.Lane) -> T.Lane:
31  match a b:
32    case T.W{ah, al} T.W{bh, bl}:
33      T.W{U32.and(ah, bh), U32.and(al, bl)}
34
35def not(a: T.Lane) -> T.Lane:
36  match a:
37    case T.W{ah, al}:
38      T.W{U32.not(ah), U32.not(al)}
39
40# ROTR^n on the halves for 0 < n < 32: each half keeps its bits shifted right
41# and takes the other half's low n bits at the top.
42def rotr_small(+hi: U32, +lo: U32, +n: Nat) -> T.Lane:
43  T.W{U32.or(U32.shrn(hi, n), U32.shln(lo, Nat.sub(32n, n))),
44    U32.or(U32.shrn(lo, n), U32.shln(hi, Nat.sub(32n, n)))}
45
46# 32 <= n < 64: rotating by 32 swaps the halves, then rotate by n - 32.
47def rotr_split(+hi: U32, +lo: U32, +n: Nat, small: Bool) -> T.Lane:
48  match small:
49    case True{}:
50      rotr_small(hi, lo, n)
51    case False{}:
52      rotr_small(lo, hi, Nat.sub(n, 32n))
53
54# FIPS 180-4 section 3.2: ROTR^n(x) = (x >> n) OR (x << 64 - n), 0 < n < 64.
55def rotr(x: T.Lane, +n: Nat) -> T.Lane:
56  match x:
57    case T.W{+hi, +lo}:
58      rotr_split(hi, lo, n, Nat.is_lt(n, 32n))
59
60# FIPS 180-4 section 3.2: SHR^n(x) = x >> n, here for 0 < n < 32.
61def shr(x: T.Lane, +n: Nat) -> T.Lane:
62  match x:
63    case T.W{+hi, +lo}:
64      T.W{U32.shrn(hi, n), U32.or(U32.shrn(lo, n), U32.shln(hi, Nat.sub(32n, n)))}
65
66# ---------------------------------------------------------------- section 4.1.3
67
68def sum0(+x: T.Lane) -> T.Lane:
69  xor(xor(rotr(x, 28n), rotr(x, 34n)), rotr(x, 39n))
70
71def sum1(+x: T.Lane) -> T.Lane:
72  xor(xor(rotr(x, 14n), rotr(x, 18n)), rotr(x, 41n))
73
74def sigma0(+x: T.Lane) -> T.Lane:
75  xor(xor(rotr(x, 1n), rotr(x, 8n)), shr(x, 7n))
76
77def sigma1(+x: T.Lane) -> T.Lane:
78  xor(xor(rotr(x, 19n), rotr(x, 61n)), shr(x, 6n))
79
80def ch(+x: T.Lane, y: T.Lane, z: T.Lane) -> T.Lane:
81  xor(and(x, y), and(not(x), z))
82
83def maj(+x: T.Lane, +y: T.Lane, +z: T.Lane) -> T.Lane:
84  xor(xor(and(x, y), and(x, z)), and(y, z))
85
86# ---------------------------------------------------------------- constants
87
88# Section 5.3.5: the initial hash value H(0).
89def initial() -> T.State:
90  T.H{T.W{1779033703, 4089235720}, T.W{3144134277, 2227873595},
91    T.W{1013904242, 4271175723}, T.W{2773480762, 1595750129},
92    T.W{1359893119, 2917565137}, T.W{2600822924, 725511199},
93    T.W{528734635, 4215389547}, T.W{1541459225, 327033209}}
94
95# Section 4.2.3: K0 .. K79.
96def constants() -> List<&2, T.Lane>:
97  [T.W{1116352408, 3609767458}, T.W{1899447441, 602891725},
98   T.W{3049323471, 3964484399}, T.W{3921009573, 2173295548},
99   T.W{961987163, 4081628472}, T.W{1508970993, 3053834265},
100   T.W{2453635748, 2937671579}, T.W{2870763221, 3664609560},
101   T.W{3624381080, 2734883394}, T.W{310598401, 1164996542},
102   T.W{607225278, 1323610764}, T.W{1426881987, 3590304994},
103   T.W{1925078388, 4068182383}, T.W{2162078206, 991336113},
104   T.W{2614888103, 633803317}, T.W{3248222580, 3479774868},
105   T.W{3835390401, 2666613458}, T.W{4022224774, 944711139},
106   T.W{264347078, 2341262773}, T.W{604807628, 2007800933},
107   T.W{770255983, 1495990901}, T.W{1249150122, 1856431235},
108   T.W{1555081692, 3175218132}, T.W{1996064986, 2198950837},
109   T.W{2554220882, 3999719339}, T.W{2821834349, 766784016},
110   T.W{2952996808, 2566594879}, T.W{3210313671, 3203337956},
111   T.W{3336571891, 1034457026}, T.W{3584528711, 2466948901},
112   T.W{113926993, 3758326383}, T.W{338241895, 168717936},
113   T.W{666307205, 1188179964}, T.W{773529912, 1546045734},
114   T.W{1294757372, 1522805485}, T.W{1396182291, 2643833823},
115   T.W{1695183700, 2343527390}, T.W{1986661051, 1014477480},
116   T.W{2177026350, 1206759142}, T.W{2456956037, 344077627},
117   T.W{2730485921, 1290863460}, T.W{2820302411, 3158454273},
118   T.W{3259730800, 3505952657}, T.W{3345764771, 106217008},
119   T.W{3516065817, 3606008344}, T.W{3600352804, 1432725776},
120   T.W{4094571909, 1467031594}, T.W{275423344, 851169720},
121   T.W{430227734, 3100823752}, T.W{506948616, 1363258195},
122   T.W{659060556, 3750685593}, T.W{883997877, 3785050280},
123   T.W{958139571, 3318307427}, T.W{1322822218, 3812723403},
124   T.W{1537002063, 2003034995}, T.W{1747873779, 3602036899},
125   T.W{1955562222, 1575990012}, T.W{2024104815, 1125592928},
126   T.W{2227730452, 2716904306}, T.W{2361852424, 442776044},
127   T.W{2428436474, 593698344}, T.W{2756734187, 3733110249},
128   T.W{3204031479, 2999351573}, T.W{3329325298, 3815920427},
129   T.W{3391569614, 3928383900}, T.W{3515267271, 566280711},
130   T.W{3940187606, 3454069534}, T.W{4118630271, 4000239992},
131   T.W{116418474, 1914138554}, T.W{174292421, 2731055270},
132   T.W{289380356, 3203993006}, T.W{460393269, 320620315},
133   T.W{685471733, 587496836}, T.W{852142971, 1086792851},
134   T.W{1017036298, 365543100}, T.W{1126000580, 2618297676},
135   T.W{1288033470, 3409855158}, T.W{1501505948, 4234509866},
136   T.W{1607167915, 987167468}, T.W{1816402316, 1246189591}]
137
138# ---------------------------------------------------------------- section 5.1.2: padding
139
140# A base-256 representation, most significant digit first, of fixed width.
141def octets(width: Nat, +n: Nat) -> List<&2, U32>:
142  match width:
143    case 0n:
144      Nil{}
145    case 1n+p:
146      List.append(&2, U32, octets(p, Nat.div(n, 256n)),
147        [U32.from_nat(Nat.mod(n, 256n))])
148
149# The 128-bit block of the message length in bits, 8n: its low octet is
150# 8 * (n mod 32) and the fifteen above it are n div 32 in base 256
151# (8n = 256 * (n div 32) + 8 * (n mod 32)), so no Nat above n is formed.
152def length_field(+n: Nat) -> List<&2, U32>:
153  List.append(&2, U32, octets(15n, Nat.div(n, 32n)),
154    [U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n)])
155
156# The k zero bytes with n + 1 + k = 112 (mod 128): a remainder of 0..111 leaves
157# room for the length in this block, one of 112..127 needs another block.
158def zero_count_if(r: Nat, fits: Bool) -> Nat:
159  match fits:
160    case True{}:
161      Nat.sub(111n, r)
162    case False{}:
163      Nat.sub(239n, r)
164
165def zero_count(+r: Nat) -> Nat:
166  zero_count_if(r, Nat.is_le(r, 111n))
167
168def padding_suffix(+n: Nat) -> List<&2, U32>:
169  128 <> List.append(&2, U32,
170    List.replicate(U32, zero_count(Nat.mod(n, 128n)), 0), length_field(n))
171
172def pad(+bytes: List<&2, U32>) -> List<&2, U32>:
173  List.append(&2, U32, bytes, padding_suffix(List.length(&2, U32, bytes)))
174
175# ---------------------------------------------------------------- section 5.2.2: parsing
176
177def decode(a: U32, b: U32, c: U32, d: U32) -> U32:
178  U32.or(U32.or(U32.or(U32.shln(U32.and(a, 255), 24n),
179    U32.shln(U32.and(b, 255), 16n)), U32.shln(U32.and(c, 255), 8n)), U32.and(d, 255))
180
181# Big-endian 64-bit words, eight bytes each (a trailing partial word is dropped;
182# padded messages have none).
183def words(bytes: List<&2, U32>) -> List<&2, T.Lane>:
184  match bytes:
185    case a <> b <> c <> d <> e <> f <> g <> h <> rest:
186      T.W{decode(a, b, c, d), decode(e, f, g, h)} <> words(rest)
187    case _:
188      Nil{}
189
190# ---------------------------------------------------------------- section 6.4.2: the schedule
191
192# In reverse history, index j is W[t-1-j]; the zero default makes nth total.
193def nth(history: List<&2, T.Lane>, index: Nat) -> T.Lane:
194  match history index:
195    case Nil{} _:
196      T.W{0, 0}
197    case w <> rest 0n:
198      w
199    case w <> rest 1n+p:
200      nth(rest, p)
201
202def previous(history: List<&2, T.Lane>, lag: Nat) -> T.Lane:
203  nth(history, Nat.sub(lag, 1n))
204
205# W[t] = sigma1(W[t-2]) + W[t-7] + sigma0(W[t-15]) + W[t-16]
206def recurrence(+history: List<&2, T.Lane>) -> T.Lane:
207  add(add(add(sigma1(previous(history, 2n)), previous(history, 7n)),
208    sigma0(previous(history, 15n))), previous(history, 16n))
209
210def extension(rounds: Nat, +history: List<&2, T.Lane>) -> List<&2, T.Lane>:
211  match rounds:
212    case 0n:
213      Nil{}
214    case 1n+p:
215      +w = recurrence(history)
216      w <> extension(p, w <> history)
217
218# SHA-512 instantiates extra = 64, extending the 16 block words to 80.
219def schedule(extra: Nat, +block: List<&2, T.Lane>) -> List<&2, T.Lane>:
220  List.append(&2, T.Lane, block, extension(extra, List.reverse(&2, T.Lane, block)))
221
222def schedules(ws: List<&2, T.Lane>, +extra: Nat) -> List<&2, List<&2, T.Lane>>:
223  match ws:
224    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest:
225      schedule(extra, [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p]) <> schedules(rest, extra)
226    case _:
227      Nil{}
228
229def prepare(bytes: List<&2, U32>, extra: Nat) -> List<&2, List<&2, T.Lane>>:
230  schedules(words(pad(bytes)), extra)
231
232# ---------------------------------------------------------------- section 6.4.2: the rounds
233
234def step(s: T.State, k: T.Lane, w: T.Lane) -> T.State:
235  T.H{+a, +b, +c, d, +e, +f, +g, h} = s
236  +t1 = add(add(add(add(h, sum1(e)), ch(e, f, g)), k), w)
237  t2 = add(sum0(a), maj(a, b, c))
238  T.H{add(t1, t2), a, b, c, add(d, t1), e, f, g}
239
240def rounds(ks: List<&2, T.Lane>, ws: List<&2, T.Lane>) -> T.State -> T.State:
241  match ks ws:
242    case Nil{} _:
243      s => s
244    case k <> kt Nil{}:
245      s => s
246    case k <> kt w <> wt:
247      next = rounds(kt, wt)
248      s => next(step(s, k, w))
249
250def feedforward(x: T.State, y: T.State) -> T.State:
251  T.H{a, b, c, d, e, f, g, h} = x
252  T.H{i, j, k, l, m, n, o, p} = y
253  T.H{add(a, i), add(b, j), add(c, k), add(d, l), add(e, m), add(f, n), add(g, o), add(h, p)}
254
255def compress(ws: List<&2, T.Lane>, ks: List<&2, T.Lane>, +s: T.State) -> T.State:
256  feedforward(s, rounds(ks, ws)(s))
257
258def blocks(prepared: List<&2, List<&2, T.Lane>>, +ks: List<&2, T.Lane>) -> T.State -> T.State:
259  match prepared:
260    case Nil{}:
261      s => s
262    case block <> rest:
263      next = blocks(rest, ks)
264      s => next(compress(block, ks, s))
265
266def digest(s: T.State) -> List<&2, T.Lane>:
267  T.H{a, b, c, d, e, f, g, h} = s
268  [a, b, c, d, e, f, g, h]
269
270def hash(bytes: List<&2, U32>, extra: Nat, ks: List<&2, T.Lane>) -> List<&2, T.Lane>:
271  digest(blocks(prepare(bytes, extra), ks)(initial()))
272
273# SHA-512(M): the eight words H(N).
274def sha512(bytes: List<&2, U32>) -> List<&2, T.Lane>:
275  hash(bytes, 64n, constants())
276
277# ---------------------------------------------------------------- the digest as bytes
278
279# Each word most significant octet first.
280def word_octets(w: T.Lane) -> List<&2, U32>:
281  match w:
282    case T.W{+hi, +lo}:
283      [U32.and(U32.shrn(hi, 24n), 255), U32.and(U32.shrn(hi, 16n), 255),
284       U32.and(U32.shrn(hi, 8n), 255), U32.and(hi, 255),
285       U32.and(U32.shrn(lo, 24n), 255), U32.and(U32.shrn(lo, 16n), 255),
286       U32.and(U32.shrn(lo, 8n), 255), U32.and(lo, 255)]
287
288def digest_octets(ws: List<&2, T.Lane>) -> List<&2, U32>:
289  match ws:
290    case Nil{}:
291      Nil{}
292    case w <> tail:
293      List.append(&2, U32, word_octets(w), digest_octets(tail))
294
295# The 64-byte SHA-512 digest.
296def sha512_bytes(bytes: List<&2, U32>) -> List<&2, U32>:
297  digest_octets(sha512(bytes))