def lcblock64_xx

bend-osdev-crypto@0.1.0.0 · PROOF.bend:270

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

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