def ap.m13

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

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

1812def ap.m13(+x: U32) -> {X.aes.m13(x) == G.Gf8.mul(G.Gf8.aes(), 13, x) : U32}:
1813  %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.c13(_) == G.Gf8.mul(G.Gf8.aes(), 13, x) : U32}
1814  %ap.glo(13, x) : {X.aes.c13(U32.and(255, U32.and(255, x))) == _ : U32}
1815  ap.m13b(x)