def ap.m11

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

import Base
import bend-osdev-aes@0.1.0.0/aes.bend as X
import bend-osdev-gf@0.1.1.0/gf.bend as G

1807def ap.m11(+x: U32) -> {X.aes.m11(x) == G.Gf8.mul(G.Gf8.aes(), 11, x) : U32}:
1808  %Equal.sym(U32, U32.and(255, x), U32.and(255, U32.and(255, x)), Equal.sym(U32, U32.and(255, U32.and(255, x)), U32.and(255, x), ap.bb(x))) : {X.aes.c11(_) == G.Gf8.mul(G.Gf8.aes(), 11, x) : U32}
1809  %ap.glo(11, x) : {X.aes.c11(U32.and(255, U32.and(255, x))) == _ : U32}
1810  ap.m11b(x)