def ap.rounds_out

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

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

2141def ap.rounds_out(n: Nat, ks: List<&2, TT.State>, +z: TT.State) -> {A.rounds(n, X.aes.mask(z), X.aes.mask_keys(ks)) == X.aes.mask(A.rounds(n, X.aes.mask(z), X.aes.mask_keys(ks))) : TT.State}:
2142  match n ks:
2143    case 0n Con{+k, rest}:
2144      ap.last_out(z, k)
2145    case 1n+p Con{+k, rest}:
2146      %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)) : {A.rounds(p, _, X.aes.mask_keys(rest)) == X.aes.mask(A.rounds(p, _, X.aes.mask_keys(rest))) : TT.State}
2147      ap.rounds_out(p, rest, A.round(X.aes.mask(z), X.aes.mask(k)))
2148    case 0n Nil{}:
2149      Equal.sym(TT.State, X.aes.mask(X.aes.mask(z)), X.aes.mask(z), ap.mm(z))
2150    case 1n+p Nil{}:
2151      Equal.sym(TT.State, X.aes.mask(X.aes.mask(z)), X.aes.mask(z), ap.mm(z))