1 # Vendored from bend-collections 0x9ee2e9a299991dcc089fe22c7f3ceb5f 2 # (src/crypto/sha/sha256.bend), byte-identical. See core.bend header. 3 import Base 4 import ./core.bend as Core 5 import ./state.bend as S 6 import bend-kit-bytes@0.3.2.0/bytes.bend as Packed 7 import ../coordinator/QueuePolicy.bend as QueuePolicy 8 9 # Describes failures while enforcing the streaming hash input bound. 10 type StreamError is Data: 11 ResourceLimit{} 12 13 # Retains the compressed hash state and one incomplete block. 14 type Stream is Type: 15 Stream{compressed: S.State, tail: Packed.Bytes, total: Nat} 16 17 # The core refinement theorem quantifies over every constant table. 18 # Instantiate the verified core with the FIPS 180-4 constants. 19 def constants() -> List<&2, U32>: 20 [1116352408, 1899447441, 3049323471, 3921009573, 21 961987163, 1508970993, 2453635748, 2870763221, 22 3624381080, 310598401, 607225278, 1426881987, 23 1925078388, 2162078206, 2614888103, 3248222580, 24 3835390401, 4022224774, 264347078, 604807628, 25 770255983, 1249150122, 1555081692, 1996064986, 26 2554220882, 2821834349, 2952996808, 3210313671, 27 3336571891, 3584528711, 113926993, 338241895, 28 666307205, 773529912, 1294757372, 1396182291, 29 1695183700, 1986661051, 2177026350, 2456956037, 30 2730485921, 2820302411, 3259730800, 3345764771, 31 3516065817, 3600352804, 4094571909, 275423344, 32 430227734, 506948616, 659060556, 883997877, 33 958139571, 1322822218, 1537002063, 1747873779, 34 1955562222, 2024104815, 2227730452, 2361852424, 35 2428436474, 2756734187, 3204031479, 3329325298] 36 37 # SHA-256 for the reference octet-list input. 38 def sha256(bytes: List<&2, U32>) -> List<&2, U32>: 39 Core.sha256(bytes) 40 41 # Convert ASCII text to the reference octet-list input. 42 def ascii(text: String) -> List<&2, U32>: 43 Core.ascii(text) 44 45 # Format eight digest words as lowercase hexadecimal. 46 def hex(ws: List<&2, U32>) -> String: 47 Core.hex(ws) 48 49 # Big-endian octets, represented as U32 values in 0..255. 50 def digest_bytes(ws: List<&2, U32>) -> List<&2, U32>: 51 match ws: 52 case Nil{}: 53 Nil{} 54 case +w <> tail: 55 U32.and(U32.shrn(w, 24n), 255) <> 56 U32.and(U32.shrn(w, 16n), 255) <> 57 U32.and(U32.shrn(w, 8n), 255) <> 58 U32.and(w, 255) <> digest_bytes(tail) 59 60 # Return the reference digest as eight big-endian octets per word. 61 def sha256_bytes(bytes: List<&2, U32>) -> List<&2, U32>: 62 digest_bytes(sha256(bytes)) 63 64 # Compress one packed block using sixteen transient big-endian words. The file 65 # buffer stays packed; no per-byte List is constructed for complete blocks. 66 def packed.compress(words: List<&2, U32>, state: S.State) -> S.State: 67 match words: 68 case a <> b <> c <> d <> e <> f <> g <> h <> i <> j <> k <> l <> m <> n <> o <> p <> Nil{}: 69 Core.fips_compress16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, 48n, state) 70 case _: 71 state 72 73 # Read complete 64-byte blocks directly through a bounded package cursor. 74 def packed.blocks( 75 remaining: Nat, 76 in_block: Nat, 77 pair: Packed.Cursor & Maybe<&2, U32>, 78 acc: List<&2, U32>, 79 state: S.State 80 ) -> Packed.Cursor & S.State: 81 match remaining: 82 case 0n: 83 match pair: 84 case (cursor, _): 85 (cursor, state) 86 case 1n: 87 match in_block: 88 case 0n: 89 match pair: 90 case (cursor, _): 91 (cursor, state) 92 case 1n: 93 match pair: 94 case (cursor, Some{word}): 95 (cursor, packed.compress(List.reverse(&2, U32, word <> acc), state)) 96 case (cursor, None{}): 97 (cursor, state) 98 case 1n+more: 99 match pair: 100 case (cursor, _): 101 (cursor, state) 102 case 1n+more: 103 match in_block: 104 case 0n: 105 match pair: 106 case (cursor, _): 107 (cursor, state) 108 case 1n: 109 match pair: 110 case (cursor, Some{word}): 111 packed.blocks(more, 16n, Packed.Cursor.u32be(cursor), Nil{}, 112 packed.compress(List.reverse(&2, U32, word <> acc), state)) 113 case (cursor, None{}): 114 (cursor, state) 115 case 1n+left: 116 match pair: 117 case (cursor, Some{word}): 118 packed.blocks(more, left, Packed.Cursor.u32be(cursor), word <> acc, state) 119 case (cursor, None{}): 120 (cursor, state) 121 122 # Read the remaining fewer than 64 bytes for the existing constant-space tail 123 # padding routines. This list is bounded by 63 octets, regardless of file size. 124 def packed.tail( 125 remaining: Nat, 126 pair: Packed.Cursor & Maybe<&2, U32>, 127 acc: List<&2, U32> 128 ) -> Packed.Cursor & List<&2, U32>: 129 match remaining: 130 case 0n: 131 match pair: 132 case (cursor, _): 133 (cursor, List.reverse(&2, U32, acc)) 134 case 1n: 135 match pair: 136 case (cursor, Some{byte}): 137 (cursor, List.reverse(&2, U32, byte <> acc)) 138 case (cursor, None{}): 139 (cursor, Nil{}) 140 case 1n+more: 141 match pair: 142 case (cursor, Some{byte}): 143 packed.tail(more, Packed.Cursor.u8(cursor), byte <> acc) 144 case (cursor, None{}): 145 (cursor, Nil{}) 146 147 def packed.finish.tail(total: U32, pair: Packed.Cursor & List<&2, U32>, state: S.State) -> S.State: 148 match pair: 149 case (_, tail): 150 Core.finish_n(tail, U32.to_nat(total), 48n, state) 151 152 def packed.final.tail(total: U32, tail_len: Nat, cursor: Packed.Cursor, state: S.State) -> S.State: 153 match tail_len: 154 case 0n: 155 packed.finish.tail(total, (cursor, Nil{}), state) 156 case 1n+more: 157 packed.finish.tail(total, packed.tail(1n+more, Packed.Cursor.u8(cursor), Nil{}), state) 158 159 def packed.final(total: U32, tail_len: Nat, cursor: Packed.Cursor, state: S.State) -> List<&2, U32>: 160 Core.digest(packed.final.tail(total, tail_len, cursor, state)) 161 162 def packed.after_blocks(total: U32, tail_len: Nat, pair: Packed.Cursor & S.State) -> List<&2, U32>: 163 match pair: 164 case (cursor, state): 165 packed.final(total, tail_len, cursor, state) 166 167 def packed.start.blocks(+total: U32, cursor: Packed.Cursor, blocks: Nat, +tail_len: Nat) -> List<&2, U32>: 168 match blocks: 169 case 0n: 170 packed.final(total, tail_len, cursor, Core.initial()) 171 case 1n+more: 172 packed.after_blocks(total, tail_len, 173 packed.blocks(((1n+more) * 16n : Nat), 16n, Packed.Cursor.u32be(cursor), Nil{}, Core.initial())) 174 175 def packed.start(+total: U32, cursor: Packed.Cursor) -> List<&2, U32>: 176 packed.start.blocks(total, cursor, 177 Nat.div(U32.to_nat(total), 64n), Nat.mod(U32.to_nat(total), 64n)) 178 179 # SHA-256 directly over packed bytes. Full blocks are read as sixteen u32be 180 # words; only the final 0..63 octets use the existing tail padding interface. 181 def sha256_packed(bytes: Packed.Bytes) -> List<&2, U32>: 182 match bytes: 183 case Packed.Bytes{+len, buf}: 184 packed.start(len, Packed.Cursor.new(Packed.Bytes{len, buf})) 185 186 def packed.digest.finish.bytes(pair: Packed.Bytes & U32) -> Packed.Bytes: 187 match pair: 188 case (bytes, _): 189 bytes 190 191 def packed.digest.finish(pair: Packed.Cursor & Bool) -> Packed.Bytes: 192 match pair: 193 case (cursor, _): 194 packed.digest.finish.bytes(Packed.Cursor.finish(cursor)) 195 196 def packed.digest.words(words: List<&2, U32>, pair: Packed.Cursor & Bool) -> Packed.Bytes: 197 match words: 198 case Nil{}: 199 packed.digest.finish(pair) 200 case word <> rest: 201 match pair: 202 case (cursor, _) : 203 packed.digest.words(rest, Packed.Cursor.put.u32be(cursor, word)) 204 205 # Return the SHA-256 digest as packed bytes in canonical big-endian order. 206 def sha256_packed_bytes(bytes: Packed.Bytes) -> Packed.Bytes: 207 packed.digest.words(sha256_packed(bytes), 208 (Packed.Cursor.new(Packed.Bytes{32, Packed.alloc(32)}), True{})) 209 210 def stream.empty.bytes() -> Packed.Bytes: 211 Packed.Bytes{0, Packed.alloc(0)} 212 213 def stream.initial() -> Stream: 214 Stream{Core.initial(), stream.empty.bytes(), 0n} 215 216 def stream.clone.bytes(+len: U32, copies: Array & Array) -> Packed.Bytes & Packed.Bytes: 217 match copies: 218 case (left, right): 219 (Packed.Bytes{len, left}, Packed.Bytes{len, right}) 220 221 def stream.clone.tail( 222 +compressed: S.State, 223 totals: Nat & Nat, 224 copies: Packed.Bytes & Packed.Bytes 225 ) -> Stream & Stream: 226 match totals: 227 case (left_total, right_total): 228 match copies: 229 case (left_tail, right_tail): 230 (Stream{compressed, left_tail, left_total}, 231 Stream{compressed, right_tail, right_total}) 232 233 def stream.clone.parts( 234 +compressed: S.State, 235 totals: Nat & Nat, 236 tail: Packed.Bytes 237 ) -> Stream & Stream: 238 match tail: 239 case Packed.Bytes{+len, buf}: 240 stream.clone.tail(compressed, totals, 241 stream.clone.bytes(len, Packed.copy.bytes(len, buf, 242 Packed.alloc(len), 0, 0))) 243 244 def stream.clone(state: Stream) -> Stream & Stream: 245 match state: 246 case Stream{compressed, tail, +total}: 247 stream.clone.parts(compressed, QueuePolicy.nat.clone.pair(total), tail) 248 249 def stream.length(pair: Packed.Bytes & U32) -> U32: 250 match pair: 251 case (_, size): size 252 253 def stream.count(pair: Packed.Cursor & S.State) -> S.State: 254 match pair: 255 case (_, compressed): compressed 256 257 def stream.compress(bytes: Packed.Bytes, compressed: S.State) -> S.State: 258 match bytes: 259 case Packed.Bytes{+len, buf}: 260 stream.count(packed.blocks( 261 Nat.mul(Nat.div(U32.to_nat(len), 64n), 16n), 16n, 262 Packed.Cursor.u32be(Packed.Cursor.new(Packed.Bytes{len, buf})), 263 Nil{}, compressed)) 264 265 def stream.tail.result.sliced( 266 +compressed: S.State, 267 complete: Packed.Bytes, 268 pair: Packed.Bytes & Packed.Bytes, 269 total: Nat 270 ) -> Result<&1, &1, StreamError, Stream>: 271 match pair: 272 case (_, tail): 273 Done{Stream{stream.compress(complete, compressed), tail, total}} 274 def stream.tail.result( 275 +compressed: S.State, 276 joined: Packed.Bytes, 277 complete: Packed.Bytes, 278 full_length: Nat, 279 remainder: Nat, 280 total: Nat 281 ) -> Result<&1, &1, StreamError, Stream>: 282 stream.tail.result.sliced(compressed, complete, 283 Packed.slice(joined, U32.from_nat(full_length), U32.from_nat(remainder)), 284 total) 285 def stream.result.sliced( 286 +compressed: S.State, 287 pair: Packed.Bytes & Packed.Bytes, 288 full_length: Nat, 289 remainder: Nat, 290 total: Nat 291 ) -> Result<&1, &1, StreamError, Stream>: 292 match pair: 293 case (retained, complete): 294 stream.tail.result(compressed, retained, complete, full_length, 295 remainder, total) 296 297 def stream.result.lengths( 298 +compressed: S.State, 299 joined: Packed.Bytes, 300 lengths: Nat & Nat, 301 remainder: Nat, 302 total: Nat 303 ) -> Result<&1, &1, StreamError, Stream>: 304 match lengths: 305 case (for_slice, for_result): 306 stream.result.sliced(compressed, 307 Packed.slice(joined, 0, U32.from_nat(for_slice)), for_result, 308 remainder, total) 309 def stream.result( 310 +compressed: S.State, 311 joined: Packed.Bytes, 312 tail_length: Nat & Nat, 313 total: Nat 314 ) -> Result<&1, &1, StreamError, Stream>: 315 match tail_length: 316 case (full_length, remainder): 317 stream.result.lengths(compressed, joined, 318 QueuePolicy.nat.clone.pair(full_length), remainder, total) 319 def stream.joined.measured( 320 +compressed: S.State, 321 measured: Packed.Bytes & U32, 322 input_length: U32, 323 total: Nat 324 ) -> Result<&1, &1, StreamError, Stream>: 325 match measured: 326 case (joined, size): 327 +length = U32.to_nat(size) 328 +remainder = Nat.mod(length, 64n) 329 stream.result(compressed, joined, 330 (Nat.sub(length, remainder), remainder), 331 Nat.add(total, U32.to_nat(input_length))) 332 def stream.joined( 333 +compressed: S.State, 334 tail: Packed.Bytes, 335 incoming: Packed.Bytes, 336 input_length: U32, 337 total: Nat 338 ) -> Result<&1, &1, StreamError, Stream>: 339 stream.joined.measured(compressed, 340 Packed.length(Packed.concat([tail, incoming])), input_length, total) 341 342 def stream.update.checked( 343 +compressed: S.State, 344 tail: Packed.Bytes, 345 incoming: Packed.Bytes, 346 input_length: U32, 347 total: Nat, 348 valid: Bool 349 ) -> Result<&1, &1, StreamError, Stream>: 350 match valid: 351 case False{}: Fail{ResourceLimit{}} 352 case True{}: 353 stream.joined(compressed, tail, incoming, input_length, total) 354 355 def stream.update.state.lengths( 356 +compressed: S.State, 357 tail: Packed.Bytes, 358 incoming: Packed.Bytes, 359 lengths: Nat & Nat, 360 totals: Nat & Nat 361 ) -> Result<&1, &1, StreamError, Stream>: 362 match lengths: 363 case (for_update, for_limit): 364 match totals: 365 case (for_update_total, for_limit_total): 366 stream.update.checked(compressed, tail, incoming, 367 U32.from_nat(for_update), for_update_total, 368 Nat.is_le(Nat.add(for_limit_total, for_limit), 4294967295n)) 369 370 def stream.update.state( 371 state: Stream, 372 input: Packed.Bytes & U32 373 ) -> Result<&1, &1, StreamError, Stream>: 374 match state: 375 case Stream{compressed, tail, +total}: 376 match input: 377 case (incoming, input_length): 378 stream.update.state.lengths(compressed, tail, incoming, 379 QueuePolicy.nat.clone.pair(U32.to_nat(input_length)), 380 QueuePolicy.nat.clone.pair(total)) 381 382 def stream.update( 383 state: Stream, 384 incoming: Packed.Bytes 385 ) -> Result<&1, &1, StreamError, Stream>: 386 stream.update.state(state, Packed.length(incoming)) 387 388 def stream.finish.words(state: Stream) -> List<&2, U32>: 389 match state: 390 case Stream{compressed, tail, total}: 391 match tail: 392 case Packed.Bytes{+len, buf}: 393 Core.digest(packed.final.tail(U32.from_nat(total), U32.to_nat(len), 394 Packed.Cursor.new(Packed.Bytes{len, buf}), compressed)) 395 396 def stream.finish(state: Stream) -> Packed.Bytes: 397 packed.digest.words(stream.finish.words(state), 398 (Packed.Cursor.new(Packed.Bytes{32, Packed.alloc(32)}), True{}))