law Extract.correct

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

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

16# extract is RFC 5869 section 2.2 (HMAC-SHA256(salt, IKM)).
17law Extract.correct:
18  for +salt: List<&2, U32>
19  for +ikm: List<&2, U32>
20  {KDF.extract(salt, ikm) == Spec.extract(salt, ikm) : List<&2, U32>}