def W_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:342

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as LL
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as A

342def W_len(+d: Nat, +mem: List<&2, A.Block>, +hc: {Nat.is_le(Nat.mul(SC.length(A.Block, mem), 256n), SC.pow2(d)) == True{} : Bool}) -> {SC.length(U32, W(d, mem)) == SC.pow2(d) : Nat}:
343  +n = Nat.mul(SC.length(A.Block, mem), 256n)
344  Equal.trans(Nat, SC.length(U32, W(d, mem)), Nat.add(SC.length(U32, flat(mem)), SC.length(U32, pad(d, SC.length(A.Block, mem)))), SC.pow2(d),
345    LL.length_append(U32, flat(mem), pad(d, SC.length(A.Block, mem))),
346    Equal.trans(Nat, Nat.add(SC.length(U32, flat(mem)), SC.length(U32, pad(d, SC.length(A.Block, mem)))), Nat.add(n, Nat.sub(SC.pow2(d), n)), SC.pow2(d),
347      Equal.trans(Nat, Nat.add(SC.length(U32, flat(mem)), SC.length(U32, pad(d, SC.length(A.Block, mem)))), Nat.add(n, SC.length(U32, pad(d, SC.length(A.Block, mem)))), Nat.add(n, Nat.sub(SC.pow2(d), n)),
348        Equal.cong(Nat, Nat, z => Nat.add(z, SC.length(U32, pad(d, SC.length(A.Block, mem)))), SC.length(U32, flat(mem)), n, flat_len(mem)),
349        Equal.cong(Nat, Nat, z => Nat.add(n, z), SC.length(U32, pad(d, SC.length(A.Block, mem))), Nat.sub(SC.pow2(d), n), LL.length_replicate(U32, Nat.sub(SC.pow2(d), n), 0))),
350      N.sub_add(SC.pow2(d), n, hc)))