def cam_fl_inv

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:287

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/camellia.bend as C

287def cam_fl_inv(x: L.LcBlock64, k: L.LcBlock64) -> {x == C.cam.flinv(C.cam.fl(x, k), k) : L.LcBlock64}:
288  match x k:
289    case L.LcBlock64{+x1, +x2} L.LcBlock64{+k1, +k2}:
290      %u32_xx(x1, U32.or(U32.xor(x2, L.lc.rotl(U32.and(x1, k1), 1n)), k2)) : {L.LcBlock64{x1, x2} == L.LcBlock64{_, U32.xor(U32.xor(x2, L.lc.rotl(U32.and(x1, k1), 1n)), L.lc.rotl(U32.and(_, k1), 1n))} : L.LcBlock64}
291      %u32_xx(x2, L.lc.rotl(U32.and(x1, k1), 1n)) : {L.LcBlock64{x1, x2} == L.LcBlock64{x1, _} : L.LcBlock64}
292      {==}