From 5c001338aa5ebea875eb829ecbbf9071e3bd993b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Tue, 28 Jul 2026 05:42:48 +0000
Subject: [PATCH 1/9] Register package-owned replay formats

Includes progress/20260728T054228Z.md.
---
 HexInterval/Experiment/PackageRegistry.lean   | 135 ++++++++---
 HexInterval/Experiment/PayloadArena.lean      | 103 ++++++--
 HexInterval/Experiment/PayloadSession.lean    |  41 ++--
 HexInterval/SPEC/hex-interval.md              |  91 ++++---
 .../HexInterval/PayloadArenaConformance.lean  |   9 +
 .../PayloadSessionConformance.lean            | 225 +++++++++++++++++-
 progress/20260728T054228Z.md                  |  35 +++
 7 files changed, 533 insertions(+), 106 deletions(-)
 create mode 100644 progress/20260728T054228Z.md

diff --git a/HexInterval/Experiment/PackageRegistry.lean b/HexInterval/Experiment/PackageRegistry.lean
index 238410140..38989ba29 100644
--- a/HexInterval/Experiment/PackageRegistry.lean
+++ b/HexInterval/Experiment/PackageRegistry.lean
@@ -24,10 +24,12 @@ the external policy driver.  Updating a package cache cannot alter its stable
 operations, registrations, callbacks, routes, or start checks.  Package caches
 are performance state only: for the same request and logical budget, cache
 contents must not change the callback's observable outcome.  Semantic state
-instead needs an explicit versioned dependency and wakeup protocol.  Immutable
+instead needs an explicit versioned dependency and wakeup protocol. Immutable
 proof-payload drafts travel beside the outcome; a session layer must freeze
 them in a separate per-run arena before their identifiers enter engine
-provenance.
+provenance. Each handler also owns cache-independent replay formats. Their
+validators check bounded representation shape without adding any arithmetic
+or function case split to the generic registry.
 -/
 
 namespace Hex.Interval.Experiment.Propagator
@@ -38,6 +40,50 @@ structure Plan (Fact : Type) where
   outcome : Outcome Fact
   drafts : List PayloadArena.Draft
 
+/-- One cache-independent, rule-local replay representation.  The validator is
+called only after generic arena preflight has bounded the draft and its body.
+It checks representation shape, not mathematical soundness. -/
+structure ReplayFormat where
+  role : PayloadArena.Role
+  schema : Nat
+  validateBody : List Nat -> Bool
+
+namespace ReplayFormat
+
+def sameAddress (left right : ReplayFormat) : Bool :=
+  left.role == right.role && left.schema == right.schema
+
+def replayKey (rule : RuleKey) (format : ReplayFormat) :
+    PayloadArena.ReplayKey :=
+  { rule, role := format.role, schema := format.schema }
+
+end ReplayFormat
+
+/-- Immutable replay metadata selected together with one handler invocation.
+`rule` plus a format's role and numeric schema is the complete dispatch key. -/
+structure ReplaySnapshot where
+  rule : RuleKey
+  formats : Array ReplayFormat
+
+namespace ReplaySnapshot
+
+def validateDraft (snapshot : ReplaySnapshot) (draft : PayloadArena.Draft) :
+    Option PayloadArena.Invalid :=
+  let key := draft.replayKey snapshot.rule
+  match snapshot.formats.toList.find?
+      (fun format => format.role == draft.role && format.schema == draft.schema) with
+  | none => some (.undeclaredFormat key)
+  | some format =>
+      if format.validateBody draft.body then none else some (.invalidBody key)
+
+end ReplaySnapshot
+
+/-- A package plan paired with the immutable replay metadata of the exact
+handler that produced it. -/
+structure Invocation (Fact : Type) where
+  plan : Plan Fact
+  replay : ReplaySnapshot
+
 /-- The callback shape shared by direct and session-owned drivers. -/
 abbrev Invoke (Fact Cache : Type) :=
   Cache -> RuleRequest Fact -> Plan Fact × Cache
@@ -53,6 +99,8 @@ abbrev BareInvoke (Fact Cache : Type) :=
 /-- One registration and the only callback allowed to interpret its key. -/
 structure Handler (Fact Cache : Type) where
   registration : Registration
+  /-- Immutable cache-independent replay representations owned by this rule. -/
+  replayFormats : Array ReplayFormat := #[]
   invoke : Invoke Fact Cache
 
 namespace Handler
@@ -79,13 +127,16 @@ def statelessDroppingDrafts (registration : Registration)
 
 /-- A cache-independent callback that returns complete reply-local evidence. -/
 def readOnlyPlanned (registration : Registration)
