Add proof-producing policy sessions

HexInterval/SPEC/hex-interval.md

@@ -1071,6 +1071,14 @@ experimental. The older direct registry and engine interfaces remain available
 for search experiments, but proof-producing execution goes through the
 session.
 
+`PolicySession.Session` is the corresponding proof-producing policy canary.
+Its checked start stores one bundle containing the engine, policy, and arena
+limits and owns the resulting `Policy.State`, exact registry, and arena.
+`Session.view` returns the same owned session with traversal accounting
+committed, while `Session.choose` accepts only a checked selection or
+dismissal and returns the next coherent session. No public transition accepts
+separately assembled engine, registry, policy state, or arena values.
+
 The explicit registration and validation boundary is fixed. Discovery and
 scheduling above it remain empirical: one arm uses an incremental registry
 worklist to share facts and retain state, while a second traverses the same
@@ -1207,9 +1215,9 @@ construction and identifier assignment are one traversal, so a relocated
 identifier denotes exactly the entry appended for its local draft.
 Candidate, instantiation, and equality roles are distinct, and ordinary replay
 lookup checks the expected role. Failure returns the old arena.
-The session commits that returned arena only if submission of the relocated
-outcome also succeeds. Before freezing, it checks the candidate and suggestion
-list lengths against the engine's own trusted limits. Let
+Both private sessions commit that returned arena only if submission of the
+relocated outcome also succeeds. Before freezing, they check the candidate and
+suggestion list lengths against the engine's own trusted limits. Let
 `requiredUses = maxOutcomeCandidates + maxOutcomeSuggestions *
 (maxProposalItems + 1)`: every candidate and suggestion costs one payload use,
 and every suggestion may be an instantiation with at most
@@ -1315,14 +1323,31 @@ requires a live session and no retained retry or instantiation. At a FIFO
 fixed point this predicate is the sole gate between saturated and incomplete.
 Package `failed`/`resourceLimit` results, malformed evidence, dropped narrowing
 suggestions, and unprocessed retained narrowing therefore cannot be laundered
-into saturation. The next policy experiment must preserve this same session
-transaction while allowing an external policy to choose invocations,
-instantiations, equalities, retries, and splits; it must not regain access to
-separable engine, registry, and arena values. The FIFO session can already
-freeze an instantiation and its nested equality payloads, but it deliberately
-has no public admission escape hatch. Honest session-level execution coverage
-for the resulting equality contractor therefore belongs to that private
-policy-session layer, not to a test-only constructor or engine replacement.
+into saturation.
+
+The policy session now preserves the same transaction while allowing an
+external policy to select invocations and retries, instantiations, equality
+contractors, and splits, or to dismiss any live offer. A selected invocation
+or retry routes through `Registry.invokePlanned`, which returns the plan paired
+with the exact selected handler's replay snapshot. The session calls that
+sealed snapshot's paired freeze operation, submits the relocated reply through
+`Policy.State`, and commits the new arena only for an accepted reply. A missing
+or malformed format and package-local payload-use, draft-count, draft-cell,
+atom, or schema excess consume a bounded synthetic failed reply: the cache may
+record the attempt, the arena, facts, and history do not commit, and the
+private session remains live but permanently incomplete. Exhausting remaining
+whole-run entry or body-cell capacity after an earlier commit instead returns
+a non-live session after clearing the selected request while preserving the
+preceding arena and history.
+The policy can observe a bounded view and echo a semantic selection, but
+cannot extract and later recombine the engine, registry, arena, or policy
+bookkeeping. Its `Session.complete` predicate additionally scans for live
+invocation and equality work and treats retries and instantiations, but not
+optional splits, as closure obligations. The policy state's monotone
+incompleteness bit covers failed replies, rejected or stale narrowing
+suggestions, and required dismissals; the session bit covers evidence lost
+outside those policy transitions. Engine-resource or structurally invalid
+snapshots also become non-live.
 
 ### Action kinds
 
@@ -1844,15 +1869,20 @@ The policy experiment proceeds in replaceable increments:
    retryable enclosure, a structure-triggered alternate form, equality
    contraction, and a function-owned split landmark.
 
-The concrete package canary reaches step 6 with the unchanged external driver.
-One deterministic schedule selects subtraction and multiplication propagation,
-the structure matcher, instantiation admission, the centered function's split
-handler and forward propagator, equality contraction, reciprocal propagation,
-a precision retry, and finally the centered function's split suggestion. It
-adds the centered node at generation one, narrows both representations to
-`[0,1/4]`, improves the enclosure of `1/3` at effort one, and returns a prepared
-plan at `x = 1/2` while the effort-two retry remains live. No branch is
-executed, so this is evidence for policy routing and freshness, not for scope
+The concrete package canary reaches step 6 in both search-only and
+proof-producing modes. One deterministic schedule selects subtraction and
+multiplication propagation, the structure matcher, instantiation admission,
+the centered function's split handler and forward propagator, equality
+contraction, reciprocal propagation, a precision retry, and finally the
+centered function's split suggestion. It adds the centered node at generation
+one, narrows both representations to `[0,1/4]`, improves the enclosure of
+`1/3` at effort one, and returns a prepared plan at `x = 1/2`. The
+proof-producing schedule also dismisses the effort-two retry and therefore
+retains an honest incomplete marker. Its arena contains the exact sequence of
+fact, instance, and equality roles; the admitted instance event, equality
+edge, and centered fact provenance resolve to entries owned by their
+originating package actions. No branch is executed, so this is evidence for
+policy routing, ownership, evidence freezing, and freshness, not for scope
 creation or split interiority.
 
 Once policy control begins, the wrapper is the sole scheduling authority for
@@ -2417,6 +2447,13 @@ typical, boundary, and adversarial inputs. In particular it includes:
   and a function-owned split in a checked event order; it returns an
   endpoint-resource-checked plan at `1/2`, leaves the next retry offer live,
   and performs no branch/interiority step;
+- the proof-producing policy session over those same packages, selecting every
+  offer class through one private owner, retaining exact fact, instance, and
+  equality replay formats, rolling back a prospectively frozen rejected write
+  and both malformed and undeclared formats, keeping package-local payload
+  use, draft-count, draft-cell, atom, and schema bounds live but incomplete,
+  making genuine mid-run whole-arena exhaustion fatal, and exposing an empty
+  failed frontier as incomplete rather than saturated;
 - undirected equality transport, including incomparable endpoint facts that
   improve both sides atomically, equality chains, reactivation after a later
   function improvement, and an original expression transferring its bound to