src/crypto/sha512/core.bend source
src/crypto/sha512/core.bend on the hub · documented module
# Generated by tools/generators/sha512_gen.py; do not edit by hand.import Baseimport ./types.bend as T# SHA-512 (FIPS 180-4) on byte lists. A 64-bit word is two native U32 halves# (T.W{hi, lo}); every rotation is fused into its two half-word expressions,# the message schedule lives in a rolling window of the last sixteen words# (no 80-word list is built), and the round constants are one list walked# once per block. Proved equal to spec/crypto/sha512.bend for every input in# proofs/crypto/sha512/.# The sixteen most recent schedule words, newest first: W[t-1] .. W[t-16].type Sched is Data: 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}# ---------------------------------------------------------------- 64-bit words# (a + b) mod 2^64: the carry out of the low halves is 1 exactly when their# wrapped sum is below an addend.def add(a: T.Lane, b: T.Lane) -> T.Lane: match a b: case T.W{ah, +al} T.W{bh, bl}: +lo = U32.add(al, bl) T.W{U32.add(U32.add(ah, bh), Bool.to_u32(U32.is_lt(lo, al))), lo}# FIPS 180-4 (4.10): ROTR28 ^ ROTR34 ^ ROTR39def big0(x: T.Lane) -> T.Lane: match x: case T.W{+hi, +lo}: 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))), 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)))}# FIPS 180-4 (4.11): ROTR14 ^ ROTR18 ^ ROTR41def big1(x: T.Lane) -> T.Lane: match x: case T.W{+hi, +lo}: 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))), 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)))}# FIPS 180-4 (4.12): ROTR1 ^ ROTR8 ^ SHR7def small0(x: T.Lane) -> T.Lane: match x: case T.W{+hi, +lo}: 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)), 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)))}# FIPS 180-4 (4.13): ROTR19 ^ ROTR61 ^ SHR6def small1(x: T.Lane) -> T.Lane: match x: case T.W{+hi, +lo}: 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)), 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)))}def choose(x: T.Lane, y: T.Lane, z: T.Lane) -> T.Lane: match x y z: case T.W{+xh, +xl} T.W{yh, yl} T.W{zh, zl}: T.W{U32.xor(U32.and(xh, yh), U32.and(U32.not(xh), zh)), U32.xor(U32.and(xl, yl), U32.and(U32.not(xl), zl))}def majority(x: T.Lane, y: T.Lane, z: T.Lane) -> T.Lane: match x y z: case T.W{+xh, +xl} T.W{+yh, +yl} T.W{+zh, +zl}: T.W{U32.xor(U32.xor(U32.and(xh, yh), U32.and(xh, zh)), U32.and(yh, zh)), U32.xor(U32.xor(U32.and(xl, yl), U32.and(xl, zl)), U32.and(yl, zl))}# ---------------------------------------------------------------- one round, one blockdef step(s: T.State, k: T.Lane, w: T.Lane) -> T.State: T.H{+a, +b, +c, d, +e, +f, +g, h} = s +t1 = add(add(add(add(h, big1(e)), choose(e, f, g)), k), w) t2 = add(big0(a), majority(a, b, c)) T.H{add(t1, t2), a, b, c, add(d, t1), e, f, g}def feedforward(x: T.State, y: T.State) -> T.State: T.H{a, b, c, d, e, f, g, h} = x T.H{i, j, k, l, m, n, o, p} = y 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)}# W[t] from W[t-2], W[t-7], W[t-15], W[t-16].def next(+w2: T.Lane, w7: T.Lane, +w15: T.Lane, w16: T.Lane) -> T.Lane: add(add(add(small1(w2), w7), small0(w15)), w16)# The remaining q rounds (64 after the block's own sixteen): each derives its# schedule word from the window, then drops the oldest word.def window_rounds(q: Nat, win: Sched, ks: List<&2, T.Lane>, s: T.State) -> T.State: match q win ks: case 0n _ _: s case 1n+r _ Nil{}: s case 1n+r Win{a, +b, c, d, e, f, +g, h, i, j, k, l, m, n, +o, +p} x <> xt: +w = next(b, g, o, p) 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))# The block's own words first, then q window rounds (q = 64 for SHA-512);# win is the block reversed.def block_rounds(ws: List<&2, T.Lane>, +q: Nat, win: Sched, ks: List<&2, T.Lane>, s: T.State) -> T.State: match ws ks: case Nil{} _: window_rounds(q, win, ks, s) case w <> wt Nil{}: s case w <> wt k <> kt: block_rounds(wt, q, win, kt, step(s, k, w))def compress16(+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, +q: Nat, ks: List<&2, T.Lane>, +s: T.State) -> T.State: feedforward(s, block_rounds([a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p], q, Win{p, o, n, m, l, k, j, i, h, g, f, e, d, c, b, a}, ks, s))# Every whole block of sixteen words; a shorter tail is ignored (padded# messages have none).def blocks(ws: List<&2, T.Lane>, +q: Nat, +ks: List<&2, T.Lane>, s: T.State) -> T.State: match ws: case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> rest: blocks(rest, q, ks, compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, ks, s)) case _: s# ---------------------------------------------------------------- bytes in and outdef pack(a: U32, b: U32, c: U32, d: U32) -> U32: U32.or(U32.or(U32.or(U32.shln(U32.and(a, 255), 24n), U32.shln(U32.and(b, 255), 16n)), U32.shln(U32.and(c, 255), 8n)), U32.and(d, 255))# Big-endian 64-bit words, eight bytes each.def lanes(bytes: List<&2, U32>) -> List<&2, T.Lane>: match bytes: case a <> b <> c <> d <> e <> f <> g <> h <> rest: T.W{pack(a, b, c, d), pack(e, f, g, h)} <> lanes(rest) case _: Nil{}def base256(width: Nat, +n: Nat) -> List<&2, U32>: match width: case 0n: Nil{} case 1n+p: List.append(&2, U32, base256(p, Nat.div(n, 256n)), [U32.from_nat(Nat.mod(n, 256n))])# 8n as sixteen big-endian octets: n div 32 in the top fifteen, 8 (n mod 32) last.def bit_length(+n: Nat) -> List<&2, U32>: List.append(&2, U32, base256(15n, Nat.div(n, 32n)), [U32.shln(U32.from_nat(Nat.mod(n, 32n)), 3n)])def zeros_if(r: Nat, fits: Bool) -> Nat: match fits: case True{}: Nat.sub(111n, r) case False{}: Nat.sub(239n, r)def zeros(+r: Nat) -> Nat: zeros_if(r, Nat.is_le(r, 111n))# 0x80, zeros up to 112 mod 128, then the 128-bit bit length.def suffix(+n: Nat) -> List<&2, U32>: 128 <> List.append(&2, U32, List.replicate(U32, zeros(Nat.mod(n, 128n)), 0), bit_length(n))def octets(+x: U32, tail: List<&2, U32>) -> List<&2, U32>: U32.and(U32.shrn(x, 24n), 255) <> U32.and(U32.shrn(x, 16n), 255) <> U32.and(U32.shrn(x, 8n), 255) <> U32.and(x, 255) <> taildef lane_octets(l: T.Lane, tail: List<&2, U32>) -> List<&2, U32>: match l: case T.W{+hi, +lo}: octets(hi, octets(lo, tail))# The 64-byte digest H0 .. H7.def digest_bytes(s: T.State) -> List<&2, U32>: T.H{a, b, c, d, e, f, g, h} = s lane_octets(a, lane_octets(b, lane_octets(c, lane_octets(d, lane_octets(e, lane_octets(f, lane_octets(g, lane_octets(h, Nil{}))))))))# ---------------------------------------------------------------- constantsdef initial() -> T.State: T.H{T.W{1779033703, 4089235720}, T.W{3144134277, 2227873595}, T.W{1013904242, 4271175723}, T.W{2773480762, 1595750129}, T.W{1359893119, 2917565137}, T.W{2600822924, 725511199}, T.W{528734635, 4215389547}, T.W{1541459225, 327033209}}def round_constants() -> List<&2, T.Lane>: [T.W{1116352408, 3609767458}, T.W{1899447441, 602891725}, T.W{3049323471, 3964484399}, T.W{3921009573, 2173295548}, T.W{961987163, 4081628472}, T.W{1508970993, 3053834265}, T.W{2453635748, 2937671579}, T.W{2870763221, 3664609560}, T.W{3624381080, 2734883394}, T.W{310598401, 1164996542}, T.W{607225278, 1323610764}, T.W{1426881987, 3590304994}, T.W{1925078388, 4068182383}, T.W{2162078206, 991336113}, T.W{2614888103, 633803317}, T.W{3248222580, 3479774868}, T.W{3835390401, 2666613458}, T.W{4022224774, 944711139}, T.W{264347078, 2341262773}, T.W{604807628, 2007800933}, T.W{770255983, 1495990901}, T.W{1249150122, 1856431235}, T.W{1555081692, 3175218132}, T.W{1996064986, 2198950837}, T.W{2554220882, 3999719339}, T.W{2821834349, 766784016}, T.W{2952996808, 2566594879}, T.W{3210313671, 3203337956}, T.W{3336571891, 1034457026}, T.W{3584528711, 2466948901}, T.W{113926993, 3758326383}, T.W{338241895, 168717936}, T.W{666307205, 1188179964}, T.W{773529912, 1546045734}, T.W{1294757372, 1522805485}, T.W{1396182291, 2643833823}, T.W{1695183700, 2343527390}, T.W{1986661051, 1014477480}, T.W{2177026350, 1206759142}, T.W{2456956037, 344077627}, T.W{2730485921, 1290863460}, T.W{2820302411, 3158454273}, T.W{3259730800, 3505952657}, T.W{3345764771, 106217008}, T.W{3516065817, 3606008344}, T.W{3600352804, 1432725776}, T.W{4094571909, 1467031594}, T.W{275423344, 851169720}, T.W{430227734, 3100823752}, T.W{506948616, 1363258195}, T.W{659060556, 3750685593}, T.W{883997877, 3785050280}, T.W{958139571, 3318307427}, T.W{1322822218, 3812723403}, T.W{1537002063, 2003034995}, T.W{1747873779, 3602036899}, T.W{1955562222, 1575990012}, T.W{2024104815, 1125592928}, T.W{2227730452, 2716904306}, T.W{2361852424, 442776044}, T.W{2428436474, 593698344}, T.W{2756734187, 3733110249}, T.W{3204031479, 2999351573}, T.W{3329325298, 3815920427}, T.W{3391569614, 3928383900}, T.W{3515267271, 566280711}, T.W{3940187606, 3454069534}, T.W{4118630271, 4000239992}, T.W{116418474, 1914138554}, T.W{174292421, 2731055270}, T.W{289380356, 3203993006}, T.W{460393269, 320620315}, T.W{685471733, 587496836}, T.W{852142971, 1086792851}, T.W{1017036298, 365543100}, T.W{1126000580, 2618297676}, T.W{1288033470, 3409855158}, T.W{1501505948, 4234509866}, T.W{1607167915, 987167468}, T.W{1816402316, 1246189591}]# ---------------------------------------------------------------- SHA-512def hash_padded(bytes: List<&2, U32>) -> List<&2, U32>: digest_bytes(blocks(lanes(bytes), 64n, round_constants(), initial()))def sha512(+bytes: List<&2, U32>) -> List<&2, U32>: hash_padded(List.append(&2, U32, bytes, suffix(List.length(&2, U32, bytes))))