def ap.rowb0
bend-osdev-aes@0.1.0.0 · PROOF.bend:1926
import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-collections@1.0.0.0/src/crypto/aes/sbox.bend as SB
1926def ap.rowb0(+a: U32, +b: U32, +c: U32, +d: U32) -> {U32.xor(U32.xor(U32.xor(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d)) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c))), U32.and(255, d))) : U32}:
1927 %Equal.sym(U32, SB.xtime(U32.and(255, a)), U32.and(255, SB.xtime(U32.and(255, a))), ap.xtb(a)) : {U32.xor(U32.xor(U32.xor(_, SB.mul3(U32.and(255, b))), U32.and(255, c)), U32.and(255, d)) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c))), U32.and(255, d))) : U32}
1928 %Equal.sym(U32, SB.mul3(U32.and(255, b)), U32.and(255, SB.mul3(U32.and(255, b))), ap.m3b(b)) : {U32.xor(U32.xor(U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), _), U32.and(255, c)), U32.and(255, d)) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c))), U32.and(255, d))) : U32}
1929 %Equal.sym(U32, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b)))), U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), ap.xorb(SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b)))) : {U32.xor(U32.xor(_, U32.and(255, c)), U32.and(255, d)) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c))), U32.and(255, d))) : U32}
1930 %Equal.sym(U32, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c)), U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c))), ap.xorb(U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b)))), c)) : {U32.xor(_, U32.and(255, d)) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c))), U32.and(255, d))) : U32}
1931 %Equal.sym(U32, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c))), U32.and(255, d)), U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c))), U32.and(255, d))), ap.xorb(U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c)), d)) : {_ == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, SB.xtime(U32.and(255, a))), U32.and(255, SB.mul3(U32.and(255, b))))), U32.and(255, c))), U32.and(255, d))) : U32}
1932 {==}