def cam_fl_step

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

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
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

334def cam_fl_step(a: L.LcBlock64, b: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamFl{a, b}, C.cam.op(C.LcCamFl{a, b}, s)) : M.CmBlock}:
335  match a b s:
336    case L.LcBlock64{+a0, +a1} L.LcBlock64{+b0, +b1} M.CmBlock{+s0, +s1, +s2, +s3}:
337      %cam_fl_inv(L.LcBlock64{s0, s1}, L.LcBlock64{a0, a1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{C.cam.hi(_), C.cam.lo(_), C.cam.hi(C.cam.fl(C.cam.flinv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1})), C.cam.lo(C.cam.fl(C.cam.flinv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}), L.LcBlock64{b0, b1}))} : M.CmBlock}
338      %cam_flinv_inv(L.LcBlock64{s2, s3}, L.LcBlock64{b0, b1}) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, s1, C.cam.hi(_), C.cam.lo(_)} : M.CmBlock}
339      {==}