def row_rw

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:313

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/sub.bend as SB

313def row_rw(+v: T.State, +rest: List<&2, U32>) -> {SB.row(SB.app(SB.row_words(v), rest)) == (v, rest) : T.State & List<&2, U32>}:
314  match v:
315    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}}:
316      {==}