--- name: formally-verify description: >- Guides formal verification of algorithms, data structures, and properties in the ComposeLife project using Lean 4 and Mathlib. Covers mathematical specification, equivalence reduction, metric-based completeness, invariant-based soundness, timeout avoidance, Lean modularization, C/Kotlin FFI bridge interop, and verification checks. --- # Formally Verify Skill Use this skill when formally verifying an algorithm, data structure, or mathematical property in the **ComposeLife** codebase using Lean 4 and Mathlib. The repository pairs Kotlin Multiplatform implementations with formal Lean 4 models, connected via C FFI bridges (and Kotlin/Native cinterop) for runtime validation and differential conformance testing. --- ## 🎯 Verification Criteria (Definition of Done) A verification task is only complete when: 1. **The Target Theorem is Proven in its Unmodified Form**: The master theorem statement matches the specification without introducing artificial preconditions or weakening the theorem's guarantees. 2. **Zero `sorry`s**: No `sorry`s anywhere in tracked project files. 3. **Zero Custom Axioms**: The theorem must depend strictly on the standard Lean 4 core axioms: ```lean [propext, Classical.choice, Quot.sound] ``` No custom `axiom` declarations or unverified assumptions. 4. **Clean Compilation**: `lake build :static` succeeds with **0 warnings and 0 errors**. 5. **Differential & Conformance Tests Pass**: All Kotlin/Native bridge tests and randomized fuzz tests pass cleanly via Gradle (`./gradlew ::check`). --- ## 🏛️ Architecture & Workflow Formal verification follows a 6-phase lifecycle: ```mermaid graph TD A["Phase 1: Mathematical Specification vs Executable Model"] --> B["Phase 2: Master Theorem & Equivalence Reduction"] B --> C1["Phase 3: Completeness / Reachability (Metric Progress)"] B --> C2["Phase 4: Soundness / Invariant Preservation (Structural Candidates)"] C1 --> D["Phase 5: Submodule Modularization & DAG Architecture"] C2 --> D D --> E["Phase 6: C / Kotlin FFI & Differential Testing"] E --> F["Phase 7: Final Audit (Axioms, Sorries, Checks)"] ``` --- ## 📋 Step-by-Step Guide ### Phase 1: Mathematical Specification vs Executable Model 1. **Define the Ground Truth Specification**: - Model the mathematical truth declaratively (e.g. relations, set comprehension, inductive predicates, or closed-form expressions). - Use exact, uncompromised mathematical types (such as `Nat`, `Int`, `Rat`, or inductive structures) rather than lossy representations to avoid rounding errors and floating-point ambiguity. 2. **Define the Executable Algorithmic Model**: - Model the algorithm as it executes in practice (e.g. step functions, recursors, loop iterations, or state machines). - Ensure the algorithmic model matches the design intended for production code in Kotlin. --- ### Phase 2: Master Theorem & Equivalence Reduction 1. **State the Master Theorem**: ```lean theorem algorithm_correctness (inputs : InputType) : algorithmExecutable inputs ↔ SpecificationPredicate inputs ``` 2. **Prove a Reduction Lemma Early**: - Factor out trivial edge cases (e.g. empty collections, identity inputs, degenerate bounds) into base lemmas. - Separate the equivalence into two independent directions: - **Completeness (No False Negatives)**: Every element or state satisfying the specification is produced or reached by the algorithm. - **Soundness (No False Positives)**: Every element or state produced by the algorithm satisfies the specification. --- ### Phase 3: Proving Completeness (Progress & Reachability) 1. **Construct a Strictly Monotonic Progress Metric**: - When an algorithm iterates or steps toward a goal state, avoid inducting directly on complex multidimensional structures. - Construct a non-negative progress metric $D : \text{State} \to \mathbb{N}$ that measures distance to completion or target state. 2. **Prove Abstract Reachability**: - Prove that for every non-terminal state $s$ with $D(s) > 0$: - The step does not prematurely terminate. - The next state either achieves the goal or strictly decreases the metric: $D(\text{step}(s)) < D(s)$. 3. **Bound the Fuel / Iteration Budget**: - Prove by well-founded induction on $D(s)$ (or natural number induction on fuel) that any initial budget $\text{fuel} \ge D(s_0)$ guarantees reaching the target state without skipping. --- ### Phase 4: Proving Soundness & Avoiding Timeouts 1. **Formulate Inductive Invariants**: - Define an invariant predicate $I(s)$ that holds on the initial state $s_0$ and implies the desired postcondition at termination. - Prove step preservation: $I(s) \implies I(\text{step}(s))$. 2. **Prevent Combinatorial State Explosion (Deterministic Timeouts)**: > [!CAUTION] > Never unfold recursive functions with complex nested conditionals directly inside arithmetic goals or heavy automation (`simp`, `split_ifs`, `whnf`). This causes exponential branch blowup and deterministic timeouts. 3. **The Structural Candidate Lemma Pattern**: - Encapsulate the finite transition possibilities of the step function into a simple membership lemma: ```lean theorem step_candidates (s : State) : step s ∈ [candidate₁ s, candidate₂ s, ..., candidateₖ s] ``` - Case split on the finite list of candidates rather than destructing internal condition trees. 4. **Domain Partitioning**: - When conditions involve directional signs or inequalities, partition the input domain into disjoint regions where sign variables are fixed. - In fixed-sign subdomains, denominators do not change sign, and linear arithmetic (`linarith`), normalization (`ring`), and positivity (`positivity`) tactics can resolve goals in constant time without branching. --- ### Phase 5: Submodule Modularization & Clean File Organization When a verification file exceeds 1,500–2,000 lines, split it into a clean Directed Acyclic Graph (DAG) of submodules: - **`Specification.lean` / `Types.lean`**: Domain types, predicates, and declarative specifications. - **`Step.lean` / `Model.lean`**: Executable transitions, structural candidate lemmas, and directional properties. - **`Completeness.lean`**: Progress metric definition, distance descent lemmas, and reachability theorems. - **`Soundness.lean`**: Invariant preservation across partitioned domains and soundness induction. - **`Properties.lean`**: High-level module importing submodules and stating the master correctness theorems. > [!IMPORTANT] > - Ensure **every `.lean` file** begins with the Apache 2.0 license header from `config/license.template`. > - Modularization enables Lake to compile submodules in parallel, cutting build times and preventing editor lockups. > - Remove all leftover exploratory duplicate theorems (e.g. `*_dup`). --- ### Phase 6: C / Kotlin FFI & Differential Conformance Testing 1. **Lossless Type Marshaling**: - Connect the Lean model to Kotlin via C ABI bindings. - When converting between Kotlin primitives (e.g. IEEE-754 floats) and exact mathematical models (e.g. dyadic rationals `Rat`): - Unpack binary representations faithfully (e.g. evaluating sign, exponent, and fraction bitfields) to preserve exact numerical values. - Never cast raw bit patterns directly into integer values. 2. **Memory & Runtime Safety**: - Ensure Lean runtime initialization (`lean_initialize_runtime_module`) is called once. - Correctly manage Lean reference counting (`lean_dec_ref`, `lean_alloc_array`, `lean_box_*`, `lean_unbox_*`). 3. **Differential Fuzz Testing**: - In Kotlin tests, write randomized property-based tests running hundreds of iterations comparing Kotlin implementations against the Lean oracle: ```kotlin assertEquals(oracle.compute(inputs), kotlinImplementation(inputs)) ``` 4. **Gradle Native Cache Invalidation**: - When modifying C or Lean native static libraries, rerun native test binaries with `--no-build-cache --rerun-tasks` to ensure the linker doesn't reuse stale executables. --- ## 🤖 Multi-Agent Proving Architecture & Cadence Management For non-trivial formal verification tasks, structuring the proving process across specialized subagents with strict cadences and automated supervisory audits ensures steady progress and prevents stalling: ```mermaid graph TD User["User Request"] --> Main["Main Agent (Supervisor & Auditor)"] Main -->|Schedules| Cron["4-Min Recurring Check-In (schedule cron)"] Main -->|Spawns & Oversees| PM["Proof Manager (Architect)"] PM -->|Delegates 2-3 min lemmas| LP["Lemma Prover (Tactical)"] LP -->|Proves & commits lemma| Code["Lean 4 Codebase"] Code -->|lake build check| PM Cron -.->|Wakes up & audits| Main Main -->|Anti-cheat audit: 0 sorry, 0 axiom, unweakened signatures| Code ``` ### Agent Roles & Separation of Concerns 1. **Main Agent (Supervisor & Anti-Cheat Auditor)**: - **High-level control**: Maintains the master plan, initiates the subagent team, and delivers the final walkthrough to the user. - **Recurring audit cron**: Schedules a 4-minute recurring background check-in (`schedule` with `CronExpression: "*/4 * * * *"`, `IsDaemon: false`). - **Anti-cheat enforcement**: - Audits for 0 `sorry`s, 0 `admit`s, and 0 custom `axiom`s. - Strictly verifies that **target theorem signatures are not weakened** (e.g. ensuring subagents do not add intermediate conditions or invariants as unproven hypotheses on the master theorem instead of discharging them). - Confirms `#print axioms` strictly reports `[propext, Classical.choice, Quot.sound]`. - Validates full builds via `lake build :static` and `./gradlew ::check`. 2. **`proof_manager` (Proof Architect & Manager)**: - **Architecture & DAG**: Defines the roadmap of intermediate lemmas across domain submodules. - **Delegation**: Supplies `lemma_prover` with precise lemma signatures, target files, and tactical hints. - **Cadence management**: Enforces that `lemma_prover` must make progress on a ~3-minute cadence. If `lemma_prover` stalls or takes longer than 3 minutes on a single lemma, `proof_manager` immediately decomposes the lemma into smaller sub-lemmas. - **Assembly**: Chains proven lemmas together into higher-level theorems and verifies static builds. 3. **`lemma_prover` (Tactical Lemma Prover)**: - **Single focus**: Proves isolated, tightly scoped lemmas and integrates them directly into the `.lean` files. - **Tactic specialization**: Applies local solvers (`omega`, `linarith`, `ring`, `aesop`, `positivity`, `split_ifs`) without needing to understand the global architectural DAG. ### Operational Rules - **The 3-Minute Progress Rule**: A lemma that takes longer than 3 minutes to discharge is almost always too large or missing a key structural helper (e.g., candidate set enumeration, monotonicity lemma, or domain partition). Decompose early. - **The 4-Minute Audit Loop**: The Main Agent uses background cron triggers to verify that active subagents are making observable git changes, compile builds cleanly, and respect all anti-cheat rules. - **Strict Signature Invariance**: Intermediate hypotheses (such as step sign equality or transition classifications) must be discharged as lemmas from the input preconditions, never hoisted into the master theorem's signature. --- ## 🔍 Verification Commands & Audit Checklist Execute these exact verification checks before concluding any formal verification task: ```bash # 1. Clean Lake build (must compile with 0 warnings, 0 errors) cd lake clean && lake build :static # 2. Axioms verification (must only report [propext, Classical.choice, Quot.sound]) lake env lean --run - << 'EOF' import .Properties #print axioms . EOF # 3. Check for any sorrys in the codebase (must return 0 results) grep -rn "sorry" / # 4. Check for any custom axioms (must return 0 results) grep -rn "axiom" / # 5. Run full Gradle checks, conformance tests, and Detekt inspections cd ./gradlew ::check --no-build-cache ``` --- ## 💡 Practical Proof Tactics Reference | Tactic | Best Used For | | :--- | :--- | | `omega` | Natural number and integer linear arithmetic, modulo arithmetic, Presburger constraints, fuel bounds. | | `linarith` | Linear real, rational, or ordered field inequalities with hypotheses. | | `ring` | Ring equalities on algebraic structures (expanding polynomials, verifying common denominators). | | `positivity` | Automatically discharging strict positivity ($> 0$), non-negativity ($\ge 0$), or non-zero ($\ne 0$) goals. | | `rcases` / `obtain` | Destructing existential hypotheses (`∃ x, ...`) and conjunctions without deeply nested indentation. | | `split_ifs with h` | Splitting conditional expressions while retaining the condition hypothesis $h$. | | `aesop` | Automated proof search for propositional logic, set memberships, and basic structural goals. |