~/jendhub

src/crypto/sha512/core.bend

bend-collections-laws-crypto@1.0.0.0 · 232 lines · 29 definitions

1# Generated by tools/generators/sha512_gen.py; do not edit by hand.
2import Base
3import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T
4
5# SHA-512 (FIPS 180-4) on byte lists. A 64-bit word is two native U32 halves
6# (T.W{hi, lo}); every rotation is fused into its two half-word expressions,
7# the message schedule lives in a rolling window of the last sixteen words
8# (no 80-word list is built), and the round constants are one list walked
9# once per block. Proved equal to spec/crypto/sha512.bend for every input in
10# proofs/crypto/sha512/.
11
12# The sixteen most recent schedule words, newest first: W[t-1] .. W[t-16].
13type Sched is Data:
14  Win{a: T.Lane, b: T.Lane, c: T.Lane, d: T.Lane, e: T.Lane, f: T.Lane, g: T.Lane, h: T.Lane, i: T.Lane, j: T.Lane, k: T.Lane, l: T.Lane, m: T.Lane, n: T.Lane, o: T.Lane, p: T.Lane}
15
16# ---------------------------------------------------------------- 64-bit words
17
18# (a + b) mod 2^64: the carry out of the low halves is 1 exactly when their
19# wrapped sum is below an addend.
20def add(a: T.Lane, b: T.Lane) -> T.Lane:
21  match a b:
22    case T.W{ah, +al} T.W{bh, bl}:
23      +lo = U32.add(al, bl)
24      T.W{U32.add(U32.add(ah, bh), Bool.to_u32(U32.is_lt(lo, al))), lo}
25
26# FIPS 180-4 (4.10): ROTR28 ^ ROTR34 ^ ROTR39
27def big0(x: T.Lane) -> T.Lane:
28  match x:
29    case T.W{+hi, +lo}:
30      T.W{U32.xor(U32.xor(U32.or(U32.shrn(hi, 28n), U32.shln(lo, 4n)), U32.or(U32.shrn(lo, 2n), U32.shln(hi, 30n))), U32.or(U32.shrn(lo, 7n), U32.shln(hi, 25n))),
31        U32.xor(U32.xor(U32.or(U32.shrn(lo, 28n), U32.shln(hi, 4n)), U32.or(U32.shrn(hi, 2n), U32.shln(lo, 30n))), U32.or(U32.shrn(hi, 7n), U32.shln(lo, 25n)))}
32
33# FIPS 180-4 (4.11): ROTR14 ^ ROTR18 ^ ROTR41
34def big1(x: T.Lane) -> T.Lane:
35  match x:
36    case T.W{+hi, +lo}:
37      T.W{U32.xor(U32.xor(U32.or(U32.shrn(hi, 14n), U32.shln(lo, 18n)), U32.or(U32.shrn(hi, 18n), U32.shln(lo, 14n))), U32.or(U32.shrn(lo, 9n), U32.shln(hi, 23n))),
38        U32.xor(U32.xor(U32.or(U32.shrn(lo, 14n), U32.shln(hi, 18n)), U32.or(U32.shrn(lo, 18n), U32.shln(hi, 14n))), U32.or(U32.shrn(hi, 9n), U32.shln(lo, 23n)))}
39
40# FIPS 180-4 (4.12): ROTR1 ^ ROTR8 ^ SHR7
41def small0(x: T.Lane) -> T.Lane:
42  match x:
43    case T.W{+hi, +lo}:
44      T.W{U32.xor(U32.xor(U32.or(U32.shrn(hi, 1n), U32.shln(lo, 31n)), U32.or(U32.shrn(hi, 8n), U32.shln(lo, 24n))), U32.shrn(hi, 7n)),
45        U32.xor(U32.xor(U32.or(U32.shrn(lo, 1n), U32.shln(hi, 31n)), U32.or(U32.shrn(lo, 8n), U32.shln(hi, 24n))), U32.or(U32.shrn(lo, 7n), U32.shln(hi, 25n)))}
46
47# FIPS 180-4 (4.13): ROTR19 ^ ROTR61 ^ SHR6
48def small1(x: T.Lane) -> T.Lane:
49  match x:
50    case T.W{+hi, +lo}:
51      T.W{U32.xor(U32.xor(U32.or(U32.shrn(hi, 19n), U32.shln(lo, 13n)), U32.or(U32.shrn(lo, 29n), U32.shln(hi, 3n))), U32.shrn(hi, 6n)),
52        U32.xor(U32.xor(U32.or(U32.shrn(lo, 19n), U32.shln(hi, 13n)), U32.or(U32.shrn(hi, 29n), U32.shln(lo, 3n))), U32.or(U32.shrn(lo, 6n), U32.shln(hi, 26n)))}
53
54def choose(x: T.Lane, y: T.Lane, z: T.Lane) -> T.Lane:
55  match x y z:
56    case T.W{+xh, +xl} T.W{yh, yl} T.W{zh, zl}:
57      T.W{U32.xor(U32.and(xh, yh), U32.and(U32.not(xh), zh)),
58        U32.xor(U32.and(xl, yl), U32.and(U32.not(xl), zl))}
59
60def majority(x: T.Lane, y: T.Lane, z: T.Lane) -> T.Lane:
61  match x y z:
62    case T.W{+xh, +xl} T.W{+yh, +yl} T.W{+zh, +zl}:
63      T.W{U32.xor(U32.xor(U32.and(xh, yh), U32.and(xh, zh)), U32.and(yh, zh)),
64        U32.xor(U32.xor(U32.and(xl, yl), U32.and(xl, zl)), U32.and(yl, zl))}
65
66# ---------------------------------------------------------------- one round, one block
67
68def step(s: T.State, k: T.Lane, w: T.Lane) -> T.State:
69  T.H{+a, +b, +c, d, +e, +f, +g, h} = s
70  +t1 = add(add(add(add(h, big1(e)), choose(e, f, g)), k), w)
71  t2 = add(big0(a), majority(a, b, c))
72  T.H{add(t1, t2), a, b, c, add(d, t1), e, f, g}
73
74def feedforward(x: T.State, y: T.State) -> T.State:
75  T.H{a, b, c, d, e, f, g, h} = x
76  T.H{i, j, k, l, m, n, o, p} = y
77  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)}
78
79# W[t] from W[t-2], W[t-7], W[t-15], W[t-16].
80def next(+w2: T.Lane, w7: T.Lane, +w15: T.Lane, w16: T.Lane) -> T.Lane:
81  add(add(add(small1(w2), w7), small0(w15)), w16)
82
83# The remaining q rounds (64 after the block's own sixteen): each derives its
84# schedule word from the window, then drops the oldest word.
85def window_rounds(q: Nat, win: Sched, ks: List<&2, T.Lane>, s: T.State) -> T.State:
86  match q win ks:
87    case 0n _ _:
88      s
89    case 1n+r _ Nil{}:
90      s
91    case 1n+r Win{a, +b, c, d, e, f, +g, h, i, j, k, l, m, n, +o, +p} x <> xt:
92      +w = next(b, g, o, p)
93      window_rounds(r, Win{w, a, b, c, d, e, f, g, h, i, j, k, l, m, n, o}, xt, step(s, x, w))
94
95# The block's own words first, then q window rounds (q = 64 for SHA-512);
96# win is the block reversed.
97def block_rounds(ws: List<&2, T.Lane>, +q: Nat, win: Sched, ks: List<&2, T.Lane>, s: T.State) -> T.State:
98  match ws ks:
99    case Nil{} _:
100      window_rounds(q, win, ks, s)
101    case w <> wt Nil{}:
102      s
103    case w <> wt k <> kt:
104      block_rounds(wt, q, win, kt, step(s, k, w))
105
106def compress16(+a: T.Lane, +b: T.Lane, +c: T.Lane, +d: T.Lane,
107  +e: T.Lane, +f: T.Lane, +g: T.Lane, +h: T.Lane,
108  +i: T.Lane, +j: T.Lane, +k: T.Lane, +l: T.Lane,
109  +m: T.Lane, +n: T.Lane, +o: T.Lane, +p: T.Lane, +q: Nat, ks: List<&2, T.Lane>, +s: T.State) -> T.State:
110  feedforward(s, block_rounds([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], q,
111    Win{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, ks, s))
112
113# Every whole block of sixteen words; a shorter tail is ignored (padded
114# messages have none).
115def blocks(ws: List<&2, T.Lane>, +q: Nat, +ks: List<&2, T.Lane>, s: T.State) -> T.State:
116  match ws:
117    case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest:
118      blocks(rest, q, ks, compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s))
119    case _:
120      s
121
122# ---------------------------------------------------------------- bytes in and out
123
124def pack(a: U32, b: U32, c: U32, d: U32) -> U32:
125  U32.or(U32.or(U32.or(U32.shln(U32.and(a, 255), 24n),
126    U32.shln(U32.and(b, 255), 16n)), U32.shln(U32.and(c, 255), 8n)), U32.and(d, 255))
127
128# Big-endian 64-bit words, eight bytes each.
129def lanes(bytes: List<&2, U32>) -> List<&2, T.Lane>:
130  match bytes:
131    case a <> b <> c <> d <> e <> f <> g <> h <> rest:
132      T.W{pack(a, b, c, d), pack(e, f, g, h)} <> lanes(rest)
133    case _:
134      Nil{}
135
136def base256(width: Nat, +n: Nat) -> List<&2, U32>:
137  match width:
138    case 0n:
139      Nil{}
140    case 1n+p:
141      List.append(&2, U32, base256(p, Nat.div(n, 256n)), [U32.from_nat(Nat.mod(n, 256n))])
142
143# 8n as sixteen big-endian octets: n div 32 in the top fifteen, 8 (n mod 32) last.
144def bit_length(+n: Nat) -> List<&2, U32>:
145  List.append(&2, U32, base256(15n, Nat.div(n, 32n)), [U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n)])
146
147def zeros_if(r: Nat, fits: Bool) -> Nat:
148  match fits:
149    case True{}:
150      Nat.sub(111n, r)
151    case False{}:
152      Nat.sub(239n, r)
153
154def zeros(+r: Nat) -> Nat:
155  zeros_if(r, Nat.is_le(r, 111n))
156
157# 0x80, zeros up to 112 mod 128, then the 128-bit bit length.
158def suffix(+n: Nat) -> List<&2, U32>:
159  128 <> List.append(&2, U32, List.replicate(U32, zeros(Nat.mod(n, 128n)), 0), bit_length(n))
160
161def octets(+x: U32, tail: List<&2, U32>) -> List<&2, U32>:
162  U32.and(U32.shrn(x, 24n), 255) <> U32.and(U32.shrn(x, 16n), 255) <>
163  U32.and(U32.shrn(x, 8n), 255) <> U32.and(x, 255) <> tail
164
165def lane_octets(l: T.Lane, tail: List<&2, U32>) -> List<&2, U32>:
166  match l:
167    case T.W{+hi, +lo}:
168      octets(hi, octets(lo, tail))
169
170# The 64-byte digest H0 .. H7.
171def digest_bytes(s: T.State) -> List<&2, U32>:
172  T.H{a, b, c, d, e, f, g, h} = s
173  lane_octets(a, lane_octets(b, lane_octets(c, lane_octets(d,
174    lane_octets(e, lane_octets(f, lane_octets(g, lane_octets(h, Nil{}))))))))
175
176# ---------------------------------------------------------------- constants
177
178def initial() -> T.State:
179  T.H{T.W{1779033703, 4089235720}, T.W{3144134277, 2227873595},
180    T.W{1013904242, 4271175723}, T.W{2773480762, 1595750129},
181    T.W{1359893119, 2917565137}, T.W{2600822924, 725511199},
182    T.W{528734635, 4215389547}, T.W{1541459225, 327033209}}
183
184def round_constants() -> List<&2, T.Lane>:
185  [T.W{1116352408, 3609767458}, T.W{1899447441, 602891725},
186   T.W{3049323471, 3964484399}, T.W{3921009573, 2173295548},
187   T.W{961987163, 4081628472}, T.W{1508970993, 3053834265},
188   T.W{2453635748, 2937671579}, T.W{2870763221, 3664609560},
189   T.W{3624381080, 2734883394}, T.W{310598401, 1164996542},
190   T.W{607225278, 1323610764}, T.W{1426881987, 3590304994},
191   T.W{1925078388, 4068182383}, T.W{2162078206, 991336113},
192   T.W{2614888103, 633803317}, T.W{3248222580, 3479774868},
193   T.W{3835390401, 2666613458}, T.W{4022224774, 944711139},
194   T.W{264347078, 2341262773}, T.W{604807628, 2007800933},
195   T.W{770255983, 1495990901}, T.W{1249150122, 1856431235},
196   T.W{1555081692, 3175218132}, T.W{1996064986, 2198950837},
197   T.W{2554220882, 3999719339}, T.W{2821834349, 766784016},
198   T.W{2952996808, 2566594879}, T.W{3210313671, 3203337956},
199   T.W{3336571891, 1034457026}, T.W{3584528711, 2466948901},
200   T.W{113926993, 3758326383}, T.W{338241895, 168717936},
201   T.W{666307205, 1188179964}, T.W{773529912, 1546045734},
202   T.W{1294757372, 1522805485}, T.W{1396182291, 2643833823},
203   T.W{1695183700, 2343527390}, T.W{1986661051, 1014477480},
204   T.W{2177026350, 1206759142}, T.W{2456956037, 344077627},
205   T.W{2730485921, 1290863460}, T.W{2820302411, 3158454273},
206   T.W{3259730800, 3505952657}, T.W{3345764771, 106217008},
207   T.W{3516065817, 3606008344}, T.W{3600352804, 1432725776},
208   T.W{4094571909, 1467031594}, T.W{275423344, 851169720},
209   T.W{430227734, 3100823752}, T.W{506948616, 1363258195},
210   T.W{659060556, 3750685593}, T.W{883997877, 3785050280},
211   T.W{958139571, 3318307427}, T.W{1322822218, 3812723403},
212   T.W{1537002063, 2003034995}, T.W{1747873779, 3602036899},
213   T.W{1955562222, 1575990012}, T.W{2024104815, 1125592928},
214   T.W{2227730452, 2716904306}, T.W{2361852424, 442776044},
215   T.W{2428436474, 593698344}, T.W{2756734187, 3733110249},
216   T.W{3204031479, 2999351573}, T.W{3329325298, 3815920427},
217   T.W{3391569614, 3928383900}, T.W{3515267271, 566280711},
218   T.W{3940187606, 3454069534}, T.W{4118630271, 4000239992},
219   T.W{116418474, 1914138554}, T.W{174292421, 2731055270},
220   T.W{289380356, 3203993006}, T.W{460393269, 320620315},
221   T.W{685471733, 587496836}, T.W{852142971, 1086792851},
222   T.W{1017036298, 365543100}, T.W{1126000580, 2618297676},
223   T.W{1288033470, 3409855158}, T.W{1501505948, 4234509866},
224   T.W{1607167915, 987167468}, T.W{1816402316, 1246189591}]
225
226# ---------------------------------------------------------------- SHA-512
227
228def hash_padded(bytes: List<&2, U32>) -> List<&2, U32>:
229  digest_bytes(blocks(lanes(bytes), 64n, round_constants(), initial()))
230
231def sha512(+bytes: List<&2, U32>) -> List<&2, U32>:
232  hash_padded(List.append(&2, U32, bytes, suffix(List.length(&2, U32, bytes))))