-    (invoke : RuleRequest Fact -> Plan Fact) : Handler Fact Cache :=
-  { registration, invoke := fun cache request => (invoke request, cache) }
+    (invoke : RuleRequest Fact -> Plan Fact)
+    (replayFormats : Array ReplayFormat := #[]) : Handler Fact Cache :=
+  { registration, replayFormats
+    invoke := fun cache request => (invoke request, cache) }
 
 /-- A stateless callback that returns complete reply-local evidence. -/
 def statelessPlanned (registration : Registration)
-    (invoke : RuleRequest Fact -> Plan Fact) : Handler Fact Unit :=
-  readOnlyPlanned registration invoke
+    (invoke : RuleRequest Fact -> Plan Fact)
+    (replayFormats : Array ReplayFormat := #[]) : Handler Fact Unit :=
+  readOnlyPlanned registration invoke replayFormats
 
 end Handler
 
@@ -145,6 +196,7 @@ end DispatchCode
 inductive RegistryError where
   | duplicateOperation (key : OpKey)
   | duplicateRule (key : RuleKey)
+  | duplicateFormat (key : PayloadArena.ReplayKey)
   | undeclaredHead (rule : RuleKey) (head : OpKey)
   | resourceLimit (resource : Resource)
   deriving DecidableEq, Repr
@@ -164,14 +216,26 @@ def declaresOperation (operations required : Array Operation) (key : OpKey) : Bo
   operations.any (fun operation => operation.key == key) ||
     required.any (fun operation => operation.key == key)
 
-def validateHandlerHeads (operations required : Array Operation) :
+def duplicateFormat? (rule : RuleKey) :
+    List ReplayFormat -> Option PayloadArena.ReplayKey
+  | [] => none
+  | format :: formats =>
+      if formats.any (fun other => format.sameAddress other) then
+        some (format.replayKey rule)
+      else
+        duplicateFormat? rule formats
+
+def validateHandlers (operations required : Array Operation) :
     List (Handler Fact Cache) -> Except RegistryError Unit
   | [] => pure ()
   | handler :: handlers =>
-      if declaresOperation operations required handler.registration.head then
-        validateHandlerHeads operations required handlers
-      else
+      if !declaresOperation operations required handler.registration.head then
         throw (.undeclaredHead handler.registration.key handler.registration.head)
+      else
+        match duplicateFormat? handler.registration.key
+            handler.replayFormats.toList with
+        | some key => throw (.duplicateFormat key)
+        | none => validateHandlers operations required handlers
 
 def addHandlers (packageIndex : Nat) : Nat -> List (Handler Fact Cache) ->
     Array Registration -> Array Route ->
@@ -192,7 +256,7 @@ def flatten : Nat -> List (Package Fact) -> Array Operation ->
   | _, [], operations, registrations, routes =>
       pure (operations, registrations, routes)
   | packageIndex, package :: rest, operations, registrations, routes => do
-      validateHandlerHeads package.operations package.requiredOperations
+      validateHandlers package.operations package.requiredOperations
         package.handlers.toList
       let operations <- addOperations package.operations.toList operations
       let (registrations, routes) <-
@@ -209,12 +273,15 @@ def preflight (limits : Limits) (packages : Array (Package Fact)) :
   for package in packages do
     operationCount := operationCount + package.operations.size
     ruleCount := ruleCount + package.handlers.size
-    metadataCount := metadataCount + package.operations.size +
-      package.requiredOperations.size + package.handlers.size
     if limits.maxOperations < operationCount then
       throw (.resourceLimit .operations)
     if limits.maxRules < ruleCount then
       throw (.resourceLimit .rules)
+    let replayFormatCount :=
+      package.handlers.foldl
+        (fun count handler => count + handler.replayFormats.size) 0
+    metadataCount := metadataCount + package.operations.size +
+      package.requiredOperations.size + package.handlers.size + replayFormatCount
     if limits.maxOperations + limits.maxRules < metadataCount then
       throw (.resourceLimit .registryEntries)
     if package.operations.any
@@ -228,8 +295,9 @@ def preflight (limits : Limits) (packages : Array (Package Fact)) :
 
 /-- Resource-preflight package metadata before duplicate scans or flattened
 array allocation.  The aggregate metadata cap also bounds external signature
-requirements and empty-package churn.  Assembly order is package-major and
-then handler-major; exact operation and rule keys are unique in the snapshot. -/
+requirements, replay formats, and empty-package churn.  Assembly order is
+package-major and then handler-major; exact operation and rule keys are unique
+in the snapshot. -/
 def buildWithin (limits : Limits) (packages : Array (Package Fact)) :
     Except RegistryError (Registry Fact) :=
   match preflight limits packages with
@@ -303,37 +371,48 @@ end Registration
 
 namespace Registry
 
+/-- A negative plan for a dispatch failure before any callback or replay
+format can be selected. -/
+def failedInvocation (rule : RuleKey) (code : Nat) : Invocation Fact :=
+  { plan := { outcome := .failed code, drafts := [] }
+    replay := { rule, formats := #[] } }
+
 /-- Route one engine-owned rule identifier to its package callback and retain
-its reply-local proof drafts. Dispatch uses compact validated indices; it never
-branches on the semantic operation or rule key. Only the selected package
-cache is replaced. -/
+its reply-local proof drafts together with that handler's replay formats.
+Dispatch uses compact validated indices; it never branches on the semantic
+operation or rule key. Only the selected package cache is replaced. -/
 def invokePlanned (registry : Registry Fact) (request : RuleRequest Fact) :
-    Plan Fact × Registry Fact :=
+    Invocation Fact × Registry Fact :=
   match registry.routes[request.action.rule.index]? with
-  | none => ({ outcome := .failed DispatchCode.missingRoute, drafts := [] }, registry)
+  | none =>
+      (failedInvocation request.action.key DispatchCode.missingRoute, registry)
   | some route =>
       match registry.registrations[request.action.rule.index]? with
       | none =>
-          ({ outcome := .failed DispatchCode.missingRegistration, drafts := [] }, registry)
+          (failedInvocation request.action.key DispatchCode.missingRegistration, registry)
       | some registration =>
           match registry.packages[route.package]? with
-          | none => ({ outcome := .failed DispatchCode.missingPackage, drafts := [] }, registry)
+          | none =>
+              (failedInvocation request.action.key DispatchCode.missingPackage, registry)
           | some package =>
               match package.handlers[route.handler]? with
               | none =>
-                  ({ outcome := .failed DispatchCode.missingHandler, drafts := [] }, registry)
+                  (failedInvocation request.action.key DispatchCode.missingHandler, registry)
               | some handler =>
                   if !registration.same handler.registration then
-                    ({ outcome := .failed DispatchCode.registryMismatch, drafts := [] }, registry)
+                    (failedInvocation request.action.key DispatchCode.registryMismatch, registry)
                   else if !handler.registration.accepts request then
-                    ({ outcome := .failed DispatchCode.requestMismatch, drafts := [] }, registry)
+                    (failedInvocation request.action.key DispatchCode.requestMismatch, registry)
                   else
                     let (plan, cache) := handler.invoke package.cache request
                     let package :=
                       { package with
                         cache := cache
                         invocations := package.invocations + 1 }
-                    (plan,
+                    ({ plan
+                       replay :=
+                         { rule := handler.registration.key
+                           formats := handler.replayFormats } },
                       { registry with
                         packages := registry.packages.set! route.package package })
 
@@ -342,8 +421,8 @@ proof-producing session must use `invokePlanned` and freeze its drafts before
 submission. -/
 def invokeDroppingDrafts (registry : Registry Fact) (request : RuleRequest Fact) :
     Outcome Fact × Registry Fact :=
-  let (plan, registry) := registry.invokePlanned request
-  (plan.outcome, registry)
+  let (invocation, registry) := registry.invokePlanned request
+  (invocation.plan.outcome, registry)
 
 end Registry
 
diff --git a/HexInterval/Experiment/PayloadArena.lean b/HexInterval/Experiment/PayloadArena.lean
index 216078bcd..ea48f0265 100644
--- a/HexInterval/Experiment/PayloadArena.lean
+++ b/HexInterval/Experiment/PayloadArena.lean
@@ -53,6 +53,30 @@ structure Entry where
   body : List Nat
   deriving Repr
 
+/-- The immutable dispatch address for semantic replay.  The numeric schema
+is local to one rule and role; unrelated handlers may deliberately reuse it. -/
+structure ReplayKey where
+  rule : RuleKey
+  role : Role
+  schema : Nat
+  deriving DecidableEq, Repr
+
+namespace Draft
+
+/-- Resolve a reply-local draft's full replay address under its handler. -/
+def replayKey (rule : RuleKey) (draft : Draft) : ReplayKey :=
+  { rule, role := draft.role, schema := draft.schema }
+
+end Draft
+
+namespace Entry
+
+/-- The full replay address retained by a frozen arena entry. -/
+def replayKey (entry : Entry) : ReplayKey :=
+  { rule := entry.origin.key, role := entry.role, schema := entry.schema }
+
+end Entry
+
 /-- Append-only replay storage.  `bodyCells` is maintained by `freeze`, making
 the aggregate body bound independent of later arena size. -/
 structure Arena where
@@ -109,6 +133,9 @@ inductive Invalid where
   | danglingReference (label : PayloadId)
   | wrongRole (label : PayloadId) (expected actual : Role)
   | extraDraft (label : PayloadId)
+  | wrongOwner (expected actual : RuleKey)
+  | undeclaredFormat (key : ReplayKey)
+  | invalidBody (key : ReplayKey)
   deriving DecidableEq, Repr
 
 /-- A trusted arena limit exhausted before allocation. -/
@@ -264,6 +291,14 @@ structure BoundedDrafts where
   drafts : List Draft
   cells : Nat
 
+def validateDrafts (validateDraft : Draft -> Option Invalid) :
+    List Draft -> Option Invalid
+  | [] => none
+  | draft :: drafts =>
+      match validateDraft draft with
+      | some error => some error
+      | none => validateDrafts validateDraft drafts
+
 /-- Traverse a reply body through the first cell beyond its local budget.
 Every visited atom is checked before its cell is charged, so an oversized
 boundary atom reports `.atom`. Cells after a `.draftCells` stop are
@@ -350,33 +385,55 @@ def freezeDrafts (arena : Arena) (origin : Action)
     appendDrafts origin arena.entries bounded.drafts
   ({ entries, bodyCells := arena.bodyCells + bounded.cells }, relocations)
 
-/-- Validate and freeze every reply-local payload reference in an outcome.
+/-- Validate and freeze every reply-local payload reference using the exact
+replay-format snapshot selected for the invocation.
 
-This function does not mutate the supplied arena.  A caller should retain the
+Reply-local body and draft bounds and exact coverage are checked before
+`validateDraft` runs, so a package validator only receives locally bounded,
+structurally relevant inputs. Only structurally and format-valid evidence is
+then compared with remaining whole-run capacity. The validator establishes
+representation shape only. Semantic replay must decode the same immutable
+entry and recheck the rule-specific mathematics.
+
+This function does not mutate the supplied arena. A caller should retain the
 returned arena only if the surrounding reply transaction also commits.
 Starting from `arena.wellFormed`, every ready result remains well formed.
-Callers must supply that precondition until a later session abstraction owns
-the arena by construction. -/
+Direct callers must supply that precondition; the checked session owns a
+well-formed arena by construction. -/
+def freezeChecked (limits : Limits) (arena : Arena) (origin : Action)
+    (owner : RuleKey) (validateDraft : Draft -> Option Invalid)
+    (outcome : Outcome Fact) (drafts : List Draft) : Result Fact :=
+  if owner != origin.key then
+    .invalid (.wrongOwner origin.key owner) arena
+  else
+    match preflightUses limits.maxUses outcome with
+    | .error resource => .resourceLimit resource arena
+    | .ok _ =>
+         let uses := outcomeUses outcome
+         match preflightLocal limits drafts with
+         | .error resource => .resourceLimit resource arena
+         | .ok bounded =>
+             match validate uses bounded.drafts with
+             | some error => .invalid error arena
+             | none =>
+                 match validateDrafts validateDraft bounded.drafts with
+                 | some error => .invalid error arena
+                 | none =>
+                     match preflightWhole limits arena bounded with
+                     | .error resource => .resourceLimit resource arena
+                     | .ok _ =>
+                         let (prospective, relocations) :=
+                           freezeDrafts arena origin bounded
+                         match relocateOutcome relocations outcome with
+                         | .error error => .invalid error arena
+                        | .ok outcome =>
+                            .ready prospective outcome
+
+/-- Standalone structural freezing with no package format validation.
+Proof-producing sessions use `freezeChecked` with the selected handler's
+immutable replay snapshot. -/
 def freeze (limits : Limits) (arena : Arena) (origin : Action)
     (outcome : Outcome Fact) (drafts : List Draft) : Result Fact :=
-  match preflightUses limits.maxUses outcome with
-  | .error resource => .resourceLimit resource arena
-  | .ok _ =>
-      let uses := outcomeUses outcome
-      match preflightLocal limits drafts with
-      | .error resource => .resourceLimit resource arena
-      | .ok bounded =>
-          match validate uses bounded.drafts with
-          | some error => .invalid error arena
-          | none =>
-              match preflightWhole limits arena bounded with
-              | .error resource => .resourceLimit resource arena
-              | .ok _ =>
-                  let (prospective, relocations) :=
-                    freezeDrafts arena origin bounded
-                  match relocateOutcome relocations outcome with
-                  | .error error => .invalid error arena
-                  | .ok outcome =>
-                      .ready prospective outcome
+  freezeChecked limits arena origin origin.key (fun _ => none) outcome drafts
 
 end Hex.Interval.Experiment.PayloadArena
diff --git a/HexInterval/Experiment/PayloadSession.lean b/HexInterval/Experiment/PayloadSession.lean
index 676c83ac8..5a53eb09a 100644
--- a/HexInterval/Experiment/PayloadSession.lean
+++ b/HexInterval/Experiment/PayloadSession.lean
@@ -18,22 +18,24 @@ compiled it, and one immutable proof-payload arena. Its private constructor
 prevents callers from pairing independently assembled values.
 
 For a rule action, `advance` invokes the routed package, freezes and relocates
-all reply-local proof labels prospectively, and submits the relocated outcome.
-The new arena commits only when engine submission succeeds. Package caches may
-still record a failed invocation because they are explicitly non-semantic;
-engine facts, expression nodes, provenance, and the arena remain atomic.
-Malformed package evidence is submitted to the engine as a failed rule reply:
-the request latch is cleared, the session remains usable, and completeness is
-permanently lost. Exceeding a package-local payload-use, draft, draft-cell,
-atom, or schema bound has the same recoverable behavior. Exhausting remaining
-whole-run arena entry or body capacity after earlier commits, or encountering
-an engine-invalid transition, instead returns a non-live session snapshot
-which cannot later be resumed and mislabeled saturated. This cumulative stop
-is an intentional conservative policy for the eager prototype: an otherwise
-valid selected transition could not be retained, so the session treats it like
-global engine-resource exhaustion rather than skipping required work. Package
-failure and unprocessed narrowing suggestions likewise make the final status
-incomplete.
+all reply-local proof labels prospectively, checks their bounded bodies with
+the exact invoked handler's immutable replay formats, and submits the relocated
+outcome. The new arena commits only when both format checking and engine
+submission succeed. Package caches may still record a failed invocation
+because they are explicitly non-semantic; engine facts, expression nodes,
+provenance, and the arena remain atomic. Malformed package evidence, including
+an undeclared or invalid replay format, is submitted to the engine as a failed
+rule reply: the request latch is cleared, the session remains usable, and
+completeness is permanently lost. Exceeding a package-local payload-use,
+draft, draft-cell, atom, or schema bound has the same recoverable behavior.
+Exhausting remaining whole-run arena entry or body capacity after earlier
+commits, or encountering an engine-invalid transition, instead returns a
+non-live session snapshot which cannot later be resumed and mislabeled
+saturated. This cumulative stop is an intentional conservative policy for the
+eager prototype: an otherwise valid selected transition could not be retained,
+so the session treats it like global engine-resource exhaustion rather than
+skipping required work. Package failure and unprocessed narrowing suggestions
+likewise make the final status incomplete.
 -/
 
 namespace Hex.Interval.Experiment.PayloadSession
@@ -224,7 +226,9 @@ opaque Session.advance (session : Session Fact) : Step Fact :=
     .invalidEngine session
   else match session.engine.poll with
   | .request request engine =>
-      let (plan, registry) := session.registry.invokePlanned request
+      let (invocation, registry) := session.registry.invokePlanned request
+      let replay := invocation.replay
+      let plan := invocation.plan
       if !outcomeListsBounded engine.limits plan.outcome then
         match engine.submit (request.action.reply plan.outcome) with
         | .accepted _ _ =>
@@ -238,7 +242,8 @@ opaque Session.advance (session : Session Fact) : Step Fact :=
         | .factResourceLimit budget next =>
             .factResource budget (haltRegistry session next registry)
       else
-        match PayloadArena.freeze session.arenaLimits session.arena request.action
+        match PayloadArena.freezeChecked session.arenaLimits session.arena
+            request.action replay.rule replay.validateDraft
             plan.outcome plan.drafts with
         | .invalid error _ =>
             failPayload session engine registry request.action error
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 7ffcf8c5c..479ed3b8f 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -1012,29 +1012,44 @@ start rather than advertised as compatible.
 
 `Registry.invokePlanned` cross-checks the flattened registration, routed handler
 metadata, and structural projection of an engine-produced request before
-entering the callback, then replaces only the selected package's cache. It is
-the proof-producing registry route because it retains the callback's
-reply-local drafts for freezing. Neither it nor
+entering the callback, then replaces only the selected package's cache. It
+returns a plan containing the outcome and all reply-local payload drafts,
+paired with the exact selected handler's immutable replay snapshot. The
+planned route is proof-producing, but neither it nor
 `Registry.invokeDroppingDrafts` is an authentication boundary: the engine
 still authenticates the pending serial, application, fact values, and
-versions. The explicitly named dropping-drafts adapter exists only for search
-experiments.
-
-The current package type does not yet carry replay decoders or a schema
-registry. Arena drafts do carry an explicit numeric payload schema, but a
-production checked assembly API should return operation metadata,
-registrations, callback routes, configuration validation, and the
-payload-freezing/replay schema implementations as one coherent snapshot.
-Whether that snapshot retains existential packages, compiles one dispatch
-function, supports hot replacement, or uses another lookup structure remains
-experimental. `PayloadSession.Session` now has a
-private constructor and its checked start owns the matching engine, registry,
-arena, and arena limits; the bounded `Run` result also has a private
-constructor, so its stop classification can only come from session execution.
-The older direct registry and engine interfaces remain available for search
-experiments, but proof-producing execution goes through the session. A
-different callback implementation under the same versioned rule schema
-remains valid only when its retained payloads replay under that schema.
+versions. The explicitly named dropping-drafts adapter discards drafts and
+replay metadata only for search experiments.
+
+Each handler now carries cache-independent replay-format declarations beside
+its registration and callback. A declaration consists of a payload role, a
+rule-local numeric schema variant, and a body-shape validator. The immutable
+dispatch key is `(RuleKey, role, schema)`: two unrelated function packages may
+reuse the same role and local schema number without sharing a validator.
+Registry assembly rejects duplicate `(role, schema)` declarations within a
+handler, and counts declarations against its metadata bound.
+
+`PayloadSession.Session` has a private constructor and its checked start owns
+the matching engine, registry, arena, and arena limits; the bounded `Run`
+result also has a private constructor, so its stop classification can only
+come from session execution. During an invocation, generic arena preflight
+first bounds the number of drafts, body cells, atoms, schemas, and payload
+uses. Only then does the session run the selected package's body validators.
+It rejects an undeclared role/schema pair, a malformed body, or a mismatched
+rule owner without committing the prospective arena or engine outcome.
+Package caches may record the failed attempt because they remain non-semantic.
+
+This first format API validates representation shape only. It does not attest
+that a body proves the proposed interval fact, instance, or equality. The
+Mathlib companion must dispatch on the same immutable key, decode the frozen
+entry independently of package cache state, and recheck the corresponding
+rule theorem during semantic replay. A different callback implementation
+under an existing versioned rule schema is compatible only when every retained
+payload still passes that semantic replay. Whether production retains these
+existential snapshots, compiles a dispatch table, adds typed decoders, supports
+hot replacement, or uses another lookup structure remains experimental. The
+older direct registry and engine interfaces remain available for search
+experiments, but proof-producing execution goes through the session.
 
 The explicit registration and validation boundary is fixed. Discovery and
 scheduling above it remain empirical: one arm uses an incremental registry
@@ -1260,17 +1275,19 @@ entry and cell capacity.
 Each frozen entry stores its originating action, semantic role, numeric
 payload schema, and uninterpreted `List Nat` body. It derives the rule owner
 only from `origin.key`, avoiding two stored identities which could disagree.
-Package-owned decoding and schema lookup, typed atom encodings, byte limits,
-and semantic replay are still missing. Instantiation family labels and custom
-split-reason numbers also remain untyped representation gaps. The FIFO session
-turns any positive compatibility callback whose local identifier lacks a
-draft into a failed rule transition, so no unrelocated package-local
-identifier reaches its retained provenance. Its monotone `droppedWork` flag
-means exactly that required work was lost; it is not itself a terminal-state
-claim. The exported `Session.complete` predicate additionally 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
+The session now performs package-owned format lookup and bounded body-shape
+validation under the full `(RuleKey, role, schema)` key. Typed decoding, typed
+atom encodings, byte limits, and semantic replay are still missing.
+Instantiation family labels and custom split-reason numbers also remain
+untyped representation gaps. The FIFO session turns any positive
+compatibility callback whose local identifier lacks a draft, or whose draft
+fails format validation, into a failed rule transition, so no unvalidated
+package-local identifier reaches its retained provenance. Its monotone
+`droppedWork` flag means exactly that required work was lost; it is not itself
+a terminal-state claim. The exported `Session.complete` predicate additionally
+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,
@@ -2320,14 +2337,20 @@ typical, boundary, and adversarial inputs. In particular it includes:
   independently appended packages using `List Nat` and `Bool` caches, exact
   route and final-program signature checks, external required signatures,
   duplicate operation/rule-key and undeclared-head rejection, cache-preserving
-  rejection of wrong routes, and a `Type 1` registry threaded through both
-  drivers;
+  rejection of wrong routes, duplicate replay-format rejection, and a `Type 1`
+  registry threaded through both drivers;
 - a private package session which freezes and relocates reply-local evidence,
   continues independent work after malformed or locally oversized drafts,
   retains incompleteness across a later successful reply, charges nested
   equality payload uses, keeps derived draft-cell accounting tied to the exact
   bounded transaction, and intentionally reserves fatal entry/body-cell stops
   for genuine remaining-capacity exhaustion after an earlier arena commit;
+- two unrelated opaque function packages which both use local fact schema `7`
+  but retain distinct `(RuleKey, role, schema)` addresses and validate
+  incompatible bounded body shapes; undeclared formats, malformed bodies, and
+  format failure after a previously committed invocation leave no partial
+  current transaction, while generic body-resource refusal precedes package
+  validation;
 - an anchor-local opaque shape rule which distinguishes `x * (one - x)` from
   products with a reversed difference or a different repeated input, proposes
   the exact existing node identifiers while receiving no fact inputs, repeats
diff --git a/conformance/HexInterval/PayloadArenaConformance.lean b/conformance/HexInterval/PayloadArenaConformance.lean
index 571a1c3ea..4948e5429 100644
--- a/conformance/HexInterval/PayloadArenaConformance.lean
+++ b/conformance/HexInterval/PayloadArenaConformance.lean
@@ -18,6 +18,7 @@ def node (index : Nat) : NodeId := { index }
 def payload (index : Nat) : PayloadId := { index }
 
 def rule : RuleKey := { name := "payload-arena.test" }
+def otherRule : RuleKey := { name := "payload-arena.other" }
 
 def action (serial : Nat) : Action :=
   { serial
@@ -159,6 +160,14 @@ def mixedRequest : InstantiationRequest :=
       label.index == 0 && seedPreserved arena
   | _ => false
 
+-- A replay-format snapshot cannot be paired with another rule's action.
+#guard
+  match freezeChecked generous seeded (action 0) otherRule (fun _ => none)
+      (factOutcome 0) [factDraft 0] with
+  | .invalid (.wrongOwner expected actual) arena =>
+      expected == rule && actual == otherRule && seedPreserved arena
+  | _ => false
+
 #guard
   match freeze generous seeded (action 0) (factOutcome 0)
       [factDraft 0, factDraft 0 [11]] with
diff --git a/conformance/HexInterval/PayloadSessionConformance.lean b/conformance/HexInterval/PayloadSessionConformance.lean
index d7d15eb91..ae5623c79 100644
--- a/conformance/HexInterval/PayloadSessionConformance.lean
+++ b/conformance/HexInterval/PayloadSessionConformance.lean
@@ -107,6 +107,22 @@ def arenaLimits : PayloadArena.Limits :=
     maxSchema := 10
     maxUses := 8 }
 
+def pairFormat : ReplayFormat :=
+  { role := .fact
+    schema := 1
+    validateBody := fun body =>
+      match body with
+      | [_, 99] => true
+      | _ => false }
+
+def oneCellFormat : ReplayFormat :=
+  { role := .fact
+    schema := 1
+    validateBody := fun body =>
+      match body with
+      | [_] => true
+      | _ => false }
+
 def goodPlan (request : RuleRequest Nat) : Plan Nat :=
   match request.writes with
   | [target] =>
@@ -126,7 +142,31 @@ def goodPackage : Package Nat :=
     cache := ()
     operations := #[sourceOperation, mysteryOperation]
     handlers :=
-      #[Handler.statelessPlanned (registration goodKey) goodPlan] }
+      #[Handler.statelessPlanned (registration goodKey) goodPlan #[pairFormat]] }
+
+def undeclaredPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers := #[Handler.statelessPlanned (registration goodKey) goodPlan] }
+
+def malformedPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration goodKey) goodPlan #[oneCellFormat]] }
+
+def duplicateFormatPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration goodKey) goodPlan
+          #[pairFormat,
+            { role := .fact
+              schema := 1
+              validateBody := fun _ => true }]] }
 
 def lateExtraPlan (request : RuleRequest Nat) : Plan Nat :=
   if request.action.node == node 1 then
