def ap.mm
bend-osdev-aes@0.1.0.0 · PROOF.bend:1998
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/types.bend as TT
1998def ap.mm(+s: TT.State) -> {X.aes.mask(X.aes.mask(s)) == X.aes.mask(s) : TT.State}:
1999 match s:
2000 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}}:
2001 %Equal.sym(U32, U32.and(255, U32.and(255, z0)), U32.and(255, z0), ap.bb(z0)) : {TT.S{TT.W{_, U32.and(255, U32.and(255, z1)), U32.and(255, U32.and(255, z2)), U32.and(255, U32.and(255, z3))}, TT.W{U32.and(255, U32.and(255, z4)), U32.and(255, U32.and(255, z5)), U32.and(255, U32.and(255, z6)), U32.and(255, U32.and(255, z7))}, TT.W{U32.and(255, U32.and(255, z8)), U32.and(255, U32.and(255, z9)), U32.and(255, U32.and(255, z10)), U32.and(255, U32.and(255, z11))}, TT.W{U32.and(255, U32.and(255, z12)), U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2002 %Equal.sym(U32, U32.and(255, U32.and(255, z1)), U32.and(255, z1), ap.bb(z1)) : {TT.S{TT.W{U32.and(255, z0), _, U32.and(255, U32.and(255, z2)), U32.and(255, U32.and(255, z3))}, TT.W{U32.and(255, U32.and(255, z4)), U32.and(255, U32.and(255, z5)), U32.and(255, U32.and(255, z6)), U32.and(255, U32.and(255, z7))}, TT.W{U32.and(255, U32.and(255, z8)), U32.and(255, U32.and(255, z9)), U32.and(255, U32.and(255, z10)), U32.and(255, U32.and(255, z11))}, TT.W{U32.and(255, U32.and(255, z12)), U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2003 %Equal.sym(U32, U32.and(255, U32.and(255, z2)), U32.and(255, z2), ap.bb(z2)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), _, U32.and(255, U32.and(255, z3))}, TT.W{U32.and(255, U32.and(255, z4)), U32.and(255, U32.and(255, z5)), U32.and(255, U32.and(255, z6)), U32.and(255, U32.and(255, z7))}, TT.W{U32.and(255, U32.and(255, z8)), U32.and(255, U32.and(255, z9)), U32.and(255, U32.and(255, z10)), U32.and(255, U32.and(255, z11))}, TT.W{U32.and(255, U32.and(255, z12)), U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2004 %Equal.sym(U32, U32.and(255, U32.and(255, z3)), U32.and(255, z3), ap.bb(z3)) : {TT.S{TT.W{U32.and(255, z0), U32.and(255, z1), U32.and(255, z2), _}, TT.W{U32.and(255, U32.and(255, z4)), U32.and(255, U32.and(255, z5)), U32.and(255, U32.and(255, z6)), U32.and(255, U32.and(255, z7))}, TT.W{U32.and(255, U32.and(255, z8)), U32.and(255, U32.and(255, z9)), U32.and(255, U32.and(255, z10)), U32.and(255, U32.and(255, z11))}, TT.W{U32.and(255, U32.and(255, z12)), U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2005 %Equal.sym(U32, U32.and(255, U32.and(255, z4)), U32.and(255, z4), ap.bb(z4)) : {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, U32.and(255, z5)), U32.and(255, U32.and(255, z6)), U32.and(255, U32.and(255, z7))}, TT.W{U32.and(255, U32.and(255, z8)), U32.and(255, U32.and(255, z9)), U32.and(255, U32.and(255, z10)), U32.and(255, U32.and(255, z11))}, TT.W{U32.and(255, U32.and(255, z12)), U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2006 %Equal.sym(U32, U32.and(255, U32.and(255, z5)), U32.and(255, z5), ap.bb(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), _, U32.and(255, U32.and(255, z6)), U32.and(255, U32.and(255, z7))}, TT.W{U32.and(255, U32.and(255, z8)), U32.and(255, U32.and(255, z9)), U32.and(255, U32.and(255, z10)), U32.and(255, U32.and(255, z11))}, TT.W{U32.and(255, U32.and(255, z12)), U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2007 %Equal.sym(U32, U32.and(255, U32.and(255, z6)), U32.and(255, z6), ap.bb(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), _, U32.and(255, U32.and(255, z7))}, TT.W{U32.and(255, U32.and(255, z8)), U32.and(255, U32.and(255, z9)), U32.and(255, U32.and(255, z10)), U32.and(255, U32.and(255, z11))}, TT.W{U32.and(255, U32.and(255, z12)), U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2008 %Equal.sym(U32, U32.and(255, U32.and(255, z7)), U32.and(255, z7), ap.bb(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{U32.and(255, U32.and(255, z8)), U32.and(255, U32.and(255, z9)), U32.and(255, U32.and(255, z10)), U32.and(255, U32.and(255, z11))}, TT.W{U32.and(255, U32.and(255, z12)), U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2009 %Equal.sym(U32, U32.and(255, U32.and(255, z8)), U32.and(255, z8), ap.bb(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{_, U32.and(255, U32.and(255, z9)), U32.and(255, U32.and(255, z10)), U32.and(255, U32.and(255, z11))}, TT.W{U32.and(255, U32.and(255, z12)), U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2010 %Equal.sym(U32, U32.and(255, U32.and(255, z9)), U32.and(255, z9), ap.bb(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), _, U32.and(255, U32.and(255, z10)), U32.and(255, U32.and(255, z11))}, TT.W{U32.and(255, U32.and(255, z12)), U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2011 %Equal.sym(U32, U32.and(255, U32.and(255, z10)), U32.and(255, z10), ap.bb(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), _, U32.and(255, U32.and(255, z11))}, TT.W{U32.and(255, U32.and(255, z12)), U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2012 %Equal.sym(U32, U32.and(255, U32.and(255, z11)), U32.and(255, z11), ap.bb(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{U32.and(255, U32.and(255, z12)), U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2013 %Equal.sym(U32, U32.and(255, U32.and(255, z12)), U32.and(255, z12), ap.bb(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{_, U32.and(255, U32.and(255, z13)), U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2014 %Equal.sym(U32, U32.and(255, U32.and(255, z13)), U32.and(255, z13), ap.bb(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), _, U32.and(255, U32.and(255, z14)), U32.and(255, 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}
2015 %Equal.sym(U32, U32.and(255, U32.and(255, z14)), U32.and(255, z14), ap.bb(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), _, U32.and(255, 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}
2016 %Equal.sym(U32, U32.and(255, U32.and(255, z15)), U32.and(255, z15), ap.bb(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}
2017 {==}