feat(interval): emit proofs from retained branch trees

HexInterval/Experiment/BranchProof.lean

@@ -0,0 +1,139 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+
+module
+
+public import HexInterval.Experiment.BranchTree
+public import HexInterval.Experiment.ProofFrontend
+
+@[expose] public section
+
+/-!
+# Generic branch-tree proof emission
+
+This frontend folds a settled retained branch tree from its leaves to its root.
+It knows no fact representation, mathematical function, proof schema, or
+branch policy.  Client callbacks replay an exact closed leaf and join an exact
+split; the generic fold validates tree shape, total coverage, and the final
+Lean type.
+
+Runtime tree data remains untrusted.  Every callback result is an ordinary
+`Expr`, and later callback applications plus the final type check force the
+kernel-facing theorem structure.  Pending, blocked, failed, unreachable,
+duplicated, or cyclic nodes are rejected before a root term is returned.
+-/
+
+namespace Hex.Interval.Experiment.BranchProof
+
+open Lean Meta
+open BranchTree
+
+/-- Structural traversal resources, independent of search resources already
+charged by `BranchTree`. -/
+structure Limits where
+  maxNodes : Nat
+  maxDepth : Nat
+  deriving DecidableEq, Repr
+
+/-- Proof-producing operations for one semantics adapter and package set. -/
+structure Emitter (Fact PolicyState : Type) where
+  leaf : BranchTree.Leaf Fact PolicyState ->
+    TargetRun.Result Fact PolicyState -> MetaM Expr
+  split : BranchTree.Leaf Fact PolicyState ->
+    TargetRun.Result Fact PolicyState -> BranchStart.Children Fact ->
+    Expr -> Expr -> MetaM Expr
+
+structure Output (Fact PolicyState : Type) where
+  proof : Expr
+  seen : List Nat
+  source : BranchTree.Leaf Fact PolicyState
+
+def overlap (left right : List Nat) : Bool :=
+  left.any right.contains
+
+def sameInput [DecidableEq Fact]
+    (left right : SemanticReplay.CheckerInput Fact) : Bool :=
+  left.baseProgram == right.baseProgram &&
+    left.initialFacts == right.initialFacts && left.target == right.target
+
+def sameChild [DecidableEq Fact]
+    (scope : Propagator.Policy.ScopeId) (depth : Nat)
+    (input : SemanticReplay.CheckerInput Fact)
+    (source : BranchTree.Leaf Fact PolicyState) : Bool :=
+  source.scope == scope && source.depth == depth && sameInput source.input input
+
+partial def emitAt [DecidableEq Fact]
+    (limits : Limits) (emitter : Emitter Fact PolicyState)
+    (tree : BranchTree.State Fact PolicyState) (depth : Nat)
+    (id : BranchTree.TreeId) : MetaM (Output Fact PolicyState) := do
+  if depth > limits.maxDepth then
+    throwError "interval branch proof: traversal depth exhausted"
+  let some node := tree.nodes[id.index]?
+    | throwError "interval branch proof: missing node {id.index}"
+  match node with
+  | .pending _ =>
+      throwError "interval branch proof: pending node {id.index} is not closed"
+  | .leaf source ending =>
+      match ending with
+      | .result run =>
+          unless BranchStart.sameInput source.scope source.input run do
+            throwError "interval branch proof: leaf input does not match its run"
+          pure
+            { proof := ← emitter.leaf source run
+              seen := [id.index]
+              source }
+      | .blocked _ _ =>
+          throwError "interval branch proof: blocked node {id.index} is not closed"
+      | .startError _ =>
+          throwError "interval branch proof: failed node {id.index} is not closed"
+  | .split source run children left right =>
+      if left.index <= id.index || right.index <= id.index then
+        throwError "interval branch proof: child does not follow its parent"
+      if left.index == right.index then
+        throwError "interval branch proof: split reuses one child"
+      let leftOutput ← emitAt limits emitter tree (depth + 1) left
+      let rightOutput ← emitAt limits emitter tree (depth + 1) right
+      unless BranchStart.sameInput source.scope source.input run do
+        throwError "interval branch proof: split input does not match its run"
+      unless sameInput source.input children.parent do
+        throwError "interval branch proof: split parent input changed"
+      unless sameChild children.leftScope children.depth children.left
+          leftOutput.source do
+        throwError "interval branch proof: left child input changed"
+      unless sameChild children.rightScope children.depth children.right
+          rightOutput.source do
+        throwError "interval branch proof: right child input changed"
+      if overlap leftOutput.seen rightOutput.seen then
+        throwError "interval branch proof: subtrees share a node"
+      let proof ← emitter.split source run children
+        leftOutput.proof rightOutput.proof
+      pure
+        { proof
+          seen := id.index :: (leftOutput.seen ++ rightOutput.seen)
+          source }
+
+/-- Emit one root theorem only from a settled, totally covered tree.
+
+`expected` is normally the current goal type.  The final check is deliberately
+inside the generic frontend, so even a single-leaf tree cannot return an
+unrelated callback term. -/
+def emit [DecidableEq Fact] (limits : Limits) (emitter : Emitter Fact PolicyState)
+    (tree : BranchTree.State Fact PolicyState) (expected : Expr) : MetaM Expr := do
+  if !tree.frontier.isEmpty then
+    throwError "interval branch proof: tree still has pending work"
+  if tree.nodes.isEmpty then
+    throwError "interval branch proof: tree has no root"
+  if tree.nodes.size > limits.maxNodes then
+    throwError "interval branch proof: node budget exhausted"
+  let output ← emitAt limits emitter tree 0 { index := 0 }
+  if output.seen.length != tree.nodes.size then
+    throwError "interval branch proof: tree contains unreachable nodes"
+  let proof ← instantiateMVars output.proof
+  unless ← isDefEq (← inferType proof) expected do
+    throwError "interval branch proof: emitted root has the wrong type"
+  pure proof
+
+end Hex.Interval.Experiment.BranchProof

