[P2] Derive agent proposal schemas from verified stable-ID record and variant types

[wsdt]

Audit: 2026-09-05, commit 2b3b1ee24da2.
Classification: Documented agent-language integration gap; next bounded architectural slice. Priority: P2.

Finding

AgentDefinition v1 already provides stable identities, deterministic AgentGraph output, and a byte-preserved Runtime v1 projection. It does not derive the provider's proposal grammar from the program's checked types.

The owning specification explicitly identifies this as the next bounded gate: docs/LANGUAGE-NATIVE-AGENT-OBJECT-V1.md. src/agent_definition.rs currently holds type-role identifiers and structured Runtime v1 material, while src/agent_runtime.rs admits separately authored tool/action schemas.

Proposed implementation boundary

Add a versioned compiler product resolving the Proposal role to actual verified stable-ID record/variant declarations. Derive a closed proposal schema and a typed decoder from the same retained HIR, including exact scalar representations, required fields/cases, numeric bounds, source/type revision, and unsupported-profile facts.

Start with a closed monomorphic scalar-record/variant subset. Reject recursive, borrowed, resource-bearing, or otherwise unadmitted values with explicit diagnostics. Do not expose a loosely typed “JSON object” escape hatch.

The model/provider can be asked to generate this grammar, but decoder validation remains mandatory. A proposal is data and must not construct Authorized<T> or a publication token.

Acceptance criteria

• Source, HIR, proposal grammar, typed decoder, and AgentGraph all refer to the same stable type identities and revision.
• A display rename preserves semantic identity while an actual type change invalidates stale proposals/schemas.
• Wrong case/field, extra field, missing field, unknown schema version, malformed exact integer, and cross-agent proposal are rejected before effects.
• Generated Python/TypeScript/Rust consumers preserve integers beyond JavaScript's safe-integer range.
• An offline scripted provider exercise uses the generated grammar and independently replays the resulting evidence.
• AgentDefinition/Profile v1 known answers remain byte-frozen; use additive versioning.
• Add the gate to the existing agent-runtime/image harnesses and update only the affected completion claims.

Dependencies: checked record/variant metadata already exists; broad collections and live provider integration are not required for this first slice.

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-17

Suggested scope: L. Dependencies: None required.

[wsdt]

Implemented in 5eb83640 (on main).

State before: src/agent_definition.rs recorded a Proposal-role stable_id as an opaque string with nothing connecting it to a .spx declaration; the graph's references.program_declarations was []. docs/LANGUAGE-NATIVE-AGENT-OBJECT-V1.md:298 named this the next gate.

Implemented (src/agent_proposal.rs + shape.rs + decode.rs): compile_agent_proposal_schema(module, path, definition) compiles the module through check + hir::resolve, resolves the definition's Proposal stable_id against ResolvedProgram::types, and derives semaprax.agent-proposal-schema.v1 plus a typed decoder from that same retained HIR. Admitted subset is a closed monomorphic record/variant over bool, i32, i64, u8, usize, string, exactly the first slice the issue asked for; recursive, generic, class, f64, Bytes, char, nested-record and automatic-field-identity subjects are rejected with explicit diagnostics (SPX-G548–SPX-G551). There is no loosely typed JSON-object escape hatch.

Exact integers travel as canonical decimal strings. The schema document carries identities and representations only, never display names, so a display rename preserves both proposal_type_revision and the schema digest while an actual type change invalidates them — tested in both directions.

DecodedProposal is data: it constructs no Authorized<T>, no publication token, no capability and no effect.

Coordinator-verified: cargo test --locked -p semaprax --test agent_runtime_v1 → 29 passed, 0 failed (22 before), run after rebasing onto current main and hand-merging a completion-matrix conflict. That harness still asserts the frozen AgentDefinition/Profile v1 known answers sha256:82ab9abb… and sha256:0dc7ce1d…, so v1 remains byte-frozen and the work is additive as required.

8 new tests cover derivation, bundle replay and tamper; display rename versus three type changes; the enumerated decoder rejections (noncanonical, unknown schema version, reordered fields, record-versus-variant confusion, cross-agent proposal, stale digest, extra/missing/wrong field, wrong case, mismatched representation, oversized string, oversized document, 9 malformed integers, 4 out-of-bound); exactness at i64::MIN, i64::MAX, u64::MAX and 2^53+1; and one offline scripted-provider run decoded through the generated grammar whose evidence independently replays and whose tampered evidence does not.

Acceptance criteria NOT satisfied

• "Generated Python/TypeScript/Rust consumers preserve integers beyond JavaScript's safe-integer range." No clients were generated. The decimal-string wire that makes one writable is shipped, and exactness was proven in Rust at i64::MIN/i64::MAX/u64::MAX/2^53+1 — but that is the contract, not the consumers. Recorded as an explicit nonclaim in the specification and the matrix rather than glossed.
• The Runtime v1 projection still carries its own authored action/tool schemas; the derived grammar is an additive product beside them, not a replacement. The specification's "next gate" wording now says so instead of claiming the replacement.

Language limit discovered

Copy Variants v1 (SPX-T215) admits only i64/bool in variant case payloads, and a generic record's fields (SPX-T223) only i64/bool/its own parameters. The derivation handles the full scalar set, but string/u8/usize are exercisable in records only. Worth knowing before anyone designs a proposal type around a variant payload.