Vero Python Pitfalls

Python → Lean 4 — Known Pitfalls

Benchmark-quality baseline

The Lean benchmark is allowed to be smaller than the Python repo, but it must not silently change the selected APIs' observable semantics. Before compressing scaffold/context, confirm that the LLM still has enough information to reconstruct:

• success and failure paths;
• mutation/aliasing effects that become input-output relations in Lean;
• boundary behavior for empty inputs, malformed inputs, overflow, and exceptional cases;
• cross-API laws such as encode/decode or push/pop round trips.

If a source behavior is intentionally omitted, record it as a curation decision instead of leaving a weak spec that makes the omission invisible.

Integer division

Python a // b is floor division (rounds toward −∞). Lean's Int.div// is truncated (rounds toward 0). They differ for negatives.

If the Python source only ever uses non-negative operands, Int.div is fine — but document the assumption.

range(...) semantics

Python range(a, b) is [a, a+1, ..., b-1]. Use List.range' (start, length) — not List.range (which is [0, ..., n-1]).

range(2, 5)   # [2, 3, 4]

→

List.range' 2 3   -- [2, 3, 4]; length = b - a

For descending or step-N ranges, write a recursive helper.

Mutability + aliasing

Python lists / dicts are mutable. Lean has no in-place mutation in the pure subset. The curator-given translation:

• lst.append(x) → lst ++ [x] (new list)
• dct[k] = v → dct.insert k v returning a new map
• Python's reliance on identity (lst is other_lst) cannot be expressed; flag with @review human.

If the Python code relies on mutating a parameter and reading the mutation in the caller, the spec almost certainly needs reformulation as input → output. Discuss with the curator.

For buffer-writing APIs, do not replace "writes prefix and preserves suffix" with "returns some new list" unless the spec explicitly captures the old buffer, written length, prefix, suffix, and failure unchanged behavior. This is the same failure mode as Json's SerializeInto contract drift.

None vs Option

Python's None is the only inhabitant of NoneType. Lean's none : Option α requires the type α to be inferred or annotated. Translation:

def lookup(k: int) -> int | None:
    return self.dict.get(k)

→

def lookup (k : Int) (s : State) : Option Int := s.dict.find? k

Avoid Option Unit for "side-effect succeeded?" — use Bool or a dedicated Result enum.

Float

Lean's Float is IEEE 754 double, same as Python's. But: Float does not have decidable equality and arithmetic isn't pure (NaN, ±0). Heavily prefer Int if the Python contract allows integer reasoning.

If a spec must talk about Float, name the floating-point assumption explicitly in spec_helper_* and flag with @review human.

String iteration

Python for c in s iterates Unicode code points. Lean's String API has String.toList : String → List Char — use that, not String.length for character counts (which counts UTF-8 bytes in some configurations).

dict ordering

Python 3.7+ guarantees insertion order on dict. Lean's Std.HashMap does not. If insertion order is observable in the spec, translate to AssocList Key Value (preserves order, less efficient — but specs care more).

Recursion depth

Python tolerates moderate recursion via tail-call-stack tricks; Lean prefers partial def or a structurally-decreasing recursive definition. Long-running iterative algorithms in Python often need refactoring as Nat.rec / List.foldl in Lean.

print / input / file I/O

These APIs have no place in the benchmark. Skip them and add an @review human annotation in the manifest noting the omission. If a spec actually depends on a side effect (rare in benchmark code), discuss with the curator.