Bind interval packages to proof payload sessions

HexInterval/Experiment/DyadicRules.lean

@@ -473,7 +473,7 @@ def arithmeticPackage (config : Config) (real : DomainId) : Package Fact :=
         Handler.statelessPlanned squareForward (invokeSquareForward config),
         Handler.statelessPlanned reciprocalForward (invokeReciprocalForward config),
         Handler.statelessPlanned reciprocalBackward (invokeReciprocalBackward config)]
-    acceptsLimits := fun _ limits =>
+    acceptsLimits := fun _ limits _ =>
       config.maxReciprocalEffort ≤ limits.maxEffort &&
         config.reciprocalPrecisionsAllowed &&
         2 ≤ limits.maxObservationValue && 60 ≤ limits.maxDiagnosticValue &&
@@ -491,7 +491,7 @@ def centeredPackage (config : Config) (real : DomainId) : Package Fact :=
       #[Handler.statelessPlanned centeredForward (invokeCenteredForward config),
         Handler.statelessDroppingDrafts centeredSplit invokeCenteredSplit,
         Handler.statelessPlanned centeredInstantiate invokeCenteredInstantiate]
-    acceptsLimits := fun _ limits =>
+    acceptsLimits := fun _ limits _ =>
       4 ≤ limits.maxObservationValue &&
         71 ≤ limits.maxDiagnosticValue &&
         1 ≤ limits.maxOutcomeCandidates && 1 ≤ limits.maxOutcomeSuggestions &&
@@ -505,6 +505,19 @@ def buildRegistry (config : Config) (real : DomainId) (limits : Limits) :
   Propagator.Registry.buildWithin limits
     #[arithmeticPackage config real, centeredPackage config real]
 
+/-- The legacy search-only driver allocates no proof payloads. Packages used
+through it must therefore accept the empty arena envelope as well as the
+engine limits. Proof-producing execution supplies its real envelope through
+`PayloadSession`. -/
+def searchArenaLimits : PayloadArena.Limits :=
+  { maxEntries := 0
+    maxBodyCells := 0
+    maxDrafts := 0
+    maxDraftCells := 0
+    maxAtom := 0
+    maxSchema := 0
+    maxUses := 0 }
+
 inductive StartError where
   | incompatibleLimits
   | registry (error : RegistryError)
@@ -524,7 +537,8 @@ def start (config : Config) (real : DomainId) (program : Program)
       | .error error => .error (.engine (.engine error))
       | .ok () =>
           if !registry.acceptsProgram program then .error .operationMismatch
-          else if !registry.acceptsLimits program limits then .error .incompatibleLimits
+          else if !registry.acceptsLimits program limits searchArenaLimits then
+            .error .incompatibleLimits
           else
             match DyadicInterval.start config.endpointLimit program registry.registrations
                 rawFacts limits with

HexInterval/Experiment/PackageRegistry.lean

@@ -97,15 +97,17 @@ introduced by this package, while `requiredOperations` records exact
 signatures supplied elsewhere but interpreted by its matchers.  A handler may
 target such an external operation; final head validation remains the engine's
 responsibility once the complete program is available.  `acceptsLimits` is a
-package-owned configuration preflight, not a soundness boundary: every reply
-is still checked against the engine limits. -/
+package-owned configuration preflight over the engine and payload-arena
+envelopes, not a soundness boundary: every reply is still checked by both
+owners. -/
 structure Package (Fact : Type) where
   Cache : Type
   cache : Cache
   operations : Array Operation := #[]
   requiredOperations : Array Operation := #[]
   handlers : Array (Handler Fact Cache)
-  acceptsLimits : Program -> Limits -> Bool := fun _ _ => true
+  acceptsLimits : Program -> Limits -> PayloadArena.Limits -> Bool :=
+    fun _ _ _ => true
   /-- Non-semantic routing telemetry used to check that only the selected
   package snapshot changes. -/
   invocations : Nat := 0
@@ -256,12 +258,13 @@ def acceptsProgram (registry : Registry Fact) (program : Program) : Bool :=
     registry.packages.all fun package =>
       package.requiredOperations.all (operationAccepted program)
 
-/-- Run every package-owned configuration preflight over the final program and
-engine resource envelope. -/
+/-- Run every package-owned configuration preflight over the final program,
+engine resource envelope, and proof-payload arena envelope. -/
 def acceptsLimits (registry : Registry Fact) (program : Program)
-    (limits : Limits) : Bool :=
+    (limits : Limits) (arenaLimits : PayloadArena.Limits) : Bool :=
   DispatchCode.requestMismatch ≤ limits.maxDiagnosticValue &&
-    registry.packages.all fun package => package.acceptsLimits program limits
+    registry.packages.all fun package =>
+      package.acceptsLimits program limits arenaLimits
 
 end Registry
 

HexInterval/Experiment/PayloadArena.lean

@@ -87,12 +87,19 @@ def wellFormed (arena : Arena) : Bool :=
 
 end Arena
 
-/-- Trusted bounds for the prospective whole arena. -/
+/-- Trusted per-reply and whole-run bounds for prospective freezing. -/
 structure Limits where
+  /-- Cumulative frozen entries retained by the whole run. -/
   maxEntries : Nat
+  /-- Cumulative encoded body cells retained by the whole run. -/
   maxBodyCells : Nat
+  /-- Drafts supplied by one package reply. -/
+  maxDrafts : Nat
+  /-- Encoded body cells supplied by one package reply. -/
+  maxDraftCells : Nat
   maxAtom : Nat
   maxSchema : Nat
+  /-- Payload-bearing proposal positions traversed in one reply. -/
   maxUses : Nat
   deriving DecidableEq, Repr
 
