def lane_eq
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/index.bend:84
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index.bend as Index
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/argon2.bend as I
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as SG
84def lane_eq(+b: A.Block, +n: Nat) -> {I.lane(b, n) == SG.lane(b, n) : T.Lane}:
85 Equal.trans(T.Lane, I.at(I.row_at(b, Nat.div(n, 16n)), Nat.mod(n, 16n)), I.at(SG.row(b, Nat.div(n, 16n)), Nat.mod(n, 16n)), SG.lane(b, n),
86 Equal.cong(T.State, T.Lane, z => I.at(z, Nat.mod(n, 16n)), I.row_at(b, Nat.div(n, 16n)), SG.row(b, Nat.div(n, 16n)), row_at_eq(b, Nat.div(n, 16n))),
87 at_eq(SG.row(b, Nat.div(n, 16n)), Nat.mod(n, 16n)))