def pack_eq

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

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

64def pack_eq(+bs: List<&2, U32>) -> {IH.pack(bs) == SA.pack(bs) : Array<U32>}:
65  Equal.trans(Array<U32>, IH.fill(IH.words(bs), 0, Array.new(U32, IH.depth_go(32n, List.length(&2, U32, IH.words(bs)), 0n, Nat.is_le(List.length(&2, U32, IH.words(bs)), 1n)), 0)), IH.fill(SA.words(bs), 0, Array.new(U32, IH.depth_go(32n, List.length(&2, U32, SA.words(bs)), 0n, Nat.is_le(List.length(&2, U32, SA.words(bs)), 1n)), 0)), SA.pack(bs),
66    Equal.cong(List<&2, U32>, Array<U32>, +z => IH.fill(z, 0, Array.new(U32, IH.depth_go(32n, List.length(&2, U32, z), 0n, Nat.is_le(List.length(&2, U32, z), 1n)), 0)), IH.words(bs), SA.words(bs), words_eq(bs)),
67    pack_fin(SA.words(bs)))