[P0] Derive streaming structured-output decoding from the checked Proposal type

Summary

Turn the existing bounded Proposal grammar into a streaming, provider-neutral structured-output decoder generated from the actual checked Proposal record or variant. Invalid output must fail before authorization without buffering unbounded responses.

Why this matters competitively

Axis and MoonBit emphasize constrained generation; NTNT emphasizes intent validation. Semaprax can go further by deriving one grammar for provider prompting, streaming validation, decoding, replay, and generated clients from the same stable-ID HIR type.

Current state at the audit baseline

Agent Proposal Schema v1 derives a closed monomorphic scalar grammar and typed decoder from checked HIR.
Generated Proposal clients exist in bounded form.
The current runtime generally consumes complete scripted proposal bytes.
Nested values, richer collections, streaming, and provider transport remain incomplete.

Audit baseline: ae25c6a49dc09ec4613c7a6f52a27daa69dcd3f3 (2026-09-11). Recheck main, this issue, and the owning specifications before changing code; later commits may have superseded individual details.

Required outcome

Define a deterministic event/byte streaming decoder that accepts only the canonical output language generated from the Proposal type, enforces depth/field/case/byte/work limits incrementally, reports stable semantic locations, and yields one typed Proposal only after complete successful validation.

In scope

Grammar generation for admitted records, variants, scalars, Bytes/String, Option/Result, and bounded collections as support permits.
Canonical field/case identity and ordering policy.
Incremental UTF-8 and JSON/token validation.
Early refusal of unknown, duplicate, missing, reordered, or over-limit material according to the chosen grammar.
Streaming usage counters and cancellation.
Provider prompt/schema projection and decoder generated from one grammar object.
Independent replay and generated-client conformance.

Explicitly out of scope

Accepting arbitrary natural-language repair around malformed structured output.
Letting providers define the authoritative schema.
Silently dropping unknown fields.
Buffering an unbounded completion before validation.
Executing tool calls emitted in provider-native format without Proposal decoding.

Starting points in the repository

Agent Proposal Schema v1 docs/code
std/data-json*/
generated TypeScript/Python/Rust Proposal clients
agent runtime and provider response modules
diagnostic catalogue

Use rg to find the current owners of the named schema, diagnostic, operation, or test before editing. Do not assume a path is still authoritative merely because it is listed here.

Implementation sequence

Specify a canonical Proposal grammar projection that includes stable type/field/case IDs, allowed textual encoding, ordering, exact integer transport, and all hard limits.
Generate both whole-document and incremental decoders from the same grammar tables. The streaming decoder must carry explicit parser state and bounded partial-token storage.
Define behavior for unknown fields, duplicate fields, missing fields, variant tags, trailing data, whitespace, exact integer boundaries, UTF-8 splits across chunks, and cancellation between chunks.
Keep parser state separate from semantic authority. Only a completed decoded Proposal can be passed to authorize.
Expose expected-next grammar states to provider adapters and later constrained-decoding APIs without granting the provider the ability to widen them.
Bind the grammar digest and ordered chunk/result digest into model evidence. Replay must reproduce the same typed Proposal or refusal independent of the provider.
Extend generated clients and deterministic fixtures to emit valid and hostile chunk sequences, including one-byte chunks and split Unicode escapes.
Add fuzz/property tests within strict limits and retain minimized distinct failures.

Failure and security cases that must be considered

Chunk boundaries can split UTF-8, escapes, numbers, or length framing.
A streaming parser can accept duplicate/reordered fields differently than the whole decoder.
Early schema prompting and final decoding can diverge if generated by separate code.
Error recovery can accidentally accept a later valid object after malformed prefix data.
Exact integer values outside JSON-safe ranges must not pass through JavaScript numbers.

Required tests and evidence

