feat(interval): retain bounded branch trees

HexInterval/Experiment/BranchTree.lean

@@ -0,0 +1,259 @@
+/-
+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.BranchStart
+
+@[expose] public section
+
+/-!
+# Resource-bounded branch trees
+
+This experiment retains a complete runtime tree while repeatedly running
+ordinary target-directed sessions and expanding accepted split plans.  It is
+generic in the fact domain, executable packages, and external policy state.
+
+The tree is search data, not proof evidence.  In particular, a runtime
+contradiction leaf is not a proof of `False`, and a pair of target leaves is
+not a proof of their parent target.  The proof frontend must separately replay
+each retained leaf and join checked child evidence through a split schema.
+-/
+
+namespace Hex.Interval.Experiment.BranchTree
+
+open Propagator PolicySession SemanticReplay TargetRun BranchStart
+
+/-- Which child is being initialized.  Policies may use this to fork private
+state differently on the two sides. -/
+inductive Side where
+  | left
+  | right
+  deriving DecidableEq, Repr
+
+/-- Replaceable pending-leaf order. -/
+inductive Order where
+  | depthFirst
+  | breadthFirst
+  deriving DecidableEq, Repr
+
+/-- Global tree resources.  Child sessions retain their independent engine,
+policy, and payload limits. -/
+structure Limits where
+  branch : BranchStart.Limits
+  maxSteps : Nat
+  maxSplits : Nat
+  maxLeaves : Nat
+  leafFuel : Nat
+  deriving DecidableEq, Repr
+
+/-- Everything needed to run and split one pending leaf. -/
+structure Config (Fact PolicyState : Type) : Type 1 where
+  factDomain : FactDomain Fact
+  packages : Array (Package Fact)
+  sessionLimits : PolicySession.Limits
+  controller : TargetRun.Controller Fact PolicyState
+  splitter : BranchStart.Splitter Fact
+  forkPolicy : PolicyState -> Side -> PolicyState
+  order : Order
+  limits : Limits
+
+/-- Stable index into the append-only node array. -/
+structure TreeId where
+  index : Nat
+  deriving DecidableEq, Repr
+
+/-- Exact input, scope, depth, and private policy state of one leaf. -/
+structure Leaf (Fact PolicyState : Type) where
+  scope : Propagator.Policy.ScopeId
+  depth : Nat
+  input : CheckerInput Fact
+  policyState : PolicyState
+
+/-- A leaf whose policy session can still be run. -/
+structure Job (Fact PolicyState : Type) : Type 1 where
+  scope : Propagator.Policy.ScopeId
+  depth : Nat
+  input : CheckerInput Fact
+  policyState : PolicyState
+  session : PolicySession.Session Fact
+
+/-- Why a split result was retained as a blocked leaf. -/
+inductive Blocked where
+  | splitRejected (error : BranchStart.Error)
+  | splitLimit
+  | leafLimit
+  deriving DecidableEq, Repr
+
+/-- Terminal runtime data for a leaf.  None of these constructors is proof
+evidence. -/
+inductive LeafEnd (Fact PolicyState : Type) : Type 1
+  | result (run : TargetRun.Result Fact PolicyState)
+  | blocked (run : TargetRun.Result Fact PolicyState) (reason : Blocked)
+  | startError (error : PolicySession.StartError)
+
+/-- One retained runtime-tree node.  A split node stores the exact validated
+child snapshots and both child identities, even if a child session failed to
+start. -/
+inductive Node (Fact PolicyState : Type) : Type 1
+  | pending (job : Job Fact PolicyState)
+  | leaf (source : Leaf Fact PolicyState) (ending : LeafEnd Fact PolicyState)
+  | split (source : Leaf Fact PolicyState)
+      (run : TargetRun.Result Fact PolicyState)
+      (children : BranchStart.Children Fact) (left right : TreeId)
+
+/-- Monotone retained state for one tree.  `leaves` counts current leaves, so
+an accepted binary split increases it by exactly one. -/
+structure State (Fact PolicyState : Type) : Type 1 where
+  nodes : Array (Node Fact PolicyState)
+  frontier : List TreeId
+  branch : BranchStart.State
+  splits : Nat
+  leaves : Nat
+  steps : Nat
+
+/-- Failure before a coherent root tree exists. -/
+inductive StartError where
+  | leafLimit
+  | scopeLimit
+  | unknownTarget
+  | session (error : PolicySession.StartError)
+  deriving DecidableEq, Repr
+
+/-- An append-only tree should only schedule valid pending nodes. -/
+inductive Error where
+  | missingNode (id : TreeId)
+  | settledNode (id : TreeId)
+  deriving DecidableEq, Repr
+
+def sourceOf (job : Job Fact PolicyState) : Leaf Fact PolicyState :=
+  { scope := job.scope
+    depth := job.depth
+    input := job.input
+    policyState := job.policyState }
+
+/-- A tree is settled exactly when it has no runnable leaf.  It may still
+contain blocked, unfinished, or failed leaves. -/
+def State.settled (state : State Fact PolicyState) : Bool :=
+  state.frontier.isEmpty
+
+/-- The global processing budget may leave a nonempty frontier. -/
+def State.stepLimited (limits : Limits) (state : State Fact PolicyState) : Bool :=
+  state.steps >= limits.maxSteps && !state.frontier.isEmpty
+
+/-- Build a coherent root session from the exact caller input. -/
+def start (config : Config Fact PolicyState) (scope : Propagator.Policy.ScopeId)
+    (input : CheckerInput Fact) (policyState : PolicyState) :
+    Except StartError (State Fact PolicyState) := do
+  if config.limits.maxLeaves = 0 then throw .leafLimit
+  if config.limits.branch.maxScopes = 0 then throw .scopeLimit
+  if (input.baseProgram.node? input.target.node).isNone then
+    throw StartError.unknownTarget
+  let session <-
+    match PolicySession.Session.start config.factDomain input.baseProgram
+        config.packages input.initialFacts config.sessionLimits scope with
+    | .ok session => pure session
+    | .error error => throw (.session error)
+  let root : Job Fact PolicyState :=
+    { scope, depth := 0, input, policyState, session }
+  pure
+    { nodes := #[.pending root]
+      frontier := [{ index := 0 }]
+      branch := BranchStart.State.start session
+      splits := 0
+      leaves := 1
+      steps := 0 }
+
+def schedule (order : Order) (rest fresh : List TreeId) : List TreeId :=
+  match order with
+  | .depthFirst => fresh ++ rest
+  | .breadthFirst => rest ++ fresh
+
+def childNode (config : Config Fact PolicyState) (side : Side)
+    (scope : Propagator.Policy.ScopeId) (depth : Nat) (input : CheckerInput Fact)
+    (policyState : PolicyState) : Node Fact PolicyState × Bool :=
+  let childState := config.forkPolicy policyState side
+  let source : Leaf Fact PolicyState := { scope, depth, input, policyState := childState }
+  match PolicySession.Session.start config.factDomain input.baseProgram
+      config.packages input.initialFacts config.sessionLimits scope with
+  | .ok session =>
+      (.pending
+        { scope := source.scope
+          depth := source.depth
+          input := source.input
+          policyState := source.policyState
+          session }, true)
+  | .error error => (.leaf source (.startError error), false)
+
+def retainLeaf (state : State Fact PolicyState) (id : TreeId)
+    (source : Leaf Fact PolicyState) (ending : LeafEnd Fact PolicyState)
+    (rest : List TreeId) : State Fact PolicyState :=
+  { state with
+    nodes := state.nodes.set! id.index (.leaf source ending)
+    frontier := rest
+    steps := state.steps + 1 }
+
+/-- Process one pending leaf.  Split rejection and tree-resource exhaustion
+are terminal leaf data; only a malformed internal frontier returns `Error`. -/
+def step [DecidableEq Fact] (config : Config Fact PolicyState)
+    (state : State Fact PolicyState) : Except Error (State Fact PolicyState) := do
+  if state.steps >= config.limits.maxSteps then return state
+  let some id := state.frontier.head? | return state
+  let rest := state.frontier.tail
+  let some node := state.nodes[id.index]? | throw (.missingNode id)
+  let .pending job := node | throw (.settledNode id)
+  let source := sourceOf job
+  let run := TargetRun.drive config.factDomain job.input.target.node
+    job.input.target.fact config.controller config.limits.leafFuel
+    job.session job.policyState
+  let .split plan := run.stop |
+    return retainLeaf state id source (.result run) rest
+  if state.splits >= config.limits.maxSplits then
+    return retainLeaf state id source (.blocked run .splitLimit) rest
+  if state.leaves + 1 > config.limits.maxLeaves then
+    return retainLeaf state id source (.blocked run .leafLimit) rest
+  match BranchStart.prepare config.limits.branch state.branch run.session plan
+      job.input.target config.splitter with
+  | .error error =>
+      pure (retainLeaf state id source (.blocked run (.splitRejected error)) rest)
+  | .ok (branch, children) =>
+      let leftId : TreeId := { index := state.nodes.size }
+      let rightId : TreeId := { index := state.nodes.size + 1 }
+      let (leftNode, leftPending) := childNode config .left children.leftScope
+        children.depth children.left run.policyState
+      let (rightNode, rightPending) := childNode config .right children.rightScope
+        children.depth children.right run.policyState
+      let fresh :=
+        (if leftPending then [leftId] else []) ++
+          (if rightPending then [rightId] else [])
+      pure
+        { nodes := (state.nodes.set! id.index
+              (.split source run children leftId rightId)).push leftNode |>.push rightNode
+          frontier := schedule config.order rest fresh
+          branch
+          splits := state.splits + 1
+          leaves := state.leaves + 1
+          steps := state.steps + 1 }
+
+/-- Run for at most the caller fuel and never beyond the retained global step
+budget.  A nonempty frontier in the result is an honest partial tree. -/
+def runFrom [DecidableEq Fact] (config : Config Fact PolicyState) :
+    Nat -> State Fact PolicyState -> Except Error (State Fact PolicyState)
+  | 0, state => pure state
+  | fuel + 1, state =>
+      if state.settled || state.steps >= config.limits.maxSteps then pure state
+      else do
+        let state ← step config state
+        runFrom config fuel state
+
+termination_by fuel _ => fuel
+
+/-- Consume the configured global processing budget. -/
+def run [DecidableEq Fact] (config : Config Fact PolicyState)
+    (state : State Fact PolicyState) : Except Error (State Fact PolicyState) :=
+  runFrom config config.limits.maxSteps state
+
+end Hex.Interval.Experiment.BranchTree

