def ap.row

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

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G
import bend-osdev-gf@0.1.1.0/LAWS.bend as GL

1861def ap.row(+k: U32, +x1: U32, +x2: U32, +x3: U32, +x4: U32) -> {G.Gf8.mul(G.Gf8.aes(), k, U32.xor(U32.xor(U32.xor(x1, x2), x3), x4)) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, x1), G.Gf8.mul(G.Gf8.aes(), k, x2)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, x3), G.Gf8.mul(G.Gf8.aes(), k, x4))) : U32}:
1862  %Equal.sym(U32, G.Gf8.mul(G.Gf8.aes(), k, U32.xor(U32.xor(U32.xor(x1, x2), x3), x4)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, U32.xor(U32.xor(x1, x2), x3)), G.Gf8.mul(G.Gf8.aes(), k, x4)), ap.mx(k, U32.xor(U32.xor(x1, x2), x3), x4)) : {_ == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, x1), G.Gf8.mul(G.Gf8.aes(), k, x2)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, x3), G.Gf8.mul(G.Gf8.aes(), k, x4))) : U32}
1863  %Equal.sym(U32, G.Gf8.mul(G.Gf8.aes(), k, U32.xor(U32.xor(x1, x2), x3)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, U32.xor(x1, x2)), G.Gf8.mul(G.Gf8.aes(), k, x3)), ap.mx(k, U32.xor(x1, x2), x3)) : {G.Gf8.add(_, G.Gf8.mul(G.Gf8.aes(), k, x4)) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, x1), G.Gf8.mul(G.Gf8.aes(), k, x2)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, x3), G.Gf8.mul(G.Gf8.aes(), k, x4))) : U32}
1864  %Equal.sym(U32, G.Gf8.mul(G.Gf8.aes(), k, U32.xor(x1, x2)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, x1), G.Gf8.mul(G.Gf8.aes(), k, x2)), ap.mx(k, x1, x2)) : {G.Gf8.add(G.Gf8.add(_, G.Gf8.mul(G.Gf8.aes(), k, x3)), G.Gf8.mul(G.Gf8.aes(), k, x4)) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, x1), G.Gf8.mul(G.Gf8.aes(), k, x2)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, x3), G.Gf8.mul(G.Gf8.aes(), k, x4))) : U32}
1865  GL.add_assoc(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), k, x1), G.Gf8.mul(G.Gf8.aes(), k, x2)), G.Gf8.mul(G.Gf8.aes(), k, x3), G.Gf8.mul(G.Gf8.aes(), k, x4))