def cap

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/top.bend:115

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/arith.bend as AR2
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/src/crypto/argon2/memory.bend as M
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as SG

115# 256 m' <= 2^(8 + k).
116def cap(+n: Nat, +h: {Nat.is_le(M.levels(n), 23n) == True{} : Bool}) -> {Nat.is_le(Nat.mul(SC.length(A.Block, SC.replicate(A.Block, n, SG.zero())), 256n), SC.pow2(Nat.add(8n, M.levels(n)))) == True{} : Bool}:
117  +k = M.levels(n)
118  %Equal.sym(Nat, SC.length(A.Block, SC.replicate(A.Block, n, SG.zero())), n, LL.length_replicate(A.Block, n, SG.zero())) : {Nat.is_le(Nat.mul(_, 256n), SC.pow2(Nat.add(8n, k))) == True{} : Bool}
119  %d8(SC.pow2(k)) : {Nat.is_le(Nat.mul(n, 256n), _) == True{} : Bool}
120  AR2.mul_le(n, SC.pow2(k), 256n, levels_ok(n, h))