def ap.ismask

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

import Base
import bend-osdev-aes@0.1.0.0/aes.bend as X
import bend-collections@1.0.0.0/src/crypto/aes/types.bend as TT

2100def ap.ismask(+x: TT.State, +v: TT.State, +e: {x == X.aes.mask(v) : TT.State}) -> {x == X.aes.mask(x) : TT.State}:
2101  %Equal.sym(TT.State, x, X.aes.mask(v), e) : {_ == X.aes.mask(_) : TT.State}
2102  Equal.sym(TT.State, X.aes.mask(X.aes.mask(v)), X.aes.mask(v), ap.mm(v))