Memory.rows8_words: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as Memory
Lines 318-329 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&start_line=318&end_line=329

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

def rows8_words(+b: A.Block) -> {SB.rows8(SB.words(b)) == b : A.Block}:
  match b:
    case A.B{+r0, +r1, +r2, +r3, +r4, +r5, +r6, +r7}:
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      %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}
      {==}

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend&name=row_rw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=app
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=row
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=row_words
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=rows8
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=rows8_0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=rows8_1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=rows8_2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=rows8_3
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=rows8_4
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=rows8_5
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=rows8_6
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=rows8_7
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend&name=words
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend&name=State