def ap.imixg
bend-osdev-aes@0.1.0.0 · PROOF.bend:1830
import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
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
1830def ap.imixg(+p: U32, +q: U32, +r: U32, +s: U32) -> {X.aes.imix0(p, q, r, s) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}:
1831 %Equal.sym(U32, X.aes.m14(p), G.Gf8.mul(G.Gf8.aes(), 14, p), ap.m14(p)) : {U32.xor(U32.xor(_, X.aes.m11(q)), U32.xor(X.aes.m13(r), X.aes.m9(s))) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}
1832 %Equal.sym(U32, X.aes.m11(q), G.Gf8.mul(G.Gf8.aes(), 11, q), ap.m11(q)) : {U32.xor(U32.xor(G.Gf8.mul(G.Gf8.aes(), 14, p), _), U32.xor(X.aes.m13(r), X.aes.m9(s))) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}
1833 %Equal.sym(U32, X.aes.m13(r), G.Gf8.mul(G.Gf8.aes(), 13, r), ap.m13(r)) : {U32.xor(U32.xor(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), U32.xor(_, X.aes.m9(s))) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}
1834 %Equal.sym(U32, X.aes.m9(s), G.Gf8.mul(G.Gf8.aes(), 9, s), ap.m9(s)) : {U32.xor(U32.xor(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), U32.xor(G.Gf8.mul(G.Gf8.aes(), 13, r), _)) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}
1835 %Equal.sym(U32, U32.xor(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), ap.xg(14, 11, p, q)) : {U32.xor(_, U32.xor(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}
1836 %Equal.sym(U32, U32.xor(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s)), ap.xg(13, 9, r, s)) : {U32.xor(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), _) == G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, p), G.Gf8.mul(G.Gf8.aes(), 11, q)), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, r), G.Gf8.mul(G.Gf8.aes(), 9, s))) : U32}
1837 ap.xg0(G.Gf8Bits.xor(G.Gf8Bits.of(G.Gf8.mul(G.Gf8.aes(), 14, p)), G.Gf8Bits.of(G.Gf8.mul(G.Gf8.aes(), 11, q))), G.Gf8Bits.xor(G.Gf8Bits.of(G.Gf8.mul(G.Gf8.aes(), 13, r)), G.Gf8Bits.of(G.Gf8.mul(G.Gf8.aes(), 9, s))))