[P2] Bind deterministic agent stages to verified source functions and execute one typed lifecycle

[wsdt]

Audit: 2026-09-05, commit 2b3b1ee24da2.
Classification: Documented core-agent integration gap; proposed bounded language feature. Priority: P2.

Finding

AgentDefinition currently records identities for initialize, observe, authorize, and reduce, but does not execute those declarations as Semaprax functions. The owning specification says so explicitly: docs/LANGUAGE-NATIVE-AGENT-OBJECT-V1.md and docs/LANGUAGE-NATIVE-AGENT-OBJECT-V1.md. src/agent_harness.rs composes existing runtime/payment kernels and likewise disclaims language-level transition execution.

The result is a useful graph/profile bridge, but the semantic program and harness still do not derive operational behavior from one checked source object.

First implementation boundary

After proposal grammar and deployment binding are defined, compile a single acyclic lifecycle whose deterministic stage IDs resolve to actual verified .spx functions. Start with scalar/closed-record task, state, observation, proposal, outcome, and result types. Validate the stage signatures, ownership modes, effects, and graph edges from the same HIR used for ordinary execution.

Execute the deterministic stages with a retained interpreter product and a scripted model proposal. Limit execute initially to one explicitly injected read operation or an effect-free fixture. The authorizing transition must produce an opaque, one-use authorization value bound to the exact proposal/state/policy, not a boolean or hash that any caller can manufacture.

Acceptance criteria

• Changing a stage's source changes the compiled agent semantics and invalidates old graph/run bindings.
• Unresolved IDs, incompatible signatures, incorrect ownership, undeclared effects, stale proposals, and substituted states reject before host work.
• Only the validated authorize stage can construct the one-use authorization value; reduce/observe/model output cannot.
• Success, rejection, model failure, effect failure, cancellation, and budget exhaustion have deterministic state/cleanup/evidence behavior.
• One offline end-to-end example proves task → initialize → observe → propose → authorize → execute → reduce → result.
• Runtime v1 compatibility bytes and APIs remain frozen.
• Source remains the Git/review authority; descriptive AgentGraph JSON carries no ambient execution or publication capability.

Keep syntax minimal and versioned; a binding document referencing existing declarations can precede a new agent syntax. Durable resume is dependent work, not an implicit property of this lifecycle.

Agent handoff

Recheck the working revision and existing issues first. Read AGENTS.md, the relevant completion-matrix row, and the owning versioned specifications. This proposed slice must preserve canonical source, independent replay, precise target admission, and separately granted authority. Place regressions in the existing owning harness. Execute the applicable quality gates and record what actually ran; unrun native, hosted, or device evidence must stay unpromoted.

Audit revision scope

Runtime observations in this ticket belong to commit 2b3b1ee. A final source-tree comparison against e1c5b56 was used to check for obvious superseding changes. That later snapshot was not rebuilt or exhaustively retested. Reproduce on the intended fixing revision before implementation.

Audit ID: SPX-AUDIT-20260905-21

Suggested scope: L. Dependencies: SPX-AUDIT-20260905-17, SPX-AUDIT-20260905-18.

[wsdt]

Not implemented. Leaving open with the blocker identified precisely, so the next attempt starts from a known missing seam rather than rediscovering it.

Its two named dependencies are now done and on main: #64 (proposal grammar from verified types, 5eb83640) and #65 (definition/deployment separation, 661a36c8).

The concrete blocker

This ticket requires executing four stage functions with typed arguments from a retained interpreter product. That seam does not exist:

• interpreter::prepared::prepare_resolved_zero_arg_i64 is the only retained-HIR product, and it is zero-argument and additionally requires entry_id == program.entrypoint (src/interpreter/prepared.rs:97). It can run only the module's main, not four named stages.
• interpreter::interpret (src/interpreter.rs:1866) takes a source_path and re-reads and re-verifies the file on every call, so it is not a retained product at all.
• ArgumentValue (src/interpreter.rs:241) is scalar-only. No record or variant argument can be supplied — although the internal Value::Record (src/interpreter.rs:3179) shows records are representable at runtime, so this is an API boundary rather than a representational limit.
• evaluate_resolved_owned_data takes &ResolvedProgram but is restricted to a borrowed Slice<u8> entry and bytes-shaped results.

So the prerequisite is a new retained, multi-argument, record-capable evaluation seam inside a 6658-line module that carries its own size budget and known-answer gates — an L-scope interpreter slice that must land before the lifecycle compiler, the opaque one-use authorization value, the injected read operation, and the six terminal-behaviour cases.

Why nothing was built

Implementing the binding half without execution would leave this ticket's central criterion — an opaque one-use authorization value that only the validated authorize stage can construct, produced by actually running that stage — as unexercised scaffolding. Per this repository's rule that no feature is implemented without its executable gate, that is worse than an honest gap.

Suggested re-scope

Split the interpreter seam into its own ticket and make this one depend on it:

