PROOF.lcblock64_xx: def of bend-osdev-crypto@0.1.0.0
Import: import bend-osdev-crypto@0.1.0.0/PROOF.bend as PROOF
Lines 270-275 of bend-osdev-crypto@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-crypto@0.1.0.0/PROOF.bend&start_line=270&end_line=275

import Base
import bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend as L
import bend-osdev-crypto@0.1.0.0/inst_lc.bend as LC

def lcblock64_xx(s: L.LcBlock64, k: L.LcBlock64) -> {s == LC.CrBlk64.xor(LC.CrBlk64.xor(s, k), k) : L.LcBlock64}:
  match s k:
    case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1}:
      %u32_xx(a0, b0) : {L.LcBlock64{a0, a1} == L.LcBlock64{_, U32.xor(U32.xor(a1, b1), b1)} : L.LcBlock64}
      %u32_xx(a1, b1) : {L.LcBlock64{a0, a1} == L.LcBlock64{a0, _} : L.LcBlock64}
      {==}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/PROOF.bend&name=u32_xx
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-crypto@0.1.0.0/inst_lc.bend&name=CrBlk64.xor
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-legacy-ciphers@0.1.0.0/legacy_ciphers.bend&name=LcBlock64