def cam_f2

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

import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
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

55def cam_f2(+t: C.LcCamTabs, +k: L.LcBlock64, s: M.CmBlock) -> {s == C.cam.unop(C.LcCamF2{t, k}, C.cam.op(C.LcCamF2{t, k}, s)) : M.CmBlock}:
56  match s:
57    case M.CmBlock{+s0, +s1, +s2, +s3}:
58      %CoreL.u32_xor_cancel(s0, C.cam.hi(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{_, U32.xor(U32.xor(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))), s2, s3} : M.CmBlock}
59      %CoreL.u32_xor_cancel(s1, C.cam.lo(C.cam.f(t, L.LcBlock64{s2, s3}, k))) : {M.CmBlock{s0, s1, s2, s3} == M.CmBlock{s0, _, s2, s3} : M.CmBlock}
60      {==}