[ecto]

What

Loon can now state laws, check proofs of them, and has begun proving its own kernel sound.

The kernel and loon prove (crates/loon-lang/src/verify/)

• [law name [params] [= lhs rhs]], optionally :given [[= a b] ...] for conditional laws. [proof name steps...] with unfold, rewrite (:rev, :at N, :in h), induction (one hypothesis per recursive field), cases on variables or on any total-fn term (:as h), sym, refl, admit (taints). Mutual induction via :mutual. Constructor injectivity on hypotheses; ex falso on distinct constructors. Obligations from conditional laws are discharged by normalization, an in-scope hypothesis, or a settled law.
• Goals close by evaluating total definitions and canonicalizing + and any operator declared [ac op assoc comm :unit u law], active only once those laws are kernel-proven and shape-checked.
• loon prove DIR: bounded falsification first (generic ADT enumeration on the EIR VM, smallest counterexample, vacuous inputs never prove), then the kernel in dependency order, a canary check, and a text or --json report with the blake3 hash of the frozen defs. An unsound run scores 0 and exits 2.

Div effect (check/termination.rs): structural recursion is inferred total, including mutually recursive groups with a shared measure; everything else carries Div. E0405 when a fn annotated #{} may diverge. Not a capability, never grantable.

Corpora

• verify/: list laws, Hutton compiler correctness, Peano arithmetic through mul-assoc, Gauss and sum-of-odds, conditional laws such as left-cancellation of append. 27 proven.
• verify/meta/: the kernel's own term language, substitution, non-linear first-order matching, and a fuel-indexed leftmost-outermost evaluator. Proven: substitution composition, match soundness (apply-match p t = t), fuel composition and monotonicity. 32 proven.
• Both corpora sound, nothing admitted, 4 deliberately false laws each falsified.

Why

docs/plans/2026-10-28-verify-autoresearch.md (design, grammar, the overnight loop) and docs/plans/2026-10-28-self-verifying-kernel.md (the 7-rung ladder; rungs 0-3 are in this PR). The goal is a verification story that fits invisible types: no dependent types, no tactic language, a kernel an auditor can read, proofs as data an agent loop can search for. The ladder's end is the kernel's soundness proof run through the kernel itself.

Reviewer notes

• Trust surface: substitution, one-step unfolding, first-order matching (modulo commutativity for declared AC ops), constructor-match normalization, AC canonicalization, the induction scheme (structural, mutual, strong-on-size for mutual groups), obligation discharge, and verify/infer.rs, a small HM used for law param and scrutinee types because the language checker does not generalize top-level fns. A wrong type there would make a cases split unsound; it fails closed. Each of these is either modeled in verify/meta/ or listed as an assumption in the plan.
• Builtins like reverse/map have no Loon body, so they are bridged by bounded-only laws in verify/builtins.oo, reported as bounded, never proven.
• Two existing effect-row tests changed fixtures from #{} to #{Div} because their recursion is genuinely non-structural.
• Found and left alone, outside scope: the VM does not bind variables in nested constructor patterns; the checker shares one Cons instantiation per function; the ownership checker flags a variable used in two match arms.
• cargo test --workspace: 920 pass. Release-build loon prove takes 3 s on verify/ and 8 s on verify/meta/.

🤖 Generated with Claude Code