Intent Runtime Protocol

C3-RUN-001 — Typed host interface

Under intent-preview the language-level boundary is:

IntentEngine.run<I,O>(request: IntentRequest<I,O>, engine: &IntentEngine)
  -> IntentOutcome<O> effects { intent, plus the intent interface's effect bound }

This is a normative future interface, not an implemented library signature. IntentRequest contains the intent and authority references, exact input type/value, closed context, policy, generator configuration, request identity, and budgets. IntentOutcome contains a tagged result, typed output when successful, the last admitted revision if any, evidence/receipt references, budget consumption, and a stable diagnostic otherwise. Persistent requests contain capability requirements only; live handles arrive from the host.

Each call has a statically known candidate-effect bound from the checked intent interface, even when its concrete request is loaded dynamically. The call’s effect set is intent union that bound. Generated code, typed plans, and nested calls must remain within it and the policy’s operation allowlist; dynamic resolution cannot widen the caller’s effect set. An unknown bound prevents typed admission rather than being inferred from a later successful candidate.

The request nonce is host-assigned and unique in the owning run journal. Reusing the same request identity denotes replay/recovery of that run, not a fresh resource allowance or permission to repeat its effects. A deliberate new run requires a fresh nonce and fresh admission under current authority. Concurrent duplicate submissions join the recorded run rather than dispatching a second executor; a host unable to resolve that ownership rejects the duplicate.

Input/output types are owned, serializable, capability-free values under the selected runtime edition. Proof terms are artifact references, not arbitrary runtime closures. A malformed input or unsupported output representation is rejected before generation. An available model is not implicit compiler or bootstrap authority: ordinary builds, artifact loads, and proof checks remain model-free unless the caller explicitly requests this host operation.

C3-RUN-002 — Resolution and admission state machine

The ordered phases and permitted successors are:

Phase	Successful successor	Other permitted result
sealed	formalizing	invalid input, unsupported profile
formalizing	awaiting-approval	unresolved ambiguity, generator failure
awaiting-approval	resolving	denied/missing approval, bounded revision to formalizing
resolving	validating	bounded candidate retry, generation failure
validating	admitted	bounded retry to resolving, rejected/unsupported evidence
admitted	executing	expired/revoked capability, changed dependency
executing	completed	runtime failure, replan, indeterminate external effect

Every active phase also permits cancellation or resource exhaustion. Retries increment counters and preserve the sealed request; they are not new unlimited runs. Before approval, a new interpretation gets a new formalization identity. After approval, retries retain that formalization and its required obligations. Execution replanning returns to resolving with a new revision, a recorded current-state input, and the remaining contract obligations; it cannot undo already committed effects or reauthorize a changed contract.

No candidate execution effects occur before admission. Generation and checking may use only their separately granted capabilities (for example a permitted model request or isolated test process). Admission requires checked code/plan typing, complete requirement coverage, valid interpretation approval, all pre-effect obligations, and an admissible path for required runtime checks. Deferred postchecks are explicitly pending, not already passed.

C3-RUN-003 — Code and typed-plan products

A code candidate is an immutable checked implementation with exact entrypoint, signature, effects, dependencies, edition, and implementation identity. It must satisfy the approved contract and all policy-required evidence. Generated source cannot amend that contract or replace its test/obligation definitions.

A typed plan is a finite acyclic graph of calls to existing checked Algorithm entrypoints or Flow operations. Each node binds an exact operation identity, typed arguments from immutable literals/request inputs/earlier outputs, capability requirements, and explicit predecessor edges. Output bindings select the plan’s typed result. Node identifiers are unique; references resolve; graph order is a stable topological order with lexical node-ID tie breaking. Cycles, dangling outputs, type mismatches, and undeclared effects are rejected.

There are no raw shell/tool names, arbitrary prompt strings as operations, or untyped “do whatever is needed” nodes. Branching, errors, retries, and durable effects use existing checked operations with their declared semantics; a plan does not create a second unmodeled executor. Potentially interfering effects must be ordered or covered by the selected operation/scheduler’s checked concurrency contract. The composed plan, not merely each node, must meet the approved contract. Open-ended planning happens through bounded admitted revisions, not cycles concealed in a static plan.

C3-RUN-004 — Budgets and generator provenance

The host supplies finite limits for attempts, revisions, elapsed time, input and output model tokens, model cost in integer micro-units of a named billing unit, proof/check steps and memory, artifact/context bytes, and execution actions. Zero means zero allowance, never unlimited. Limits may be reduced but cannot be increased by candidate text; a new grant is required to increase them. Nested requests consume the parent’s remaining limits as well as their own. Failures, rejected proposals, and retries consume resources.

Before a provider call the host reserves an enforceable upper bound on usage; if the provider cannot enforce the configured limit, the call is unsupported. Usage uncertainty is recorded conservatively against the reservation until reconciled. The host clock meters elapsed time; clock identity/durations are recorded without making replay depend on the current wall clock.

Generator provenance binds provider, declared model/version, protocol, recipe, parameters, request/response content references, toolchain, and reported usage. An unavailable provider version or nondeterministic generation is not silently substituted. A new permitted provider choice is a recorded attempt under policy. Provider labels are attestations, not cryptographic evidence of hidden weights. The proposal remains untrusted irrespective of the generator’s reputation.

C3-RUN-005 — Execution, completion, and failure

Immediately before each effectful operation, revalidate current capabilities, resource reservations, dependency bindings, admission, and applicable prechecks. Proof/approval caching cannot reuse a live grant from another host or scope. Success requires an output of the declared type and all required postchecks; record both the executed revision and its actual evidence. A failed postcheck returns failure with the actual committed effects/receipts preserved.

Terminal outcome tags are completed, rejected, unresolved, unsupported, inconclusive, failed, cancelled, and indeterminate. rejected identifies an invalid candidate/request or denied admission; unresolved identifies missing interpretation/authority or exhausted allowed candidate attempts without an admitted result; inconclusive identifies a checking/resource limit, never a negative theorem. failed records an admitted execution error. Cancellation prevents subsequent dispatch, but cannot retract an in-flight external effect. If that effect’s outcome is unknown, the overall outcome is indeterminate with cancellation recorded as the cause.

A terminal receipt includes the failure phase, stable diagnostic, last revision, consumed budgets, completed/uncertain effects, and any typed partial observations authorized by the contract. Partial observations are not an O success value. The host must not fabricate success or hide uncertainty to satisfy autonomy.

C3-RUN-006 — Replay and recovery

Flow records model responses, formalization decisions, approval, admitted artifact identity, actual inputs, and execution outcomes as durable activities. Replay consumes those records without calling the model, reapproving prose, or executing recorded effects again. A history/artifact mismatch is a replay error, not a request to regenerate a plausible replacement. Proof rechecking may be performed offline and deterministically against recorded inputs; it creates new validation evidence without rewriting the historical decision.

On recovery, do not infer that an absent receipt means an external action did not happen. Preserve Core-2 action identities, deduplication, and separately authorized reconciliation; unsupported reconciliation leaves indeterminate. New decisions require a new recorded activity and freshly checked authority. Replay is not exactly-once physical execution and cannot grant expired rights.

C3-RUN-007 — Canonical runtime snapshot and ZDE projection

Future implementation must publish bounded typed state through the canonical Zerg snapshot, with no UI-only authoritative store. Its proof_intent projection contains run/parent/revision IDs, phase/outcome, intent and formalization IDs, approved statement IDs, assumptions and axiom footprints, obligation kinds and statuses, checker/profile IDs, proposing/approving principals and policy, candidate kind and implementation/plan identity, budgets used/remaining, attempt counts, receipt references, and explicit uncertain-effect summaries.

Lists are bounded by a host-advertised snapshot limit; truncation includes total counts and content references, never hides the fact that pending or failed obligations exist. No live capabilities, secrets, private prompts, or private proof bodies appear in a public projection. Authorized detail retrieval uses the same content-access policy as the runtime.

Reuse workflow/backlog/timeline views for lifecycle and attempts. Add a Proof/Intent detail projection for interpretation ownership, assumptions, formal claims, assurance differences, and indeterminate effects where generic rendering loses those meanings. Runtime snapshot contract tests and user-visible ZDE tests ship with the runtime implementation or an explicitly paired change; this specification delivery does not implement either surface.