def state_bytes_eq
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/hash.bend:260
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend as Hash
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA
260def state_bytes_eq(+v: T.State) -> {I.state_bytes(v) == SA.state_bytes(v) : List<&2, U32>}:
261 match v:
262 case T.V{T.W{l0, h0}, T.W{l1, h1}, T.W{l2, h2}, T.W{l3, h3}, T.W{l4, h4}, T.W{l5, h5}, T.W{l6, h6}, T.W{l7, h7}, T.W{l8, h8}, T.W{l9, h9}, T.W{l10, h10}, T.W{l11, h11}, T.W{l12, h12}, T.W{l13, h13}, T.W{l14, h14}, T.W{l15, h15}}:
263 {==}