def rows8_words
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:318
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as Memory
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
318def rows8_words(+b: A.Block) -> {SB.rows8(SB.words(b)) == b : A.Block}:
319 match b:
320 case A.B{+r0, +r1, +r2, +r3, +r4, +r5, +r6, +r7}:
321 %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r0), SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))))), (r0, SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))))), row_rw(r0, SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))))) : {SB.rows8_0(_) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
322 %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r1), SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))))), (r1, SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))), row_rw(r1, SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))))) : {SB.rows8_1(r0, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
323 %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r2), SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))), (r2, SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))), row_rw(r2, SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))))) : {SB.rows8_2(r0, r1, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
324 %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r3), SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))), (r3, SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))), row_rw(r3, SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))))) : {SB.rows8_3(r0, r1, r2, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
325 %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r4), SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))), (r4, SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))), row_rw(r4, SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))))) : {SB.rows8_4(r0, r1, r2, r3, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
326 %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r5), SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))), (r5, SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))), row_rw(r5, SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{})))) : {SB.rows8_5(r0, r1, r2, r3, r4, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
327 %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r6), SB.app(SB.row_words(r7), Nil{}))), (r6, SB.app(SB.row_words(r7), Nil{})), row_rw(r6, SB.app(SB.row_words(r7), Nil{}))) : {SB.rows8_6(r0, r1, r2, r3, r4, r5, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
328 %Equal.sym(T.State & List<&2, U32>, SB.row(SB.app(SB.row_words(r7), Nil{})), (r7, Nil{}), row_rw(r7, Nil{})) : {SB.rows8_7(r0, r1, r2, r3, r4, r5, r6, _) == A.B{r0, r1, r2, r3, r4, r5, r6, r7} : A.Block}
329 {==}