def rows_eq7

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

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/types.bend as A
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend as SB
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

195def rows_eq7(+r0: T.State, +r1: T.State, +r2: T.State, +r3: T.State, +r4: T.State, +r5: T.State, +r6: T.State, p: T.State & List<&2, U32>) -> {SB.rows8_7(r0, r1, r2, r3, r4, r5, r6, p) == SA.rows_of7(r0, r1, r2, r3, r4, r5, r6, p) : A.Block}:
196  match p:
197    case Tuple{+x, ws}:
198      {==}