@@ -168,7 +208,8 @@ def badReplyPackage : Package Nat :=
     cache := ()
     operations := #[sourceOperation, mysteryOperation]
     handlers :=
-      #[Handler.statelessPlanned (registration badReplyKey) badReplyPlan] }
+      #[Handler.statelessPlanned (registration badReplyKey) badReplyPlan
+          #[oneCellFormat]] }
 
 def badPayloadPlan (request : RuleRequest Nat) : Plan Nat :=
   match request.writes with
@@ -185,7 +226,8 @@ def badPayloadPackage : Package Nat :=
     cache := ()
     operations := #[sourceOperation, mysteryOperation]
     handlers :=
-      #[Handler.statelessPlanned (registration badPayloadKey) badPayloadPlan] }
+      #[Handler.statelessPlanned (registration badPayloadKey) badPayloadPlan
+          #[oneCellFormat]] }
 
 def barePackage : Package Nat :=
   { Cache := Unit
@@ -395,6 +437,92 @@ def arenaAwarePackage : Package Nat :=
       4 ≤ payloadLimits.maxEntries && 8 ≤ payloadLimits.maxUses &&
         8 ≤ payloadLimits.maxDraftCells }
 
+/-- Two unrelated opaque function packages deliberately assign different
+formats to the same role-local schema number. -/
+def leftOp : OpKey := { name := "payload-session.opaque-left" }
+def rightOp : OpKey := { name := "payload-session.opaque-right" }
+def leftKey : RuleKey := { name := "payload-session.opaque-left.forward" }
+def rightKey : RuleKey := { name := "payload-session.opaque-right.forward" }
+
+def leftOperation : Operation :=
+  { key := leftOp, inputs := [real], output := real }
+
+def rightOperation : Operation :=
+  { key := rightOp, inputs := [real], output := real }
+
+def opaqueRegistration (key : RuleKey) (head : OpKey) : Registration :=
+  { key
+    head
+    kind := .forward
+    watches := [.argument 0]
+    writes := [.result] }
+
+def leftFormat : ReplayFormat :=
+  { role := .fact
+    schema := 7
+    validateBody := fun body =>
+      match body with
+      | [11] => true
+      | _ => false }
+
+def rightFormat : ReplayFormat :=
+  { role := .fact
+    schema := 7
+    validateBody := fun body =>
+      match body with
+      | [22, 23] => true
+      | _ => false }
+
+def opaquePlan (fact label : Nat) (body : List Nat)
+    (request : RuleRequest Nat) : Plan Nat :=
+  match request.writes with
+  | [target] =>
+      { outcome :=
+          .success [{ node := target, fact, payload := payload label }] [] {}
+        drafts :=
+          [{ label := payload label, role := .fact, schema := 7, body }] }
+  | _ => { outcome := .failed 5, drafts := [] }
+
+def leftPackage : Package Nat :=
+  { Cache := Nat
+    cache := 0
+    operations := #[sourceOperation, leftOperation]
+    handlers :=
+      #[{ registration := opaqueRegistration leftKey leftOp
+          replayFormats := #[leftFormat]
+          invoke := fun cache request => (opaquePlan 11 711 [11] request, cache + 1) }] }
+
+def rightPackage : Package Nat :=
+  { Cache := List Nat
+    cache := []
+    operations := #[rightOperation]
+    requiredOperations := #[sourceOperation]
+    handlers :=
+      #[{ registration := opaqueRegistration rightKey rightOp
+          replayFormats := #[rightFormat]
+          invoke := fun cache request =>
+            (opaquePlan 22 722 [22, 23] request,
+              request.action.node.index :: cache) }] }
+
+def wrongRightPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[rightOperation]
+    requiredOperations := #[sourceOperation]
+    handlers :=
+      #[Handler.statelessPlanned (opaqueRegistration rightKey rightOp)
+          (opaquePlan 22 722 [11]) #[rightFormat]] }
+
+def opaqueProgram : Program :=
+  { operations := #[sourceOperation, leftOperation, rightOperation]
+    nodes :=
+      #[instruction 0,
+        instruction 1 [node 0],
+        instruction 2 [node 0]] }
+
+def opaqueLimits : Propagator.Limits :=
+  { limits with maxOperations := 6, maxRules := 4 }
+
 def start (package : Package Nat)
     (payloadLimits : PayloadArena.Limits := arenaLimits) :
     Except PayloadSession.StartError (PayloadSession.Session Nat) :=
@@ -449,11 +577,21 @@ def oversizedProgram : Program :=
   { program with
     nodes := program.nodes.push (instruction 1 [node 0]) |>.push (instruction 1 [node 0]) }
 
+def startOpaque (right : Package Nat) :
+    Except PayloadSession.StartError (PayloadSession.Session Nat) :=
+  PayloadSession.Session.start factDomain opaqueProgram #[leftPackage, right]
+    #[3, 0, 0] opaqueLimits arenaLimits
+
 def goodRun? : Option (PayloadSession.Run Nat) :=
   match start goodPackage with
   | .ok session => some (session.drive 8)
   | .error _ => none
 
+def opaqueRun? : Option (PayloadSession.Run Nat) :=
+  match startOpaque rightPackage with
+  | .ok session => some (session.drive 8)
+  | .error _ => none
+
 -- Separate replies may use the same local label; the session commits distinct
 -- arena entries and only relocated global identifiers reach provenance.
 #guard
@@ -481,6 +619,87 @@ def goodRun? : Option (PayloadSession.Run Nat) :=
         | _, _, _, _ => false
   | none => false
 
+-- A replay format is local to its rule.  These unrelated packages reuse
+-- `(fact, 7)` but validate different bodies and retain distinct full keys.
+#guard
+  match opaqueRun? with
+  | some run =>
+      run.stop == .saturated && run.session.engine.history.size == 2 &&
+        run.session.arena.entries.size == 2 &&
+        match run.session.arena.entry? (payload 0) .fact,
+            run.session.arena.entry? (payload 1) .fact with
+        | some left, some right =>
+            left.replayKey ==
+                { rule := leftKey, role := .fact, schema := 7 } &&
+              right.replayKey ==
+                { rule := rightKey, role := .fact, schema := 7 } &&
+              left.body == [11] && right.body == [22, 23] &&
+              (run.session.registry.packages[0]?).any
+                (fun package => package.invocations == 1) &&
+              (run.session.registry.packages[1]?).any
+                (fun package => package.invocations == 1)
+        | _, _ => false
+  | none => false
+
+-- The right package cannot borrow the left package's validator merely because
+-- both use the same local schema number.
+#guard
+  match startOpaque wrongRightPackage with
+  | .ok session =>
+      match session.advance with
+      | .advanced afterLeft =>
+          match afterLeft.advance with
+          | .invalidPayload (.invalidBody key) stopped =>
+              key ==
+                  { rule := rightKey, role := .fact, schema := 7 } &&
+                stopped.arena.entries.size == 1 &&
+                stopped.engine.history.size == 1 && !stopped.live
+          | _ => false
+      | _ => false
+  | .error _ => false
+
+-- Duplicate local declarations are rejected during registry assembly.
+#guard
+  match start duplicateFormatPackage with
+  | .error (.registry (.duplicateFormat key)) =>
+      key == { rule := goodKey, role := .fact, schema := 1 }
+  | _ => false
+
+-- A used draft must name a declared role/schema pair and satisfy that
+-- format's bounded structural validator.
+#guard
+  match start undeclaredPackage with
+  | .ok session =>
+      match session.advance with
+      | .invalidPayload (.undeclaredFormat key) stopped =>
+          key == { rule := goodKey, role := .fact, schema := 1 } &&
+            stopped.arena.entries.isEmpty &&
+            stopped.engine.history.isEmpty && !stopped.live
+      | _ => false
+  | .error _ => false
+
+#guard
+  match start malformedPackage with
+  | .ok session =>
+      match session.advance with
+      | .invalidPayload (.invalidBody key) stopped =>
+          key == { rule := goodKey, role := .fact, schema := 1 } &&
+            stopped.arena.entries.isEmpty &&
+            stopped.engine.history.isEmpty && !stopped.live
+      | _ => false
+  | .error _ => false
+
+-- Generic body bounds run before a package-owned validator.
+#guard
+  match start malformedPackage { arenaLimits with maxBodyCells := 1 } with
+  | .ok session =>
+      match session.advance with
+      | .payloadResource .bodyCells stopped =>
+          stopped.arena.entries.isEmpty &&
+            stopped.engine.history.isEmpty && !stopped.live
+      | _ => false
+  | .error _ => false
+
 -- A fully frozen prospective arena is discarded when engine admission rejects
 -- an undeclared write.
 #guard
diff --git a/progress/20260728T054228Z.md b/progress/20260728T054228Z.md
new file mode 100644
index 000000000..82cf753de
--- /dev/null
+++ b/progress/20260728T054228Z.md
@@ -0,0 +1,35 @@
+# Package-owned replay formats
+
+## Accomplished
+
+- Added cache-independent replay formats to each propagator handler, keyed by
+  its stable rule, payload role, and rule-local schema.
+- Paired every planned invocation with the exact selected handler's immutable
+  replay snapshot.
+- Made checked arena freezing run generic proposal and body preflight before
+  package format validation, with atomic failure for wrong owners, undeclared
+  formats, and malformed bodies.
+- Rejected duplicate role/schema declarations during bounded registry
+  assembly and counted formats against registry metadata limits.
+- Added conformance with two unrelated opaque function packages that safely
+  reuse one local schema number but accept incompatible body formats.
+- Documented that format validation checks representation shape only and that
+  semantic replay must independently decode and recheck the rule theorem.
+- Built the focused arena, registry, session, conformance, and complete
+  `HexIntervalExperiment` targets successfully.
+
+## Current frontier
+
+The generic engine can now retain and structurally dispatch arbitrary
+package-owned replay formats without interpreting a function or arithmetic
+operation. It does not yet have typed decoders or Mathlib soundness replay.
+
+## Next step
+
+Use the same invocation snapshot and checked-freeze call in the policy-owned
+session, then implement one package-owned semantic replay canary in the
+Mathlib bridge.
+
+## Blockers
+
+None.

From 830d0fe604c7eecd84ce0e56747a9c6cea4b6a09 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Tue, 28 Jul 2026 05:50:06 +0000
Subject: [PATCH 2/9] Register dyadic replay formats

Includes progress/20260728T054939Z.md.
---
 HexInterval/Experiment/DyadicRules.lean       | 53 +++++++----
 HexInterval/Experiment/PackageRegistry.lean   |  8 +-
 HexInterval/Experiment/PayloadArena.lean      |  9 +-
 HexInterval/Experiment/Propagator.lean        |  6 +-
 HexInterval/SPEC/hex-interval.md              | 14 +++
 .../HexInterval/DyadicRulesConformance.lean   | 87 +++++++++++++++++--
 .../PayloadSessionConformance.lean            | 25 ++++--
 progress/20260728T054939Z.md                  | 37 ++++++++
 progress/20260728T055344Z.md                  | 18 ++++
 9 files changed, 220 insertions(+), 37 deletions(-)
 create mode 100644 progress/20260728T054939Z.md
 create mode 100644 progress/20260728T055344Z.md

