LAWS.kbkdf_hmac_sha256_vector: law of bend-osdev-crypto@0.1.0.0
Import: import bend-osdev-crypto@0.1.0.0/LAWS.bend as LAWS
Lines 621-628 of bend-osdev-crypto@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-crypto@0.1.0.0/LAWS.bend&start_line=621&end_line=628

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-crypto@0.1.0.0/hmac.bend as Hm
import bend-osdev-crypto@0.1.0.0/inst_sha2.bend as SH
import bend-osdev-crypto@0.1.0.0/kbkdf.bend as Kb

# KBKDF in counter mode over HMAC-SHA-256 (32-bit counter and [L]_2), the
# key "secret key bytes", Label "label", Context "context", 32 bytes:
# Python's cryptography's KBKDFHMAC gives this value. Stated on the stream
# (what CrKbkdf.counter_kdf returns once its length checks pass): those
# checks compare with 2^32, which --verdict's kernel cannot compute in time;
# check.bend runs the checked derivation
law kbkdf_hmac_sha256_vector:
  {Kb.CrKbkdf.counter_stream(~Hm.CrHmacKey, ~Hm.CrHmac.mac(~SH.CrSha2.sha256), ~4n, Hm.CrHmac.key(~64n, ~SH.CrSha2.sha256, B.Octets.of_string("secret key bytes")), Kb.CrKbkdf.fixed(~4n, B.Octets.of_string("label"), B.Octets.of_string("context"), 32n), 32n) == B.Octets.of_list([36, 187, 186, 187, 150, 131, 248, 143, 109, 68, 1, 79, 191, 147, 235, 99, 232, 125, 99, 110, 60, 243, 238, 232, 217, 114, 189, 30, 217, 156, 9, 202]) : B.Octets}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_list
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.of_string
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/hmac.bend&name=CrHmac.key
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/hmac.bend&name=CrHmac.mac
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/hmac.bend&name=CrHmacKey
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/inst_sha2.bend&name=CrSha2.sha256
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/kbkdf.bend&name=CrKbkdf.counter_stream
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/kbkdf.bend&name=CrKbkdf.fixed