def ap.subl
bend-osdev-aes@0.1.0.0 · PROOF.bend:2019
import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
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
2019def ap.subl(+s: TT.State) -> {A.sub_bytes(X.aes.mask(s)) == X.aes.mask(A.sub_bytes(X.aes.mask(s))) : TT.State}:
2020 match s:
2021 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}}:
2022 %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}
2023 %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}
2024 %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}
2025 %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}
2026 %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}
2027 %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}
2028 %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}
2029 %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}
2030 %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}
2031 %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}
2032 %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}
2033 %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}
2034 %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}
2035 %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}
2036 %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}
2037 %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}
2038 {==}