HexInterval/SPEC/hex-interval.md

@@ -1711,13 +1711,32 @@ runs the arbitrary exponential propagator in each, and retains two target
 leaves. Separate guards show that one global step leaves both children pending,
 and that zero split or one-leaf budgets retain an explicitly blocked root.
 
-This runtime tree contains no proof evidence. The existing two-child proof
-canary separately demonstrates how exact retained child runs can be replayed
-and joined, but the manager does not yet emit that term. The proof-tree layer
-must emit a theorem only when every coverage child is closed by replay or a
-checked refutation. For best-bound mode, unfinished leaves must contribute
-their inherited parent fact to the global hull; they never inherit a tighter
-sibling fact.
+This runtime tree contains no proof evidence. The separate generic
+`BranchProof` frontend now folds a settled retained tree bottom-up. It first
+binds every leaf and split result back to its exact scope, base program, and
+initial fact array. Each child is checked against the exact child input stored
+by its parent, including that input's target. Pending, blocked, failed,
+dangling, shared, cyclic, and unreachable nodes are rejected. Client callbacks
+then replay each closed leaf and apply each package-owned split join; the final
+emitted expression must have the requested Lean target type. A callback can
+therefore cause rejection or choose a different kernel-checkable proof, but
+tree data itself cannot become evidence.
+
+Every child admitted by a split's coverage theorem must eventually close by
+replaying a proof of its target or by deriving a package-checked refutation.
+A retained runtime result is not by itself a proof of closure: the leaf
+callback must turn it into the corresponding kernel-checked evidence before
+the bottom-up join can accept it.
+
+The distinct-assumption ReLU canary now runs through this generic path. Its
+retained root has two exact live target children; the leaf callback invokes the
+unchanged generic chronology emitter with the side-specific proof registry, and the
+split callback applies `replaySplit`. The resulting expression is assigned to
+an ordinary declaration and its axiom report is compile-checked. Separate
+negative tests reject the delivered step-limited partial tree, a fork whose
+two edges share one child, and an otherwise valid but unreachable extra node.
+For best-bound mode, unfinished leaves must contribute their inherited parent
+fact to the global hull; they never inherit a tighter sibling fact.
 
 Several operational choices deliberately remain experimental:
 
@@ -1754,8 +1773,7 @@ runtime and Mathlib semantic
 companion. Remaining acceptance tests include a theorem whose proof
 mathematically requires branching, a nested split, a child-local
 instantiation, a sibling-reference attack, a non-interior repeated split,
-per-leaf fuel exhaustion with no theorem emitted, and proof emission refusing
-the delivered step-limited partial tree.
+and per-leaf fuel exhaustion with no theorem emitted.
 
 ### Proof-producing frontend