diff --git a/HexInterval/Experiment/DyadicRules.lean b/HexInterval/Experiment/DyadicRules.lean
index 3b80b6a5b..031cd71be 100644
--- a/HexInterval/Experiment/DyadicRules.lean
+++ b/HexInterval/Experiment/DyadicRules.lean
@@ -203,10 +203,11 @@ structure Config where
 
 /-! ## Reply-local proof payloads
 
-Labels distinguish uses only within one callback reply.  Version-zero recipes
-have empty bodies: after freezing, replay dispatch is determined by the
-engine-owned origin rule, semantic role, and schema.  This deliberately avoids
-a second central recipe tag alongside `PayloadArena.Entry.origin`.
+Labels distinguish uses only within one callback reply. Payload-schema-zero
+recipes have empty bodies: after freezing, replay dispatch is determined by
+the engine-owned origin rule compatibility epoch, semantic role, and payload
+schema. This deliberately avoids a second central recipe tag alongside
+`PayloadArena.Entry.origin`.
 -/
 
 def factLabel : PayloadId := { index := 0 }
@@ -217,6 +218,21 @@ def emptyDraft (label : PayloadId) (role : PayloadArena.Role) :
     PayloadArena.Draft :=
   { label, role, schema := 0, body := [] }
 
+/-- Payload-schema-zero dyadic recipes have no body cells. Exact empty-list
+matching rejects trailing data instead of silently accepting a future recipe
+variant. -/
+def emptyFormat (role : PayloadArena.Role) : ReplayFormat :=
+  { role
+    schema := 0
+    validateBody := fun body =>
+      match body with
+      | [] => true
+      | _ :: _ => false }
+
+def factHandler (registration : Registration)
+    (invoke : RuleRequest Fact -> Plan Fact) : Handler Fact Unit :=
+  Handler.statelessPlanned registration invoke #[emptyFormat .fact]
+
 def withoutPayloads (outcome : Outcome Fact) : Plan Fact :=
   { outcome, drafts := [] }
 
@@ -461,18 +477,18 @@ def arithmeticPackage (config : Config) (real : DomainId) : Package Fact :=
     cache := ()
     operations := arithmeticOperations real
     handlers :=
-      #[Handler.statelessPlanned oneForward (invokeOneForward config),
-        Handler.statelessPlanned negForward (invokeNegForward config),
-        Handler.statelessPlanned negBackward (invokeNegBackward config),
-        Handler.statelessPlanned subForward (invokeSubForward config),
-        Handler.statelessPlanned subLeft (invokeSubLeft config),
-        Handler.statelessPlanned subRight (invokeSubRight config),
-        Handler.statelessPlanned mulForward (invokeMulForward config),
-        Handler.statelessPlanned mulLeft (invokeMulLeft config),
-        Handler.statelessPlanned mulRight (invokeMulRight config),
-        Handler.statelessPlanned squareForward (invokeSquareForward config),
-        Handler.statelessPlanned reciprocalForward (invokeReciprocalForward config),
-        Handler.statelessPlanned reciprocalBackward (invokeReciprocalBackward config)]
+      #[factHandler oneForward (invokeOneForward config),
+        factHandler negForward (invokeNegForward config),
+        factHandler negBackward (invokeNegBackward config),
+        factHandler subForward (invokeSubForward config),
+        factHandler subLeft (invokeSubLeft config),
+        factHandler subRight (invokeSubRight config),
+        factHandler mulForward (invokeMulForward config),
+        factHandler mulLeft (invokeMulLeft config),
+        factHandler mulRight (invokeMulRight config),
+        factHandler squareForward (invokeSquareForward config),
+        factHandler reciprocalForward (invokeReciprocalForward config),
+        factHandler reciprocalBackward (invokeReciprocalBackward config)]
     acceptsLimits := fun _ limits _ =>
       config.maxReciprocalEffort ≤ limits.maxEffort &&
         config.reciprocalPrecisionsAllowed &&
@@ -488,9 +504,10 @@ def centeredPackage (config : Config) (real : DomainId) : Package Fact :=
     operations := centeredOperations real
     requiredOperations := centeredRequirements real
     handlers :=
-      #[Handler.statelessPlanned centeredForward (invokeCenteredForward config),
+      #[factHandler centeredForward (invokeCenteredForward config),
         Handler.statelessDroppingDrafts centeredSplit invokeCenteredSplit,
-        Handler.statelessPlanned centeredInstantiate invokeCenteredInstantiate]
+        Handler.statelessPlanned centeredInstantiate invokeCenteredInstantiate
+          #[emptyFormat .instance, emptyFormat .equality]]
     acceptsLimits := fun _ limits _ =>
       4 ≤ limits.maxObservationValue &&
         71 ≤ limits.maxDiagnosticValue &&
diff --git a/HexInterval/Experiment/PackageRegistry.lean b/HexInterval/Experiment/PackageRegistry.lean
index 38989ba29..35db72258 100644
--- a/HexInterval/Experiment/PackageRegistry.lean
+++ b/HexInterval/Experiment/PackageRegistry.lean
@@ -40,9 +40,11 @@ structure Plan (Fact : Type) where
   outcome : Outcome Fact
   drafts : List PayloadArena.Draft
 
-/-- One cache-independent, rule-local replay representation.  The validator is
-called only after generic arena preflight has bounded the draft and its body.
-It checks representation shape, not mathematical soundness. -/
+/-- One cache-independent replay representation local to the owning handler's
+exact `RuleKey` compatibility epoch.  Its numeric schema is a recipe variant
+inside that epoch.  The validator is called only after generic arena preflight
+has bounded the draft and its body. It checks representation shape, not
+mathematical soundness. -/
 structure ReplayFormat where
   role : PayloadArena.Role
   schema : Nat
diff --git a/HexInterval/Experiment/PayloadArena.lean b/HexInterval/Experiment/PayloadArena.lean
index ea48f0265..51426440b 100644
--- a/HexInterval/Experiment/PayloadArena.lean
+++ b/HexInterval/Experiment/PayloadArena.lean
@@ -36,7 +36,8 @@ inductive Role where
   deriving DecidableEq, Repr
 
 /-- One package-produced recipe.  `label` is local to this reply, while
-`schema` selects the package-owned decoder for the opaque body. -/
+`schema` selects a package-owned body variant within the originating
+`RuleKey.schema` compatibility epoch. -/
 structure Draft where
   label : PayloadId
   role : Role
@@ -53,8 +54,10 @@ structure Entry where
   body : List Nat
   deriving Repr
 
-/-- The immutable dispatch address for semantic replay.  The numeric schema
-is local to one rule and role; unrelated handlers may deliberately reuse it. -/
+/-- The immutable dispatch address for semantic replay.  `rule.schema` is the
+handler/theorem compatibility epoch; this structure's numeric `schema` is a
+recipe variant local to that exact rule and role.  Dispatch is exact on all
+three fields, with no newest-version or schema-only fallback. -/
 structure ReplayKey where
   rule : RuleKey
   role : Role
diff --git a/HexInterval/Experiment/Propagator.lean b/HexInterval/Experiment/Propagator.lean
index 4722bf324..8e8dc554d 100644
--- a/HexInterval/Experiment/Propagator.lean
+++ b/HexInterval/Experiment/Propagator.lean
@@ -147,8 +147,10 @@ end Program
 
 /-! # Rule registration -/
 
-/-- Stable rule name.  `schema` versions the proof payload understood by the
-companion checker. -/
+/-- Stable rule name and compatibility epoch.  `schema` versions the complete
+handler/theorem contract; replay requires this exact key and never falls back
+to a newer epoch.  A payload's own schema is a separate recipe variant within
+this epoch. -/
 structure RuleKey where
   name : String
   schema : Nat := 1
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 479ed3b8f..b9bb04dca 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -1029,6 +1029,13 @@ reuse the same role and local schema number without sharing a validator.
 Registry assembly rejects duplicate `(role, schema)` declarations within a
 handler, and counts declarations against its metadata bound.
 
+There are two independent version axes. `RuleKey.schema` is the compatibility
+epoch for the complete handler and companion theorem contract. The payload
+`schema` in a draft or arena entry is a recipe variant within that exact rule
+epoch and semantic role. Replay requires an exact match on the whole
+`(RuleKey, role, payload schema)` address. It never selects the newest
+`RuleKey.schema`, and it never dispatches from a payload schema alone.
+
 `PayloadSession.Session` has a private constructor and its checked start owns
 the matching engine, registry, arena, and arena limits; the bounded `Run`
 result also has a private constructor, so its stop classification can only
@@ -1278,6 +1285,10 @@ only from `origin.key`, avoiding two stored identities which could disagree.
 The session now performs package-owned format lookup and bounded body-shape
 validation under the full `(RuleKey, role, schema)` key. Typed decoding, typed
 atom encodings, byte limits, and semantic replay are still missing.
+The first real dyadic packages declare payload schema `0` separately for each
+fact, instance, or equality handler. Each body validator accepts exactly the
+empty list and rejects every trailing cell; the rule key still distinguishes
+the theorem epoch and owner.
 Instantiation family labels and custom split-reason numbers also remain
 untyped representation gaps. The FIFO session turns any positive
 compatibility callback whose local identifier lacks a draft, or whose draft
@@ -2351,6 +2362,9 @@ typical, boundary, and adversarial inputs. In particular it includes:
   format failure after a previously committed invocation leave no partial
   current transaction, while generic body-resource refusal precedes package
   validation;
+- real dyadic fact and instantiation packages running through the private
+  proof session with exact empty-body schema `0` declarations, including
+  rejection of a trailing body cell and distinct rule-epoch ownership;
 - an anchor-local opaque shape rule which distinguishes `x * (one - x)` from
   products with a reversed difference or a different repeated input, proposes
   the exact existing node identifiers while receiving no fact inputs, repeats
diff --git a/conformance/HexInterval/DyadicRulesConformance.lean b/conformance/HexInterval/DyadicRulesConformance.lean
index d5f3ffa2b..be6b092f4 100644
--- a/conformance/HexInterval/DyadicRulesConformance.lean
+++ b/conformance/HexInterval/DyadicRulesConformance.lean
@@ -5,6 +5,7 @@ Authors: Kim Morrison
 -/
 
 import HexInterval.Experiment.DyadicRules
+import HexInterval.Experiment.PayloadSession
 import HexInterval.Experiment.PolicyDriver
 
 /-!
@@ -37,7 +38,7 @@ def config : Config :=
 abbrev ConcreteRegistry := Propagator.Registry Fact
 
 def limits : Experiment.Propagator.Limits :=
