def new_mem

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

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/array.bend as AR
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
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as SG

591# The zeroed array is the memory of mm zero blocks.
592def new_mem(+d: Nat, +mm: Nat, +hc: {Nat.is_le(Nat.mul(mm, 256n), SC.pow2(d)) == True{} : Bool}) -> {Array.new(U32, d, 0) == AR.thaw(U32, mt(d, SC.replicate(A.Block, mm, SG.zero()))) : Array<U32>}:
593  +z = SC.replicate(A.Block, mm, SG.zero())
594  +n = Nat.mul(mm, 256n)
595  +t = AR.trep(U32, d, 0)
596  +ew = Equal.trans(List<&2, U32>, W(d, z), SC.append(U32, SC.replicate(U32, n, 0), SC.replicate(U32, Nat.sub(SC.pow2(d), n), 0)), SC.replicate(U32, SC.pow2(d), 0),
597    Equal.trans(List<&2, U32>, W(d, z), SC.append(U32, SC.replicate(U32, n, 0), pad(d, SC.length(A.Block, z))), SC.append(U32, SC.replicate(U32, n, 0), SC.replicate(U32, Nat.sub(SC.pow2(d), n), 0)),
598      Equal.cong(List<&2, U32>, List<&2, U32>, x => SC.append(U32, x, pad(d, SC.length(A.Block, z))), flat(z), SC.replicate(U32, n, 0), flat_zero(mm)),
599      Equal.cong(Nat, List<&2, U32>, x => SC.append(U32, SC.replicate(U32, n, 0), pad(d, x)), SC.length(A.Block, z), mm, LL.length_replicate(A.Block, mm, SG.zero()))),
600    Equal.trans(List<&2, U32>, SC.append(U32, SC.replicate(U32, n, 0), SC.replicate(U32, Nat.sub(SC.pow2(d), n), 0)), SC.replicate(U32, Nat.add(n, Nat.sub(SC.pow2(d), n)), 0), SC.replicate(U32, SC.pow2(d), 0),
601      LL.replicate_add(U32, n, Nat.sub(SC.pow2(d), n), 0),
602      Equal.cong(Nat, List<&2, U32>, x => SC.replicate(U32, x, 0), Nat.add(n, Nat.sub(SC.pow2(d), n)), SC.pow2(d), N.sub_add(SC.pow2(d), n, hc))))
603  +et = Equal.trans(AR.Tree<U32>, t, tree(d, AR.slots(U32, t)), tree(d, W(d, z)),
604    tree_ext(d, t, AR.trep_perfect(U32, d, 0)),
605    Equal.cong(List<&2, U32>, AR.Tree<U32>, x => tree(d, x), AR.slots(U32, t), W(d, z), Equal.trans(List<&2, U32>, AR.slots(U32, t), SC.replicate(U32, SC.pow2(d), 0), W(d, z), AR.trep_slots(U32, d, 0), Equal.sym(List<&2, U32>, W(d, z), SC.replicate(U32, SC.pow2(d), 0), ew))))
606  Equal.trans(Array<U32>, Array.new(U32, d, 0), AR.thaw(U32, t), AR.thaw(U32, mt(d, z)), AR.new(U32, d, 0), Equal.cong(AR.Tree<U32>, Array<U32>, x => AR.thaw(U32, x), t, tree(d, W(d, z)), et))