Bind interval packages to proof payload sessions

[kim-em]

Purpose

Make proof-producing execution over arbitrary function packages own one coherent engine, registry, and immutable evidence arena.

What this establishes

• callbacks return an outcome plus exact reply-local proof drafts;
• a private-constructor session assembles the matching registry and engine itself;
• invocation, bounded payload validation/relocation, reply admission, and arena commit form one transition;
• generic engine preflight bounds the program before package-specific scans;
• outer reply lists are checked against engine bounds before arena traversal, and session start checks coherent per-reply use limits;
• the engine exposes one exact retained/dropped suggestion split, shared with completeness accounting;
• package-local use, atom, and schema excess consumes a failed reply, preserves independent work, and permanently withholds completeness;
• whole-run arena entry/body exhaustion and engine-invalid transitions remain fatal and non-resumable;
• rejected replies cannot commit prospective evidence;
• malformed package evidence becomes a failed live rule transition, preserves other work, and permanently prevents a false saturation report;
• the durable droppedWork field is distinct from the exported Session.complete fixed-point predicate;
• Run has a private constructor, so stop classifications cannot be paired with arbitrary sessions;
• nested instantiation and equality payloads relocate atomically; honest admission/execution is intentionally left to the private policy-session layer.

The FIFO session is an ownership and transaction experiment. External policy selection and package-owned semantic replay are the next stacked layers. The eager arena entry budget is deliberately documented as an action/draft waste bound rather than an accepted-fact bound.

Verification

• lake build HexInterval.Experiment.PayloadSession HexInterval.PayloadSessionConformance HexIntervalExperiment
• git diff --check
• no added native_decide, axiom, or sorry

Stacked on #9035.