LAWS.aesround_rfc10032: law of bend-osdev-aead@0.1.0.0
Import: import bend-osdev-aead@0.1.0.0/LAWS.bend as LAWS
Lines 54-57 of bend-osdev-aead@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-aead@0.1.0.0/LAWS.bend&start_line=54&end_line=57

import Base
import bend-osdev-aead@0.1.0.0/aesround.bend as R

# RFC 10032, Appendix A.1: AESRound(000102..0f, 101112..1f) =
# 7a7b4e5638782546a8c0477a3b813f43
law aesround_rfc10032:
  {R.AdAes.round(R.AdAes.sbox(), R.AdBlk{66051, 67438087, 134810123, 202182159}, R.AdBlk{269554195, 336926231, 404298267, 471670303}) == R.AdBlk{2054901334, 947397958, 2831173498, 998326083} : R.AdBlk}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aesround.bend&name=AdAes.round
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aesround.bend&name=AdAes.sbox
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aead@0.1.0.0/aesround.bend&name=AdBlk