HexInterval/SPEC/hex-interval.md

@@ -1688,21 +1688,44 @@ runtime contradiction separately but deliberately refuses to treat that flag
 as proof closure; the frontend must first resolve an established bottom fact
 and apply the refutation schema described above.
 
-The remaining tree manager should retain internal nodes recording validated
-plans and checked child facts, and leaves retaining either a target proof, a
-checked contradiction, or an explicit unfinished result. It may emit a theorem
-only when every coverage child is closed. For best-bound mode, unfinished
-leaves contribute their inherited parent fact to the global hull; they never
-inherit a tighter sibling fact. Live-leaf and total branch-decision limits
-remain to be added beside the delivered split-depth and total-created-scope
-limits and the per-session engine and payload limits.
+The first generic runtime tree manager now retains internal nodes recording
+validated plans and exact child inputs, and leaves recording target,
+contradiction, saturation, resource failure, split refusal, session-start
+failure, or any other precise `TargetRun` result. It stores the append-only
+node array and a separate pending frontier, so a global step limit returns an
+honest partial tree rather than relabelling unexplored leaves as closed.
+Independent limits bound processed leaves, accepted splits, current leaf
+count, split depth, total created scopes, and each leaf run's policy fuel in
+addition to the per-session engine and payload limits. Split- and leaf-limit
+exhaustion is retained at the exact parent leaf. A child session which cannot
+start is likewise retained beside its sibling instead of silently deleting
+the branch.
+
+The manager is function- and representation-independent. Its configuration
+supplies the fact domain, runtime packages, controller, splitter, child-policy
+fork, and pending order. The initial orders are depth-first and breadth-first;
+their frontier transformation is separately tested so later best-first or
+hybrid queues do not affect branch validation. The exponential conformance
+tree selects the authenticated root split, starts both exact scoped children,
+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.
 
 Several operational choices deliberately remain experimental:
 
 - restart a child session from a checked snapshot, or add a sealed session-fork
   operation which preserves reusable work and immutable payload sharing;
-- depth-first execution for small proof memory, best-first execution for early
-  target closure, or a bounded hybrid frontier;
+- use the delivered depth-first or breadth-first list frontier, or replace it
+  with best-first execution or a bounded hybrid without changing retained
+  nodes;
 - store branch-local program suffixes directly, or hash-cons identical
   instantiations above the scope layer;
 - retain `Dyadic` in real-domain executable plans while keeping the proof
@@ -1726,12 +1749,13 @@ replays them, and `replaySplit` produces the joined entailment evidence.
 `closeRelu` specializes that evidence to the ordinary theorem `0 ≤ max x 0`.
 Each rule rejects the unsplit top fact, and mutating either quote to use its
 sibling's assumption makes emission fail. The package remains a compact
-conformance fixture while
-we decide which parts belong in the Mathlib-free runtime and Mathlib semantic
+conformance fixture while we decide which parts belong in the Mathlib-free
+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, and
-fuel exhaustion with no theorem emitted.
+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.
 
 ### Proof-producing frontend