~/bend-docscommunity

src/crypto/hash.bend source

src/crypto/hash.bend on the hub · documented module

# Generated by tools/generators/hash_gen.py; do not edit by hand.import Baseimport ./sha/state.bend as S256import ./sha/core.bend as C256import ./sha/sha256.bend as SHA256import ./sha512/types.bend as T512import ./sha512/core.bend as C512import ./keccak/types.bend as TKimport ./keccak/permutation.bend as Pimport ./sha3/core.bend as C3# Hash functions: one-shot and incremental.##   sha256(bytes), sha512(bytes), sha3_256(bytes)       the digest (32, 64, 32 bytes)#   new_sha256(), new_sha512(), new_sha3_256()          an empty Hasher#   update(h, bytes)                                    h with bytes appended#   update_all(h, chunks)                               update with each chunk in turn#   digest(h)                                           the digest of everything appended## Bytes are U32 values, each < 256 (List<&2, U32>). A Hasher keeps the chaining# state, the bytes of the unfinished block (fewer than one block) and the total# length; update compresses every block it completes, and digest pads the# buffered tail with the total length. Proved (proofs/crypto/hash/laws.bend):# each one-shot function equals its executable specification, and for every# list of chunks, digest(update_all(new_X(), chunks)) == X(concat(chunks)).# Hashers are values: update returns a new one, the old one is unchanged.# A chaining state and the buffered bytes of the unfinished block.type Sha256State is Data:  St256{s: S256.State, buf: List<&2, U32>}type Sha512State is Data:  St512{s: T512.State, buf: List<&2, U32>}type Sha3State is Data:  St3{s: TK.State, buf: List<&2, U32>}type Hasher is Data:  Sha256H{st: Sha256State, len: Nat}  Sha512H{st: Sha512State, len: Nat}  Sha3H{st: Sha3State, len: Nat}# ---------------------------------------------------------------- one-shot# SHA-256 (FIPS 180-4), 32 bytes.def sha256(bytes: List<&2, U32>) -> List<&2, U32>:  SHA256.sha256_bytes(bytes)# SHA-512 (FIPS 180-4), 64 bytes.def sha512(bytes: List<&2, U32>) -> List<&2, U32>:  C512.sha512(bytes)# SHA3-256 (FIPS 202), 32 bytes.def sha3_256(bytes: List<&2, U32>) -> List<&2, U32>:  C3.sha3_256(bytes)# ---------------------------------------------------------------- SHA-256 (FIPS 180-4)# One block read 4 bytes at a time into its 16 words, or Short when# fewer than 64 bytes are left.type Read256 is Data:  Blk256{w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32, rest: List<&2, U32>}  Short256{}def read256_16(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32, w15: U32) -> Read256:  Blk256{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, bytes}def read256_15(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32, w14: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_16(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_14(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32, w13: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_15(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_13(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32, w12: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_14(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_12(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32, w11: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_13(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_11(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32, w10: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_12(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_10(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32, w9: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_11(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_9(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32, w8: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_10(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_8(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32, w7: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_9(rest, w0, w1, w2, w3, w4, w5, w6, w7, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_7(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32, w6: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_8(rest, w0, w1, w2, w3, w4, w5, w6, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_6(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32, w5: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_7(rest, w0, w1, w2, w3, w4, w5, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_5(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32, w4: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_6(rest, w0, w1, w2, w3, w4, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_4(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32, w3: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_5(rest, w0, w1, w2, w3, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_3(bytes: List<&2, U32>, w0: U32, w1: U32, w2: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_4(rest, w0, w1, w2, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_2(bytes: List<&2, U32>, w0: U32, w1: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_3(rest, w0, w1, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_1(bytes: List<&2, U32>, w0: U32) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_2(rest, w0, C256.pack(b0, b1, b2, b3))    case _:      Short256{}def read256_0(bytes: List<&2, U32>) -> Read256:  match bytes:    case b0 <> b1 <> b2 <> b3 <> rest:      read256_1(rest, C256.pack(b0, b1, b2, b3))    case _:      Short256{}# Compress every whole block (fuel bounds the count: any fuel >= the number of# blocks reads them all; fewer leaves the rest buffered, still correct). The# chaining state and the unread bytes; orig is the list the read r started at.# q is the algorithm's round parameter (48n), kept a variable for the proofs.def absorb256(fuel: Nat, r: Read256, orig: List<&2, U32>, +q: Nat, s: S256.State) -> Sha256State:  match fuel r:    case 0n _:      St256{s, orig}    case 1n+p Short256{}:      St256{s, orig}    case 1n+p Blk256{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, +rest}:      absorb256(p, read256_0(rest), rest, q, C256.fips_compress16(w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, q, s))def step256(st: Sha256State, xs: List<&2, U32>, +q: Nat) -> Sha256State:  match st:    case St256{s, buf}:      +bytes = List.append(&2, U32, buf, xs)      absorb256(List.length(&2, U32, bytes), read256_0(bytes), bytes, q, s)def finish256(st: Sha256State, +len: Nat, +q: Nat) -> List<&2, U32>:  match st:    case St256{s, buf}:      SHA256.digest_bytes(C256.digest(C256.block_bytes(List.append(&2, U32, buf, C256.suffix(len)), q, C256.round_constants(), s)))# ---------------------------------------------------------------- SHA-512 (FIPS 180-4)# One block read 8 bytes at a time into its 16 words, or Short when# fewer than 128 bytes are left.type Read512 is Data:  Blk512{w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane, w13: T512.Lane, w14: T512.Lane, w15: T512.Lane, rest: List<&2, U32>}  Short512{}def read512_16(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane, w13: T512.Lane, w14: T512.Lane, w15: T512.Lane) -> Read512:  Blk512{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, bytes}def read512_15(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane, w13: T512.Lane, w14: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_16(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_14(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane, w13: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_15(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_13(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane, w12: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_14(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_12(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane, w11: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_13(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_11(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane, w10: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_12(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_10(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane, w9: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_11(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_9(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane, w8: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_10(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_8(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane, w7: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_9(rest, w0, w1, w2, w3, w4, w5, w6, w7, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_7(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane, w6: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_8(rest, w0, w1, w2, w3, w4, w5, w6, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_6(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane, w5: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_7(rest, w0, w1, w2, w3, w4, w5, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_5(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane, w4: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_6(rest, w0, w1, w2, w3, w4, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_4(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane, w3: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_5(rest, w0, w1, w2, w3, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_3(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane, w2: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_4(rest, w0, w1, w2, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_2(bytes: List<&2, U32>, w0: T512.Lane, w1: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_3(rest, w0, w1, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_1(bytes: List<&2, U32>, w0: T512.Lane) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_2(rest, w0, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}def read512_0(bytes: List<&2, U32>) -> Read512:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read512_1(rest, T512.W{C512.pack(b0, b1, b2, b3), C512.pack(b4, b5, b6, b7)})    case _:      Short512{}# Compress every whole block (fuel bounds the count: any fuel >= the number of# blocks reads them all; fewer leaves the rest buffered, still correct). The# chaining state and the unread bytes; orig is the list the read r started at.# q is the algorithm's round parameter (64n), kept a variable for the proofs.def absorb512(fuel: Nat, r: Read512, orig: List<&2, U32>, +q: Nat, s: T512.State) -> Sha512State:  match fuel r:    case 0n _:      St512{s, orig}    case 1n+p Short512{}:      St512{s, orig}    case 1n+p Blk512{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, +rest}:      absorb512(p, read512_0(rest), rest, q, C512.compress16(w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, q, C512.round_constants(), s))def step512(st: Sha512State, xs: List<&2, U32>, +q: Nat) -> Sha512State:  match st:    case St512{s, buf}:      +bytes = List.append(&2, U32, buf, xs)      absorb512(List.length(&2, U32, bytes), read512_0(bytes), bytes, q, s)def finish512(st: Sha512State, +len: Nat, +q: Nat) -> List<&2, U32>:  match st:    case St512{s, buf}:      C512.digest_bytes(C512.blocks(C512.lanes(List.append(&2, U32, buf, C512.suffix(len))), q, C512.round_constants(), s))# ---------------------------------------------------------------- SHA3-256 (FIPS 202)# One block read 8 bytes at a time into its 17 words, or Short when# fewer than 136 bytes are left.type Read3 is Data:  Blk3{w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane, w14: TK.Lane, w15: TK.Lane, w16: TK.Lane, rest: List<&2, U32>}  Short3{}def read3_17(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane, w14: TK.Lane, w15: TK.Lane, w16: TK.Lane) -> Read3:  Blk3{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, bytes}def read3_16(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane, w14: TK.Lane, w15: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_17(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_15(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane, w14: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_16(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_14(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane, w13: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_15(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_13(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane, w12: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_14(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_12(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane, w11: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_13(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_11(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane, w10: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_12(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_10(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane, w9: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_11(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_9(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane, w8: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_10(rest, w0, w1, w2, w3, w4, w5, w6, w7, w8, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_8(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane, w7: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_9(rest, w0, w1, w2, w3, w4, w5, w6, w7, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_7(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane, w6: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_8(rest, w0, w1, w2, w3, w4, w5, w6, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_6(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane, w5: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_7(rest, w0, w1, w2, w3, w4, w5, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_5(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane, w4: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_6(rest, w0, w1, w2, w3, w4, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_4(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane, w3: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_5(rest, w0, w1, w2, w3, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_3(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane, w2: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_4(rest, w0, w1, w2, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_2(bytes: List<&2, U32>, w0: TK.Lane, w1: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_3(rest, w0, w1, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_1(bytes: List<&2, U32>, w0: TK.Lane) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_2(rest, w0, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}def read3_0(bytes: List<&2, U32>) -> Read3:  match bytes:    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> rest:      read3_1(rest, TK.W{C3.pack(b0, b1, b2, b3), C3.pack(b4, b5, b6, b7)})    case _:      Short3{}# Compress every whole block (fuel bounds the count: any fuel >= the number of# blocks reads them all; fewer leaves the rest buffered, still correct). The# chaining state and the unread bytes; orig is the list the read r started at.# q is the algorithm's round parameter (24n), kept a variable for the proofs.def absorb3(fuel: Nat, r: Read3, orig: List<&2, U32>, +q: Nat, s: TK.State) -> Sha3State:  match fuel r:    case 0n _:      St3{s, orig}    case 1n+p Short3{}:      St3{s, orig}    case 1n+p Blk3{w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16, +rest}:      absorb3(p, read3_0(rest), rest, q, P.rounds(q, 0n, C3.inject(s, w0, w1, w2, w3, w4, w5, w6, w7, w8, w9, w10, w11, w12, w13, w14, w15, w16)))def step3(st: Sha3State, xs: List<&2, U32>, +q: Nat) -> Sha3State:  match st:    case St3{s, buf}:      +bytes = List.append(&2, U32, buf, xs)      absorb3(List.length(&2, U32, bytes), read3_0(bytes), bytes, q, s)def finish3(st: Sha3State, +len: Nat, +q: Nat) -> List<&2, U32>:  match st:    case St3{s, buf}:      C3.digest_bytes(C3.absorb(C3.lanes(List.append(&2, U32, buf, C3.suffix(len))), q, s))# ---------------------------------------------------------------- the Hasherdef new_sha256() -> Hasher:  Sha256H{St256{C256.initial(), Nil{}}, 0n}def new_sha512() -> Hasher:  Sha512H{St512{C512.initial(), Nil{}}, 0n}def new_sha3_256() -> Hasher:  Sha3H{St3{C3.zero(), Nil{}}, 0n}def update(h: Hasher, +bytes: List<&2, U32>) -> Hasher:  match h:    case Sha256H{st, len}:      Sha256H{step256(st, bytes, 48n), Nat.add(len, List.length(&2, U32, bytes))}    case Sha512H{st, len}:      Sha512H{step512(st, bytes, 64n), Nat.add(len, List.length(&2, U32, bytes))}    case Sha3H{st, len}:      Sha3H{step3(st, bytes, 24n), Nat.add(len, List.length(&2, U32, bytes))}def fold(chunks: List<&2, List<&2, U32>>, h: Hasher) -> Hasher:  match chunks:    case Nil{}:      h    case c <> rest:      fold(rest, update(h, c))def update_all(h: Hasher, chunks: List<&2, List<&2, U32>>) -> Hasher:  fold(chunks, h)def digest(h: Hasher) -> List<&2, U32>:  match h:    case Sha256H{st, len}:      finish256(st, len, 48n)    case Sha512H{st, len}:      finish512(st, len, 64n)    case Sha3H{st, len}:      finish3(st, len, 24n)