LAWS.aes_round_trip: law of bend-osdev-aes@0.1.0.0
Import: import bend-osdev-aes@0.1.0.0/LAWS.bend as LAWS
Lines 8-14 of bend-osdev-aes@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-aes@0.1.0.0/LAWS.bend&start_line=8&end_line=14

import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
import bend-osdev-aes@0.1.0.0/aes.bend as X

# AES (aes.bend): decryption undoes encryption, for every key (every value
# of CmAesKey, whatever its number of rounds and round keys: AES-128, AES-192
# and AES-256 among them) and every block
law aes_round_trip:
  for k: X.CmAesKey
  for +b: M.CmBlock
  {X.CmAes.decrypt(k, X.CmAes.encrypt(k, b)) == b : M.CmBlock}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/aes.bend&name=Schedule
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.top
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=CmAes.decrypt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=CmAes.encrypt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=CmAesKey
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=CmBlock