Laws.Extract.correct: law of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/kdf/laws.bend as Laws
Lines 16-20 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/kdf/laws.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/kdf/laws.bend&start_line=16&end_line=20

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

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/mac/hmac.bend&name=sign_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/hkdf.bend&name=extract
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/kdf.bend&name=extract