def ap.m9

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

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

1802def ap.m9(+x: U32) -> {X.aes.m9(x) == G.Gf8.mul(G.Gf8.aes(), 9, x) : U32}:
1803  %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.c9(_) == G.Gf8.mul(G.Gf8.aes(), 9, x) : U32}
1804  %ap.glo(9, x) : {X.aes.c9(U32.and(255, U32.and(255, x))) == _ : U32}
1805  ap.m9b(x)