def ap.cipher_out

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

import Base
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

2167def ap.cipher_out(+nr: Nat, ks: List<&2, TT.State>, +s: TT.State) -> {A.cipher(nr, X.aes.mask(s), X.aes.mask_keys(ks)) == X.aes.mask(A.cipher(nr, X.aes.mask(s), X.aes.mask_keys(ks))) : TT.State}:
2168  match ks:
2169    case Con{+k, rest}:
2170      %Equal.sym(TT.State, A.add_round_key(X.aes.mask(s), X.aes.mask(k)), X.aes.mask(A.add_round_key(X.aes.mask(s), X.aes.mask(k))), ap.arkl(s, k)) : {A.rounds(Nat.sub(nr, 1n), _, X.aes.mask_keys(rest)) == X.aes.mask(A.rounds(Nat.sub(nr, 1n), _, X.aes.mask_keys(rest))) : TT.State}
2171      ap.rounds_out(Nat.sub(nr, 1n), rest, A.add_round_key(X.aes.mask(s), X.aes.mask(k)))
2172    case Nil{}:
2173      Equal.sym(TT.State, X.aes.mask(X.aes.mask(s)), X.aes.mask(s), ap.mm(s))