def lanes
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as Coreimport Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as T
128# Big-endian 64-bit words, eight bytes each.
129def lanes(bytes: List<&2, U32>) -> List<&2, T.Lane>:
130 match bytes:
131 case a <> b <> c <> d <> e <> f <> g <> h <> rest:
132 T.W{pack(a, b, c, d), pack(e, f, g, h)} <> lanes(rest)
133 case _:
134 Nil{}
Uses (4)
Used by (12)
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes:sha_okb
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance:sha512_correct
- bend-collections-laws-crypto@1.0.0.0/src/crypto/hash:finish512
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental:absorb512_inv
- bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental:finish512_eta
- …