1. Retained multi-argument evaluation — extend the prepared product to call a non-entrypoint function by stable id with record/variant arguments and results, preserving the existing zero-arg entrypoint path and its known answers.
2. Then this ticket: the acyclic lifecycle, signature/ownership/effect validation against the same HIR, the opaque authorization value, and the six terminal cases.

Also worth carrying forward from #64: Copy Variants v1 (SPX-T215) admits only i64/bool in variant case payloads, so stage types built on variant payloads are constrained today.

[wsdt]

The blocker recorded above is now removed. The retained multi-argument interpreter seam landed in 88ff00b8 on main. This issue stays open — the lifecycle compiler, the opaque one-use authorization value and the six terminal cases are still unbuilt — but the prerequisite that made them impossible is gone.

What exists now

src/interpreter/retained_call.rs, exposed as semaprax::interpreter::retained_call:

pub fn prepare_retained_call(&hir::ResolvedProgram, entry_id: &str)
    -> Result<PreparedRetainedCall, Vec<Diagnostic>>;
pub fn evaluate_retained_call(&hir::ResolvedProgram, &PreparedRetainedCall,
    arguments: &[RetainedValue], max_steps: usize)
    -> Result<RetainedCallEvaluation, Vec<Diagnostic>>;

RetainedValue covers Bool | I32 | I64 | U8 | Usize | Bytes | Record | Variant, with records and variants keyed only by DeclarationId, never display names — which is what this issue needs for stage identities to survive a rename. RetainedCallEvaluation carries the function id, a closed outcome (Returned | LanguageFailure | FuelExhausted | CallDepthExceeded | GuardError), cleanup events, fuel accounting and contract failure detail.

prepare_retained_call runs hir::validate, byte-capacity analysis, the interpreter's own admission and scan_closure once. evaluate_retained_call re-runs none of it — it re-checks only that retained positions still name the same identities and the signature is unchanged, then enters the standard Evaluator::call_frame. No source_path anywhere, which was the defect in interpret.

Each of the four blockers recorded above is addressed: a non-entrypoint function by stable id; record and variant arguments and results; genuinely retained across calls; and not restricted to a borrowed Slice<u8> entry.

The existing entrypoint path is preserved

prepare_resolved_zero_arg_i64 is behaviourally untouched — same entry_id == program.entrypoint requirement, same admission, same answers. Its index-building loop and dispatch guard were extracted into shared helpers so both products have one owner for bounds and duplicate-identity rules; the existing unit test guards that extraction and still passes. A new test pins the frozen interpret envelope for app.main (returned/i64/"42") and requires the new seam to agree.

One thing deliberately not done

string fields are rejected, not admitted. #64's proposal schema admits string, but no interpreter record or variant classifier admits ResolvedType::String — classify_record and is_admitted_owned_byte_variant both exclude it, and owned UTF-8 lives on a separate profile with its own materialization budget. Admitting it would introduce a new owned cleanup leaf kind into the interpreter's classifier ahead of the shared cleanup machinery and the native/Wasm backends, which is exactly the "cleanup-plan vectors are canonical runtime order" and "no backend accidents" line in AGENTS.md.

So the admitted vocabulary is the proposal-schema scalar set minus string, plus owned Bytes (which the aggregate profile actually requires: a variant is only admitted if it bears a Bytes field, and a by-value nominal parameter must be a class). string, char, f32, f64, borrowed carriers and generic shapes fail closed with a located SPX-F102 carrying a real span. Documented as Missing.

Anyone building the lifecycle on this must know: stage types cannot carry string today. That is a real constraint on #72's typed task/state/observation/proposal shapes, not an oversight.

Ownership and cleanup

Admission runs entirely through existing classifiers, so ownership errors stay compile-time diagnostics. Execution enters the same call_frame, so contracts, sticky failure selection, fuel and depth are unchanged. A staged owned Bytes argument is charged against the same verified byte-data capacity a bytes_copy consumes and the allocation counters are seeded to match, so a host argument cannot mint capacity. Per #75, a Copy carrier (which aliases by Arc) is harvested by reference while an owned carrier must be uniquely held or fails closed. Result leaves settle in declared field order read from the record's own inventory — never sorted or repaired. No public unchecked-HIR constructor was added.

Coordinator-verified

cargo test --locked -p semaprax --test interpreter_v1 → 30 passed, 0 failed (18 new), and --test module_size → 1 passed, both re-run by me on the rebased tree after confirming the rebase completed. cargo fmt --all --check clean. src/interpreter.rs is 6766 against its 6819 budget; the new files are 883 and 507 lines. No budget touched.

Rejection cases covered: unresolved stable id, non-persistent identity, signature outside the profile, non-admitted argument type (f64, char, string), non-admitted result type, argument-count and argument-kind mismatch, foreign record identity, unknown field identity, missing and duplicated field, a retained product pointed at a different program, and over-capacity staged bytes. Every admission rejection asserts SPX-F102 with its reason, that no SPX-F105 guard appears, and that a span is attached.

One test earns particular mention: one_retained_product_serves_several_invocations_without_reverification prepares, then appends a duplicate function so hir::validate would reject the program, then asserts prepare_retained_call now fails while the already-retained product still dispatches. That makes "retained without re-verification" an observed behaviour rather than a claim.