Whole and streaming decoders agree for every valid and invalid corpus case.
One-byte and adversarial chunking covers UTF-8, surrogate escapes, integers, field names, variant tags, and end-of-document.
Unknown, duplicate, missing, excessive, reordered, and trailing material produce stable refusal codes.
Exact signed/unsigned extrema survive TypeScript/Python/Rust clients without precision loss.
Cancellation and byte/work/depth limits stop before further allocation or provider reads.
The same grammar generates provider schema/prompt data, decoder, and clients.

Acceptance criteria

A model stream yields either one fully typed Proposal or one closed refusal; never a partially authorized value.
Decoder memory and work are bounded independently of provider behavior.
Grammar identity is stable under display renames and changes under semantic type changes.
Whole-document, streaming, replay, and generated clients are conformant.
The implementation integrates with model.invoke and Direct Runtime v2.

Dependencies and sequencing

[P0] Add a provider-independent model.invoke effect to the source-native Agent runtime

Rules for the implementing agent

Read AGENTS.md, docs/COMPLETION-MATRIX.md, docs/ROADMAP.md, docs/QUALITY-GATES.md, and every owning versioned specification named above before editing.
Prefer extending the existing semantic object, operation table, diagnostic catalogue, profile dispatcher, or evidence harness. Do not create a parallel source of truth.
Preserve canonical source, persistent identities, revision binding, fail-closed replay, deterministic rendering, and the separation between evidence and authority.
A local test is local evidence. A hosted run is hosted evidence. A generated artifact is not a support or publication decision. Record exactly what ran and do not widen claims.
Any new wire format, ABI, descriptor, carrier, evidence document, or compatibility surface requires an explicit versioned schema, independent decoder/replay, hostile-input tests, bounds, and nonclaims.
Never grant ambient filesystem, process, network, model, signing, payment, commit, publication, or registry authority merely because a declaration, receipt, test, or proof exists.
Keep changes reviewable. Split implementation into commits that each preserve the existing test suite, and explain any known-answer update field by field.
Do not weaken or delete a failing regression to obtain green CI. Fix the cause or narrow the admitted feature with a stable diagnostic.

Definition of done

The implementation, tests, documentation, status wording, diagnostics, and evidence agree on one exact scope. Targeted tests pass, the applicable repository quality gate passes, hostile cases fail with the documented stable reason, and no unrelated public surface or authority is widened.

docs(agent-runtime): specify the Live Invocation Contract v1

feat(agent-runtime): derive a bounded rich interaction schema from ch…

feat(model-budget-policy): admit model calls, retries and failover ag…

feat(agent-runtime): derive a streaming Proposal decoder from the che…

style: use repeat_n and apply fmt in the streaming decoder tests

Landed (`d939ed5c`, `760e41fb`) — issue stays open on the kernel wiring

src/streaming_proposal_decode.rs + tests + docs/STREAMING-PROPOSAL-DECODE-V1.md.
20 selected, 20 passed. Coordinator re-ran fmt and
clippy --all-targets -D warnings centrally (one manual_repeat_n fixed by
using repeat_n, not by allowing it), both exit 0.

Confirmed nothing was pre-delivered: docs/LIVE-INVOCATION-CONTRACT-V1.md's own
downstream table says "No receipt document, no streaming transport... implementing
the policy behind each is the named downstream issue's scope", unchanged by #177.

The determinism test found a real bug — in the first implementation of this module

identical_bytes_produce_identical_outcomes_regardless_of_chunk_boundaries
takes four documents (valid, multi-byte UTF-8, semantic refusal, corrupted UTF-8),
splits each at every offset, and also feeds each one byte at a time,
asserting every outcome equals the whole-chunk outcome.

The first cut of push() accepted the moment it saw the document's terminal
newline. That passed whole-chunk feeding and split-in-two feeding, and failed
one-byte-at-a-time — it accepted before trailing garbage arriving in a later
single-byte chunk could be seen.

