def okm_length

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/kdf/okm.bend:272

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hkdf.bend as Spec

272def okm_length(+prk: List<&2, U32>, +info: List<&2, U32>, +len: Nat) -> {List.length(&2, U32, Spec.okm(prk, info, len)) == len : Nat}:
273  +tb = Spec.t_blocks(Spec.block_count(len), prk, info, Nil{}, 0n)
274  length_take(tb, len, %Equal.sym(Nat, List.length(&2, U32, tb), Nat.mul(Spec.block_count(len), 32n), blocks_len(Spec.block_count(len), prk, info, Nil{}, 0n)) : {Nat.is_le(len, _) == True{} : Bool}; ceil_ok(len))