1 import Base 2 import ../../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. 19 def 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 25 def 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 30 def 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 35 def 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. 42 def 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. 47 def 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. 55 def 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. 61 def 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 68 def sum0(+x: T.Lane) -> T.Lane: 69 xor(xor(rotr(x, 28n), rotr(x, 34n)), rotr(x, 39n)) 70 71 def sum1(+x: T.Lane) -> T.Lane: 72 xor(xor(rotr(x, 14n), rotr(x, 18n)), rotr(x, 41n)) 73 74 def sigma0(+x: T.Lane) -> T.Lane: 75 xor(xor(rotr(x, 1n), rotr(x, 8n)), shr(x, 7n)) 76 77 def sigma1(+x: T.Lane) -> T.Lane: 78 xor(xor(rotr(x, 19n), rotr(x, 61n)), shr(x, 6n)) 79 80 def ch(+x: T.Lane, y: T.Lane, z: T.Lane) -> T.Lane: 81 xor(and(x, y), and(not(x), z)) 82 83 def 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). 89 def 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. 96 def 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. 141 def 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. 152 def 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. 158 def 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 165 def zero_count(+r: Nat) -> Nat: 166 zero_count_if(r, Nat.is_le(r, 111n)) 167 168 def 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 172 def 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 177 def 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). 183 def 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. 193 def 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 202 def 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] 206 def 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 210 def 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. 219 def 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 222 def 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 229 def 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 234 def 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 240 def 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 250 def 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 255 def compress(ws: List<&2, T.Lane>, ks: List<&2, T.Lane>, +s: T.State) -> T.State: 256 feedforward(s, rounds(ks, ws)(s)) 257 258 def 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 266 def 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 270 def 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). 274 def 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. 280 def 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 288 def 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. 296 def sha512_bytes(bytes: List<&2, U32>) -> List<&2, U32>: 297 digest_octets(sha512(bytes))