def words_eq

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend as IH
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as SA

20def words_eq(+bs: List<&2, U32>) -> {IH.words(bs) == SA.words(bs) : List<&2, U32>}:
21  match bs:
22    case Nil{}:
23      {==}
24    case b0 <> Nil{}:
25      {==}
26    case b0 <> b1 <> Nil{}:
27      {==}
28    case b0 <> b1 <> b2 <> Nil{}:
29      {==}
30    case +b0 <> +b1 <> +b2 <> +b3 <> +rest:
31      Equal.cong(List<&2, U32>, List<&2, U32>, z => IH.word(b0, b1, b2, b3) <> z, IH.words(rest), SA.words(rest), words_eq(rest))