PROOF.ap.top: def of bend-osdev-aes@0.1.0.0
Import: import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
Lines 2220-2225 of bend-osdev-aes@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&start_line=2220&end_line=2225

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
import bend-collections@1.0.0.0/src/crypto/aes/aes.bend as A
import bend-collections@1.0.0.0/src/crypto/aes/types.bend as TT

def ap.top(+nr: Nat, +ks: List<&2, TT.State>, +b: M.CmBlock) -> {X.aes.out(X.aes.inv_cipher(nr, X.aes.mask_keys(ks), X.aes.state16(M.cm.bytes_of(M.cm.block_of(A.bytes_of(A.cipher(nr, X.aes.state_in(b), X.aes.mask_keys(ks)))))))) == b : M.CmBlock}:
  %Equal.sym(TT.State, X.aes.state_in(b), X.aes.mask(X.aes.state_in(b)), ap.in_mask(b)) : {X.aes.out(X.aes.inv_cipher(nr, X.aes.mask_keys(ks), X.aes.state16(M.cm.bytes_of(M.cm.block_of(A.bytes_of(A.cipher(nr, _, X.aes.mask_keys(ks)))))))) == b : M.CmBlock}
  %Equal.sym(TT.State, X.aes.state16(M.cm.bytes_of(M.cm.block_of(A.bytes_of(A.cipher(nr, X.aes.mask(X.aes.state_in(b)), X.aes.mask_keys(ks)))))), X.aes.mask(A.cipher(nr, X.aes.mask(X.aes.state_in(b)), X.aes.mask_keys(ks))), ap.state_back(A.cipher(nr, X.aes.mask(X.aes.state_in(b)), X.aes.mask_keys(ks)))) : {X.aes.out(X.aes.inv_cipher(nr, X.aes.mask_keys(ks), _)) == b : M.CmBlock}
  %ap.cipher_out(nr, ks, X.aes.state_in(b)) : {X.aes.out(X.aes.inv_cipher(nr, X.aes.mask_keys(ks), _)) == b : M.CmBlock}
  %Equal.sym(TT.State, X.aes.inv_cipher(nr, X.aes.mask_keys(ks), A.cipher(nr, X.aes.mask(X.aes.state_in(b)), X.aes.mask_keys(ks))), X.aes.mask(X.aes.state_in(b)), ap.cipher_inv(nr, ks, X.aes.state_in(b))) : {X.aes.out(_) == b : M.CmBlock}
  ap.out_in(b)

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/aes.bend&name=bytes_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/aes.bend&name=cipher
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/types.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.cipher_inv
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.cipher_out
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.in_mask
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.out_in
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.state_back
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.inv_cipher
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.mask
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.mask_keys
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.out
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.state16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.state_in
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=CmBlock
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.block_of
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.bytes_of