def cam_flinv_inv

bend-osdev-camellia@0.1.0.0 · PROOF.bend:29

import Base
import bend-osdev-cipher-core@0.1.0.0/cipher_core.bend as L
import bend-osdev-cipher-core@0.1.0.0/LAWS.bend as CoreL
import bend-osdev-camellia@0.1.0.0/camellia.bend as C

29def cam_flinv_inv(y: L.LcBlock64, k: L.LcBlock64) -> {y == C.cam.fl(C.cam.flinv(y, k), k) : L.LcBlock64}:
30  match y k:
31    case L.LcBlock64{+y1, +y2} L.LcBlock64{+k1, +k2}:
32      %CoreL.u32_xor_cancel(y2, L.lc.rotl(U32.and(U32.xor(y1, U32.or(y2, k2)), k1), 1n)) : {L.LcBlock64{y1, y2} == L.LcBlock64{U32.xor(U32.xor(y1, U32.or(y2, k2)), U32.or(_, k2)), _} : L.LcBlock64}
33      %CoreL.u32_xor_cancel(y1, U32.or(y2, k2)) : {L.LcBlock64{y1, y2} == L.LcBlock64{_, y2} : L.LcBlock64}
34      {==}