~/jendhub

def sp_lt_inv

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:1248

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

1248def sp_lt_inv(+s: M.CmBlock) -> {s == P.sp.ilt(P.sp.lt(s)) : M.CmBlock}:
1249  %sp_lt8(P.sp.lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s)))))))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(P.sp.lt7(_))))))) : M.CmBlock}
1250  %sp_lt7(P.sp.lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s))))))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(P.sp.lt4(P.sp.ilt5(P.sp.lt6(_)))))) : M.CmBlock}
1251  %sp_lt6(P.sp.lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s)))))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(P.sp.lt4(P.sp.ilt5(_))))) : M.CmBlock}
1252  %sp_lt5(P.sp.lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s))))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(P.sp.lt4(_)))) : M.CmBlock}
1253  %sp_lt4(P.sp.lt3(P.sp.lt2(P.sp.lt1(s)))) : {s == P.sp.ilt1(P.sp.ilt2(P.sp.lt3(_))) : M.CmBlock}
1254  %sp_lt3(P.sp.lt2(P.sp.lt1(s))) : {s == P.sp.ilt1(P.sp.ilt2(_)) : M.CmBlock}
1255  %sp_lt2(P.sp.lt1(s)) : {s == P.sp.ilt1(_) : M.CmBlock}
1256  sp_lt1(s)

Uses (21)

Used by (1)