def blocks_len

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hkdf.bend as Spec
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hmac.bend as HMAC
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/mac/hmac.bend as MacP

254# RFC 5869's T(1) | ... | T(n) has 32n bytes.
255def blocks_len(n: Nat, +prk: List<&2, U32>, +info: List<&2, U32>, +prev: List<&2, U32>, +i: Nat) -> {List.length(&2, U32, Spec.t_blocks(n, prk, info, prev, i)) == Nat.mul(n, 32n) : Nat}:
256  match n:
257    case 0n:
258      {==}
259    case 1n+ +m:
260      +s = HMAC.hmac(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)])))
261      +tb = Spec.t_blocks(m, prk, info, s, 1n+i)
262      %Equal.sym(Nat, List.length(&2, U32, List.append(&2, U32, s, tb)), Nat.add(List.length(&2, U32, s), List.length(&2, U32, tb)), length_append(s, tb)) : {_ == Nat.mul(1n+m, 32n) : Nat}
263      %Equal.sym(Nat, List.length(&2, U32, s), 32n, MacP.hmac_len(prk, List.append(&2, U32, prev, List.append(&2, U32, info, [U32.from_nat(1n+i)])))) : {Nat.add(_, List.length(&2, U32, tb)) == Nat.mul(1n+m, 32n) : Nat}
264      %Equal.sym(Nat, List.length(&2, U32, tb), Nat.mul(m, 32n), blocks_len(m, prk, info, s, 1n+i)) : {Nat.add(32n, _) == Nat.mul(1n+m, 32n) : Nat}
265      {==}