law Expand.correct

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

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

22# expand is RFC 5869 section 2.3, and fails exactly where it is undefined.
23law Expand.correct:
24  for +prk: List<&2, U32>
25  for +info: List<&2, U32>
26  for +len: Nat
27  {KDF.expand(prk, info, len) == as_result(Spec.expand(prk, info, len)) : Result<&2, &2, KDF.KdfError, List<&2, U32>>}