def sp_lt_invd
bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:1258
import bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-legacy-ciphers@0.1.0.0/serpent.bend as P
1258def sp_lt_invd(+s: M.CmBlock) -> {s == P.sp.lt(P.sp.ilt(s)) : M.CmBlock}:
1259 %sp_lt1d(P.sp.ilt2(P.sp.lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s)))))))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(_))))))) : M.CmBlock}
1260 %sp_lt2d(P.sp.lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s))))))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(_)))))) : M.CmBlock}
1261 %sp_lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s)))))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(_))))) : M.CmBlock}
1262 %sp_lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s))))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(_)))) : M.CmBlock}
1263 %sp_lt5d(P.sp.lt6(P.sp.lt7(P.sp.ilt8(s)))) : {s == P.sp.lt8(P.sp.lt7(P.sp.lt6(_))) : M.CmBlock}
1264 %sp_lt6(P.sp.lt7(P.sp.ilt8(s))) : {s == P.sp.lt8(P.sp.lt7(_)) : M.CmBlock}
1265 %sp_lt7(P.sp.ilt8(s)) : {s == P.sp.lt8(_) : M.CmBlock}
1266 sp_lt8d(s)