def ap.mixi
bend-osdev-aes@0.1.0.0 · PROOF.bend:2070
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
2070def ap.mixi(+s: TT.State) -> {X.aes.inv_mix(A.mix_columns(X.aes.mask(s))) == X.aes.mask(s) : TT.State}:
2071 match s:
2072 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}}:
2073 %Equal.sym(TT.Quad, X.aes.imix_w(A.mix_column(TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)})), TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, ap.mixc(z0, z1, z2, z3)) : {TT.S{_, X.aes.imix_w(A.mix_column(TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)})), X.aes.imix_w(A.mix_column(TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)})), X.aes.imix_w(A.mix_column(TT.W{U32.and(255, z12), U32.and(255, z13), U32.and(255, z14), 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}
2074 %Equal.sym(TT.Quad, X.aes.imix_w(A.mix_column(TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)})), TT.W{U32.and(255, z4), U32.and(255, z5), U32.and(255, z6), U32.and(255, z7)}, ap.mixc(z4, z5, z6, z7)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), U32.and(255, z3)}, _, X.aes.imix_w(A.mix_column(TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)})), X.aes.imix_w(A.mix_column(TT.W{U32.and(255, z12), U32.and(255, z13), U32.and(255, z14), 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}
2075 %Equal.sym(TT.Quad, X.aes.imix_w(A.mix_column(TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)})), TT.W{U32.and(255, z8), U32.and(255, z9), U32.and(255, z10), U32.and(255, z11)}, ap.mixc(z8, z9, z10, 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)}, _, X.aes.imix_w(A.mix_column(TT.W{U32.and(255, z12), U32.and(255, z13), U32.and(255, z14), 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}
2076 %Equal.sym(TT.Quad, X.aes.imix_w(A.mix_column(TT.W{U32.and(255, z12), U32.and(255, z13), U32.and(255, z14), U32.and(255, z15)})), TT.W{U32.and(255, z12), U32.and(255, z13), U32.and(255, z14), U32.and(255, z15)}, ap.mixc(z12, z13, z14, 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)}, _} == 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}
2077 {==}