def ap.state_back
bend-osdev-aes@0.1.0.0 · PROOF.bend:2188
import bend-osdev-aes@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
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
2188def ap.state_back(+e: TT.State) -> {X.aes.state16(M.cm.bytes_of(M.cm.block_of(A.bytes_of(e)))) == X.aes.mask(e) : TT.State}:
2189 match e:
2190 case TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}:
2191 %Equal.sym(List<&2, U32>, M.cm.bytes_onto(M.cm.block16(e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, e10, e11, e12, e13, e14, e15), Nil{}), Con{B.byte(e0), Con{B.byte(e1), Con{B.byte(e2), Con{B.byte(e3), Con{B.byte(e4), Con{B.byte(e5), Con{B.byte(e6), Con{B.byte(e7), Con{B.byte(e8), Con{B.byte(e9), Con{B.byte(e10), Con{B.byte(e11), Con{B.byte(e12), Con{B.byte(e13), Con{B.byte(e14), Con{B.byte(e15), Nil{}}}}}}}}}}}}}}}}}, sp.blk16g(e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, e10, e11, e12, e13, e14, e15, Nil{})) : {X.aes.state16(_) == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2192 %Equal.sym(U32, B.byte(e0), U32.and(255, e0), ap.bylo(e0)) : {TT.S{TT.W{_, B.byte(e1), B.byte(e2), B.byte(e3)}, TT.W{B.byte(e4), B.byte(e5), B.byte(e6), B.byte(e7)}, TT.W{B.byte(e8), B.byte(e9), B.byte(e10), B.byte(e11)}, TT.W{B.byte(e12), B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2193 %Equal.sym(U32, B.byte(e1), U32.and(255, e1), ap.bylo(e1)) : {TT.S{TT.W{U32.and(255, e0), _, B.byte(e2), B.byte(e3)}, TT.W{B.byte(e4), B.byte(e5), B.byte(e6), B.byte(e7)}, TT.W{B.byte(e8), B.byte(e9), B.byte(e10), B.byte(e11)}, TT.W{B.byte(e12), B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2194 %Equal.sym(U32, B.byte(e2), U32.and(255, e2), ap.bylo(e2)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), _, B.byte(e3)}, TT.W{B.byte(e4), B.byte(e5), B.byte(e6), B.byte(e7)}, TT.W{B.byte(e8), B.byte(e9), B.byte(e10), B.byte(e11)}, TT.W{B.byte(e12), B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2195 %Equal.sym(U32, B.byte(e3), U32.and(255, e3), ap.bylo(e3)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), _}, TT.W{B.byte(e4), B.byte(e5), B.byte(e6), B.byte(e7)}, TT.W{B.byte(e8), B.byte(e9), B.byte(e10), B.byte(e11)}, TT.W{B.byte(e12), B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2196 %Equal.sym(U32, B.byte(e4), U32.and(255, e4), ap.bylo(e4)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), U32.and(255, e3)}, TT.W{_, B.byte(e5), B.byte(e6), B.byte(e7)}, TT.W{B.byte(e8), B.byte(e9), B.byte(e10), B.byte(e11)}, TT.W{B.byte(e12), B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2197 %Equal.sym(U32, B.byte(e5), U32.and(255, e5), ap.bylo(e5)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), U32.and(255, e3)}, TT.W{U32.and(255, e4), _, B.byte(e6), B.byte(e7)}, TT.W{B.byte(e8), B.byte(e9), B.byte(e10), B.byte(e11)}, TT.W{B.byte(e12), B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2198 %Equal.sym(U32, B.byte(e6), U32.and(255, e6), ap.bylo(e6)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), U32.and(255, e3)}, TT.W{U32.and(255, e4), U32.and(255, e5), _, B.byte(e7)}, TT.W{B.byte(e8), B.byte(e9), B.byte(e10), B.byte(e11)}, TT.W{B.byte(e12), B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2199 %Equal.sym(U32, B.byte(e7), U32.and(255, e7), ap.bylo(e7)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), U32.and(255, e3)}, TT.W{U32.and(255, e4), U32.and(255, e5), U32.and(255, e6), _}, TT.W{B.byte(e8), B.byte(e9), B.byte(e10), B.byte(e11)}, TT.W{B.byte(e12), B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2200 %Equal.sym(U32, B.byte(e8), U32.and(255, e8), ap.bylo(e8)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), U32.and(255, e3)}, TT.W{U32.and(255, e4), U32.and(255, e5), U32.and(255, e6), U32.and(255, e7)}, TT.W{_, B.byte(e9), B.byte(e10), B.byte(e11)}, TT.W{B.byte(e12), B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2201 %Equal.sym(U32, B.byte(e9), U32.and(255, e9), ap.bylo(e9)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), U32.and(255, e3)}, TT.W{U32.and(255, e4), U32.and(255, e5), U32.and(255, e6), U32.and(255, e7)}, TT.W{U32.and(255, e8), _, B.byte(e10), B.byte(e11)}, TT.W{B.byte(e12), B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2202 %Equal.sym(U32, B.byte(e10), U32.and(255, e10), ap.bylo(e10)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), U32.and(255, e3)}, TT.W{U32.and(255, e4), U32.and(255, e5), U32.and(255, e6), U32.and(255, e7)}, TT.W{U32.and(255, e8), U32.and(255, e9), _, B.byte(e11)}, TT.W{B.byte(e12), B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2203 %Equal.sym(U32, B.byte(e11), U32.and(255, e11), ap.bylo(e11)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), U32.and(255, e3)}, TT.W{U32.and(255, e4), U32.and(255, e5), U32.and(255, e6), U32.and(255, e7)}, TT.W{U32.and(255, e8), U32.and(255, e9), U32.and(255, e10), _}, TT.W{B.byte(e12), B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2204 %Equal.sym(U32, B.byte(e12), U32.and(255, e12), ap.bylo(e12)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), U32.and(255, e3)}, TT.W{U32.and(255, e4), U32.and(255, e5), U32.and(255, e6), U32.and(255, e7)}, TT.W{U32.and(255, e8), U32.and(255, e9), U32.and(255, e10), U32.and(255, e11)}, TT.W{_, B.byte(e13), B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2205 %Equal.sym(U32, B.byte(e13), U32.and(255, e13), ap.bylo(e13)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), U32.and(255, e3)}, TT.W{U32.and(255, e4), U32.and(255, e5), U32.and(255, e6), U32.and(255, e7)}, TT.W{U32.and(255, e8), U32.and(255, e9), U32.and(255, e10), U32.and(255, e11)}, TT.W{U32.and(255, e12), _, B.byte(e14), B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2206 %Equal.sym(U32, B.byte(e14), U32.and(255, e14), ap.bylo(e14)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), U32.and(255, e3)}, TT.W{U32.and(255, e4), U32.and(255, e5), U32.and(255, e6), U32.and(255, e7)}, TT.W{U32.and(255, e8), U32.and(255, e9), U32.and(255, e10), U32.and(255, e11)}, TT.W{U32.and(255, e12), U32.and(255, e13), _, B.byte(e15)}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2207 %Equal.sym(U32, B.byte(e15), U32.and(255, e15), ap.bylo(e15)) : {TT.S{TT.W{U32.and(255, e0), U32.and(255, e1), U32.and(255, e2), U32.and(255, e3)}, TT.W{U32.and(255, e4), U32.and(255, e5), U32.and(255, e6), U32.and(255, e7)}, TT.W{U32.and(255, e8), U32.and(255, e9), U32.and(255, e10), U32.and(255, e11)}, TT.W{U32.and(255, e12), U32.and(255, e13), U32.and(255, e14), _}} == X.aes.mask(TT.S{TT.W{e0, e1, e2, e3}, TT.W{e4, e5, e6, e7}, TT.W{e8, e9, e10, e11}, TT.W{e12, e13, e14, e15}}) : TT.State}
2208 {==}