def pack_fin

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

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

58def pack_fin(+ws: List<&2, U32>) -> {IH.fill(ws, 0, Array.new(U32, IH.depth_go(32n, List.length(&2, U32, ws), 0n, Nat.is_le(List.length(&2, U32, ws), 1n)), 0)) == SA.fill(ws, 0, Array.new(U32, SA.depth_go(32n, List.length(&2, U32, ws), 0n, Nat.is_le(List.length(&2, U32, ws), 1n)), 0)) : Array<U32>}:
59  +n = List.length(&2, U32, ws)
60  Equal.trans(Array<U32>, IH.fill(ws, 0, Array.new(U32, IH.depth_go(32n, n, 0n, Nat.is_le(n, 1n)), 0)), IH.fill(ws, 0, Array.new(U32, SA.depth_go(32n, n, 0n, Nat.is_le(n, 1n)), 0)), SA.fill(ws, 0, Array.new(U32, SA.depth_go(32n, n, 0n, Nat.is_le(n, 1n)), 0)),
61    Equal.cong(Nat, Array<U32>, z => IH.fill(ws, 0, Array.new(U32, z, 0)), IH.depth_go(32n, n, 0n, Nat.is_le(n, 1n)), SA.depth_go(32n, n, 0n, Nat.is_le(n, 1n)), depth_eq(32n, n, 0n, Nat.is_le(n, 1n))),
62    fill_eq(ws, 0, Array.new(U32, SA.depth_go(32n, n, 0n, Nat.is_le(n, 1n)), 0)))