PROOF.ap.rowb1: def of bend-osdev-aes@0.1.0.0
Import: import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
Lines 1934-1940 of bend-osdev-aes@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&start_line=1934&end_line=1940

import Base
import bend-collections@1.0.0.0/src/crypto/aes/sbox.bend as SB

def ap.rowb1(+a: U32, +b: U32, +c: U32, +d: U32) -> {U32.xor(U32.xor(U32.xor(U32.and(255, a), SB.xtime(U32.and(255, b))), SB.mul3(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, a), U32.and(255, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(U32.and(255, c))))), U32.and(255, d))) : U32}:
  %Equal.sym(U32, SB.xtime(U32.and(255, b)), U32.and(255, SB.xtime(U32.and(255, b))), ap.xtb(b)) : {U32.xor(U32.xor(U32.xor(U32.and(255, a), _), SB.mul3(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, a), U32.and(255, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(U32.and(255, c))))), U32.and(255, d))) : U32}
  %Equal.sym(U32, SB.mul3(U32.and(255, c)), U32.and(255, SB.mul3(U32.and(255, c))), ap.m3b(c)) : {U32.xor(U32.xor(U32.xor(U32.and(255, a), U32.and(255, SB.xtime(U32.and(255, b)))), _), 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, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(U32.and(255, c))))), U32.and(255, d))) : U32}
  %Equal.sym(U32, U32.xor(U32.and(255, a), U32.and(255, SB.xtime(U32.and(255, b)))), U32.and(255, U32.xor(U32.and(255, a), U32.and(255, SB.xtime(U32.and(255, b))))), ap.xorb(a, SB.xtime(U32.and(255, b)))) : {U32.xor(U32.xor(_, U32.and(255, SB.mul3(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, a), U32.and(255, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(U32.and(255, c))))), U32.and(255, d))) : U32}
  %Equal.sym(U32, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(U32.and(255, c)))), U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(U32.and(255, c))))), ap.xorb(U32.xor(U32.and(255, a), U32.and(255, SB.xtime(U32.and(255, b)))), SB.mul3(U32.and(255, 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, a), U32.and(255, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(U32.and(255, c))))), U32.and(255, d))) : U32}
  %Equal.sym(U32, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(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, a), U32.and(255, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(U32.and(255, c))))), U32.and(255, d))), ap.xorb(U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(U32.and(255, c)))), d)) : {_ == U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, U32.xor(U32.and(255, a), U32.and(255, SB.xtime(U32.and(255, b))))), U32.and(255, SB.mul3(U32.and(255, c))))), U32.and(255, d))) : U32}
  {==}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/sbox.bend&name=mul3
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/sbox.bend&name=xtime
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.m3b
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.xorb
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.xtb