Hash.block_bytes_eq: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend as Hash
Lines 265-277 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend&start_line=265&end_line=277

import Base
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/argon2.bend as SA

# The bytes of a block, row by row.
def block_bytes_eq(+b: A.Block) -> {I.block_bytes(b) == SA.block_bytes(b) : List<&2, U32>}:
  match b:
    case A.B{+r0, +r1, +r2, +r3, +r4, +r5, +r6, +r7}:
      %Equal.sym(List<&2, U32>, I.state_bytes(r0), SA.state_bytes(r0), state_bytes_eq(r0)) : {List.concat(&2, U32, [_, I.state_bytes(r1), I.state_bytes(r2), I.state_bytes(r3), I.state_bytes(r4), I.state_bytes(r5), I.state_bytes(r6), I.state_bytes(r7)]) == SA.block_bytes(A.B{r0, r1, r2, r3, r4, r5, r6, r7}) : List<&2, U32>}
      %Equal.sym(List<&2, U32>, I.state_bytes(r1), SA.state_bytes(r1), state_bytes_eq(r1)) : {List.concat(&2, U32, [SA.state_bytes(r0), _, I.state_bytes(r2), I.state_bytes(r3), I.state_bytes(r4), I.state_bytes(r5), I.state_bytes(r6), I.state_bytes(r7)]) == SA.block_bytes(A.B{r0, r1, r2, r3, r4, r5, r6, r7}) : List<&2, U32>}
      %Equal.sym(List<&2, U32>, I.state_bytes(r2), SA.state_bytes(r2), state_bytes_eq(r2)) : {List.concat(&2, U32, [SA.state_bytes(r0), SA.state_bytes(r1), _, I.state_bytes(r3), I.state_bytes(r4), I.state_bytes(r5), I.state_bytes(r6), I.state_bytes(r7)]) == SA.block_bytes(A.B{r0, r1, r2, r3, r4, r5, r6, r7}) : List<&2, U32>}
      %Equal.sym(List<&2, U32>, I.state_bytes(r3), SA.state_bytes(r3), state_bytes_eq(r3)) : {List.concat(&2, U32, [SA.state_bytes(r0), SA.state_bytes(r1), SA.state_bytes(r2), _, I.state_bytes(r4), I.state_bytes(r5), I.state_bytes(r6), I.state_bytes(r7)]) == SA.block_bytes(A.B{r0, r1, r2, r3, r4, r5, r6, r7}) : List<&2, U32>}
      %Equal.sym(List<&2, U32>, I.state_bytes(r4), SA.state_bytes(r4), state_bytes_eq(r4)) : {List.concat(&2, U32, [SA.state_bytes(r0), SA.state_bytes(r1), SA.state_bytes(r2), SA.state_bytes(r3), _, I.state_bytes(r5), I.state_bytes(r6), I.state_bytes(r7)]) == SA.block_bytes(A.B{r0, r1, r2, r3, r4, r5, r6, r7}) : List<&2, U32>}
      %Equal.sym(List<&2, U32>, I.state_bytes(r5), SA.state_bytes(r5), state_bytes_eq(r5)) : {List.concat(&2, U32, [SA.state_bytes(r0), SA.state_bytes(r1), SA.state_bytes(r2), SA.state_bytes(r3), SA.state_bytes(r4), _, I.state_bytes(r6), I.state_bytes(r7)]) == SA.block_bytes(A.B{r0, r1, r2, r3, r4, r5, r6, r7}) : List<&2, U32>}
      %Equal.sym(List<&2, U32>, I.state_bytes(r6), SA.state_bytes(r6), state_bytes_eq(r6)) : {List.concat(&2, U32, [SA.state_bytes(r0), SA.state_bytes(r1), SA.state_bytes(r2), SA.state_bytes(r3), SA.state_bytes(r4), SA.state_bytes(r5), _, I.state_bytes(r7)]) == SA.block_bytes(A.B{r0, r1, r2, r3, r4, r5, r6, r7}) : List<&2, U32>}
      %Equal.sym(List<&2, U32>, I.state_bytes(r7), SA.state_bytes(r7), state_bytes_eq(r7)) : {List.concat(&2, U32, [SA.state_bytes(r0), SA.state_bytes(r1), SA.state_bytes(r2), SA.state_bytes(r3), SA.state_bytes(r4), SA.state_bytes(r5), SA.state_bytes(r6), _]) == SA.block_bytes(A.B{r0, r1, r2, r3, r4, r5, r6, r7}) : List<&2, U32>}
      {==}

Uses (10):
  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=List.concat
  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/hash.bend&name=state_bytes_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=block_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend&name=state_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=block_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend&name=state_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend&name=Block