def tf_unop_op

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

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/twofish.bend as F

443def tf_unop_op(o: F.LcTfOp, +s: M.CmBlock) -> {s == F.tf.unop(o, F.tf.op(o, s)) : M.CmBlock}:
444  match o:
445    case F.LcTfBswap{}:
446      tf_bswap(s)
447    case F.LcTfWhite{k}:
448      block_xx(s, k)
449    case F.LcTfRound{tb, sk, ka, kb}:
450      tf_round(tb, sk, ka, kb, s)
451    case F.LcTfSwap{}:
452      match s:
453        case M.CmBlock{a, b, c, d}:
454          {==}