-  { maxOperations := 16
+  { maxOperations := 24
     maxNodes := 32
     maxRules := 16
     maxArity := 4
@@ -330,6 +331,51 @@ def payloadLimits : PayloadArena.Limits :=
     maxSchema := 0
     maxUses := 3 }
 
+def trailingPayloadLimits : PayloadArena.Limits :=
+  { payloadLimits with maxBodyCells := 1 }
+
+def proofPayloadLimits : PayloadArena.Limits :=
+  { maxEntries := 8
+    maxBodyCells := 0
+    maxAtom := 0
+    maxSchema := 0
+    maxUses := PayloadSession.requiredUses limits }
+
+def proofProgram : Program :=
+  { operations := allOperations
+    nodes := #[instruction 0] }
+
+def proofSession? : Option (PayloadSession.Session Fact) :=
+  match PayloadSession.Session.start
+      (DyadicInterval.factDomain endpointLimit) proofProgram
+      #[arithmeticPackage config real, centeredPackage config real]
+      #[DyadicInterval.Fact.whole] limits proofPayloadLimits with
+  | .ok session => some session
+  | .error _ => none
+
+def proofRun? : Option (PayloadSession.Run Fact) := do
+  let session <- proofSession?
+  pure (session.drive 8)
+
+-- A real dyadic function package crosses the private proof-session boundary;
+-- its empty payload-schema-zero body is checked under the exact rule epoch and then
+-- retained in provenance.
+#guard
+  match proofRun? with
+  | some run =>
+      run.stop == .saturated && run.session.complete &&
+        run.session.engine.history.size == 1 &&
+        run.session.arena.entries.size == 1 &&
+        run.session.arena.bodyCells == 0 &&
+        exactFact run.session.engine 0 (finite 1 false 1 false) &&
+        match run.session.arena.entry? { index := 0 } .fact with
+        | some entry =>
+            entry.replayKey ==
+                { rule := oneForwardKey, role := .fact, schema := 0 } &&
+              oneForwardKey.schema == 1 && entry.body.isEmpty
+        | none => false
+  | none => false
+
 def ruleIdFrom? (key : RuleKey) : Nat -> List Registration -> Option RuleId
   | _, [] => none
   | index, registration :: registrations =>
@@ -393,17 +439,26 @@ def ownsV0 (arena : PayloadArena.Arena) (payload : PayloadId)
           plannedRequest? registry 7 oneForwardKey (node 1) .forward [node 1],
           plannedRequest? registry 8 centeredInstantiateKey (node 3) .instantiate [] with
       | some factRequest, some instanceRequest =>
-          let (factPlan, registry) := registry.invokePlanned factRequest
-          match PayloadArena.freeze payloadLimits .empty factRequest.action
+          let (factInvocation, registry) := registry.invokePlanned factRequest
+          let factReplay := factInvocation.replay
+          let factPlan := factInvocation.plan
+          match PayloadArena.freezeChecked payloadLimits .empty factRequest.action
+              factReplay.rule factReplay.validateDraft
               factPlan.outcome factPlan.drafts with
           | .ready factArena (.success [candidate] [] _) =>
-              let (instancePlan, _) := registry.invokePlanned instanceRequest
-              match PayloadArena.freeze payloadLimits factArena instanceRequest.action
+              let (instanceInvocation, _) := registry.invokePlanned instanceRequest
+              let instanceReplay := instanceInvocation.replay
+              let instancePlan := instanceInvocation.plan
+              match PayloadArena.freezeChecked payloadLimits factArena
+                  instanceRequest.action instanceReplay.rule
+                  instanceReplay.validateDraft
                   instancePlan.outcome instancePlan.drafts with
               | .ready arena (.success [] [.instantiate request] _) =>
                   match request.equalities with
                   | [equality] =>
-                      candidate.payload.index == 0 &&
+                      factReplay.rule == oneForwardKey &&
+                        instanceReplay.rule == centeredInstantiateKey &&
+                        candidate.payload.index == 0 &&
                         request.payload.index == 1 &&
                         equality.payload.index == 2 &&
                         arena.entries.size == 3 && arena.bodyCells == 0 &&
@@ -415,6 +470,26 @@ def ownsV0 (arena : PayloadArena.Arena) (payload : PayloadId)
           | _ => false
       | _, _ => false
 
+-- The real payload-schema-zero fact format rejects a trailing cell after generic
+-- body and atom preflight has accepted the bounded draft.
+#guard
+  match registry? with
+  | some registry =>
+      match plannedRequest? registry 9 oneForwardKey (node 1) .forward [node 1] with
+      | some request =>
+          let (invocation, _) := registry.invokePlanned request
+          match PayloadArena.freezeChecked trailingPayloadLimits .empty request.action
+              invocation.replay.rule invocation.replay.validateDraft
+              invocation.plan.outcome
+              [{ label := factLabel, role := .fact, schema := 0, body := [0] }] with
+          | .invalid (.invalidBody key) arena =>
+              key ==
+                  { rule := oneForwardKey, role := .fact, schema := 0 } &&
+                arena.entries.isEmpty
+          | _ => false
+      | none => false
+  | none => false
+
 -- The anchor-local match remains fresh after its own append-only extension.
 -- Selecting it again is a structural duplicate, and the matcher is not
 -- spuriously requeued as a whole-program dependency.
diff --git a/conformance/HexInterval/PayloadSessionConformance.lean b/conformance/HexInterval/PayloadSessionConformance.lean
index ae5623c79..ab8832052 100644
--- a/conformance/HexInterval/PayloadSessionConformance.lean
+++ b/conformance/HexInterval/PayloadSessionConformance.lean
@@ -318,7 +318,19 @@ def nestedPackage : Package Nat :=
     cache := ()
     operations := #[sourceOperation, mysteryOperation]
     handlers :=
-      #[Handler.statelessPlanned (registration nestedKey) nestedPlan] }
+      #[Handler.statelessPlanned (registration nestedKey) nestedPlan
+          #[{ role := .instance
+              schema := 2
+              validateBody := fun body =>
+                match body with
+                | [_] => true
+                | _ => false },
+            { role := .equality
+              schema := 3
+              validateBody := fun body =>
+                match body with
+                | [_] => true
+                | _ => false }]] }
 
 def nestedUsesPlan (request : RuleRequest Nat) : Plan Nat :=
   { outcome :=
@@ -432,7 +444,7 @@ def arenaAwarePackage : Package Nat :=
     cache := ()
     operations := #[sourceOperation, mysteryOperation]
     handlers :=
-      #[Handler.statelessPlanned (registration goodKey) goodPlan]
+      #[Handler.statelessPlanned (registration goodKey) goodPlan #[pairFormat]]
     acceptsLimits := fun _ _ payloadLimits =>
       4 ≤ payloadLimits.maxEntries && 8 ≤ payloadLimits.maxUses &&
         8 ≤ payloadLimits.maxDraftCells }
@@ -653,7 +665,8 @@ def opaqueRun? : Option (PayloadSession.Run Nat) :=
               key ==
                   { rule := rightKey, role := .fact, schema := 7 } &&
                 stopped.arena.entries.size == 1 &&
-                stopped.engine.history.size == 1 && !stopped.live
+                stopped.engine.history.size == 1 && stopped.live &&
+                stopped.droppedWork && !stopped.complete
           | _ => false
       | _ => false
   | .error _ => false
@@ -674,7 +687,8 @@ def opaqueRun? : Option (PayloadSession.Run Nat) :=
       | .invalidPayload (.undeclaredFormat key) stopped =>
           key == { rule := goodKey, role := .fact, schema := 1 } &&
             stopped.arena.entries.isEmpty &&
-            stopped.engine.history.isEmpty && !stopped.live
+            stopped.engine.history.isEmpty && stopped.live &&
+            stopped.droppedWork && !stopped.complete
       | _ => false
   | .error _ => false
 
@@ -685,7 +699,8 @@ def opaqueRun? : Option (PayloadSession.Run Nat) :=
       | .invalidPayload (.invalidBody key) stopped =>
           key == { rule := goodKey, role := .fact, schema := 1 } &&
             stopped.arena.entries.isEmpty &&
-            stopped.engine.history.isEmpty && !stopped.live
+            stopped.engine.history.isEmpty && stopped.live &&
+            stopped.droppedWork && !stopped.complete
       | _ => false
   | .error _ => false
 
diff --git a/progress/20260728T054939Z.md b/progress/20260728T054939Z.md
new file mode 100644
index 000000000..36db1d854
--- /dev/null
+++ b/progress/20260728T054939Z.md
@@ -0,0 +1,37 @@
+# Replay formats on the hardened payload session
+
+## Accomplished
+
+- Rebased package-owned replay formats onto the hardened payload session.
+- Preserved the hardened recovery rule for malformed evidence: discard the
+  prospective arena, clear the reply through a failed transition, retain a
+  live session, and mark dropped work.
+- Declared exact payload-schema-zero formats for every real dyadic fact,
+  instance, and equality handler.
+- Made the schema-zero validator accept only an empty body and added a checked
+  rejection of a trailing cell after generic body preflight.
+- Ran a real dyadic package through the private proof session and retained its
+  frozen entry under the owning rule, role, and payload schema.
+- Documented the independent version axes: `RuleKey.schema` is the
+  handler/theorem compatibility epoch, while payload `schema` is a recipe
+  variant inside that exact epoch. Replay has no newest-version or schema-only
+  fallback.
+- Preserved the two unrelated opaque-package tests and updated their malformed
+  format expectations for the hardened session.
+- Built the focused arena, registry, session, dyadic-rule, conformance, and
+  complete `HexIntervalExperiment` targets successfully.
+
+## Current frontier
+
+Real and opaque arbitrary-function packages now use the same checked
+package-owned format path. Structural validation still does not establish the
+mathematical meaning of an entry.
+
+## Next step
+
+Carry the exact replay snapshot through the private policy session, then add a
+Mathlib companion canary that decodes an entry and reapplies its rule theorem.
+
+## Blockers
+
+None.
diff --git a/progress/20260728T055344Z.md b/progress/20260728T055344Z.md
new file mode 100644
index 000000000..ebc532d99
--- /dev/null
+++ b/progress/20260728T055344Z.md
@@ -0,0 +1,18 @@
+# Accomplished
+
+- Rebased the replay-format work onto `d8ba1794`.
+- Preserved the explicit `*DroppingDrafts` compatibility API names while retaining package-owned replay formats and the real dyadic format migration.
+- Resolved the rebase conflicts and rebuilt the focused interval experiment and conformance targets successfully.
+
+# Current frontier
+
+- Package-owned replay formats now validate encoded payloads before invocation, and the dyadic packages exercise the mechanism.
+- Semantic replay of accepted payloads remains future work.
+
+# Next step
+
+- Extend the private-policy session and Mathlib bridge with semantic replay implementations for concrete propagator packages.
+
+# Blockers
+
+- None.

From ec4760b889fa57ef657aaaffb699f43c72ba6468 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Tue, 28 Jul 2026 06:13:01 +0000
Subject: [PATCH 3/9] Seal package replay snapshots

---
 HexInterval/Experiment/PackageRegistry.lean   | 76 +++++++++++++------
 HexInterval/Experiment/PayloadArena.lean      |  9 ++-
 HexInterval/Experiment/PayloadSession.lean    |  3 +-
 HexInterval/Experiment/PolicyFrontier.lean    |  2 +
 HexInterval/Experiment/Propagator.lean        |  5 ++
 HexInterval/SPEC/hex-interval.md              | 35 ++++++---
 bench/HexInterval/IntervalSchedulerSpike.lean |  2 +
 .../DyadicIntervalConformance.lean            |  2 +
 .../HexInterval/DyadicRulesConformance.lean   | 16 ++--
 .../PackageRegistryConformance.lean           | 16 +---
 .../PayloadSessionConformance.lean            | 10 +++
 .../HexInterval/PolicyConformance.lean        |  2 +
 .../HexInterval/PropagatorConformance.lean    |  2 +
 .../HexInterval/StructureViewConformance.lean |  2 +
 progress/20260728T061241Z.md                  | 39 ++++++++++
 15 files changed, 160 insertions(+), 61 deletions(-)
 create mode 100644 progress/20260728T061241Z.md

diff --git a/HexInterval/Experiment/PackageRegistry.lean b/HexInterval/Experiment/PackageRegistry.lean
index 35db72258..b09dff4bd 100644
--- a/HexInterval/Experiment/PackageRegistry.lean
+++ b/HexInterval/Experiment/PackageRegistry.lean
@@ -64,28 +64,48 @@ end ReplayFormat
 /-- Immutable replay metadata selected together with one handler invocation.
 `rule` plus a format's role and numeric schema is the complete dispatch key. -/
 structure ReplaySnapshot where
+  private mk ::
   rule : RuleKey
   formats : Array ReplayFormat
 
+private def makeReplay (rule : RuleKey)
+    (formats : Array ReplayFormat) : ReplaySnapshot :=
+  { rule, formats }
+
 namespace ReplaySnapshot
 
 def validateDraft (snapshot : ReplaySnapshot) (draft : PayloadArena.Draft) :
     Option PayloadArena.Invalid :=
   let key := draft.replayKey snapshot.rule
-  match snapshot.formats.toList.find?
+  match snapshot.formats.find?
       (fun format => format.role == draft.role && format.schema == draft.schema) with
   | none => some (.undeclaredFormat key)
   | some format =>
       if format.validateBody draft.body then none else some (.invalidBody key)
 
+/-- Freeze one plan through the rule owner and body validators carried by this
+single immutable snapshot. Proof-producing sessions use this paired operation
+instead of independently supplying an owner and validator. -/
+def freeze (snapshot : ReplaySnapshot) (limits : PayloadArena.Limits)
+    (arena : PayloadArena.Arena) (origin : Action)
+    (outcome : Outcome Fact) (drafts : List PayloadArena.Draft) :
+    PayloadArena.Result Fact :=
+  PayloadArena.freezeChecked limits arena origin snapshot.rule
+    snapshot.validateDraft outcome drafts
+
 end ReplaySnapshot
 
 /-- A package plan paired with the immutable replay metadata of the exact
 handler that produced it. -/
 structure Invocation (Fact : Type) where
+  private mk ::
   plan : Plan Fact
   replay : ReplaySnapshot
 
+private def makeInvocation (plan : Plan Fact)
+    (replay : ReplaySnapshot) : Invocation Fact :=
+  { plan, replay }
+
 /-- The callback shape shared by direct and session-owned drivers. -/
 abbrev Invoke (Fact Cache : Type) :=
   Cache -> RuleRequest Fact -> Plan Fact × Cache
@@ -101,9 +121,9 @@ abbrev BareInvoke (Fact Cache : Type) :=
 /-- One registration and the only callback allowed to interpret its key. -/
 structure Handler (Fact Cache : Type) where
   registration : Registration
+  invoke : Invoke Fact Cache
   /-- Immutable cache-independent replay representations owned by this rule. -/
   replayFormats : Array ReplayFormat := #[]
-  invoke : Invoke Fact Cache
 
 namespace Handler
 
@@ -176,6 +196,7 @@ structure Route where
 immutable after assembly; invocation updates only one existential package's
 cache and non-semantic invocation counter. -/
 structure Registry (Fact : Type) where
+  private mk ::
   packages : Array (Package Fact)
   operations : Array Operation
   registrations : Array Registration
@@ -194,6 +215,15 @@ def requestMismatch : Nat := 245
 
 end DispatchCode
 
+private def makeRegistry (packages : Array (Package Fact))
+    (operations : Array Operation) (registrations : Array Registration)
+    (routes : Array Route) : Registry Fact :=
+  { packages, operations, registrations, routes }
+
+private def replacePackage (registry : Registry Fact) (index : Nat)
+    (package : Package Fact) : Registry Fact :=
+  { registry with packages := registry.packages.set! index package }
+
 /-- Failure while flattening independently supplied packages. -/
 inductive RegistryError where
   | duplicateOperation (key : OpKey)
@@ -267,10 +297,11 @@ def flatten : Nat -> List (Package Fact) -> Array Operation ->
 
 def preflight (limits : Limits) (packages : Array (Package Fact)) :
     Except RegistryError Unit := do
-  if limits.maxOperations + limits.maxRules < packages.size then
+  if limits.maxRegistryEntries < packages.size then
     throw (.resourceLimit .registryEntries)
   let mut operationCount := 0
   let mut ruleCount := 0
+  let mut replayFormatCount := 0
   let mut metadataCount := 0
   for package in packages do
     operationCount := operationCount + package.operations.size
@@ -279,12 +310,15 @@ def preflight (limits : Limits) (packages : Array (Package Fact)) :
       throw (.resourceLimit .operations)
     if limits.maxRules < ruleCount then
       throw (.resourceLimit .rules)
-    let replayFormatCount :=
+    let packageFormatCount :=
       package.handlers.foldl
         (fun count handler => count + handler.replayFormats.size) 0
+    replayFormatCount := replayFormatCount + packageFormatCount
+    if limits.maxReplayFormats < replayFormatCount then
+      throw (.resourceLimit .replayFormats)
     metadataCount := metadataCount + package.operations.size +
