def ap.rounds_inv

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

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

2153def ap.rounds_inv(n: Nat, ks: List<&2, TT.State>, +z: TT.State) -> {X.aes.inv_rounds(n, X.aes.mask_keys(ks), A.rounds(n, X.aes.mask(z), X.aes.mask_keys(ks))) == X.aes.mask(z) : TT.State}:
2154  match n ks:
2155    case 0n Con{+k, rest}:
2156      ap.last_inv(z, k)
2157    case 1n+p Con{+k, rest}:
2158      %Equal.sym(TT.State, A.round(X.aes.mask(z), X.aes.mask(k)), X.aes.mask(A.round(X.aes.mask(z), X.aes.mask(k))), ap.round_out(z, k)) : {X.aes.inv_round(X.aes.inv_rounds(p, X.aes.mask_keys(rest), A.rounds(p, _, X.aes.mask_keys(rest))), X.aes.mask(k)) == X.aes.mask(z) : TT.State}
2159      %Equal.sym(TT.State, X.aes.inv_rounds(p, X.aes.mask_keys(rest), A.rounds(p, X.aes.mask(A.round(X.aes.mask(z), X.aes.mask(k))), X.aes.mask_keys(rest))), X.aes.mask(A.round(X.aes.mask(z), X.aes.mask(k))), ap.rounds_inv(p, rest, A.round(X.aes.mask(z), X.aes.mask(k)))) : {X.aes.inv_round(_, X.aes.mask(k)) == X.aes.mask(z) : TT.State}
2160      %ap.round_out(z, k) : {X.aes.inv_round(_, X.aes.mask(k)) == X.aes.mask(z) : TT.State}
2161      ap.round_inv(z, k)
2162    case 0n Nil{}:
2163      ap.mm(z)
2164    case 1n+p Nil{}:
2165      ap.mm(z)