Formally Verify

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 sorrys: No sorrys anywhere in tracked project files.
3. Zero Custom Axioms: The theorem must depend strictly on the standard Lean 4 core axioms:

   [propext, Classical.choice, Quot.sound]

   No custom axiom declarations or unverified assumptions.
4. Clean Compilation: lake build <Target>: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 :<module>:check).

🏛️ Architecture & Workflow

Formal verification follows a 6-phase lifecycle:

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:

   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:

     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.