def ap.rowb2
bend-osdev-aes@0.1.0.0 · PROOF.bend:1942
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
1942def ap.rowb2(+a: U32, +b: U32, +c: U32, +d: U32) -> {U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c))), SB.mul3(U32.and(255, d))) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c))))), U32.and(255, SB.mul3(U32.and(255, d))))) : U32}:
1943 %Equal.sym(U32, SB.xtime(U32.and(255, c)), U32.and(255, SB.xtime(U32.and(255, c))), ap.xtb(c)) : {U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), _), SB.mul3(U32.and(255, d))) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c))))), U32.and(255, SB.mul3(U32.and(255, d))))) : U32}
1944 %Equal.sym(U32, SB.mul3(U32.and(255, d)), U32.and(255, SB.mul3(U32.and(255, d))), ap.m3b(d)) : {U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, b)), U32.and(255, SB.xtime(U32.and(255, c)))), _) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c))))), U32.and(255, SB.mul3(U32.and(255, d))))) : U32}
1945 %Equal.sym(U32, U32.xor(U32.and(255, a), U32.and(255, b)), U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), ap.xorb(a, b)) : {U32.xor(U32.xor(_, U32.and(255, SB.xtime(U32.and(255, c)))), U32.and(255, SB.mul3(U32.and(255, d)))) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c))))), U32.and(255, SB.mul3(U32.and(255, d))))) : U32}
1946 %Equal.sym(U32, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c)))), U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c))))), ap.xorb(U32.xor(U32.and(255, a), U32.and(255, b)), SB.xtime(U32.and(255, c)))) : {U32.xor(_, U32.and(255, SB.mul3(U32.and(255, d)))) == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c))))), U32.and(255, SB.mul3(U32.and(255, d))))) : U32}
1947 %Equal.sym(U32, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c))))), U32.and(255, SB.mul3(U32.and(255, d)))), U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c))))), U32.and(255, SB.mul3(U32.and(255, d))))), ap.xorb(U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c)))), SB.mul3(U32.and(255, d)))) : {_ == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, b))), U32.and(255, SB.xtime(U32.and(255, c))))), U32.and(255, SB.mul3(U32.and(255, d))))) : U32}
1948 {==}