def chain_bytes_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/hash.bend:74

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/blake/blake2b/sized.bend as IH
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

74def chain_bytes_eq(+h: T.Chain) -> {IH.chain_bytes(h) == SA.chain_bytes(h) : List<&2, U32>}:
75  match h:
76    case T.H{T.W{l0, u0}, T.W{l1, u1}, T.W{l2, u2}, T.W{l3, u3}, T.W{l4, u4}, T.W{l5, u5}, T.W{l6, u6}, T.W{l7, u7}}:
77      {==}