santosomar/general-secure-coding-agent-skills/c-cpp-to-lean4-translator

C/C++ → Lean 4 Translator

Lean is for when you need a proof, not a check. Dafny asks an SMT solver "is this true?"; Lean asks you to construct the proof term. More work, more control, no timeouts.

When Lean over Dafny

The functional lift

Lean is purely functional. The translation path is: imperative C → functional model → proof about the model.

The state monad escape hatch

If the imperative structure is too tangled to lift functionally, use StateM:

def impStep : StateM (Array Int) Unit := do
  let a ← get
  if h : 0 < a.size then
    set (a.set ⟨0, h⟩ 42)
 
-- Reason about the result:
theorem impStep_sets_zero (a : Array Int) (h : 0 < a.size) :
  (impStep.run a).2.get ⟨0, h⟩ = 42 := by simp [impStep, StateT.run]

But prefer the functional lift — proofs over folds are easier than proofs over monadic runs.

Worked example

C:

// Count elements equal to target
size_t count(const int* a, size_t n, int target) {
    size_t c = 0;
    for (size_t i = 0; i < n; ++i)
        if (a[i] == target) ++c;
    return c;
}

Lean — functional lift:

def count (a : List Int) (target : Int) : Nat :=
  a.foldl (fun c x => if x = target then c + 1 else c) 0
 
-- Spec via List.countP from Mathlib
theorem count_eq_countP (a : List Int) (target : Int) :
    count a target = a.countP (· = target) := by
  induction a with
  | nil => rfl
  | cons x xs ih =>
    simp only [count, List.foldl_cons, List.countP_cons]
    split <;> simp [ih, count]

Notes:

• List instead of Array — easier induction. If you need Array for the performance story, prove on List and transport via Array.toList.
• The theorem connects our count to Mathlib's countP — once connected, all of Mathlib's lemmas about countP apply to us for free.
• size_t → Nat (unbounded). If we cared about SIZE_MAX, we'd add a separate bound theorem.

Proof patterns you'll need

Do not

• Do not translate to Lean when Dafny would verify automatically. Lean proofs are manual labor; only pay for what you need.
• Do not state the theorem as "equals the C code." State it as "satisfies this mathematical property." The C is an implementation; the theorem is about the spec.
• Do not fight Lean's termination checker with partial def. partial means "trust me" — you lose proofs-by-induction. Find the structural argument.
• Do not reinvent Mathlib. List.countP, List.Sorted, Nat.gcd — they exist, with lemma libraries. Connect to them.

Output format

## Functional model
<Lean def — the translated algorithm>
 
## Theorem
<what property this proves — connected to Mathlib where possible>
 
## Proof
<tactic script — or `sorry` placeholders with notes on what's left>
 
## Model fidelity
<where the Lean model diverges from the C: unbounded ints, List vs Array, etc.>