The fix is a real design constraint, now documented: push() can never return
Accepted. Seeing the terminal newline only stops it refusing, because a later
chunk may still deliver trailing data. Only the caller's explicit finish()
("no more bytes") can accept, so all semantic decode moved into finish().

A test that merely fed the input in two halves would have shipped the bug.

Criteria → test → control

criterion	test	control
A prefix is never mistaken for a complete value	`every_strict_prefix_is_incomplete_only_the_complete_document_is_accepted`	every truncation `Incomplete`; only the full document plus `finish()` is `Accepted`
Incomplete and invalid never collapsed	`incomplete_and_refused_are_never_textually_confusable`	`Incomplete` carries no code or message field at all; all 12 `STREAM-*` codes pairwise distinct and none contains "incomplete"
Derived from the checked type, proven not asserted	`streaming_outcome_agrees_with_the_whole_document_decoder_for_every_case`	10 cases — valid, unknown/missing/duplicate field, wrong type, out-of-range int, oversized string, trailing data, valid and unknown variant tag — each cross-checked against `CompiledInteractionSchema::decode` directly
Delegated refusal names the real diagnostic	`semantic_refusal_carries_the_underlying_diagnostic_code`	asserts the whole-decoder's own code appears in the streamed refusal
No unbounded buffering	`byte_bound_is_enforced_at_its_exact_limit` (65536), `depth_bound_...` (64), `string_token_bound_...` (8192)	each: exactly-at-bound still `Incomplete`, bound+1 `Refused` with its specific code
Closed refusal vocabulary, never a raw exception	8 structural tests across `STREAM-START`, `STREAM-WHITESPACE`, `STREAM-STRING` ×2, `STREAM-BRACKET`, `STREAM-UTF8`, `STREAM-TRAILING` ×2	each paired with the legal document accepted
Cancellation and premature EOF	`cancel_refuses_an_in_progress_stream_with_the_given_reason`, `cancel_after_acceptance_cannot_retroactively_unauthorize_the_decoded_value`, `finish_refuses_a_stream_that_never_reached_its_terminal_newline`, `a_refusal_is_sticky_across_further_pushes`	—

Making Incomplete carry no code or message structurally is stronger than
asserting the two are distinct: there is no field in which an incomplete state
could ever masquerade as a refusal.

A pre-existing test-infra bug fixed in passing

The temp-.spx naming pattern copied from agent_interaction_schema/tests.rs
(pid + nanosecond timestamp) collides under this crate's parallel test
threads, producing an intermittent "semantic patch source changed after its
initial revision check" failure. An atomic counter was added in the new test file
only. Worth knowing that the original pattern is still in use elsewhere and can
flake the same way.

Why this stays open

