def block_bytes_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/hash.bend:265

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

265# The bytes of a block, row by row.
266def block_bytes_eq(+b: A.Block) -> {I.block_bytes(b) == SA.block_bytes(b) : List<&2, U32>}:
267  match b:
268    case A.B{+r0, +r1, +r2, +r3, +r4, +r5, +r6, +r7}:
269      %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>}
270      %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>}
271      %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>}
272      %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>}
273      %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>}
274      %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>}
275      %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>}
276      %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>}
277      {==}