PROOF.aria_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 8386-8395 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=8386&end_line=8395

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

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

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=aria_diffd
  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