@@ -106,8 +113,14 @@ inductive Invalid where
 
 /-- A trusted arena limit exhausted before allocation. -/
 inductive Resource where
+  /-- The remaining whole-run entry capacity is exhausted. -/
   | entries
+  /-- The remaining whole-run body-cell capacity is exhausted. -/
   | bodyCells
+  /-- One reply supplied too many drafts. -/
+  | drafts
+  /-- One reply supplied too many encoded body cells. -/
+  | draftCells
   | atom
   | schema
   | uses
@@ -243,13 +256,26 @@ def validate (uses : List Use) (drafts : List Draft) : Option Invalid :=
       | some error => some error
       | none => checkCoverage uses drafts
 
-/-- Consume a body-cell budget while checking every encoded recipe atom. -/
+/-- One exact draft list after reply-local bounds have been checked. Its
+private constructor prevents callers from pairing an invented cell count with
+different drafts before cumulative preflight or freezing. -/
+structure BoundedDrafts where
+  private mk ::
+  drafts : List Draft
+  cells : Nat
+
+/-- 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
+deliberately not inspected. -/
 def consumeBody (maxAtom : Nat) : Nat -> List Nat -> Except Resource Nat
   | remaining, [] => pure remaining
-  | 0, _ :: _ => throw .bodyCells
-  | remaining + 1, atom :: atoms =>
+  | remaining, atom :: atoms =>
       if maxAtom < atom then throw .atom
-      else consumeBody maxAtom remaining atoms
+      else
+        match remaining with
+        | 0 => throw .draftCells
+        | remaining + 1 => consumeBody maxAtom remaining atoms
 
 def consumeDrafts (maxAtom : Nat) :
     Nat -> List Draft -> Except Resource Nat
@@ -258,26 +284,35 @@ def consumeDrafts (maxAtom : Nat) :
       let remaining ← consumeBody maxAtom remaining draft.body
       consumeDrafts maxAtom remaining drafts
 
-/-- Check aggregate entry, draft-work, schema, and cell limits before
-constructing any new entry.  In particular the draft list is bounded by both
-remaining arena room and `maxUses` before the quadratic exact-coverage checks
-run. -/
-def preflight (limits : Limits) (arena : Arena) (drafts : List Draft) :
-    Except Resource Nat := do
+/-- Check only reply-local draft, schema, atom, and cell bounds. The returned
+opaque transaction retains the exact list whose cell count was derived.
+Exact draft coverage must still be validated before whole-run capacity is
+consulted. -/
+opaque preflightLocal (limits : Limits) (drafts : List Draft) :
+    Except Resource BoundedDrafts := do
+  if !listWithin limits.maxDrafts drafts then
+    throw .drafts
+  if drafts.any (fun draft => limits.maxSchema < draft.schema) then
+    throw .schema
+  let remaining ← consumeDrafts limits.maxAtom limits.maxDraftCells drafts
+  pure { drafts, cells := limits.maxDraftCells - remaining }
+
+/-- Compare an already locally bounded and exactly validated transaction with
+remaining whole-run capacity. Consequently `.entries` and `.bodyCells` mean
+genuine cumulative exhaustion by otherwise valid evidence. -/
+def preflightWhole (limits : Limits) (arena : Arena)
+    (bounded : BoundedDrafts) : Except Resource Unit := do
   if limits.maxEntries < arena.entries.size then
     throw .entries
   let entryRoom := limits.maxEntries - arena.entries.size
-  if !listWithin limits.maxUses drafts then
-    throw .uses
-  if !listWithin entryRoom drafts then
+  if !listWithin entryRoom bounded.drafts then
     throw .entries
-  if drafts.any (fun draft => limits.maxSchema < draft.schema) then
-    throw .schema
   if limits.maxBodyCells < arena.bodyCells then
     throw .bodyCells
   let cellRoom := limits.maxBodyCells - arena.bodyCells
-  let remaining ← consumeDrafts limits.maxAtom cellRoom drafts
-  pure (cellRoom - remaining)
+  if cellRoom < bounded.cells then
+    throw .bodyCells
+  pure ()
 
 structure Relocation where
   source : PayloadId
@@ -310,9 +345,10 @@ def appendDrafts (origin : Action) :
       (entries, { source := draft.label, global } :: relocations)
 
 def freezeDrafts (arena : Arena) (origin : Action)
-    (drafts : List Draft) (addedCells : Nat) : Arena × List Relocation :=
-  let (entries, relocations) := appendDrafts origin arena.entries drafts
-  ({ entries, bodyCells := arena.bodyCells + addedCells }, relocations)
+    (bounded : BoundedDrafts) : Arena × List Relocation :=
+  let (entries, relocations) :=
+    appendDrafts origin arena.entries bounded.drafts
+  ({ entries, bodyCells := arena.bodyCells + bounded.cells }, relocations)
 
 /-- Validate and freeze every reply-local payload reference in an outcome.
 
@@ -327,17 +363,20 @@ def freeze (limits : Limits) (arena : Arena) (origin : Action)
   | .error resource => .resourceLimit resource arena
   | .ok _ =>
       let uses := outcomeUses outcome
-      match preflight limits arena drafts with
+      match preflightLocal limits drafts with
       | .error resource => .resourceLimit resource arena
-      | .ok addedCells =>
-          match validate uses drafts with
+      | .ok bounded =>
+          match validate uses bounded.drafts with
           | some error => .invalid error arena
           | none =>
-              let (prospective, relocations) :=
-                freezeDrafts arena origin drafts addedCells
-              match relocateOutcome relocations outcome with
-              | .error error => .invalid error arena
-              | .ok outcome =>
-                  .ready prospective outcome
+              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
 
 end Hex.Interval.Experiment.PayloadArena