What remains for this issue

The lifecycle compiler over the four stage ids, signature/ownership/effect validation against the same HIR, the opaque one-use authorization value only the validated authorize stage can construct, the single injected read operation, and the six terminal-behaviour cases. #66 remains dependent on this issue, not on the seam.

[wsdt]

Implemented in 35a1399d (on main), built on the retained seam from 88ff00b8.

New semaprax::agent_lifecycle plus tests/agent_runtime_v1/agent_lifecycle_v1.rs as a module of the existing harness — no new test binary, no CLI verb.

The compiler

Resolves the AgentDefinition's four deterministic operation ids to real ResolvedFunctions from the same HIR ordinary execution uses, then validates arity, per-parameter OwnershipMode against the AgentGraph v1 relationships (initialize/reduce consume, observe/authorize borrow), effects.is_empty(), the six role types, the Task/Outcome {Bytes,i64} shapes, the Proposal scalar projection, the derived two-case grant/refusal decision variant, and a genuinely-computed unique topological order over the six-stage graph. Every rejection is SPX-G570 naming the exact failing field. It then retains one PreparedRetainedCall per stage.

The authorization value — this issue's central criterion

Verified by me at the source, not taken on report. Authorized has three private fields (binding, budget, seal) and derives nothing — no Clone, Copy, Default, From. Rust's private-field rule therefore blocks a struct literal from every other module in the crate and from every consumer.

There is exactly one mint site in the lifecycle: a private fn mint, called only from run_authorize_stage, which

• requires an &AuthorizeStage — a type only stages::bind constructs, and only after the authorize role passed identity, signature, ownership, effect and decision-shape validation;
• re-checks that the retained product and the dispatched evaluation both name that exact validated function id;
• mints only when the returned variant's identity is the validated decision type and its active case is the validated grant case.

I confirmed by grep that the only mint( call in src/agent_lifecycle/ is the one inside AuthorizationOutcome::Granted. reduce, observe and a decoded proposal never reach it.

The value is spent by move (consume(self)) at the effect boundary, so one grant admits exactly one effect. Its binding is sha256(domain ‖ lifecycle-policy-digest ‖ identity-keyed state encoding ‖ exact proposal bytes ‖ grant case id ‖ program-constructed seal), and spend recomputes it from the state and proposal actually presented, refusing with SPX-G571 before calling the read operation — so a substituted state cannot slip through.

The opacity is self-enforcing rather than conventional: a source-audit test pins the mint call count, and the harness's external-consumer probe was extended so a consumer's Authorized { … }, clone::<Authorized>() and Authorized::default() all fail to compile.

Cases that execute

All six terminal cases: completed; rejected (authorize refusal, both codes, zero host calls); model_failed across five distinct documents (stale digest, cross-agent, reordered fields, out-of-range integer, missing terminal LF — each zero host calls, stopping after 2 stages); effect_failed; cancelled; budget_exhausted at two distinct stages.

Rejections executed: unresolved id; two incorrect ownership modes; incompatible result type; a declared effect on a deterministic stage; an unadmitted proposal field representation (string); a non-two-case decision variant. Stale proposals reject at the grammar before authorize; substituted state and substituted proposal reject at spend before the read.

Also proven: byte-identical evidence and digest on replay; lifecycle-bundle replay and tamper (SPX-G572); and a binding that differs for a different state, proposal and policy but is unchanged by a display rename.

Coordinator-verified

cargo test --locked -p semaprax --test agent_runtime_v1 → 42 passed, 0 failed (33 before), and --test module_size → 1 passed, both re-run by me on the rebased tree after confirming the rebase completed. cargo fmt --all --check clean. Largest new file 1050 lines, under 1500; no recorded budget touched.

Runtime v1 stays frozen. the_lifecycle_changes_no_frozen_agent_definition_byte asserts sha256:82ab9abb…, sha256:0dc7ce1d… and sha256:14981ee9… before and after compiling and running a lifecycle over the same definition, and re-checks the canonical definition source and profile bytes. agent_definition_v1's own frozen assertions pass in the same run.

Honestly not covered

• Cancellation is checked at all four stage boundaries, but only the pre-initialize boundary is deterministically reachable from a whole-run caller, so only that one executes. The test is named and commented to say so rather than implying full coverage.
• The <role>.arity and <role>.type binding checks exist but are not individually exercised by a dedicated rejection case.
• Iterative AgentStep continue/suspend/fail, typed effects beyond the one injected read, durable checkpoint/resume ([P3] Implement revision-bound agent checkpoints and resume with uncertainty reconciliation #66), and a CLI surface remain Missing.

A constraint worth recording

string is not admitted at the retained seam, and a by-value nominal stage parameter must be a Copy class while Proposal Schema v1 admits only records and variants — so a nominal Proposal carrier cannot cross a stage boundary. It crosses as its exact ordered scalar projection, keyed by the proposal type's own field identities and validated against the authorize/reduce parameter lists. Documented as a limitation, not worked around.