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

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.subl(+s: TT.State) -> {A.sub_bytes(X.aes.mask(s)) == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z0)), U32.and(255, SB.sbox(U32.and(255, z0))), ap.sbl(z0)) : {TT.S{TT.W{_, SB.sbox(U32.and(255, z1)), SB.sbox(U32.and(255, z2)), SB.sbox(U32.and(255, z3))}, TT.W{SB.sbox(U32.and(255, z4)), SB.sbox(U32.and(255, z5)), SB.sbox(U32.and(255, z6)), SB.sbox(U32.and(255, z7))}, TT.W{SB.sbox(U32.and(255, z8)), SB.sbox(U32.and(255, z9)), SB.sbox(U32.and(255, z10)), SB.sbox(U32.and(255, z11))}, TT.W{SB.sbox(U32.and(255, z12)), SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z1)), U32.and(255, SB.sbox(U32.and(255, z1))), ap.sbl(z1)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), _, SB.sbox(U32.and(255, z2)), SB.sbox(U32.and(255, z3))}, TT.W{SB.sbox(U32.and(255, z4)), SB.sbox(U32.and(255, z5)), SB.sbox(U32.and(255, z6)), SB.sbox(U32.and(255, z7))}, TT.W{SB.sbox(U32.and(255, z8)), SB.sbox(U32.and(255, z9)), SB.sbox(U32.and(255, z10)), SB.sbox(U32.and(255, z11))}, TT.W{SB.sbox(U32.and(255, z12)), SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z2)), U32.and(255, SB.sbox(U32.and(255, z2))), ap.sbl(z2)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), _, SB.sbox(U32.and(255, z3))}, TT.W{SB.sbox(U32.and(255, z4)), SB.sbox(U32.and(255, z5)), SB.sbox(U32.and(255, z6)), SB.sbox(U32.and(255, z7))}, TT.W{SB.sbox(U32.and(255, z8)), SB.sbox(U32.and(255, z9)), SB.sbox(U32.and(255, z10)), SB.sbox(U32.and(255, z11))}, TT.W{SB.sbox(U32.and(255, z12)), SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z3)), U32.and(255, SB.sbox(U32.and(255, z3))), ap.sbl(z3)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), _}, TT.W{SB.sbox(U32.and(255, z4)), SB.sbox(U32.and(255, z5)), SB.sbox(U32.and(255, z6)), SB.sbox(U32.and(255, z7))}, TT.W{SB.sbox(U32.and(255, z8)), SB.sbox(U32.and(255, z9)), SB.sbox(U32.and(255, z10)), SB.sbox(U32.and(255, z11))}, TT.W{SB.sbox(U32.and(255, z12)), SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z4)), U32.and(255, SB.sbox(U32.and(255, z4))), ap.sbl(z4)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), U32.and(255, SB.sbox(U32.and(255, z3)))}, TT.W{_, SB.sbox(U32.and(255, z5)), SB.sbox(U32.and(255, z6)), SB.sbox(U32.and(255, z7))}, TT.W{SB.sbox(U32.and(255, z8)), SB.sbox(U32.and(255, z9)), SB.sbox(U32.and(255, z10)), SB.sbox(U32.and(255, z11))}, TT.W{SB.sbox(U32.and(255, z12)), SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z5)), U32.and(255, SB.sbox(U32.and(255, z5))), ap.sbl(z5)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), U32.and(255, SB.sbox(U32.and(255, z3)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z4))), _, SB.sbox(U32.and(255, z6)), SB.sbox(U32.and(255, z7))}, TT.W{SB.sbox(U32.and(255, z8)), SB.sbox(U32.and(255, z9)), SB.sbox(U32.and(255, z10)), SB.sbox(U32.and(255, z11))}, TT.W{SB.sbox(U32.and(255, z12)), SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z6)), U32.and(255, SB.sbox(U32.and(255, z6))), ap.sbl(z6)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), U32.and(255, SB.sbox(U32.and(255, z3)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z4))), U32.and(255, SB.sbox(U32.and(255, z5))), _, SB.sbox(U32.and(255, z7))}, TT.W{SB.sbox(U32.and(255, z8)), SB.sbox(U32.and(255, z9)), SB.sbox(U32.and(255, z10)), SB.sbox(U32.and(255, z11))}, TT.W{SB.sbox(U32.and(255, z12)), SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z7)), U32.and(255, SB.sbox(U32.and(255, z7))), ap.sbl(z7)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), U32.and(255, SB.sbox(U32.and(255, z3)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z4))), U32.and(255, SB.sbox(U32.and(255, z5))), U32.and(255, SB.sbox(U32.and(255, z6))), _}, TT.W{SB.sbox(U32.and(255, z8)), SB.sbox(U32.and(255, z9)), SB.sbox(U32.and(255, z10)), SB.sbox(U32.and(255, z11))}, TT.W{SB.sbox(U32.and(255, z12)), SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z8)), U32.and(255, SB.sbox(U32.and(255, z8))), ap.sbl(z8)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), U32.and(255, SB.sbox(U32.and(255, z3)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z4))), U32.and(255, SB.sbox(U32.and(255, z5))), U32.and(255, SB.sbox(U32.and(255, z6))), U32.and(255, SB.sbox(U32.and(255, z7)))}, TT.W{_, SB.sbox(U32.and(255, z9)), SB.sbox(U32.and(255, z10)), SB.sbox(U32.and(255, z11))}, TT.W{SB.sbox(U32.and(255, z12)), SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z9)), U32.and(255, SB.sbox(U32.and(255, z9))), ap.sbl(z9)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), U32.and(255, SB.sbox(U32.and(255, z3)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z4))), U32.and(255, SB.sbox(U32.and(255, z5))), U32.and(255, SB.sbox(U32.and(255, z6))), U32.and(255, SB.sbox(U32.and(255, z7)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z8))), _, SB.sbox(U32.and(255, z10)), SB.sbox(U32.and(255, z11))}, TT.W{SB.sbox(U32.and(255, z12)), SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z10)), U32.and(255, SB.sbox(U32.and(255, z10))), ap.sbl(z10)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), U32.and(255, SB.sbox(U32.and(255, z3)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z4))), U32.and(255, SB.sbox(U32.and(255, z5))), U32.and(255, SB.sbox(U32.and(255, z6))), U32.and(255, SB.sbox(U32.and(255, z7)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z8))), U32.and(255, SB.sbox(U32.and(255, z9))), _, SB.sbox(U32.and(255, z11))}, TT.W{SB.sbox(U32.and(255, z12)), SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z11)), U32.and(255, SB.sbox(U32.and(255, z11))), ap.sbl(z11)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), U32.and(255, SB.sbox(U32.and(255, z3)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z4))), U32.and(255, SB.sbox(U32.and(255, z5))), U32.and(255, SB.sbox(U32.and(255, z6))), U32.and(255, SB.sbox(U32.and(255, z7)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z8))), U32.and(255, SB.sbox(U32.and(255, z9))), U32.and(255, SB.sbox(U32.and(255, z10))), _}, TT.W{SB.sbox(U32.and(255, z12)), SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z12)), U32.and(255, SB.sbox(U32.and(255, z12))), ap.sbl(z12)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), U32.and(255, SB.sbox(U32.and(255, z3)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z4))), U32.and(255, SB.sbox(U32.and(255, z5))), U32.and(255, SB.sbox(U32.and(255, z6))), U32.and(255, SB.sbox(U32.and(255, z7)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z8))), U32.and(255, SB.sbox(U32.and(255, z9))), U32.and(255, SB.sbox(U32.and(255, z10))), U32.and(255, SB.sbox(U32.and(255, z11)))}, TT.W{_, SB.sbox(U32.and(255, z13)), SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z13)), U32.and(255, SB.sbox(U32.and(255, z13))), ap.sbl(z13)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), U32.and(255, SB.sbox(U32.and(255, z3)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z4))), U32.and(255, SB.sbox(U32.and(255, z5))), U32.and(255, SB.sbox(U32.and(255, z6))), U32.and(255, SB.sbox(U32.and(255, z7)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z8))), U32.and(255, SB.sbox(U32.and(255, z9))), U32.and(255, SB.sbox(U32.and(255, z10))), U32.and(255, SB.sbox(U32.and(255, z11)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z12))), _, SB.sbox(U32.and(255, z14)), SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z14)), U32.and(255, SB.sbox(U32.and(255, z14))), ap.sbl(z14)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), U32.and(255, SB.sbox(U32.and(255, z3)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z4))), U32.and(255, SB.sbox(U32.and(255, z5))), U32.and(255, SB.sbox(U32.and(255, z6))), U32.and(255, SB.sbox(U32.and(255, z7)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z8))), U32.and(255, SB.sbox(U32.and(255, z9))), U32.and(255, SB.sbox(U32.and(255, z10))), U32.and(255, SB.sbox(U32.and(255, z11)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z12))), U32.and(255, SB.sbox(U32.and(255, z13))), _, SB.sbox(U32.and(255, z15))}} == X.aes.mask(A.sub_bytes(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, SB.sbox(U32.and(255, z15)), U32.and(255, SB.sbox(U32.and(255, z15))), ap.sbl(z15)) : {TT.S{TT.W{U32.and(255, SB.sbox(U32.and(255, z0))), U32.and(255, SB.sbox(U32.and(255, z1))), U32.and(255, SB.sbox(U32.and(255, z2))), U32.and(255, SB.sbox(U32.and(255, z3)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z4))), U32.and(255, SB.sbox(U32.and(255, z5))), U32.and(255, SB.sbox(U32.and(255, z6))), U32.and(255, SB.sbox(U32.and(255, z7)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z8))), U32.and(255, SB.sbox(U32.and(255, z9))), U32.and(255, SB.sbox(U32.and(255, z10))), U32.and(255, SB.sbox(U32.and(255, z11)))}, TT.W{U32.and(255, SB.sbox(U32.and(255, z12))), U32.and(255, SB.sbox(U32.and(255, z13))), U32.and(255, SB.sbox(U32.and(255, z14))), _}} == X.aes.mask(A.sub_bytes(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 (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=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.sbl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-aes@0.1.0.0/aes.bend&name=aes.mask