def ap.ex2.r
bend-osdev-aes@0.1.0.0 · PROOF.bend:1095
import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G
import bend-collections@1.0.0.0/src/crypto/aes/sbox.bend as SB
1095def ap.ex2.r(+x: U32) -> List<&2, U32>:
1096 [U32.and(255, SB.xtime(x)), U32.and(255, SB.mul3(x)), G.Gf8.mul(G.Gf8.aes(), 9, x), G.Gf8.mul(G.Gf8.aes(), 11, x), G.Gf8.mul(G.Gf8.aes(), 13, x), G.Gf8.mul(G.Gf8.aes(), 14, x), x, 0, 0, 0, 0, x, 0, 0, 0, 0, x, 0, 0, 0, 0, x, x, x, x, x]