PROOF.c6_op_unop: def of bend-osdev-legacy-ciphers@0.1.0.0
Import: import bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend as PROOF
Lines 1692-1699 of bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&start_line=1692&end_line=1699

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/cast6.bend as C6

def c6_op_unop(o: C6.LcCast6Op, +s: M.CmBlock) -> {s == C6.c6.op(o, C6.c6.unop(o, s)) : M.CmBlock}:
  match o:
    case C6.LcCast6Op{fwd, +k}:
      match fwd:
        case True{}:
          c6_qbq(k, s)
        case False{}:
          c6_qq(k, s)

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend&name=CmBlock
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=c6_qbq
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=c6_qq
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/cast6.bend&name=LcCast6Op
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/cast6.bend&name=c6.op
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/cast6.bend&name=c6.unop