PROOF.ap.out1: def of bend-osdev-aes@0.1.0.0
Import: import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
Lines 1879-1889 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=1879&end_line=1889

import Base
import bend-osdev-gf@0.1.1.0/gf.bend as G
import bend-collections@1.0.0.0/src/crypto/aes/sbox.bend as SB

def ap.out1(+a: U32, +b: U32, +c: U32, +d: U32) -> {G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, 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))), G.Gf8.mul(G.Gf8.aes(), 11, 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))))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d)))), G.Gf8.mul(G.Gf8.aes(), 9, 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, b) : U32}:
  %Equal.sym(U32, G.Gf8.mul(G.Gf8.aes(), 14, 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))), G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, b)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, d)))), ap.row(14, U32.and(255, a), SB.xtime(U32.and(255, b)), SB.mul3(U32.and(255, c)), U32.and(255, d))) : {G.Gf8.add(G.Gf8.add(_, G.Gf8.mul(G.Gf8.aes(), 11, 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))))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d)))), G.Gf8.mul(G.Gf8.aes(), 9, 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, b) : U32}
  %Equal.sym(U32, G.Gf8.mul(G.Gf8.aes(), 11, 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)))), G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, b))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, d))))), ap.row(11, U32.and(255, a), U32.and(255, b), SB.xtime(U32.and(255, c)), SB.mul3(U32.and(255, d)))) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, b)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, d)))), _), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d)))), G.Gf8.mul(G.Gf8.aes(), 9, 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, b) : U32}
  %Equal.sym(U32, G.Gf8.mul(G.Gf8.aes(), 13, U32.xor(U32.xor(U32.xor(SB.mul3(U32.and(255, a)), U32.and(255, b)), U32.and(255, c)), SB.xtime(U32.and(255, d)))), G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.mul3(U32.and(255, a))), G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, b))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, c)), G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, d))))), ap.row(13, SB.mul3(U32.and(255, a)), U32.and(255, b), U32.and(255, c), SB.xtime(U32.and(255, d)))) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, b)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, d)))), G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, b))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, d)))))), G.Gf8.add(_, G.Gf8.mul(G.Gf8.aes(), 9, 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, b) : U32}
  %Equal.sym(U32, G.Gf8.mul(G.Gf8.aes(), 9, 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))), G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 9, SB.xtime(U32.and(255, a))), G.Gf8.mul(G.Gf8.aes(), 9, SB.mul3(U32.and(255, b)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, c)), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, d)))), ap.row(9, SB.xtime(U32.and(255, a)), SB.mul3(U32.and(255, b)), U32.and(255, c), U32.and(255, d))) : {G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, b)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, d)))), G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, b))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, d)))))), G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.mul3(U32.and(255, a))), G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, b))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, c)), G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, d))))), _)) == U32.and(255, b) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, b)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, d)))), G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, b))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, d)))))), G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.mul3(U32.and(255, a))), G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, b))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, c)), G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, d))))), G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 9, SB.xtime(U32.and(255, a))), G.Gf8.mul(G.Gf8.aes(), 9, SB.mul3(U32.and(255, b)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, c)), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, d)))))), G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, a))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.mul3(U32.and(255, a))), G.Gf8.mul(G.Gf8.aes(), 9, SB.xtime(U32.and(255, a))))), G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, b))), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, b))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, b)), G.Gf8.mul(G.Gf8.aes(), 9, SB.mul3(U32.and(255, b)))))), G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, c)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, c)), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, c)))), G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, d)), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, d)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, d))), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, d)))))), ap.trans(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, b))), G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, d)), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, b)), G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, d))), G.Gf8.mul(G.Gf8.aes(), 13, SB.mul3(U32.and(255, a))), G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, b)), G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, c)), G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, d))), G.Gf8.mul(G.Gf8.aes(), 9, SB.xtime(U32.and(255, a))), G.Gf8.mul(G.Gf8.aes(), 9, SB.mul3(U32.and(255, b))), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, c)), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, d)))) : {_ == U32.and(255, b) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, a)), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, a))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.mul3(U32.and(255, a))), G.Gf8.mul(G.Gf8.aes(), 9, SB.xtime(U32.and(255, a))))), 0, ap.col10(a)) : {G.Gf8.add(G.Gf8.add(_, G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, b))), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, b))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, b)), G.Gf8.mul(G.Gf8.aes(), 9, SB.mul3(U32.and(255, b)))))), G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, c)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, c)), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, c)))), G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, d)), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, d)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, d))), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, d)))))) == U32.and(255, b) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.xtime(U32.and(255, b))), G.Gf8.mul(G.Gf8.aes(), 11, U32.and(255, b))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, b)), G.Gf8.mul(G.Gf8.aes(), 9, SB.mul3(U32.and(255, b))))), U32.and(255, b), ap.col11(b)) : {G.Gf8.add(G.Gf8.add(0, _), G.Gf8.add(G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, c)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, c)), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, c)))), G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, d)), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, d)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, d))), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, d)))))) == U32.and(255, b) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, SB.mul3(U32.and(255, c))), G.Gf8.mul(G.Gf8.aes(), 11, SB.xtime(U32.and(255, c)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, U32.and(255, c)), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, c)))), 0, ap.col12(c)) : {G.Gf8.add(G.Gf8.add(0, U32.and(255, b)), G.Gf8.add(_, G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, d)), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, d)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, d))), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, d)))))) == U32.and(255, b) : U32}
  %Equal.sym(U32, G.Gf8.add(G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 14, U32.and(255, d)), G.Gf8.mul(G.Gf8.aes(), 11, SB.mul3(U32.and(255, d)))), G.Gf8.add(G.Gf8.mul(G.Gf8.aes(), 13, SB.xtime(U32.and(255, d))), G.Gf8.mul(G.Gf8.aes(), 9, U32.and(255, d)))), 0, ap.col13(d)) : {G.Gf8.add(G.Gf8.add(0, U32.and(255, b)), G.Gf8.add(0, _)) == U32.and(255, b) : U32}
  ap.fin1(b)

Uses (16):
  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.col10
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col11
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col12
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.col13
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.fin1
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.row
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.trans
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8.add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8.aes
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-gf@0.1.1.0/gf.bend&name=Gf8.mul