CLAUDE.md

Project Overview

Lambda Compiler Kit (LCK) — Lean 4 libraries for verified compiler infrastructure. Lean v4.26.0, Lake, Mathlib v4.26.0. See README.md for usage, examples, and project structure.

Project Structure

Lck.lean          -- imports all library modules
Lck/
  Basic.lean      -- shared utilities
  Regex/          -- regex engine (Thompson NFA)
  Regex.lean      -- regex module imports
cli/              -- CLI tools (lck-grep)
test/             -- LSpec test suites
lakefile.toml     -- Lake config (deps: mathlib, LSpec)

New libraries: create Lck/<LibName>/, add Lck/<LibName>.lean, import in Lck.lean.

Development Notes

• New modules go in Lck/ and must be imported in Lck.lean
• First build fetches Mathlib (~5-10 min). lean-toolchain pins the exact Lean version.
• Build: lake build | Test: lake build test && lake exe test | Lint: lake lint
• Lint single file: lake lint Lck.Regex.Parser
• Build with warnings-as-errors: lake build --wfail
• Update dependencies: lake update | Clean build artifacts: lake clean
• Simple tests: example (see Assertions below). Complex/property-based: LSpec in test/TestLib/.

Verification Work

Proof Discipline

A theorem is either proven or NOT proven. No middle ground.

Completion criteria: zero sorries in proof body AND all dependencies, no non-standard axioms.

Language rules:

• Say "draft structure" or "proof in progress at line X" for incomplete work
• Never say "proven (modulo sorries)" or "structure is in place"

Assertions: example > #check > #eval

• example ... := by decide — preferred. Kernel-verified, proves the value is correct at compile time.
• example ... := by native_decide — fallback when decide times out (e.g., NFA compilation). Only in example statements, never in theorems. Requires set_option linter.style.nativeDecide false.
• #check (expr : Bool) — only type-checks, does NOT verify the value. Avoid in library/spec files.
• #eval — runtime evaluation, not a proof. Use only for debugging/exploration.

Proof Workflow

To see goals, the sorry must be removed first (Lean only warns on sorry, doesn't show goals). Loop: remove sorry → check goal via MCP → apply tactic → repeat until no sorries remain.

Work depth-first (one proof at a time), bottom-up (leaf lemmas first). Strategies: direct proof, contradiction, induction, case analysis, restructure statement. Escalation: 3+ approaches → restructure → search mathlib → ASK user with options.

Termination — Total Functions Only

Never use partial, fuel parameters, or bound counters. Design code so Lean's termination checker accepts it automatically — the code should speak for itself.

Structural recursion is plan A. Techniques:

• Structural recursion on inductives (lists, trees) — always accepted automatically
• CPS / continuation-passing — thread a structurally smaller input through each recursive call
• Subslice patterns — recursive calls on a strict subslice of the input (e.g., input[i+1:])

-- Good: structural recursion on remaining input, zero tactics needed
def parseDigits (input : List Char) : List Char × List Char :=
  match input with
  | c :: rest =>
    if c.isDigit then
      let (digits, remaining) := parseDigits rest
      (c :: digits, remaining)
    else ([], c :: rest)
  | [] => ([], [])

Separate tokenization from parsing. Tokenizers consume one character at a time unconditionally (structurally decreasing input). Parsers are typically LL(1) — consume one token, peek at most one ahead — so token lists decrease structurally. This separation makes termination obvious and correctness proofs modular.

decreasing_by is plan B — a code smell. It means the code doesn't make its termination obvious. If unavoidable, the proof should be short (a lemma + omega) and accompanied by a comment explaining why structural recursion isn't possible. For parsers especially — a well-understood discipline and a security boundary — there's strong motive to be strict and good reason to believe structural termination is achievable.

Smells that signal architecture problems:

• decreasing_by with multi-step advancing lemmas → restructure to make progress obvious
• Auxiliary lemmas about "what variables mean" → the types don't carry enough information
• partial as a "temporary" measure → it never gets removed