PROOF.tea_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 1484-1511 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=1484&end_line=1511

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
import bend-osdev-legacy-ciphers@0.1.0.0/tea.bend as TE

def tea_unop_op(o: TE.LcTeaOp, b: L.LcBlock64) -> {b == TE.tea.unop(o, TE.tea.op(o, b)) : L.LcBlock64}:
  match o:
    case TE.LcTeaY{+s, +ka, +kb}:
      match b:
        case L.LcBlock64{y, +z}:
          %u32_add_sub(y, TE.tea.g(z, s, ka, kb)) : {L.LcBlock64{y, z} == L.LcBlock64{_, z} : L.LcBlock64}
          {==}
    case TE.LcTeaZ{+s, +ka, +kb}:
      match b:
        case L.LcBlock64{+y, z}:
          %u32_add_sub(z, TE.tea.g(y, s, ka, kb)) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64}
          {==}
    case TE.LcXteaY{+c}:
      match b:
        case L.LcBlock64{y, +z}:
          %u32_add_sub(y, TE.xtea.g(z, c)) : {L.LcBlock64{y, z} == L.LcBlock64{_, z} : L.LcBlock64}
          {==}
    case TE.LcXteaZ{+c}:
      match b:
        case L.LcBlock64{+y, z}:
          %u32_add_sub(z, TE.xtea.g(y, c)) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64}
          {==}
    case TE.LcTeaBswap{}:
      match b:
        case L.LcBlock64{+y, +z}:
          %bswap2(y) : {L.LcBlock64{y, z} == L.LcBlock64{_, L.lc.bswap.bits(L.lc.bswap.bits(z))} : L.LcBlock64}
          %bswap2(z) : {L.LcBlock64{y, z} == L.LcBlock64{y, _} : L.LcBlock64}
          {==}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=bswap2
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend&name=u32_add_sub
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend&name=LcBlock64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend&name=lc.bswap.bits
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/tea.bend&name=LcTeaOp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/tea.bend&name=tea.g
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/tea.bend&name=tea.op
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/tea.bend&name=tea.unop
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/tea.bend&name=xtea.g