LAWS.hmac_sha256_rfc4231_2: law of bend-osdev-crypto@0.1.0.0
Import: import bend-osdev-crypto@0.1.0.0/LAWS.bend as LAWS
Lines 474-476 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=474&end_line=476

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

# RFC 4231 test case 2: HMAC-SHA-256 with the key "Jefe"
law hmac_sha256_rfc4231_2:
  {Hm.CrHmac.mac(~SH.CrSha2.sha256, Hm.CrHmac.key(~64n, ~SH.CrSha2.sha256, B.Octets.of_string("Jefe")), B.Octets.of_string("what do ya want for nothing?")) == B.Octets.of_list([91, 220, 193, 70, 191, 96, 117, 78, 106, 4, 36, 38, 8, 149, 117, 199, 90, 0, 63, 8, 157, 39, 57, 131, 157, 236, 88, 185, 100, 236, 56, 67]) : B.Octets}

Uses (7):
  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/inst_sha2.bend&name=CrSha2.sha256