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

import Base
import bend-osdev-aes@0.1.0.0/aes.bend as X
import bend-collections@1.0.0.0/src/crypto/aes/aes.bend as A
import bend-collections@1.0.0.0/src/crypto/aes/types.bend as TT
import bend-collections@1.0.0.0/src/crypto/aes/sbox.bend as SB

def ap.subi(+s: TT.State) -> {X.aes.inv_sub(A.sub_bytes(X.aes.mask(s))) == X.aes.mask(s) : TT.State}:
  match s:
    case TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}:
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z0))), U32.and(255, z0), ap.sbi(z0)) : {TT.S{TT.W{_, X.aes.isbox(SB.sbox(U32.and(255, z1))), X.aes.isbox(SB.sbox(U32.and(255, z2))), X.aes.isbox(SB.sbox(U32.and(255, z3)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z4))), X.aes.isbox(SB.sbox(U32.and(255, z5))), X.aes.isbox(SB.sbox(U32.and(255, z6))), X.aes.isbox(SB.sbox(U32.and(255, z7)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z8))), X.aes.isbox(SB.sbox(U32.and(255, z9))), X.aes.isbox(SB.sbox(U32.and(255, z10))), X.aes.isbox(SB.sbox(U32.and(255, z11)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z12))), X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z1))), U32.and(255, z1), ap.sbi(z1)) : {TT.S{TT.W{U32.and(255, z0), _, X.aes.isbox(SB.sbox(U32.and(255, z2))), X.aes.isbox(SB.sbox(U32.and(255, z3)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z4))), X.aes.isbox(SB.sbox(U32.and(255, z5))), X.aes.isbox(SB.sbox(U32.and(255, z6))), X.aes.isbox(SB.sbox(U32.and(255, z7)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z8))), X.aes.isbox(SB.sbox(U32.and(255, z9))), X.aes.isbox(SB.sbox(U32.and(255, z10))), X.aes.isbox(SB.sbox(U32.and(255, z11)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z12))), X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z2))), U32.and(255, z2), ap.sbi(z2)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), _, X.aes.isbox(SB.sbox(U32.and(255, z3)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z4))), X.aes.isbox(SB.sbox(U32.and(255, z5))), X.aes.isbox(SB.sbox(U32.and(255, z6))), X.aes.isbox(SB.sbox(U32.and(255, z7)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z8))), X.aes.isbox(SB.sbox(U32.and(255, z9))), X.aes.isbox(SB.sbox(U32.and(255, z10))), X.aes.isbox(SB.sbox(U32.and(255, z11)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z12))), X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z3))), U32.and(255, z3), ap.sbi(z3)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), _}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z4))), X.aes.isbox(SB.sbox(U32.and(255, z5))), X.aes.isbox(SB.sbox(U32.and(255, z6))), X.aes.isbox(SB.sbox(U32.and(255, z7)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z8))), X.aes.isbox(SB.sbox(U32.and(255, z9))), X.aes.isbox(SB.sbox(U32.and(255, z10))), X.aes.isbox(SB.sbox(U32.and(255, z11)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z12))), X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z4))), U32.and(255, z4), ap.sbi(z4)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, TT.W{_, X.aes.isbox(SB.sbox(U32.and(255, z5))), X.aes.isbox(SB.sbox(U32.and(255, z6))), X.aes.isbox(SB.sbox(U32.and(255, z7)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z8))), X.aes.isbox(SB.sbox(U32.and(255, z9))), X.aes.isbox(SB.sbox(U32.and(255, z10))), X.aes.isbox(SB.sbox(U32.and(255, z11)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z12))), X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z5))), U32.and(255, z5), ap.sbi(z5)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, TT.W{U32.and(255, z4), _, X.aes.isbox(SB.sbox(U32.and(255, z6))), X.aes.isbox(SB.sbox(U32.and(255, z7)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z8))), X.aes.isbox(SB.sbox(U32.and(255, z9))), X.aes.isbox(SB.sbox(U32.and(255, z10))), X.aes.isbox(SB.sbox(U32.and(255, z11)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z12))), X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z6))), U32.and(255, z6), ap.sbi(z6)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, TT.W{U32.and(255, z4), U32.and(255, z5), _, X.aes.isbox(SB.sbox(U32.and(255, z7)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z8))), X.aes.isbox(SB.sbox(U32.and(255, z9))), X.aes.isbox(SB.sbox(U32.and(255, z10))), X.aes.isbox(SB.sbox(U32.and(255, z11)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z12))), X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z7))), U32.and(255, z7), ap.sbi(z7)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), _}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z8))), X.aes.isbox(SB.sbox(U32.and(255, z9))), X.aes.isbox(SB.sbox(U32.and(255, z10))), X.aes.isbox(SB.sbox(U32.and(255, z11)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z12))), X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z8))), U32.and(255, z8), ap.sbi(z8)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)}, TT.W{_, X.aes.isbox(SB.sbox(U32.and(255, z9))), X.aes.isbox(SB.sbox(U32.and(255, z10))), X.aes.isbox(SB.sbox(U32.and(255, z11)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z12))), X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z9))), U32.and(255, z9), ap.sbi(z9)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)}, TT.W{U32.and(255, z8), _, X.aes.isbox(SB.sbox(U32.and(255, z10))), X.aes.isbox(SB.sbox(U32.and(255, z11)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z12))), X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z10))), U32.and(255, z10), ap.sbi(z10)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)}, TT.W{U32.and(255, z8), U32.and(255, z9), _, X.aes.isbox(SB.sbox(U32.and(255, z11)))}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z12))), X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z11))), U32.and(255, z11), ap.sbi(z11)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)}, TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), _}, TT.W{X.aes.isbox(SB.sbox(U32.and(255, z12))), X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z12))), U32.and(255, z12), ap.sbi(z12)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)}, TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)}, TT.W{_, X.aes.isbox(SB.sbox(U32.and(255, z13))), X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z13))), U32.and(255, z13), ap.sbi(z13)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)}, TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)}, TT.W{U32.and(255, z12), _, X.aes.isbox(SB.sbox(U32.and(255, z14))), X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z14))), U32.and(255, z14), ap.sbi(z14)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)}, TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)}, TT.W{U32.and(255, z12), U32.and(255, z13), _, X.aes.isbox(SB.sbox(U32.and(255, z15)))}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      %Equal.sym(U32, X.aes.isbox(SB.sbox(U32.and(255, z15))), U32.and(255, z15), ap.sbi(z15)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)}, TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)}, TT.W{U32.and(255, z12), U32.and(255, z13), U32.and(255, z14), _}} == X.aes.mask(TT.S{TT.W{z0, z1, z2, z3}, TT.W{z4, z5, z6, z7}, TT.W{z8, z9, z10, z11}, TT.W{z12, z13, z14, z15}}) : TT.State}
      {==}

Uses (11):
  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=bend-collections@1.0.0.0/src/crypto/aes/aes.bend&name=sub_bytes
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/sbox.bend&name=sbox
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/types.bend&name=Quad
  https://jend.leeeet.dev/definition.txt?path=bend-collections@1.0.0.0/src/crypto/aes/types.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/PROOF.bend&name=ap.sbi
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.inv_sub
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.isbox
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.mask