def ap.top

bend-osdev-aes@0.1.0.0 · PROOF.bend:2220

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

2220def 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}:
2221  %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}
2222  %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}
2223  %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}
2224  %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}
2225  ap.out_in(b)