def block_bytes

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha/packed/core_model.bend:165

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/packed/core.bend as Runtime
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as S

165# Generic block decoder over a padded byte list and any constant table. The
166# fast path below is proved equal to it with the FIPS table.
167def block_bytes(bytes: List<&2, U32>, +extra: Nat, +ks: List<&2, U32>, s: S.State) -> S.State:
168  match bytes:
169    case b0 <> b1 <> b2 <> b3 <> b4 <> b5 <> b6 <> b7 <> b8 <> b9 <> b10 <> b11 <> b12 <> b13 <> b14 <> b15 <> b16 <> b17 <> b18 <> b19 <> b20 <> b21 <> b22 <> b23 <> b24 <> b25 <> b26 <> b27 <> b28 <> b29 <> b30 <> b31 <> b32 <> b33 <> b34 <> b35 <> b36 <> b37 <> b38 <> b39 <> b40 <> b41 <> b42 <> b43 <> b44 <> b45 <> b46 <> b47 <> b48 <> b49 <> b50 <> b51 <> b52 <> b53 <> b54 <> b55 <> b56 <> b57 <> b58 <> b59 <> b60 <> b61 <> b62 <> b63 <> rest:
170      block_bytes(rest, extra, ks, window_compress16(
171        Runtime.pack(b0, b1, b2, b3), Runtime.pack(b4, b5, b6, b7), Runtime.pack(b8, b9, b10, b11), Runtime.pack(b12, b13, b14, b15),
172        Runtime.pack(b16, b17, b18, b19), Runtime.pack(b20, b21, b22, b23), Runtime.pack(b24, b25, b26, b27), Runtime.pack(b28, b29, b30, b31),
173        Runtime.pack(b32, b33, b34, b35), Runtime.pack(b36, b37, b38, b39), Runtime.pack(b40, b41, b42, b43), Runtime.pack(b44, b45, b46, b47),
174        Runtime.pack(b48, b49, b50, b51), Runtime.pack(b52, b53, b54, b55), Runtime.pack(b56, b57, b58, b59), Runtime.pack(b60, b61, b62, b63),
175        extra, ks, s))
176    case _:
177      s