def ap.m14

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

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

1817def ap.m14(+x: U32) -> {X.aes.m14(x) == G.Gf8.mul(G.Gf8.aes(), 14, x) : U32}:
1818  %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.c14(_) == G.Gf8.mul(G.Gf8.aes(), 14, x) : U32}
1819  %ap.glo(14, x) : {X.aes.c14(U32.and(255, U32.and(255, x))) == _ : U32}
1820  ap.m14b(x)