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)

Uses (9)

Used by (1)