def sp_unop_op
bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:1287
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
1287def sp_unop_op(o: P.LcSpOp, +s: M.CmBlock) -> {s == P.sp.unop(o, P.sp.op(o, s)) : M.CmBlock}:
1288 match o:
1289 case P.LcSpBswap{}:
1290 sp_bswap(s)
1291 case P.LcSpKey{k}:
1292 block_xx(s, k)
1293 case P.LcSpS{bx}:
1294 sp_sop_inv(bx, False{}, s)
1295 case P.LcSpLt{}:
1296 sp_lt_inv(s)