Lean4 Ic3

---
name: lean4-ic3
description: IC3/PDR-style inductive invariant inference — find CTIs, dispatch generalizer, grow a structure-based invariant until inductive
user_invocable: true
---

# Lean4 IC3

Property-directed reachability for Lean4 invariant proofs. Drives a CEGAR loop over
a structure-based invariant: probe each action, extract counterexamples-to-induction
(CTIs) from residual goals, dispatch a generalizer subagent to propose new conjuncts,
insert them as non-breaking structure fields, and iterate until inductive.

**Prerequisite:** The invariant MUST be a `structure`, not a flat `∧`. Adding fields
is the whole point — it must be non-breaking for existing field accessors.

## Usage

/lean4-ic3 File.lean::InvName --spec=specName --safety=safetyLemma /lean4-ic3 ... --max-iters=8 /lean4-ic3 ... --decide-cti=auto --check-n=3 /lean4-ic3 ... --generalizer=manual # default on first run /lean4-ic3 ... --generalizer=agent # dispatch ic3-generalizer

## Inputs

| Arg | Required | Default | Description |
|-----|----------|---------|-------------|
| target | Yes | — | `File.lean::StructureName` |
| --spec | Yes | — | Spec value used with `action_cases` (e.g. `tlMessages`) |
| --safety | Yes | — | Safety lemma the invariant must imply |
| --init-lemma | No | `init_preserves_inv` | Base-case lemma name |
| --step-lemma | No | `step_preserves_inv` | Inductive-step lemma name |
| --max-iters | No | 8 | Max new conjuncts added before giving up |
| --generalizer | No | manual | `manual` (prompt user) or `agent` (`ic3-generalizer`) |
| --decide-cti | No | auto | `auto` / `off` / `always` — concretize CTI via decide at small n |
| --check-n | No | 3 | n for decide-based CTI concretization |

Refuse to start if the target invariant is not a `structure` declaration — flat
conjunctions make non-breaking insertion impossible. Tell the user to refactor
first. (See CLAUDE.md "Invariant Composition: Use Structures, Not Flat Conjunctions".)

## Actions

### Phase 0 — Baseline snapshot

1. `lean_diagnostic_messages(file)` → record sorry count + diagnostic baseline.
2. `lean_file_outline(file)` → discover invariant structure fields and action names.
3. Verify `init-lemma` and `step-lemma` exist (may contain `sorry`; that is fine).
4. Snapshot the invariant structure declaration verbatim. This is the rollback point.

On any regression (later phase increases sorry count beyond baseline or adds new
diagnostics), revert to this snapshot and abort with a report.

### Phase 1 — Base case

Dispatch the base-case cascade at `init-lemma`:

intro s h_init constructor <;> first | rfl | simp [init_defs] | decide | grind

via `lean_multi_attempt`. For any field that fails:

1. `lean_goal` at the failing subgoal → the **Init CTI**.
2. Package hypotheses + negated goal and hand to Phase 3 (Generalize) with
   `cti_kind = init`.

If all fields close: move to Phase 2.

### Phase 2 — Inductive step (per action)

The core of IC3 in Lean. This phase runs a **mandatory reduction cascade**
before any CTI is extracted, and applies a **strict dispatch gate** before
invoking the generalizer. The cascade plays the role that symbolic simulation
plays in hardware IC3: it turns a monolithic preservation obligation into
localized leaf goals that can actually be generalized.

**Why the cascade matters.** In hardware PDR, SAT gives you a concrete
counterexample cube — a specific assignment to pre-state variables that
witnesses the failure. In Lean, there is no built-in symbolic executor: a
bare `sorry` at a preservation lemma leaves you with the *whole* property as
a residual goal, which contains no instantiation, no pre-state witness, no
localizable facts. The generalizer cannot do anything with that. The cascade
below is Lean's substitute for SAT: it unfolds, case-splits, and normalizes
until either the goal closes or the remaining residuals are small leaves
about specific pre-state projections.

#### Phase 2a — Reduction cascade (mandatory, per action)

1. Open `step-lemma`, run `action_cases h with <spec>` (Leslie gadget).
2. For each action case `a`, run the cascade in order. Stop at the first
   level that yields a closed goal (move to next field). If ALL levels fail,
   collect residuals for the dispatch gate.
   - **L0 — Unfold & introduce.** `intro`s on quantifiers, `refine
     ⟨?_, …, ?_⟩` to push inside the target structure, `obtain ⟨…⟩ := …`
     to destructure witnesses in hypotheses.
   - **L1 — Normalize.** `simp only [action_simp, setFn_same, setFn_ne,
     <frame lemmas for a>]`. Project the post-state delta to its minimal
     form so frame facts become syntactic.
   - **L2 — Frame close.** For each invariant field `C` whose footprint is
     disjoint from action `a`'s write set (from `#gen_frame_lemmas`-derived
     metadata), try `exact hinv.C`. If the field is partially disjoint
     (e.g., `setFn f i v` updates only at `i`), `by_cases` on the witness
     index and close the `≠ i` side with `hinv.C`.
   - **L3 — Existential witness.** For goals of the form `∃ b w, P`, try
     `obtain ⟨b, w, hP⟩ := hinv.<candidate field>; exact ⟨b, w, hP⟩` for
     each existing field whose conclusion is of similar shape. Use
     `lean_multi_attempt` to probe candidates.
   - **L4 — Closure automation.** `lean_multi_attempt` with
     `["omega", "grind", "decide", "simp [hinv]"]` — the standard tail.
     Budget: ≤5 seconds per goal.
   - **L5 — State-search.** `lean_state_search` on the residual goal. If
     one of the returned lemmas closes the goal via `lean_multi_attempt`,
     accept it.
3. Any leaf goal surviving L0–L5 becomes a **candidate CTI**. Record the
   `lean_goal` output verbatim, the action, and the cascade path taken.

#### Phase 2b — Dispatch gate (strict)

For each candidate CTI, check ALL of the following. If ANY check fails, do
NOT call the generalizer — instead, route per the "non-dispatchable"
actions below.

| Gate | Check | Failure route |
|------|-------|---------------|
| *