PROOF.aria_unop_op: 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 8375-8384 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=8375&end_line=8384

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/aria.bend as A

def aria_unop_op(o: A.LcAriaOp, +s: A.LcAriaSt) -> {s == A.aria.unop(o, A.aria.op(o, s)) : A.LcAriaSt}:
  match o:
    case A.LcAriaRk{+k}:
      aria_xor2(s, k)
    case A.LcAriaSl1{}:
      aria_sl21(s)
    case A.LcAriaSl2{}:
      aria_sl12(s)
    case A.LcAriaDiff{}:
      aria_diff(s)

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=aria_diff
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=aria_sl12
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=aria_sl21
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=aria_xor2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/aria.bend&name=LcAriaOp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/aria.bend&name=LcAriaSt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/aria.bend&name=aria.op
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/aria.bend&name=aria.unop