-      package.requiredOperations.size + package.handlers.size + replayFormatCount
-    if limits.maxOperations + limits.maxRules < metadataCount then
+      package.requiredOperations.size + package.handlers.size + packageFormatCount
+    if limits.maxRegistryEntries < metadataCount then
       throw (.resourceLimit .registryEntries)
     if package.operations.any
         (fun operation => !listWithin limits.maxArity operation.inputs) ||
@@ -296,11 +330,11 @@ def preflight (limits : Limits) (packages : Array (Package Fact)) :
       throw (.resourceLimit .arity)
 
 /-- Resource-preflight package metadata before duplicate scans or flattened
-array allocation.  The aggregate metadata cap also bounds external signature
-requirements, replay formats, and empty-package churn.  Assembly order is
-package-major and then handler-major; exact operation and rule keys are unique
-in the snapshot. -/
-def buildWithin (limits : Limits) (packages : Array (Package Fact)) :
+array allocation. Dedicated caps bound total metadata and replay-format
+declarations without borrowing executable operation headroom. Assembly order
+is package-major and then handler-major; exact operation and rule keys are
+unique in the snapshot. -/
+opaque buildWithin (limits : Limits) (packages : Array (Package Fact)) :
     Except RegistryError (Registry Fact) :=
   match preflight limits packages with
   | .error error => .error error
@@ -308,7 +342,7 @@ def buildWithin (limits : Limits) (packages : Array (Package Fact)) :
       match flatten 0 packages.toList #[] #[] #[] with
       | .error error => .error error
       | .ok (operations, registrations, routes) =>
-          .ok { packages, operations, registrations, routes }
+          .ok (makeRegistry packages operations registrations routes)
 
 /-- Resolve a contributed signature by stable key.  The returned value carries
 no `OpId`: compact identifiers belong to the final frontend program, whose
@@ -375,15 +409,16 @@ namespace Registry
 
 /-- A negative plan for a dispatch failure before any callback or replay
 format can be selected. -/