ProposalStreamDecoder is not wired behind
live_invocation::model_invoke::ProposalDecoder or the kernel — that needs
src/live_invocation/**, read-only for this lease. Recorded in the spec doc's
"What this document does not claim".

Evidence class: local, re-runnable. Not hosted.

test(streaming-proposal-decode): add a bounded deterministic fuzz/shr…

Audited against main at cc03e2e8. Not closing, and the reason matters more than the checklist.

All three of #178/#179/#180 are merged (git merge-base --is-ancestor confirms agent/issue-178-streaming-decode, -179-budgets, -180-receipts are ancestors of origin/main). The code is real and well tested. But:

model_budget_policy and model_call_receipt have zero callers outside their own modules anywhere in src/. ProposalStreamDecoder is referenced only by its own tests. provider_adapter_sdk names the other three only in doc comments — it never calls ModelPolicyLedger::reserve_attempt or constructs a ModelCallReceipt.

There is no code path in this repository today — fixture or otherwise — that dispatches one model attempt through the budget ledger, decodes it through the streaming decoder, and emits a receipt, together. Each piece is independently solid; none are connected. live_invocation::kernel's ModelHandler::invoke returns a one-shot Settled(Vec<u8>), not a chunk stream, so nothing could call the streaming decoder incrementally even if it wanted to. And per docs/LIVE-INVOCATION-CONTRACT-V1.md's own row 1, no parser/HIR/source syntax for model.invoke exists at all.

#178 criterion table

Criterion	Status	Evidence
One typed Proposal or one closed refusal; never partial authorization	met	`PushOutcome` sticky terminal state — `every_strict_prefix_is_incomplete_only_the_complete_document_is_accepted`, `a_refusal_is_sticky_across_further_pushes`
Decoder memory/work bounded independent of provider	met	each of `MAX_STREAM_BYTES`/`_DEPTH`/`_STRING_TOKENS` enforced at its exact limit, one test each
Grammar identity stable under rename, changes under semantic change	met	`display_rename_preserves_identity_structural_change_invalidates_it`
Whole-document, streaming, replay and generated clients conformant	partial	whole/streaming agreement proven; generated clients not met (the schema doc's own "Known limitations" says no generated compiled client bundles); no streaming-specific replay path
Integrates with `model.invoke` and Direct Runtime v2	not met	zero callers, as above
Fuzz/property tests with minimized failures retained	was not met — now added	below

Added this pass

bounded_deterministic_fuzz_finds_no_streaming_whole_document_disagreement (src/streaming_proposal_decode/tests.rs, landed in 2ed47537): a fixed-seed xorshift64 mutation loop (flip/delete/insert/truncate/duplicate) over four seed documents, asserting the streaming decoder never disagrees with CompiledInteractionSchema::decode across any chunking, with delta-debug shrinking (shrink_minimal_failure) so a regression reports a minimal reproduction rather than a raw blob. std-only and deterministic — proptest/quickcheck are not dependencies and adding one was out of lease.

Evidence class: local re-runnable. cargo test --locked -p semaprax --lib streaming_proposal_decode → 21 passed, 0 failed.

Remaining for closure

Wiring ProposalStreamDecoder into model_invoke's ProposalDecoder/ModelHandler seam, which first requires deciding what a streaming ModelHandler variant looks like — a design decision, not a gap-fill. Generated compiled client bundles. Source-language model.invoke syntax is a prerequisite the contract doc names as its own non-goal.

Verification note, and a dependency correction.

This issue is dependency-blocked on #177. The repository's own execution manifest computes it (ready.py reports #178 waits on [177]). I dispatched a worker against #178 directly before checking that, which was my error — anything built here now would be scaffolding on an unaccepted upstream contract, which the orchestration rules only permit when explicitly labelled pending. The worker was redirected to #177 itself.

The decoder already exists and is merged. src/streaming_proposal_decode.rs and its tests.rs — including the fixed-seed fuzz and shrink harness — are an ancestor of current main via commit c5240bf9. This was verified against the tree rather than taken from the issue thread.

But like #177's effect, it is reachable only from its own tests. There is no parser or HIR syntax for the surrounding model.invoke effect at all (rg "model\.invoke|model_invoke" src/parser/ src/lexer.rs returns nothing), and agent_lifecycle::iterative::driver::ProposalSource — the real proposal seam — has no implementor against it. So the streaming decoder is implemented and tested, not wired.

Wiring it requires the parser/HIR change that the Review checkpoint inherited from #108 gates, so it is not something a bounded worker may self-approve. That checkpoint is the real blocker for this issue, not the decoder's own completeness.

Evidence: --lib live_invocation → 92 passed, 0 failed, local and offline, fixture-backed with no live model spend. No code changed on this issue this session.

Recommend this stays blocked behind #177 rather than being worked independently — and that #177's own remaining gap (only one ModelHandler implementation exists, so provider-neutrality is asserted rather than proven) is closed first, since a streaming decoder derived from a boundary that has never faced a second transport inherits that same unproven assumption.

Landed streaming/kernel integration on main at 852aa90 (19-file implementation batch).

provider_adapter_sdk::bridge::StreamingModelHandler now negotiates before start, streams every Delta through the existing ProposalStreamDecoder, checks explicit cancellation/deadline before start and each poll, bounds request/schema/response/polls, preserves task/observation bytes with hex, and refuses malformed prefixes before further reads. It requires a single Completed plus matching settlement and refuses negative/regressing usage. live_invocation::compiled_decoder::CompiledProposalDecoder rechecks canonical responses at the kernel decode boundary before authorization.

The executable integration test now runs a real generic kernel invocation through streaming compiled decode, LiveModelPolicyHook reservation and journal receipt projection together. Another asserts one malformed Delta causes exactly one read/cancel and zero authorization. Additional hostile cases prove pre-dispatch cancellation/deadline/schema refusal, bounded Pending polling and the clamped response cap.

This resolves the old “zero callers / no path connecting decoder, policy and receipts” finding for the generic runtime. Remaining: source/Direct Runtime v2 integration, generated streaming client conformance and broader provider coverage. The adapter SDK's instance contract is one start per adapter; this is not an automatic provider factory, retry or failover implementation.

Local focused evidence: 56 selected library tests passed (one serial build), including the new integration paths, model-policy preservation tests, and receipt projection. Module-size, format and diff checks passed. No full quality suite, hosted CI, live provider or billing claim.

Implemented and pushed in b35139d. Local macOS arm64 verification: 56 selected library tests passed, module-size and format/diff checks passed. The external Rust embedding consumer compiled against the freshly built library and ran successfully. No full quality run, hosted CI, or network provider evidence is claimed.

Added a source-grammar streaming decoder that delegates final admission to CompiledAgentProposalSchema, including safe refusal of terminal LF followed by incomplete UTF-8. Added StreamingSourceProposalAdapter over the actual ordinary ProposalSource trait with an explicit fresh adapter factory for each attempt, complete iterative task/state/observation/prior effect/rejection context, source/schema binding, pre-render retained-value bounds, cancellation/deadline checks, incremental early refusal, and exact stream/settlement agreement. Tests cover real source-schema admission, fresh attempts, prompt context, early cancellation, predispatch guards, and contradictory settlement/usage.

Remains open: durable source-checkpoint adapter identities/policy and broader runtime/generated-client integration are not supplied by this ordinary source bridge.

Progress on main in c9205ad:

Direct Runtime v2 now consumes an explicit ordinary ProposalSource, including StreamingSourceProposalAdapter, through the checked iterative lifecycle and typed effect dispatcher. The driver captures the accepted canonical proposal at the effect boundary; it does not copy arbitrary provider output into effect authority.
Both streaming grammars derive their canonical outer envelope prefix from the compiled schema and reject unknown/reordered/duplicate envelope keys and mismatched identity/digest during push. Nested field/case validation still belongs to the terminal authoritative decoder.
Focused local checks pass for three-turn valid typed execution, malformed output before effects, pre-cancelled execution with no adapter construction, and settlement mismatch before effects. Existing frozen typed execution and streaming/SDK regressions also pass.

This issue remains open: nested incremental field/case grammar, expected-next states, and generated-client/chunk conformance still need implementation. No live-provider or hosted-CI claim is made.

Progress on main in b292c93 (15 files, 1,051 added lines).

Both streaming decoders now use one bounded incremental machine lowered from their actual compiled schema tables. It checks nested record/variant identities and field order, rejects unknown/duplicate/missing/reordered fields and cases before finish, and checks exact quoted integers, booleans, text byte limits and byte-array element limits. Source Proposal admission remains its existing scalar subset; this does not claim string or nested variant payload language support.

The grammar retains a DAG rather than recursively expanding nested declarations. Auxiliary sorted case tables use binary bounds per byte, avoiding repeated scans of long shared case prefixes. Parser stack, partial-token storage and grammar work are bounded; expected_next and grammar_work expose read-only state. Only the final owning whole decoder can return a typed value. Stable STREAM-GRAMMAR refusals include the compiled identity and byte offset.

Local evidence: 41 focused streaming/SDK library checks pass, including a checked large-record prefix at the 64KiB boundary, nested/refusal corpus, exact byte-array bounds, adversarial chunking and long shared variant prefixes. The existing generated-client harness physically compiled/executed TypeScript 5.8.3/Node24.3, Python3.14 and offline Rust clients; complete output, one-byte/split streams, escaped strings and signed/unsigned extrema conform. That test and Direct Runtime streaming both pass (43 focused checks total). Full/hosted gates were not rerun under the requested speed policy.

Remaining before issue closure: bind ordered chunk/result commitments into actual model-call evidence with independent replay. This should be completed with the rich attempt-observation/receipt integration in #180. No live-provider, invoice authority or hosted evidence is claimed.

Implemented the remaining ordered transport evidence binding for the admitted compiled Proposal grammar.

RecordingAdapter captures actual request, ordered Delta/Usage/Completed events, settlement/failure/start refusal, cancellation and optional explicit-clock observations as bounded commitments.
Independent replay checks exact retained events, chunk order, grammar identity, cancellation and concatenated settlement bytes without a live provider parameter.
The generic adapter evidence projection validates the live journal and seed, reconstructs the dispatched request, independently decodes the retained settlement with the compiled schema, and matches the actual journal response/Proposal commitment.
Actual source bridge tests retain and replay the same observations, reproduce typed Proposal output, and prove malformed first-chunk cancellation without a second provider poll.

This completes the evidence step alongside the previously landed compiled nested grammar, expected-next states, bounded deterministic fuzz/corpus checks, early refusals, and actual generated TypeScript/Python/Rust client conformance. The scope follows admitted source types; this does not add unsupported language shapes, real provider transports, or hosted support.

Validation: 47 focused SDK tests and 45 receipt tests pass locally. Previous grammar/client evidence is recorded on the preceding implementation comment. Only focused checks were run, per the user's explicit speed instruction; hosted CI is handled separately.

Navigation Menu

Repository navigation

[P0] Derive streaming structured-output decoding from the checked Proposal type #178

Summary

Why this matters competitively

Current state at the audit baseline

Required outcome

In scope

Explicitly out of scope

Starting points in the repository

Implementation sequence

Failure and security cases that must be considered

Required tests and evidence

Acceptance criteria

Dependencies and sequencing

Rules for the implementing agent

Definition of done

Landed (`d939ed5c`, `760e41fb`) — issue stays open on the kernel wiring

The determinism test found a real bug — in the first implementation of this module

Criteria → test → control

A pre-existing test-infra bug fixed in passing

Why this stays open

#178 criterion table

Added this pass

Remaining for closure

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

[P0] Derive streaming structured-output decoding from the checked Proposal type #178

Description

Summary

Why this matters competitively

Current state at the audit baseline

Required outcome

In scope

Explicitly out of scope

Starting points in the repository

Implementation sequence

Failure and security cases that must be considered

Required tests and evidence

Acceptance criteria

Dependencies and sequencing

Rules for the implementing agent

Definition of done

Activity

wsdt commented on Sep 12, 2026

Landed (d939ed5c, 760e41fb) — issue stays open on the kernel wiring

The determinism test found a real bug — in the first implementation of this module

Criteria → test → control

A pre-existing test-infra bug fixed in passing

Why this stays open

wsdt commented on Sep 12, 2026

#178 criterion table

Added this pass

Remaining for closure

wsdt commented on Sep 12, 2026

wsdt commented on Sep 13, 2026

wsdt commented on Sep 13, 2026

wsdt commented on Sep 13, 2026

wsdt commented on Sep 13, 2026

wsdt commented on Sep 13, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Landed (`d939ed5c`, `760e41fb`) — issue stays open on the kernel wiring