-def failedInvocation (rule : RuleKey) (code : Nat) : Invocation Fact :=
-  { plan := { outcome := .failed code, drafts := [] }
-    replay := { rule, formats := #[] } }
+private def failedInvocation (rule : RuleKey) (code : Nat) : Invocation Fact :=
+  makeInvocation
+    { outcome := .failed code, drafts := [] }
+    (makeReplay rule #[])
 
 /-- Route one engine-owned rule identifier to its package callback and retain
 its reply-local proof drafts together with that handler's replay formats.
 Dispatch uses compact validated indices; it never branches on the semantic
 operation or rule key. Only the selected package cache is replaced. -/
-def invokePlanned (registry : Registry Fact) (request : RuleRequest Fact) :
+opaque invokePlanned (registry : Registry Fact) (request : RuleRequest Fact) :
     Invocation Fact × Registry Fact :=
   match registry.routes[request.action.rule.index]? with
   | none =>
@@ -411,12 +446,9 @@ def invokePlanned (registry : Registry Fact) (request : RuleRequest Fact) :
                       { package with
                         cache := cache
                         invocations := package.invocations + 1 }
-                    ({ plan
-                       replay :=
-                         { rule := handler.registration.key
-                           formats := handler.replayFormats } },
-                      { registry with
-                        packages := registry.packages.set! route.package package })
+                    (makeInvocation plan
+                        (makeReplay handler.registration.key handler.replayFormats),
+                      replacePackage registry route.package package)
 
 /-- Explicitly evidence-discarding adapter for search experiments. A
 proof-producing session must use `invokePlanned` and freeze its drafts before
diff --git a/HexInterval/Experiment/PayloadArena.lean b/HexInterval/Experiment/PayloadArena.lean
index 51426440b..f3f6ae3c0 100644
--- a/HexInterval/Experiment/PayloadArena.lean
+++ b/HexInterval/Experiment/PayloadArena.lean
@@ -388,8 +388,9 @@ def freezeDrafts (arena : Arena) (origin : Action)
     appendDrafts origin arena.entries bounded.drafts
   ({ entries, bodyCells := arena.bodyCells + bounded.cells }, relocations)
 
-/-- Validate and freeze every reply-local payload reference using the exact
-replay-format snapshot selected for the invocation.
+/-- Low-level validation and freezing with an explicitly supplied rule owner
+and draft validator. The package layer pairs those values in one immutable
+snapshot before a proof-producing session calls this operation.
 
 Reply-local body and draft bounds and exact coverage are checked before
 `validateDraft` runs, so a package validator only receives locally bounded,
@@ -433,8 +434,8 @@ def freezeChecked (limits : Limits) (arena : Arena) (origin : Action)
                             .ready prospective outcome
 
 /-- Standalone structural freezing with no package format validation.
-Proof-producing sessions use `freezeChecked` with the selected handler's
-immutable replay snapshot. -/
+Proof-producing sessions instead use the package layer's snapshot-paired
+wrapper. -/
 def freeze (limits : Limits) (arena : Arena) (origin : Action)
     (outcome : Outcome Fact) (drafts : List Draft) : Result Fact :=
   freezeChecked limits arena origin origin.key (fun _ => none) outcome drafts
diff --git a/HexInterval/Experiment/PayloadSession.lean b/HexInterval/Experiment/PayloadSession.lean
index 5a53eb09a..ae4cdc5cd 100644
--- a/HexInterval/Experiment/PayloadSession.lean
+++ b/HexInterval/Experiment/PayloadSession.lean
@@ -242,8 +242,7 @@ opaque Session.advance (session : Session Fact) : Step Fact :=
         | .factResourceLimit budget next =>
             .factResource budget (haltRegistry session next registry)
       else
-        match PayloadArena.freezeChecked session.arenaLimits session.arena
-            request.action replay.rule replay.validateDraft
+        match replay.freeze session.arenaLimits session.arena request.action
             plan.outcome plan.drafts with
         | .invalid error _ =>
             failPayload session engine registry request.action error
diff --git a/HexInterval/Experiment/PolicyFrontier.lean b/HexInterval/Experiment/PolicyFrontier.lean
index 20486bfb2..3a90f449e 100644
--- a/HexInterval/Experiment/PolicyFrontier.lean
+++ b/HexInterval/Experiment/PolicyFrontier.lean
@@ -153,6 +153,8 @@ def engineLimits (workload : Workload) : Experiment.Propagator.Limits :=
   { maxOperations := 3
     maxNodes := nodeCount workload
     maxRules := 2
+    maxRegistryEntries := 8
+    maxReplayFormats := 0
     maxArity := arity
     maxApplications := applications
     maxQueueEntries := 4 * applications
diff --git a/HexInterval/Experiment/Propagator.lean b/HexInterval/Experiment/Propagator.lean
index 8e8dc554d..64c051a52 100644
--- a/HexInterval/Experiment/Propagator.lean
+++ b/HexInterval/Experiment/Propagator.lean
@@ -686,6 +686,7 @@ inductive Resource where
   | actions
   | effort
   | registryEntries
+  | replayFormats
   | acceptedFacts
   | retainedSuggestions
   | outcomeCandidates
@@ -701,6 +702,10 @@ structure Limits where
   maxOperations : Nat
   maxNodes : Nat
   maxRules : Nat
+  /-- Total package metadata cells, independent of executable program size. -/
+  maxRegistryEntries : Nat
+  /-- Total cache-independent proof-replay format declarations. -/
+  maxReplayFormats : Nat
   maxArity : Nat
   maxApplications : Nat
   maxQueueEntries : Nat
diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index b9bb04dca..ed8fdeed0 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -999,6 +999,11 @@ be declared as owned or required.
 `Registry.buildWithin` bounds package and metadata counts plus arities before
 flattening, builds a `Route` from each compact `RuleId` back to its package and
 handler, and rejects undeclared heads and duplicate `OpKey`s or `RuleKey`s.
+The registry constructor is private: callers can inspect a checked snapshot
+but cannot forge inconsistent flattened routes. Executable operations,
+aggregate registry metadata, and replay-format declarations have independent
+limits; adding a proof recipe cannot buy space by relaxing the frontend's
+operation cap.
 Program size and arity are bounded before exact signature lookup. The checked
 session start validates every owned and required signature against the final
 frontend program, runs each package's configuration preflight, and starts the
@@ -1019,7 +1024,9 @@ planned route is proof-producing, but neither it nor
 `Registry.invokeDroppingDrafts` is an authentication boundary: the engine
 still authenticates the pending serial, application, fact values, and
 versions. The explicitly named dropping-drafts adapter discards drafts and
-replay metadata only for search experiments.
+replay metadata only for search experiments. Registry, replay-snapshot, and
+invocation constructors are private; the checked builder and routed invocation
+are their only producers.
 
 Each handler now carries cache-independent replay-format declarations beside
 its registration and callback. A declaration consists of a payload role, a
@@ -1027,7 +1034,8 @@ rule-local numeric schema variant, and a body-shape validator. The immutable
 dispatch key is `(RuleKey, role, schema)`: two unrelated function packages may
 reuse the same role and local schema number without sharing a validator.
 Registry assembly rejects duplicate `(role, schema)` declarations within a
-handler, and counts declarations against its metadata bound.
+handler, and counts declarations against a dedicated replay-format bound as
+well as the aggregate metadata bound.
 
 There are two independent version axes. `RuleKey.schema` is the compatibility
 epoch for the complete handler and companion theorem contract. The payload
@@ -1042,21 +1050,26 @@ result also has a private constructor, so its stop classification can only
 come from session execution. During an invocation, generic arena preflight
 first bounds the number of drafts, body cells, atoms, schemas, and payload
 uses. Only then does the session run the selected package's body validators.
-It rejects an undeclared role/schema pair, a malformed body, or a mismatched
-rule owner without committing the prospective arena or engine outcome.
+The selected immutable `ReplaySnapshot` supplies its rule owner and validator
+to one paired freeze operation, so the proof-producing path cannot mix an
+owner from one package with a validator from another. It rejects an undeclared
+role/schema pair or malformed body without committing the prospective arena or
+engine outcome.
 Package caches may record the failed attempt because they remain non-semantic.
 
 This first format API validates representation shape only. It does not attest
 that a body proves the proposed interval fact, instance, or equality. The
 Mathlib companion must dispatch on the same immutable key, decode the frozen
 entry independently of package cache state, and recheck the corresponding
-rule theorem during semantic replay. A different callback implementation
-under an existing versioned rule schema is compatible only when every retained
-payload still passes that semantic replay. Whether production retains these
-existential snapshots, compiles a dispatch table, adds typed decoders, supports
-hot replacement, or uses another lookup structure remains experimental. The
-older direct registry and engine interfaces remain available for search
-experiments, but proof-producing execution goes through the session.
+rule theorem during semantic replay. Until that companion layer exists, it is
+an explicit compatibility obligation—not a property enforced by this format
+API—that a different callback implementation under an existing versioned rule
+schema leave every retained payload semantically replayable. Whether production
+retains these existential snapshots, compiles a dispatch table, adds typed
+decoders, supports hot replacement, or uses another lookup structure remains
+experimental. The older direct registry and engine interfaces remain available
+for search experiments, but proof-producing execution goes through the
+session.
 
 The explicit registration and validation boundary is fixed. Discovery and
 scheduling above it remain empirical: one arm uses an incremental registry
diff --git a/bench/HexInterval/IntervalSchedulerSpike.lean b/bench/HexInterval/IntervalSchedulerSpike.lean
index ec43a964a..b1c25fce3 100644
--- a/bench/HexInterval/IntervalSchedulerSpike.lean
+++ b/bench/HexInterval/IntervalSchedulerSpike.lean
@@ -101,6 +101,8 @@ def generousLimits (trees depth : Nat) : Limits :=
   { maxOperations := operations.size
     maxNodes := nodeCount
     maxRules := rules.size
+    maxRegistryEntries := operations.size + rules.size
+    maxReplayFormats := 0
     maxArity := 1
     maxApplications := applications
     maxQueueEntries := applications + nodeCount + 1
diff --git a/conformance/HexInterval/DyadicIntervalConformance.lean b/conformance/HexInterval/DyadicIntervalConformance.lean
index 3957d42ac..2a8523d52 100644
--- a/conformance/HexInterval/DyadicIntervalConformance.lean
+++ b/conformance/HexInterval/DyadicIntervalConformance.lean
@@ -494,6 +494,8 @@ private def engineLimits : Limits :=
   { maxOperations := 4
     maxNodes := 4
     maxRules := 0
+    maxRegistryEntries := 4
+    maxReplayFormats := 0
     maxArity := 2
     maxApplications := 0
     maxQueueEntries := 0
diff --git a/conformance/HexInterval/DyadicRulesConformance.lean b/conformance/HexInterval/DyadicRulesConformance.lean
index be6b092f4..40f2f5631 100644
--- a/conformance/HexInterval/DyadicRulesConformance.lean
+++ b/conformance/HexInterval/DyadicRulesConformance.lean
@@ -38,9 +38,11 @@ def config : Config :=
 abbrev ConcreteRegistry := Propagator.Registry Fact
 
 def limits : Experiment.Propagator.Limits :=
-  { maxOperations := 24
+  { maxOperations := 16
     maxNodes := 32
     maxRules := 16
+    maxRegistryEntries := 64
+    maxReplayFormats := 16
     maxArity := 4
     maxApplications := 64
     maxQueueEntries := 256
@@ -442,17 +444,14 @@ def ownsV0 (arena : PayloadArena.Arena) (payload : PayloadId)
           let (factInvocation, registry) := registry.invokePlanned factRequest
           let factReplay := factInvocation.replay
           let factPlan := factInvocation.plan
-          match PayloadArena.freezeChecked payloadLimits .empty factRequest.action
-              factReplay.rule factReplay.validateDraft
+          match factReplay.freeze payloadLimits .empty factRequest.action
               factPlan.outcome factPlan.drafts with
           | .ready factArena (.success [candidate] [] _) =>
               let (instanceInvocation, _) := registry.invokePlanned instanceRequest
               let instanceReplay := instanceInvocation.replay
               let instancePlan := instanceInvocation.plan
-              match PayloadArena.freezeChecked payloadLimits factArena
-                  instanceRequest.action instanceReplay.rule
-                  instanceReplay.validateDraft
-                  instancePlan.outcome instancePlan.drafts with
+              match instanceReplay.freeze payloadLimits factArena
+                  instanceRequest.action instancePlan.outcome instancePlan.drafts with
               | .ready arena (.success [] [.instantiate request] _) =>
                   match request.equalities with
                   | [equality] =>
@@ -478,8 +477,7 @@ def ownsV0 (arena : PayloadArena.Arena) (payload : PayloadId)
       match plannedRequest? registry 9 oneForwardKey (node 1) .forward [node 1] with
       | some request =>
           let (invocation, _) := registry.invokePlanned request
-          match PayloadArena.freezeChecked trailingPayloadLimits .empty request.action
-              invocation.replay.rule invocation.replay.validateDraft
+          match invocation.replay.freeze trailingPayloadLimits .empty request.action
               invocation.plan.outcome
               [{ label := factLabel, role := .fact, schema := 0, body := [0] }] with
           | .invalid (.invalidBody key) arena =>
diff --git a/conformance/HexInterval/PackageRegistryConformance.lean b/conformance/HexInterval/PackageRegistryConformance.lean
index cc41b27b4..71fc978f8 100644
--- a/conformance/HexInterval/PackageRegistryConformance.lean
+++ b/conformance/HexInterval/PackageRegistryConformance.lean
@@ -238,6 +238,8 @@ def limits : Limits :=
   { maxOperations := 8
     maxNodes := 8
     maxRules := 8
+    maxRegistryEntries := 32
+    maxReplayFormats := 8
     maxArity := 2
     maxApplications := 8
     maxQueueEntries := 16
@@ -290,7 +292,7 @@ def shortOperationLimits : Limits :=
   { limits with maxOperations := 3 }
 
 def shortMetadataLimits : Limits :=
-  { limits with maxOperations := 4, maxRules := 4 }
+  { limits with maxRegistryEntries := 8 }
 
 def nullaryLimits : Limits :=
   { limits with maxArity := 0 }
@@ -444,18 +446,6 @@ def policyDriverTypecheck {PolicyState : Type}
             registry.packages.map (fun package => package.invocations) == #[2, 0, 0]
       | _, _, _, _ => false
 
--- A corrupted static route is diagnosed before its unrelated handler can run.
-#guard
-  match registry? with
-  | none => false
-  | some registry =>
-      let corrupted :=
-        { registry with
-          routes := registry.routes.set! 0 { package := 1, handler := 0 } }
-      match (corrupted.invokeDroppingDrafts tickRequest).1 with
-      | .failed code => code == DispatchCode.registryMismatch
-      | _ => false
-
 -- The million-unit number reports work refused before execution; it is not a
 -- claimed cost observation, but it is checked by the separate diagnostic cap.
 -- The engine accepts the boundary value, rejects one above it, and reaches a
diff --git a/conformance/HexInterval/PayloadSessionConformance.lean b/conformance/HexInterval/PayloadSessionConformance.lean
index ab8832052..bb62806e6 100644
--- a/conformance/HexInterval/PayloadSessionConformance.lean
+++ b/conformance/HexInterval/PayloadSessionConformance.lean
@@ -78,6 +78,8 @@ def limits : Propagator.Limits :=
   { maxOperations := 4
     maxNodes := 4
     maxRules := 2
+    maxRegistryEntries := 16
+    maxReplayFormats := 8
     maxArity := 2
     maxApplications := 4
     maxQueueEntries := 8
@@ -678,6 +680,14 @@ def opaqueRun? : Option (PayloadSession.Run Nat) :=
       key == { rule := goodKey, role := .fact, schema := 1 }
   | _ => false
 
+-- Replay declarations have their own cap and cannot borrow operation
+-- headroom.
+#guard
+  match PayloadSession.Session.start factDomain program #[goodPackage] #[3, 0, 0]
+      { limits with maxReplayFormats := 0 } arenaLimits with
+  | .error (.registry (.resourceLimit .replayFormats)) => true
+  | _ => false
+
 -- A used draft must name a declared role/schema pair and satisfy that
 -- format's bounded structural validator.
 #guard
diff --git a/conformance/HexInterval/PolicyConformance.lean b/conformance/HexInterval/PolicyConformance.lean
index 6373b18c9..fce049b38 100644
--- a/conformance/HexInterval/PolicyConformance.lean
+++ b/conformance/HexInterval/PolicyConformance.lean
@@ -73,6 +73,8 @@ def engineLimits : Experiment.Propagator.Limits :=
   { maxOperations := 8
     maxNodes := 8
     maxRules := 8
+    maxRegistryEntries := 24
+    maxReplayFormats := 0
     maxArity := 4
     maxApplications := 16
     maxQueueEntries := 64
diff --git a/conformance/HexInterval/PropagatorConformance.lean b/conformance/HexInterval/PropagatorConformance.lean
index 54f66d52f..0d227f72c 100644
--- a/conformance/HexInterval/PropagatorConformance.lean
+++ b/conformance/HexInterval/PropagatorConformance.lean
@@ -53,6 +53,8 @@ def generous : Limits :=
   { maxOperations := 16
     maxNodes := 64
     maxRules := 16
+    maxRegistryEntries := 32
+    maxReplayFormats := 0
     maxArity := 8
     maxApplications := 128
     maxQueueEntries := 256
diff --git a/conformance/HexInterval/StructureViewConformance.lean b/conformance/HexInterval/StructureViewConformance.lean
index 9ed5f1b37..6b7d8310f 100644
--- a/conformance/HexInterval/StructureViewConformance.lean
+++ b/conformance/HexInterval/StructureViewConformance.lean
@@ -74,6 +74,8 @@ def limits : Limits :=
   { maxOperations := 16
     maxNodes := 32
     maxRules := 8
+    maxRegistryEntries := 24
+    maxReplayFormats := 0
     maxArity := 4
     maxApplications := 32
     maxQueueEntries := 64
diff --git a/progress/20260728T061241Z.md b/progress/20260728T061241Z.md
new file mode 100644
index 000000000..b6a3a0fb1
--- /dev/null
+++ b/progress/20260728T061241Z.md
@@ -0,0 +1,39 @@
+# Sealed package replay snapshots
+
+## Accomplished
+
+- Restacked package-owned replay formats onto the hardened arbitrary-package
+  session.
+- Separated executable operation, aggregate registry metadata, and replay
+  format declaration limits; the dyadic fixture again uses its original
+  operation cap.
+- Made checked registries, replay snapshots, and invocation pairings
+  constructible only inside the registry module.
+- Added a snapshot-owned freeze operation so the proof-producing session
+  cannot independently pair a rule owner with another package's validator.
+- Removed the no-longer-reachable forged-route conformance path and retained
+  malformed-request coverage through checked public APIs.
+- Avoided per-draft array-to-list allocation and restored safe positional
+  construction order for handlers.
+- Added exact replay-format resource conformance and documented semantic replay
+  compatibility as a future companion obligation rather than a current claim.
+- Rebuilt the registry, payload session, real dyadic packages, all directly
+  affected conformance targets, the scheduler bench, and
+  `HexIntervalExperiment` successfully.
+
+## Current frontier
+
+Replay representation shape is now selected and sealed with the exact
+arbitrary propagator invocation. The generic semantic checker can consume the
+same owner/role/schema key, but its branch still needs to be restacked onto
+this sealed API.
+
+## Next step
+
+Restack semantic replay and the private policy session, then make the centered
+auxiliary-expression example pass through instantiation, equality admission,
+propagation, and semantic replay under one session owner.
+
+## Blockers
+
+None.

From d387482db81f9468458b089fda1d33986bab865b Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Wed, 29 Jul 2026 05:33:22 +0000
Subject: [PATCH 4/9] Refresh package replay stack

---
 progress/20260729T053310Z.md | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 progress/20260729T053310Z.md

diff --git a/progress/20260729T053310Z.md b/progress/20260729T053310Z.md
new file mode 100644
index 000000000..2c6738c15
--- /dev/null
+++ b/progress/20260729T053310Z.md
@@ -0,0 +1,27 @@
+# Package-owned replay restack
+
+## Accomplished
+
+- Restacked sealed package-owned replay formats onto the current arbitrary
+  package session.
+- Rebuilt the experiment umbrella and package, session, and dyadic
+  conformance targets.
+- Rechecked the generated conformance target matrix, branch diff, and banned
+  declarations.
+
+## Current frontier
+
+Each arbitrary propagator package can now freeze proof data together with the
+exact package-owned validator selected by rule, semantic role, and schema.
+The structural engine still does not interpret function-specific evidence.
+
+## Next step
+
+Connect the sealed validators to semantic proof replay in the policy-driven
+session, starting with the centered auxiliary-expression canary and then a
+genuinely non-polynomial package.
+
+## Blockers
+
+None.  A lower session review is tightening per-reply resource isolation; this
+branch will be restacked again after that independent change lands.

From bca289e2a22bebd0fe7acfe77ce88f90a3b49105 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Wed, 29 Jul 2026 06:01:04 +0000
Subject: [PATCH 5/9] Migrate package replay resource envelopes

Restack sealed package replay on reply-local payload limits while preserving exact handler formats and recovery semantics.\n\nProgress: progress/20260729T060046Z.md
---
 HexInterval/SPEC/hex-interval.md              |  4 +--
 .../HexInterval/DyadicRulesConformance.lean   |  6 ++--
 .../PayloadSessionConformance.lean            | 12 ++++---
 progress/20260729T060046Z.md                  | 33 +++++++++++++++++++
 4 files changed, 46 insertions(+), 9 deletions(-)
 create mode 100644 progress/20260729T060046Z.md

diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index ed8fdeed0..1a49ae772 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -2373,8 +2373,8 @@ typical, boundary, and adversarial inputs. In particular it includes:
   but retain distinct `(RuleKey, role, schema)` addresses and validate
   incompatible bounded body shapes; undeclared formats, malformed bodies, and
   format failure after a previously committed invocation leave no partial
-  current transaction, while generic body-resource refusal precedes package
-  validation;
+  current transaction, while recoverable reply-local draft-cell refusal
+  precedes package validation;
 - real dyadic fact and instantiation packages running through the private
   proof session with exact empty-body schema `0` declarations, including
   rejection of a trailing body cell and distinct rule-epoch ownership;
diff --git a/conformance/HexInterval/DyadicRulesConformance.lean b/conformance/HexInterval/DyadicRulesConformance.lean
index 40f2f5631..fda0449d5 100644
--- a/conformance/HexInterval/DyadicRulesConformance.lean
+++ b/conformance/HexInterval/DyadicRulesConformance.lean
@@ -334,11 +334,13 @@ def payloadLimits : PayloadArena.Limits :=
     maxUses := 3 }
 
 def trailingPayloadLimits : PayloadArena.Limits :=
-  { payloadLimits with maxBodyCells := 1 }
+  { payloadLimits with maxBodyCells := 1, maxDraftCells := 1 }
 
 def proofPayloadLimits : PayloadArena.Limits :=
-  { maxEntries := 8
+  { maxEntries := PayloadSession.requiredUses limits
     maxBodyCells := 0
+    maxDrafts := PayloadSession.requiredUses limits
+    maxDraftCells := 0
     maxAtom := 0
     maxSchema := 0
     maxUses := PayloadSession.requiredUses limits }
diff --git a/conformance/HexInterval/PayloadSessionConformance.lean b/conformance/HexInterval/PayloadSessionConformance.lean
index bb62806e6..80e81613c 100644
--- a/conformance/HexInterval/PayloadSessionConformance.lean
+++ b/conformance/HexInterval/PayloadSessionConformance.lean
@@ -405,7 +405,7 @@ def recoverPackage : Package Nat :=
     cache := ()
     operations := #[sourceOperation, mysteryOperation]
     handlers :=
-      #[Handler.statelessPlanned (registration recoverKey) recoverPlan] }
+      #[Handler.statelessPlanned (registration recoverKey) recoverPlan #[pairFormat]] }
 
 def excessDrafts : List PayloadArena.Draft :=
   [{ label := payload 0, role := .fact, schema := 1, body := [] },
@@ -714,14 +714,16 @@ def opaqueRun? : Option (PayloadSession.Run Nat) :=
       | _ => false
   | .error _ => false
 
--- Generic body bounds run before a package-owned validator.
+-- A generic reply-local body bound runs before a package-owned validator and
+-- rejects only that reply.
 #guard
-  match start malformedPackage { arenaLimits with maxBodyCells := 1 } with
+  match start malformedPackage { arenaLimits with maxDraftCells := 1 } with
   | .ok session =>
       match session.advance with
-      | .payloadResource .bodyCells stopped =>
+      | .rejectedPayload .draftCells stopped =>
           stopped.arena.entries.isEmpty &&
-            stopped.engine.history.isEmpty && !stopped.live
+            stopped.engine.history.isEmpty && stopped.live &&
+            stopped.droppedWork && !stopped.complete
       | _ => false
   | .error _ => false
 
diff --git a/progress/20260729T060046Z.md b/progress/20260729T060046Z.md
new file mode 100644
index 000000000..4461d20c2
--- /dev/null
+++ b/progress/20260729T060046Z.md
@@ -0,0 +1,33 @@
+# Package replay resource-isolation restack
+
+## Accomplished
+
+- Restacked the sealed package-owned replay snapshots onto payload-session head
+  `2a11ecbc`.
+- Preserved exact `(RuleKey, role, schema)` dispatch for both unrelated opaque
+  packages and every real dyadic schema-zero fact, instance, and equality
+  format.
+- Migrated proof-session envelopes to explicit reply-local draft and
+  draft-cell limits while retaining cumulative entry and body-cell limits.
+- Changed the format-precedence canary to exercise recoverable reply-local
+  draft-cell refusal before package validation.
+- Registered the lower-stack recovery canary's successful reply with the
+  exact selected handler format.
+- Rebuilt the focused arena, registry, payload-session, policy, dyadic, and
+  experiment conformance graph. The generated conformance target matrix,
+  whitespace check, and banned-addition scan pass.
+
+## Current frontier
+
+Package replay remains sealed to the exact invoked handler and now follows the
+payload session's reply-local versus cumulative resource semantics.
+
+## Next step
+
+Restack the private policy session onto this package-replay head, discarding
+duplicate completeness fixes already supplied by the lower payload session
+while preserving centered/equality replay conformance.
+
+## Blockers
+
+None.

From ba5d9043ad67cd4fcbfbdbd8145a1994d29a10c9 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Wed, 29 Jul 2026 06:12:53 +0000
Subject: [PATCH 6/9] Keep invalid replay bodies recoverable

Validate selected package formats before cumulative arena capacity and cover the partly filled-session case.\n\nProgress: progress/20260729T061237Z.md
---
 HexInterval/SPEC/hex-interval.md              |  6 +-
 .../PayloadSessionConformance.lean            | 60 ++++++++++++++++++-
 progress/20260729T061237Z.md                  | 31 ++++++++++
 3 files changed, 94 insertions(+), 3 deletions(-)
 create mode 100644 progress/20260729T061237Z.md

diff --git a/HexInterval/SPEC/hex-interval.md b/HexInterval/SPEC/hex-interval.md
index 1a49ae772..7a69769c0 100644
--- a/HexInterval/SPEC/hex-interval.md
+++ b/HexInterval/SPEC/hex-interval.md
@@ -1185,8 +1185,10 @@ The first executable arena uses an eager but prospective transaction:
 it preflights total-proposal work and the per-reply draft, draft-cell, atom,
 and schema limits, then matches package-local labels exactly against
 package-local drafts and checks duplicate, missing, extra, and wrong-role
-entries. Only a locally bounded, exactly covered reply is compared with
-remaining whole-arena entry and body-cell capacity, relocated to fresh global
+entries. The package-owned path next checks body representation with the
+immutable replay snapshot selected by the exact invocation. Only a locally
+bounded, exactly covered, format-valid reply is compared with remaining
+whole-arena entry and body-cell capacity, relocated to fresh global
 identifiers, and appended to a new arena value. Thus malformed local evidence
 cannot be classified as cumulative exhaustion merely because earlier valid
 replies filled part of the arena. Local preflight returns an opaque
diff --git a/conformance/HexInterval/PayloadSessionConformance.lean b/conformance/HexInterval/PayloadSessionConformance.lean
index 80e81613c..e083d1404 100644
--- a/conformance/HexInterval/PayloadSessionConformance.lean
+++ b/conformance/HexInterval/PayloadSessionConformance.lean
@@ -37,6 +37,7 @@ def bodyKey : RuleKey := { name := "payload-session.mystery.body" }
 def overflowKey : RuleKey := { name := "payload-session.mystery.overflow" }
 def recoverKey : RuleKey := { name := "payload-session.mystery.recover" }
 def lateExtraKey : RuleKey := { name := "payload-session.mystery.late-extra" }
+def lateMalformedKey : RuleKey := { name := "payload-session.mystery.late-malformed" }
 
 def sourceOperation : Operation :=
   { key := sourceOp, inputs := [], output := real }
@@ -196,7 +197,32 @@ def lateExtraPackage : Package Nat :=
     cache := ()
     operations := #[sourceOperation, mysteryOperation]
     handlers :=
-      #[Handler.statelessPlanned (registration lateExtraKey) lateExtraPlan] }
+      #[Handler.statelessPlanned (registration lateExtraKey) lateExtraPlan #[pairFormat]] }
+
+def lateMalformedPlan (request : RuleRequest Nat) : Plan Nat :=
+  if request.action.node == node 1 then
+    goodPlan request
+  else
+    match request.writes with
+    | [target] =>
+        { outcome :=
+            .success
+              [{ node := target, fact := 7, payload := payload 700 }]
+              [] {}
+          drafts :=
+            [{ label := payload 700
+               role := .fact
+               schema := 1
+               body := [4] }] }
+    | _ => { outcome := .failed 1, drafts := [] }
+
+def lateMalformedPackage : Package Nat :=
+  { Cache := Unit
+    cache := ()
+    operations := #[sourceOperation, mysteryOperation]
+    handlers :=
+      #[Handler.statelessPlanned (registration lateMalformedKey)
+          lateMalformedPlan #[pairFormat]] }
 
 def badReplyPlan (_request : RuleRequest Nat) : Plan Nat :=
   { outcome :=
@@ -566,6 +592,14 @@ def lateExtraArena : PayloadArena.Limits :=
     maxDraftCells := 4
     maxUses := 2 }
 
+def lateMalformedArena : PayloadArena.Limits :=
+  { arenaLimits with
+    maxEntries := 1
+    maxBodyCells := 2
+    maxDrafts := 1
+    maxDraftCells := 2
+    maxUses := 1 }
+
 def nestedUsesLimits : Propagator.Limits :=
   { limits with
     maxOutcomeCandidates := 0
@@ -933,6 +967,30 @@ def opaqueRun? : Option (PayloadSession.Run Nat) :=
       | _ => false
   | .error _ => false
 
+-- Package-owned representation validation has the same precedence. After the
+-- first exact body fills the arena, the next locally bounded but malformed
+-- body is rejected by the selected replay snapshot rather than reported as
+-- fatal remaining-capacity exhaustion.
+#guard
+  match startWithin lateMalformedPackage oneReplyLimits lateMalformedArena with
+  | .ok session =>
+      match session.advance with
+      | .advanced first =>
+          first.arena.entries.size == 1 && first.arena.bodyCells == 2 &&
+            first.engine.history.size == 1 &&
+            match first.advance with
+            | .invalidPayload (.invalidBody key) rejected =>
+                key ==
+                    { rule := lateMalformedKey, role := .fact, schema := 1 } &&
+                  rejected.live && rejected.droppedWork && !rejected.complete &&
+                  rejected.arena.entries.size == 1 &&
+                  rejected.arena.bodyCells == 2 &&
+                  rejected.engine.history.size == 1 &&
+                  rejected.engine.metrics.ruleFailures == 1
+            | _ => false
+       | _ => false
+   | .error _ => false
+
 -- Completeness consumes the engine's exact admission plan. Here the two
 -- harmless splits fit, while a closure-relevant retry is the sole capacity
 -- drop (not a structural-depth drop).
diff --git a/progress/20260729T061237Z.md b/progress/20260729T061237Z.md
new file mode 100644
index 000000000..af782dc78
--- /dev/null
+++ b/progress/20260729T061237Z.md
@@ -0,0 +1,31 @@
+# Package replay validation-order restack
+
+## Accomplished
+
+- Restacked sealed replay snapshots onto payload-session head `b6b7d0d6`.
+- Preserved the full checked-freeze order: proposal-use preflight,
+  reply-local bounds, exact draft coverage, selected snapshot body validation,
+  remaining whole-run capacity, then freeze and relocation.
+- Registered the lower-stack late-extra recovery canary with its exact handler
+  format.
+- Added a partly filled private-session canary whose second body fails
+  `lateMalformedKey` representation validation while the first arena/history
+  commit is preserved and the session remains live but incomplete.
+- Preserved all opaque full-key and real dyadic schema-zero replay canaries.
+- Rebuilt the focused arena, registry, payload-session, policy, dyadic, and
+  experiment conformance graph. The generated target matrix, diff check, and
+  banned-addition scan pass.
+
+## Current frontier
+
+Neither structurally malformed nor package-format-invalid evidence can be
+misclassified as fatal cumulative capacity exhaustion after earlier commits.
+
+## Next step
+
+Restack the private policy-owned payload session onto this final replay head
+and retain its centered, equality, and complete choice-class conformance.
+
+## Blockers
+
+None.

From 56617543d02b9f2bb101293362677fd7fd43a594 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Wed, 29 Jul 2026 06:26:03 +0000
Subject: [PATCH 7/9] Refresh package replay after session rebase

Record the refreshed stack and validation in progress/20260729T062552Z.md.
---
 progress/20260729T062552Z.md | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 progress/20260729T062552Z.md

diff --git a/progress/20260729T062552Z.md b/progress/20260729T062552Z.md
new file mode 100644
index 000000000..83ee236de
--- /dev/null
+++ b/progress/20260729T062552Z.md
@@ -0,0 +1,25 @@
+# Accomplished
+
+- Restacked package replay on refreshed payload-session head
+  `cf11011e63be7dad99e4f78c64bfa25f175d7e1a`.
+- Preserved both the upstream registry diagnostic codes and the sealed
+  package-replay snapshot helpers through the only registry conflict.
+- Retained the structural matcher freshness canary alongside the exact
+  schema-zero dyadic format rejection canary.
+- Rechecked the sealed freeze order: payload-use and reply-local bounds, exact
+  coverage, exact package format validation, then cumulative arena capacity.
+- Passed the focused 26-target build graph, conformance-target matrix check,
+  diff hygiene, and trust scan.
+
+# Current frontier
+
+Package-owned replay formats and immutable selected-handler snapshots are
+green on the refreshed payload-session layer.
+
+# Next step
+
+Restack the policy-owned payload session on this refreshed package-replay head.
+
+# Blockers
+
+None.

From ba6ab7f139dc56537c2520f3c43e1f5124d8071d Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Wed, 29 Jul 2026 06:50:05 +0000
Subject: [PATCH 8/9] Refresh package replay after transaction rebase

Record the final lower-stack migration in progress/20260729T064950Z.md.
---
 HexInterval/Experiment/PayloadArena.lean | 34 ++++++++++++------------
 progress/20260729T064950Z.md             | 26 ++++++++++++++++++
 2 files changed, 43 insertions(+), 17 deletions(-)
 create mode 100644 progress/20260729T064950Z.md

diff --git a/HexInterval/Experiment/PayloadArena.lean b/HexInterval/Experiment/PayloadArena.lean
index f3f6ae3c0..9ac39260c 100644
--- a/HexInterval/Experiment/PayloadArena.lean
+++ b/HexInterval/Experiment/PayloadArena.lean
@@ -413,23 +413,23 @@ def freezeChecked (limits : Limits) (arena : Arena) (origin : Action)
     match preflightUses limits.maxUses outcome with
     | .error resource => .resourceLimit resource arena
     | .ok _ =>
-         let uses := outcomeUses outcome
-         match preflightLocal limits drafts with
-         | .error resource => .resourceLimit resource arena
-         | .ok bounded =>
-             match validate uses bounded.drafts with
-             | some error => .invalid error arena
-             | none =>
-                 match validateDrafts validateDraft bounded.drafts with
-                 | some error => .invalid error arena
-                 | none =>
-                     match preflightWhole limits arena bounded with
-                     | .error resource => .resourceLimit resource arena
-                     | .ok _ =>
-                         let (prospective, relocations) :=
-                           freezeDrafts arena origin bounded
-                         match relocateOutcome relocations outcome with
-                         | .error error => .invalid error arena
+        let uses := outcomeUses outcome
+        match preflightLocal limits drafts with
+        | .error resource => .resourceLimit resource arena
+        | .ok bounded =>
+            match validate uses bounded.drafts with
+            | some error => .invalid error arena
+            | none =>
+                match validateDrafts validateDraft bounded.drafts with
+                | some error => .invalid error arena
+                | none =>
+                    match preflightWhole limits arena bounded with
+                    | .error resource => .resourceLimit resource arena
+                    | .ok _ =>
+                        let (prospective, relocations) :=
+                          freezeDrafts arena origin bounded
+                        match relocateOutcome relocations outcome with
+                        | .error error => .invalid error arena
                         | .ok outcome =>
                             .ready prospective outcome
 
diff --git a/progress/20260729T064950Z.md b/progress/20260729T064950Z.md
new file mode 100644
index 000000000..532674275
--- /dev/null
+++ b/progress/20260729T064950Z.md
@@ -0,0 +1,26 @@
+# Accomplished
+
+- Restacked sealed package replay on payload-session head
+  `e8a787ab1ac43835aa631c815a065e7fb0fcd59d`.
+- Threaded the opaque `BoundedDrafts` transaction through `freezeChecked`,
+  preserving the exact sequence of use traversal, local bounds, structural
+  coverage, sealed format validation, cumulative capacity, relocation, and
+  append.
+- Retained recoverable malformed-format behavior and genuine cumulative
+  entry/body exhaustion after earlier commits.
+- Passed the focused 26-target build graph, conformance-target matrix check,
+  diff hygiene, and trust scans.
+
+# Current frontier
+
+Sealed replay formats are green on the final payload-session and
+suggestion-recovery stack.
+
+# Next step
+
+Restack the policy-owned payload session and semantic replay independently on
+this package-replay head.
+
+# Blockers
+
+None.

From 79e3c9f33527de90e2fd9400f3e81453b409db5a Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@lean-fro.org>
Date: Wed, 29 Jul 2026 07:13:49 +0000
Subject: [PATCH 9/9] Refresh package replay on final framework

Record the final framework migration in progress/20260729T071332Z.md.
---
 progress/20260729T071332Z.md | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 progress/20260729T071332Z.md

diff --git a/progress/20260729T071332Z.md b/progress/20260729T071332Z.md
new file mode 100644
index 000000000..f441ecc90
--- /dev/null
+++ b/progress/20260729T071332Z.md
@@ -0,0 +1,25 @@
+# Accomplished
+
+- Restacked sealed package replay on payload-session head
+  `019ce527f0331302a728212703c86fa1fa0f829e`.
+- Preserved direct consumption of the engine-returned suggestion admission
+  plan across replay-snapshot session changes.
+- Retained opaque bounded-draft accounting and the exact order of structural
+  coverage, sealed format validation, and cumulative capacity.
+- Preserved the late malformed-body precedence canary alongside explicit
+  capacity-versus-depth suggestion-drop accounting.
+- Passed the focused 26-target build graph, conformance-target matrix check,
+  diff hygiene, and trust scans.
+
+# Current frontier
+
+Sealed package replay is green on the final exact suggestion-admission
+framework.
+
+# Next step
+
+Restack policy-owned and semantic replay siblings on this package-replay head.
+
+# Blockers
+
+None.