Full-goal completion matrix

September 21, 2026 · View on GitHub

Status: living internal audit; v0.4.0 implementation evidence HOSTED GREEN.

Audience: maintainers, contributors, reviewers, and technical evaluators.

This document is the authoritative status audit for the complete SEMAPRAX objective. It separates the mature product requirement, the implemented bounded slice, and the functionality or support decision still needed to complete the requirement. The v0.4.0 release baseline owns the current hosted-green evidence classification.

Historical status transitions belong in the changelog. Protocol details, exact known-answer digests, test counts, and historical CI run IDs belong in the linked versioned specifications. Future sequencing belongs in the roadmap. The evidence summaries below describe the current implementation rather than repeat superseded pre-release local-only ledgers.

Status rules

StatusMeaning
ImplementedThe full completion gate is covered by executable evidence on every required target.
PartialUseful executable evidence exists, but the full completion gate remains open.
MissingNo qualifying executable evidence exists for the row.

HOSTED GREEN is an evidence classification, not a replacement for these product-completion statuses. The implemented v0.4.0 slices have the accepted hosted-green release baseline. Design-only functionality, a proof model, a private ABI, an unpublished package, and an explicit public-support decision remain distinct. A private profile tested on hosted CI is still private.

Pre-release labels such as Authored, unrun, Local, partial, and "hosted promotion pending" no longer describe the released implementation's current evidence when the only missing condition was execution of its release gates. Historical local runs remain valid historical witnesses, not the current evidence ceiling. Future or separately unimplemented gates are not marked complete by changing an evidence label.

Current summary

The separate Persistent Semantic Cache v1 implements authenticated cross-process checked-HIR reuse with independent source/HIR validation. Its release regressions are HOSTED GREEN; full incremental compilation and measured task-level performance remain open.

Release implementation evidence: HOSTED GREEN

Overall product objective: Partial

The long-term contract below contains 55 requirements: 55 Partial, 0 Implemented, 0 Missing. This is the count of the actual requirement rows: six semantic-foundation, fifteen language-and-safety, five compiler-and-target, ten ecosystem, nine application-platform, and ten agent/operations rows. The previous 50-row dashboard did not include all rows already present in its own tables. This reconciliation preserves every requirement and corrects the count; it does not add requirements or change their completion thresholds. Work-package and release-exit tables are not included in that denominator.

The released implementation includes canonical source and stable-ID HIR; bounded semantic queries, candidates and replay-checked changes; interpreter, native C11/Clang and Core-Wasm execution of admitted scalar and owned-data profiles; generated consumer and private platform integrations; and the current Agent, generics, collections, I/O, package and installed-tooling additions.

In particular, the current Agent implementation is not limited to one acyclic read. Iterative lifecycle v2, typed effects v3, and Direct Runtime v2 implement checked iterative execution with exact deployment and invocation roots. Per-operation checkpoints, pure migration, durable migration, and linked Project roles are implemented additions. Linked migration and the workspace association / migration profiles retain exact source, root, currentness, trusted-store and cumulative-accounting boundaries. Their hosted evidence is green. An explicitly configured private Unix OpenCode provider adapter additionally has local source-feedback smoke evidence. The separate source checkpoint profile v2 has local checked-driver and injected-host recovery gates, including cumulative replay fuel and model reservations. Source live migration v3 has seven local retained-Project integration gates plus source journal/runtime regressions: checked A→B→C State migration, cumulative accounting, bound schemas, and refusal before redispatch. The bound typed source-model operation now also has local ordinary and durable integration gates: decoded proposals enter typed authorization, model intent ACK precedes provider start, and uncertain/terminal recovery performs no model redispatch. Durable quoted model policy accounting remains separate #113 work. A durable source CLI remains pending. Distributed coordination, broader provider profiles remain separate functionality. Native C11 and Core Wasm Agent-stage execution now exist behind the sealed StageExecutor seam and agree with the interpreter on the bound deterministic stages of one fixture and, through a private frozen-run selector, traverse the shared proposal, fresh-grant, injected read, cancellation, lifecycle-budget and evidence-settlement kernel (agent_lifecycle::tests::lifecycle_parity). This is local, clang/node-gated evidence only. Production, live-provider, checkpoint and migration routes remain interpreter-selected; native/Wasm interpreter-fuel and cleanup-event parity are not claimed (#142/#143/#182).

The generic implementation includes argument inference v3, authored variants, compiler collections, record composition v2, multiple owners, owned Result, function values v2, and closures v2. These have hosted-green evidence for their admitted substitutions, HIR/graph/ProgramRoot replay and backend behavior; general constraints, owning captures and public generic ABI remain separate. Public generic ownership is a separate milestone with eight prerequisite gates, a distinct PG-9 decision gate, and its own standing support decision, not an outcome of that internal work; the Public Generic Ownership milestone owns it and its executable separation gate. All eight prerequisite gates (PG-1 through PG-8 - grammar, template/argument identities, compatibility rules, candidate delta, generated Rust/TypeScript/C/C++ consumers, hostile descriptor/carrier replay, cross-engine settlement, and the cross-platform milestone job itself) are hosted green together on Linux, macOS and Windows for one exact implementation commit (7def8fb1…, run 35433295593), and PG-9 was decided 2026-09-19: unsupported, unpublished. That commit predates the current head and is not a frozen candidate under issue #164; no public generic signature, descriptor, carrier, calling convention, or support claim follows from any of it, and no public support follows from the versioned descriptor/carrier code that now exists. Every physical adapter still calls a fixture endpoint rather than a compiler-derived generic export, and no compiled Wasm artifact implements the admitted provider ABI (#229). The runtime settlement corpus records the implemented native fixture subset, including bounded non-recycled identity/recreation, sibling settlement, explicit release-status propagation and real result-phase/export-failure gates, the C/C++ consumer propagation matrix and Rust explicit-settlement implementation/gates, and the remaining checked-endpoint, compiled-Wasm, consumer-matrix and all-engine evidence requirements.

The largest remaining product gaps are general ownership and lifetime safety, stable public aggregate/resource/component ABIs, a supported package ecosystem, production application tooling, broader target conformance, and the final 1.0 validation product. They are not a backlog of unexecuted v0.4.0 hosted gates.

v0.2 product-exit audit

This historical audit measures the shipped v0.2.0 objective against the broader product goal. The annotated tag resolves to 5f6fb9655fdec92c57ab71615cfd7bfa8cc76051; all 45 jobs in release run 33608662244 passed and the prerelease was published. "Exact-tag hosted" in this historical table means only the gate selected by that run. It does not imply an ignored, unprovisioned, broader-browser, physical-device, registry, or production claim.

Exit criterionEvidenceRemaining gate at that milestone
Multi-module calculator projectExact-tag hostedKeep Project Manifest admission and source closure green on subsequent release candidates.
Same verified calculator logic on native and browser lanesExact-tag hostedPreserve the identical success/failure corpus on subsequent release candidates and broaden browser engines only when claimed.
Several stable-ID functions callable from TypeScript and RustExact-tag hosted; builder remains unpublishedPublish an intentionally supported Rust entry point.
Browser calculator consumes Project exportsExact-tag Chromium, including the display-renamed fixtureAdd multi-engine evidence only when broader browser compatibility is claimed.
Project daemon inspect/derive/preview/apply/rebuild loopExact-tag hostedPreserve Transport v4's bounded authority contract on subsequent release candidates.
Stable external API survives a display renameExact-tag hostedPreserve the complete renamed Project and consumer proof on subsequent release candidates.
Project tests demonstrate native/Wasm equivalenceExact-tag hostedPreserve the full entry/test and consumer corpus on subsequent release candidates.
Multi-module line-filter productExact-tag hosted native and Node/Core-WasmAdd real-browser or multi-engine evidence before claiming that breadth.
Full promotion CI for every v0.2.0 release claimExact-tag hosted and publishedRepeat the complete blocking gate for every later release tag.

The v0.2.0 prerelease completed its artifact milestone, not the full product contract. Its narrower browser and unpublished-builder limitations remain historical facts; current evidence is recorded separately below.

Evidence owners: Project Manifest v1 and its additive profiles, Bounded Language Command I/O, Bounded Language Network I/O, Project Agent Workflow, Wasm Scalar Exports, and Native Rust Interoperability.

v0.4 product-exit audit

The current release is the SEMAPRAX v0.4.0 prerelease, commit dfc15e2ddc818fa97744b5a9d69fd6108dd6a321, published at 2026-09-10T10:31:03Z. The maintainer-confirmed implementation evidence is HOSTED GREEN. The release-note length problem is not an outstanding code or hosted-conformance gate. See the baseline and release record for provenance and the exact three-archive inventory and digests.

Exit criterionCurrent evidenceRemaining product or maintenance gate
Multi-module calculator projectHOSTED GREEN, v0.4.0Preserve manifest admission and source closure on later code changes.
Same verified calculator logic on native and browser lanesHOSTED GREEN, v0.4.0Preserve the common success/failure corpus; add browser engines only with their own evidence.
Several stable-ID functions callable from TypeScript and RustHOSTED GREEN, v0.4.0; builder remains unpublishedMake the explicit supported-publication decision.
Browser calculator consumes Project exportsHOSTED GREEN for the admitted browser profile and renamed fixtureBroader browser support remains separately scoped.
Project daemon inspect/derive/preview/apply/rebuild loopHOSTED GREEN, v0.4.0Preserve the bounded transport and publication authority contracts.
Stable external API survives a display renameHOSTED GREEN, v0.4.0Preserve source-bound descriptors and both consumer corpora.
Project tests demonstrate native/Wasm equivalenceHOSTED GREEN, v0.4.0Preserve the full admitted entry/test and consumer corpus.
Multi-module line-filter productHOSTED GREEN for admitted native and Node/Core-Wasm executionDo not infer broader browser support from this profile.
Implemented v0.4.0 release gates and published archivesHOSTED GREEN; three archives publishedLater code changes need their own evidence; release acceptance is not general production support.

The release milestone is complete. The broader product-exit objective remains Partial because publication/support decisions and functionality beyond the admitted profiles remain open, not because the implemented v0.4.0 evidence is local-only or awaiting a tag rerun. Historical workflow attempts and retained logs keep their original identities and outcomes.

WP-01–WP-15 implementation and promotion audit

This programme is separate from the 55-row product contract. "HOSTED GREEN" here refers to the implemented v0.4.0 slice. An explicit registry, API, transport or platform support decision remains separate from CI execution.

Work packageCurrent source stateEvidence owner or implemented scopeRemaining gate
WP-01 CI decompositionHOSTED GREENDedicated product/platform matrices and release aggregation; required checksPreserve the closed aggregation and no-mask policy for later code changes.
WP-02 deterministic versionReleased, v0.4.0Version 0.4.0, exact source label, manifest and unpacked CLI agreement; release processPreserve exact version/commit binding; agreement is not a signature.
WP-03 release artifactsReleased, v0.4.0Linux x86-64, Apple Silicon macOS and Windows x86-64 archives with recorded checksumsAdd targets only with their own build-host smoke; no cross-host reproducibility is claimed.
Release authenticity follow-onLocal verifier implemented; hosted signed release absentThe configured tag workflow produces per-archive attestations and a signed aggregate provenance bundle. SigstoreOfflineVerifier can replay their Sigstore v0.3 cryptography without network access against exact caller-supplied historical trusted-root bytes. Release signing policy v1 owns the identity and nonclaim boundaries.Run and review a qualifying hosted tag release, publish its immutable signed asset set, record dated evidence, and decide identity-rotation ownership. Local verification does not establish current revocation state, publication, reproducibility, or support.
WP-04 v0.2 tagged artifact/release promotionComplete for v0.2.0Historical release, gate, archive and checksum record; v0.2 evidencePreserve the historical record without reusing its run IDs for a later commit.
WP-04 v0.4 tagged artifact/release promotionComplete for v0.4.0Accepted hosted-green code baseline and published three-archive milestone; v0.4 evidenceNo outstanding changelog-length or hosted-evidence task for this code baseline; unrelated product rows are not promoted.
WP-05 doctorHOSTED GREEN for the implemented bounded profilesProbe, Linux provisioner, provisioned Linux gate, and signed install retain explicit input, role, namespace, cgroup and store boundariesComplete any still-unimplemented active-generation handoff and explicit support decision; macOS/Windows production confinement and ordinary production profiles remain separate from admitted Linux evidence.
WP-06 newHOSTED GREEN for the calculator/library templates; the additive service template is local evidence onlyGenerator, scaffold replay, CLI preservation, Project checks and platform publication for calculator/library (Scaffold Capsule v3); the additive service template composing bundled auth, storage, HTTP, jobs, metric/export, tracing, and webhook decision dependencies (Scaffold Service Template v1) passes the same developer loop, pinned by crates/semaprax-toolchain/tests/cli_new_project_v1.rs::service_template_has_exact_bytes_and_passes_the_developer_loop. The intentionally ignored installed-product journey independently performs offline cargo install, scaffolds that service outside the checkout, and asserts both its web package and its single-Wasm-layer unsigned/unpublished local OCI artifact (tests/quickstart_v1/installed_journey.rs::clean_installed_toolchain_walks_the_documented_journey).Preserve the distinction between full-toolchain staged publication and standalone creation; installed-product breadth is limited to its admitted archive cases. Give the service template its own hosted/release-archive run before treating it as HOSTED GREEN like the other two templates.
Reference application (examples/task-service-project) follow-onLocal evidence; automated regression gate now exists (not complete)Composes bundled std.auth, std.db, std.http, std.jobs, std.log, std.log.redact, std.metrics, std.export.policy, std.tracing, and std.webhook decision dependencies into the deterministic full service scenario and its authorization, validation, migration, observability, export, and webhook decisions; no host authority is claimed. The reference and generated scaffold now carry a byte-bound closed host-configuration schema plus a credential-free fixture instance: SQLite/PostgreSQL, native HTTP/TLS, OTLP, and secret references are explicit host selections, while the default selects none of their authority. check, test, and run retain the interpreter gate, with native C11 -O0/-O2 and Core Wasm conformance closure (the entry closure remains interpreter/native-only), and declared web exports remain reachable in the semantic graph. The public coding-agent transport now exercises the real Project v3 Useful Data v1 service in a disposable project through workspace/open, rename derive, change preview, impact/review, apply, and retest; all five rename artifacts bind authenticated project_schema, while review uses schema-neutral equivalence claims. Source analysis/Workspace Semantic Graph admit 2..32 modules; actual changed-file and physical managed-transaction limits remain 16. The repository fixture remains unchanged. SPX-W121 still forbids an authored aggregate alongside a Public Useful Data web export. The deterministic offline OCI target admits exact Project v3 Useful Data v1 and Project v16 Useful Data v2 carriers, packaging only their independently replayed public app.wasm; it remains an unsigned, unpublished, non-runnable OCI artifact with no host authority. OCI Deployable Artifact v1, Scaffold Service Template v1, Authentication and Sessions v1, Durable Jobs v1SPX-W121 still blocks an authored record export. Physical SQLite/PostgreSQL, HTTP/TLS, telemetry, and secret-store adapters remain external to this fixture contract. Every other Project profile remains outside OCI packaging; signed publication, hosted/release-archive evidence, and any host/publish/hosted claim for this follow-on remain separately owned.
Semantic Kernel v1 trust-reduction follow-onRung 1 reached locally; no higher rung reached, and no hosted claimSemantic Kernel v1, Kernel-0 proof mechanization, and Rung-2 Formatter Authority v1: Lean 4 proves Progress and Preservation for the entire Kernel-0 language (including Let and non-recursive Call), with ranked call-chain termination, fuel-bounded progress, substitution preservation, and finite normalization; the proof has zero sorry/admit/custom axioms, and #print axioms reports only propext/Quot.sound. Issue #188 wires a source-pinned, hostile-input-aware kernel0-lean-proof-gate into quality.sh full and the release blocker set; a hosted verdict is still pending. The executable compiler-HIR reification predicate is tested but intentionally inert by design, so it does not narrow the admitted language. The from-scratch reference interpreter agrees with the compiler interpreter on the deterministic 74-program corpus, and prior native/Core Wasm differential coverage found 591 finite-corpus comparisons with zero disagreements; neither is a general theorem. The five formatter lanes now enter a bounded production comparison adapter: exact-source replay occurs before every candidate, a fixed 20-byte caller token (the exact i64::MIN exception) accepts only byte-equal candidates, and refusal/drift/mismatch preserves the Rust borrow. No external target runs in production; counters pin ordinary formatting through all five lanes. This remains finite local evidence only: it is not a rung-2/compiler component, general backend-equivalence theorem, owned-buffer authority transfer, or hosted support claim.Quote a hosted verdict from the wired Lean gate once one exists; derive and verify certificate weights from real HIR and compute an executable normalization bound; expand adversarial differential coverage; then obtain the owned-buffer/authority decision and independent hosted gate required for rung 2.
WP-07 quickstartHOSTED GREEN for the released source workflowQuickstart, checked examples and Project product gatesBroader installation/PATH environments require their own acceptance, not inference from source execution.
WP-08 v8 specificationSpecified and implemented within its bounded profilePublic Owned Data API v1 owns identities, admission, lifetime, compatibility and completion gatesKeep the contract synchronized; do not equate specification or CI with public support.
WP-09 canonical descriptorHOSTED GREENValidated-HIR derivation, canonical digest, independent replay, stable host names, hostile cases and legacy preservationRetain exact known-answer and replay coverage on later profile changes.
WP-10 direct Bytes npm/WasmHOSTED GREENCarrier, copy-out, tuple admission, intrinsic-brand hostility, private-frame exclusion and settlementBroader browser-engine support remains an explicit future claim.
WP-11 Option<Bytes> / Result<Bytes, i64>HOSTED GREEN, boundedFixed tags, active payloads, TypeScript mapping, cleanup, retained evaluation and generated-facade hostilityGeneral variant/resource APIs and broader physical/browser profiles remain separate.
WP-12 safe native/Rust SDKHOSTED GREEN; unpublishedProvider/SDK settlement, hostile handles, O0/O2, allocation, sanitizers and locked/offline consumersMake the explicit registry/support decision; do not call generated developer-preview packages published.
WP-13 Project v8 activationHOSTED GREEN; developer-previewManifest parsing, v1–v7 preservation, routing, retained evaluation and Windows full-host npm publicationRecord the owning v8 API/package promotion decision.
WP-14 frame-payload productHOSTED GREEN, boundedShared interpreter/native/Wasm/npm/Rust corpora, display rename, consumers and sanitizersBroader browser-engine and installed-archive consumer support remains separately scoped.
WP-15 v8 promotionHOSTED GREEN release evidence; formal public promotion openPromotion Receipt v1 replays independently supplied observations without granting authorityRecord the explicit API/package support decision and any additional provisioned scope required by that decision.
Agent Transport v5 follow-onHOSTED GREEN; unpromotedRead-only descriptor/carrier methods and legacy protocol preservationMake the explicit transport support decision; preserve its read-only scope.
Agent Transport v6 public-API follow-onHOSTED GREEN; unpublished and unpromotedAuthenticated v8–v11 descriptors, replayed npm carriers, closed profile discriminants, subject binding, zero writes and generated codecsPackage and support released clients intentionally; v9–v11 package and transport promotion decisions remain separate.
Project v9 flat owned record follow-onHOSTED GREEN; unpublished and unpromotedDescriptor, retained evaluator, Wasm/npm, native/Rust settlement, Revision Store and C/C++ provider-consumer profilesComplete additional aggregate fault, architecture and support scope required for public v9 promotion.
Project v10 owned UTF-8 follow-onHOSTED GREEN; unpublished and unpromotedDescriptor/evaluator, String accounting, Wasm/npm, native/Rust settlement and exact-length UTF-8 C consumersRecord prerequisite v9 and explicit v10 promotion decisions; broader profiles remain separately gated.
Project v11 nested owned-record follow-onHOSTED GREEN; unpublished and unpromotedSeparate descriptor/evaluator replay, cumulative-boundary npm and Rust execution, C11 multi-owner settlementRecord prerequisite and v11 support decisions and complete any additional claimed platform/browser scope.
Project Revision Store v1 follow-onHOSTED GREEN for admitted Unix/Windows profiles; unpromotedAuthority, identity, bounded replay, profile round trips and publication regressionsExplicit physical-host and public-support breadth remains bounded by the owning specification.

The Project v8–v11 generated packages remain developer-preview, non-registry surfaces unless their owning promotion decision says otherwise. Their hosted implementation evidence is no longer an outstanding task. An authority-free promotion receipt is a replay mechanism, not itself a support decision.

Long-term product contract

Every row below remains Partial at the mature-product level. The linked implemented slices have HOSTED GREEN v0.4.0 evidence. A link to a private, proof-only or bounded specification does not broaden its scope. The "Complete when" column describes the remaining mature-product threshold, not a claim that all of that functionality already exists.

Semantic foundation

RequirementStatusEvidence ownerComplete when
Source Agent and generated Proposal-client executionPartial; checked source Agent selection, generated Proposal clients, iterative typed execution and retained runtime associations are implemented with hosted-green evidence. Compiled incremental Proposal grammar and ordered adapter/journal replay additionally have local focused evidence.streaming Proposal decoder, adapter evidence, Agent lowering, Agent Object, iterative lifecycle, Direct Runtime v2Broader Proposal shapes, compiled model/effect roles, maintained packaging/public ABI, provider transport and all claimed consumer/target profiles are complete. Do not reimplement the already admitted iterative lifecycle or Runtime-v2 association as a missing feature.
Agent-native semantic programPartial; AgentDefinition/AgentGraph/deployment separation, source-owned interaction facts, checked iterative typed execution, per-operation durable recovery, pure and durable migration, and linked Project/workspace associations are implemented. Stage execution is sealed behind the StageExecutor seam and one dispatch route, gated by a non-forgeable ExecutionAuthority (src/agent_lifecycle/authorization.rs): a compile_fail doctest proves the sealing supertrait is unreachable from outside the module, and the_stage_executor_seam_has_exactly_three_implementations_and_one_dispatch_route (src/agent_lifecycle/tests.rs) pins the three reviewed implementors (interpreter, native C11, Core Wasm) and zero second routes across the lifecycle, durable, rich-stage and iterative-driver modules. Bound deterministic stage bodies execute on all three and are compared value for value. A private frozen-run selector additionally carries all three through the shared proposal, authorization, injected-read, transition, cancellation, lifecycle-budget and evidence-settlement kernel. This is local clang/node-gated evidence, not a hosted or production-backend claim; production, live-provider, checkpoint and migration routes remain interpreter-selected, and native/Wasm interpreter-fuel and cleanup-event parity remain open. Frozen Runtime v1 remains a compatibility product, not the limit of current execution.RFC 0001, Agent Object, interaction facts, payment harness, typed effects, checkpoints, durable migration, linked lifecycle, linked migrationFinish the broader graph-operational programme, complete persistent/incremental semantic lifecycle and general intentions, target-runtime/provider/conformance evidence, separate raw-source authority and representative validation. Distributed writers, automatic reconciliation and general public ABI remain separate. Native/Wasm Agent-stage execution (#142/#143/#182) remains private/local until production selection, fuel/cleanup parity and hosted evidence exist.
Human-readable programPartial; canonical .spx, separate source/semantic digests, ProgramRoot v1/v2/v3, exact context and source-owned Agent/contract/test facts are retained and replayed without changing frozen identities.RFC 0001, canonical workspace revision, ProgramRoot v1, v2, v3, exact context v2, contracts/testsCanonical source round-trips every stable language feature with migrations and reviewable diffs; complete source/meaning coverage across the mature language.
Verified source semanticsPartial; exact workspace/context selection, retained HIR facts, authority-free transactions, bounded universal queries and the process-resident incremental semantic service are implemented. The stdio and MCP facades preserve their closed authority-free service contracts. The versioned Rust embedding facade exposes bounded byte-only analysis, opaque Project sessions, exact refresh/candidate replay and capability-gated deterministic execution with local lifecycle/host-consumer evidence.Architecture, Universal Query, Universal Transaction v1, v2, composition, semantic service, Rust embedding API, stdio, MCPAll admitted language features reach validated HIR only after complete type, effect, contract and ownership checks; broaden shared/durable service transports, cover every mature semantic object family, preserve comments and unrelated trivia, and broaden the transaction algebra without bypassing validation.
Cross-backend semantic equivalencePartial; admitted scalar, numeric-text, String, owned-data, generic and collection corpora execute through their interpreter, C11 and Core-Wasm profiles with hosted-green release evidence. The bounded source-level resumable slice now has a deterministic compiler-owned ordered plan for one to eight direct sequential Copy-scalar yields, an authority-free production preparation profile that emits bounded plan/state/target-bound native C11 or Core-Wasm artifacts in memory, a public bounded checkpoint envelope HMAC-authenticated under exact caller-supplied ProgramRoot/invocation/policy facts, and local cfg(test)-only execution parity evidence through the interpreter, native C11 -O0/-O2, and Core Wasm. Its per-site suspension binding commits exact checked-program, site, scalar-argument and prior-answer bits; replay checks every recorded request, and covered intermediate/final/contract failures retain normalized statuses. Its closed projection retains only the selected and authored-entrypoint direct-call closures, so disconnected yielding functions are isolated; retained helpers must remain explicit, effect-free and Copy-scalar. Ordinary native/Wasm emission still refuses yields (SPX-B116/SPX-W126); prepared artifacts and decoded checkpoints grant no execution, publication, host-call, answer, or storage authority, and arbitrary Wasm NaN-payload preservation is unclaimed because the test adapter crosses JavaScript Number. The reference v1 journal now resumes an observed partial tail without redispatch and skips cleanup on replayed in-memory terminals, but has no durable append sink or cleanup-settlement wire, so decoded terminal cleanup and crash recovery remain unclaimed. There is no owned live-frame/liveness lowering, control-dependent yield, public continuation ABI, runtime scheduler, durable checkpoint store/service or source-level resumable_effects::core reuse, and #204 remains open beyond this bounded plan.Conformance Trace, Resumable Effects v1, String operations, owned-data API, UTF-8 API, native String settlement, String interpreter, Wasm StringsEvery supported backend passes the same complete behavior, failure, cleanup and contract corpus for the mature language; separately specified opt-in or broader target profiles require their own evidence. General resumable lowering still requires control-dependent yields, owned state, effectful prefixes, a public execution/runtime profile and durable recovery.
Atomic agent changesPartial; exact-old-state rename, ReplaceBlock, AddContract, AddDeclaration and additive body ReplaceExpression validation/replay are implemented. Composition admits its bounded structural diff, rename rebase and ordered sibling-rename merge; validation remains authority-free and does not itself publish.Universal Transaction v1, v2, composition, workflow CLI, patch evidence, workspace change, Candidate Git publicationGeneral supported single- and multi-file semantic changes replay and publish atomically with recovery and provenance; preserve comments and exact unrelated trivia, broaden typed operations/preconditions, and close the remaining same-principal repository-content and publication-host hostility scope.

Language and safety

RequirementStatusEvidence ownerComplete when
Records and algebraic variantsPartial; bounded concrete and generic owned records, nested reconstruction, exact destructuring/update, multiple owners, admitted authored generic variants and owned Result execute with checked cleanup and hosted-green backend evidence for those prior profiles. Direct monomorphic String variant payloads additionally pass the local cleanup_backends::owned_string_variant gate across interpreter, C11 and Node Core Wasm; hosted validation of that addition remains separate.RFC 0002, owned records, concrete generics, nested records, destructuring, update, variants, generic variants, String variantsVerify general owned propagation, generic package signatures, nested/resource aggregates, variants, matching, cleanup and public generic ABIs. Previously green nested-relay and generic-owned gates remain regression obligations, not unexecuted tasks.
Functions, closures, interfaces, implementations, genericsPartial; explicit forwarding, scoped argument inference v3, generic owned-record/result composition, compiler collections, private function values and scalar-snapshot/generic-loop closures are implemented. Graph, cleanup and ProgramRoot replay retain exact instance and mapping identities. A separately versioned bounded owning-capture closure profile (own fn() -> R { body }, exactly one lexical owned Bytes capture and one call) additionally executes end to end on all three backends, which agree on the observable result: hir::closure::desugar_owning_closures rewrites the verified construction-plus-its-call into a direct call before resolution, and interpreter::interpret, codegen::emit_c and wasm::emit_module each apply it before their own hir::resolve. Equivalence is pinned by called_owning_closure_agrees_across_interpreter_native_and_core_wasm and uncalled_owning_closure_agrees_across_interpreter_native_and_core_wasm (tests/cleanup_backends/executable_owning_closure.rs), which compare interpreter, native -O0, native -O2 and Core Wasm results and additionally count the captured allocation as exactly one alloc and one free on every backend with a real allocator. The closure literal itself is still never lowered by any backend, and hir::resolve still refuses own fn with the stable SPX-H006 diagnostic for any caller that does not substitute first.Function Values v1, v2, Closures v1, v2, owning-capture closures v1, inference v3, record composition, multiple owners, owned Result, forwarding, compiler collectionsComplete constraints, broader inference and nested variant/Result composition, general interfaces and implementations, public callable/generic ABI and generic package signatures. The admitted inference, closures and GEN-06 hosted evidence are already present.
Option and Result; no null or unchecked exceptionsPartial; admitted owned Result construction, matching, calls and same-typed ? retain evaluation-once, conditional ownership, sticky failure and cleanup across the claimed engines; generic owned Result profiles are additive.RFC 0002, owned variants, generic owned Result, owned-data APIGeneral nested owned propagation, residual conversion, public ABI and complete target behavior are verified beyond the admitted concrete and generic profiles.
Immutable-by-default values and explicit mutationPartial; bounded scalar, field and immutable nested reconstruction profiles have hosted-green evidence.Explicit Mutation, Field Mutation, Nested Immutable UpdateVerify general aggregate, collection, borrowed and concurrency-aware mutation rules.
Unique ownership and move safetyPartial; exact cleanup/replay covers admitted records, variants, Bytes buffers, Vec, scalar/Bytes owning iterators, consuming loops, renewal and generic map/filter/fold. Vec v2 and owned iterator payload v2 retain their separate prelude/graph/cleanup versions and no public generic ABI.RFC 0003, Owning Iterators, owned payloads, loops, renewal, generic operations, byte buffer, Vec v1, Vec v2, bounded traversal, shared loansVerify general owned values and ?, aliases, control flow, FFI, cleanup and public ABI. Iterator interfaces, lazy adapters and payloads beyond the exact admitted Bytes/scalar profiles remain separate. Existing iterator and generic-owned hosted selectors are regression gates, not pending first execution.
Owned allocation and extractionPartial; frozen scalar Box v1/std.mem and additive Box<Bytes> v2 implement allocation, consuming extraction, recursive lexical cleanup, refusal-before-commit and exact graph/ProgramRoot bindings with hosted-green evidence.Box v1, Box v2, RFC 0003Broader owned payloads/composition, general allocation, public ABI, regions, arenas and shared ownership are complete. Borrowed box_get<Bytes> remains rejected by the owning profile.
Borrowed views and lifetime safetyPartial; bounded shared loans, projected fields, synchronous borrowed calls and nested paths have hosted-green evidence.Useful Text, Shared Loan Plan, Projected Field Borrow, Nested Records, Nested Destructuring, Borrowed CallsComplete general lifetime inference, mutable and escaping borrows, cross-file use and public host ABI behavior.
Regions and arenasPartial; report/model scope remains distinct from runtime placement.Region ReportRegion inference and runtime placement are implemented and verified; the report alone is insufficient.
Shared immutable ARC and managed zonesPartial; proof/model scope is unchanged by hosted execution of its tests.ARC Zone ModelLanguage, runtime, cycle, escape and concurrency semantics execute on supported targets.
Restricted unsafe and raw memoryPartialUnsafe BoundariesRaw memory operations, review policy, capability rules and target conformance are implemented and verified.
Checked, wrapping, and saturating arithmeticPartial; admitted arithmetic and checked usize correction regressions have hosted-green evidence.RFC 0001, Indexed Byte DataAll numeric widths and named arithmetic modes have complete cross-backend semantics and tests; preserve zero-multiplier and owned-cleanup regressions.
Effects and capabilitiesPartial; admitted manifests and typed operation bindings preserve explicit authority.Capability Manifest, Typed EffectsDeclared effects and build/runtime capabilities are enforced end to end, including dependencies and hosts.
Contracts and progressive verificationPartialRFC 0001Static discharge, bounded proof, runtime obligations, counterexamples and repair evidence are integrated.
Structured concurrencyPartial; the bounded Rust scoped-thread runtime adds borrowed captures, stable-ID starts/reports, cooperative cancellation, panic normalization, mandatory join and invocation-owned HTTPS settlement. This is not general language task lowering.Scoped Task Model, Structured Tasks RuntimeLanguage syntax, Sendable/Shareable checking, dependency scheduling, deterministic replay, native/Wasm task lowering and target task execution are verified.
Typed hygienic generationPartialHygienic GenerationGeneral typed synthesis is scoped, hygienic, deterministic and integrated with multi-file semantics and review.

Compiler and output targets

RequirementStatusEvidence ownerComplete when
Fast development lanePartial; interpreter, prepared Project trace, revision-replacement, and the cross-process persistent semantic cache (semaprax semantic-cache-persist/semantic-cache-load) profiles have hosted-green release evidence. The persistent cache reuses authenticated checked HIR across processes; measured on examples/calculator-project: cold check 0.03s, semantic-cache-persist 2.58s, semantic-cache-load 1.28s with full checked-HIR reuse (modules_reused:3, checked_HIR_reused:3, zero re-resolution). This is named precisely as restart-with-reuse, not hot reload, and not itself a wall-clock win at this scale. MAX_PROJECT_CHECKED_MODULE_CACHE_PREBOUND now shares the ordinary 64 MiB Workspace Semantic Graph ceiling instead of imposing a smaller independent 16 MiB limit, and an executable regression persists and reloads examples/task-service-project with checked-HIR reuse.Interpreter, Internal Strings, Prepared Project, Revision Replacement, Project Semantic Cache v1, Persistent Semantic Cache v1Incremental refresh, debugging, hot reload and semantic equivalence meet the development-performance target across the supported language and platforms; retain the task-service persistent-restart gate and add performance evidence only where it demonstrates an actual development-loop improvement.
Optimizing native lanePartialArchitectureThe production native backend covers the mature language, optimization, debug mapping and supported hosts.
WebAssembly core and componentsPartial; admitted core/component/String profiles have hosted-green evidence; private Component execution is not a stable public Component ABI.Scalar Exports, Owned ABI, UTF-8 API, Wasm Strings, WIT BoundaryStable Components, resources, capabilities, multi-engine conformance and packaging are verified for the mature supported surface.
Embedded and real-timePartialFreestanding ProfileHardware profiles, linker control, interrupts/RTOS, timing constraints and representative targets are verified.
SIMD and GPUPartialSIMD ReportVector/GPU lowering, legality, memory behavior, target selection and performance evidence are implemented.
Whole-project and per-function compiler capacity ceilingsPartial; SPX-G171 (Workspace Semantic Graph builder-bytes budget, MAX_BUILDER_BYTES = 67,108,864 bytes, src/workspace_graph.rs) and SPX-H006's cleanup-replay bounds (MAX_REPLAY_PATHS = 65,536 terminal paths per function and MAX_REPLAY_WORK_UNITS = 32,000,000 program-wide work units, src/cleanup_plan/replay.rs) are measured, named with exact constants, and pinned by boundary regression fixtures. The graph budget was raised from 18 MiB to 64 MiB only after the canonical catalog-normalizer application's complete eight-module source-test projection forecast 46,202,120 bytes but exceeded the intermediate 48 MiB ceiling during live construction. Its fully scalar, allocation-last canonical response writer and thirteen-case source suite also exceeded both the former 8,000,000-unit global skeleton preflight and an intermediate 16,000,000-unit probe while remaining below the unchanged per-function path ceiling, motivating a separate measured work-unit increase to 32,000,000. The focused interpreter/native/Core-Wasm fixture exercises both ceilings; the checked-module cache remains separate.Semantic Kernel v1, Workspace Semantic Graph, RFC 0003Reconcile the lower checked-module-cache ceiling with the graph budget and retain the catalog-normalizer near-bound executable fixture for future increases. Keep the per-function path ceiling unchanged unless a separate finite-resource case demonstrates the need.

Ecosystem interoperability

RequirementStatusEvidence ownerComplete when
Interface-first packages and target matricesPartial; the table manifest lowers onto frozen Project profiles; exact local dependency subjects, semantic locks, source capsules, scalar linking, generated Cargo inputs and bounded lock/resolve routes have hosted-green evidence. Internal generic ownership does not widen cross-package scalar signatures.Package Manifest, Project Dependencies, Project Lock, Resolution, Package Report v2, Semantic Lock v3, Resolver v2, Source Capsule, Linked Wasm BuildGeneric package signatures, general compatibility negotiation, supported publication, trusted provenance, registry and conformance are complete.
Portable canonical ABI and native fast ABIPartialABI Report, Owned Data API, UTF-8 APIStable aggregate/resource/borrowed ABIs and cross-language conformance cover supported architectures.
C and Objective-CPartial; admitted C11 provider/consumer profiles cover owned bytes, compiler-owned Option/Result, UTF-8, flat records and nested multi-owner settlement at O0/O2 with hosted-green release evidence.C Header, C/C++ Owned Data Package, Flat Record API, UTF-8 API, Nested Record APIBroader import/export, authored-variant/resource ownership, Objective-C adapters, cross-platform consumers, compatibility, maintained distribution and supported-host conformance are verified.
C++Partial; admitted scalar, Project-v8 owned-data and Project-v9 flat-record adapters have hosted-green compiled-consumer evidence.C++ Shim, Scalar Package, Owned Data Package, Flat Record AdapterCross-platform/MSVC consumers, broader aggregate failure and borrowed-lifetime profiles, maintained distribution, compatibility and supported-host conformance are complete.
Java and KotlinPartial; private JNI/emulator evidence remains private.Android JNI OwnershipPublic JVM/JNI artifacts, ownership, exceptions, packaging and conformance are verified.
Swift and Apple frameworksPartial; private framework/simulator evidence remains distinct from public/device support.Swift OwnershipPublic Swift/Objective-C API, distributable frameworks, lifecycle, ownership and device evidence are verified.
JavaScript and TypeScriptPartial; admitted Node/TypeScript/browser and generated owned-data/String consumers have hosted-green evidence.Scalar Exports, Owned Data API, UTF-8 API, Wasm Strings, String Web PackageStable general bindings, owned resources, async/callbacks, maintained packaging and the claimed multi-engine browser/runtime breadth are verified.
WIT and WebAssembly ComponentsPartial; scalar interface projection and private Component runtime profiles have hosted-green evidence.Public Scalar WIT, Private WIT BoundaryExtend the retained Project-v1 scalar interface artifact into supported Component publication; source-selected interfaces and resources run through a supported Component Model toolchain on multiple runtimes.
OpenAPI, Protobuf/gRPC, GraphQL, and SQLPartial; existing OpenAPI projection does not implement every named schema family.OpenAPIImport/export, compatibility, live conformance and all named schema families are verified.
Standard libraryPartial; the current bundled core, portable, alloc, hosted, agent and test packages have hosted-green evidence for their listed profiles. The generated catalog owns the exact inventory. Implemented additions include authenticated Vec/Box aliases, JSON decoding and cursor adapters, Reader/Writer and formatting/logging, typed paths, bounded filesystem/environment/process I/O, byte assertions/snapshots and private linked std.agent roles. The additive std.io.lines sibling package (view helpers, borrowed line observers, a preflighted line copy into caller capacity and the consuming line transition, with graph-pinned per-shape cleanup-schema selection) executes on the interpreter, C11 -O0/-O2 and repeated Core Wasm with hosted-green on the named std-library-depth job and the verify-tests shards at 1dfe12a6, outside the v0.4.0 release baseline. The additive std.path.normalize sibling package adds lexical normalization of typed Path values (separator-run collapse, . removal, .. cancellation, root and empty-result policy) with the same three-backend hosted-green evidence and a graph-pinned cleanup-schema selection. Additive std.format field padding (pad_len, append_fill, left-aligned text and right-aligned decimals, each preflighting the whole field and never truncating) runs with the existing format corpus on the same three backends. Additive std.bytes span cursors add ASCII trimming and empty-field-preserving delimiter walking with the same three-backend evidence. Additive std.log level filtering adds an explicit threshold predicate, a capacity-aware admission observer and a named drop path. Additive std.data.csv quote-aware field cursors walk one record's fields and content bounds. Additive std.test failure masks name the failing check through an exclusive per-case bit, a first-failure index and a failure count. std.data.json.dec gained buffer-free decoded comparison of two JSON string tokens, the additive std.encoding.base64 sibling package encodes padded Base64 from a borrowed view with no buffer, and std.num.overflow closed its own recorded wrapping-multiplication gap with exact two's-complement results at i64::MIN, i64::MAX and every sign combination; these three are hosted-green at 78ee5107. std.data.toml gained quoted-key validation with the full basic-string escape set and quote-aware value spans. Checked atomic writes add a fieldless WriteOutcome in private filesystem v3, with local interpreter/native/Wasm outcomes, nested refusal and malformed callback gates (project harness filesystem_v3); legacy filesystem regression gates stay intact. Effect-free policy additions cover the hosted and agent tiers without granting authority: std.fs listing cursors over the canonical immediate-name listing, the std.env.policy sibling package holding environment name and assignment policy that std.env's own effect gate would have forced to over-declare a capability, std.process exit-versus-signal settlement classification and argument admissibility, and a std.agent stage-transition, terminality and bounded retry policy that reads no clock and schedules nothing. The bundled-dependency registry (src/project/standard_dependencies.rs) now also admits std.auth, std.db, std.http, and std.jobs in an ordinary project's [dependencies] -- these shipped as pure source under std/ for issues #189-#192 but were unreachable from any project manifest until this change, pinned by unit tests in the same module.Standard Library, catalog, Authentication and Sessions v1, Durable Jobs v1, JSON Cursors, IO Cursors, IO Lines, Path Normalization, Typed Path, Filesystem v2, Checked Host Outcomes, Project v19, Environment I/O, Process I/O, Byte Assertions, Linked Agent Lifecycle, Project v16, Project v18Every required module exists at its tier with identities, contracts, effects, examples, conformance on every listed target and generated documentation; the Everyday profile and remaining offline templates ship. Full streams/traversal, broader physical providers, general Agent support and richer testing remain outside their bounded current slices.

Application platforms

RequirementStatusEvidence ownerComplete when
First-class application/state/UI dialectPartialUI SchemaTyped state/update/view, semantic controls, accessibility, navigation, assets and platform escape hatches execute.
WebPartialWasm Scalar ExportsAccessible DOM/CSS, SSR/hydration, packaging, multi-engine execution and a deployable sample are verified.
iOSPartialSwift OwnershipPublic framework/app generation, lifecycle, accessibility, signing metadata and device/simulator samples are verified.
AndroidPartialAndroid JNI OwnershipPublic AAR/app generation, lifecycle, accessibility, packaging and emulator/device samples are verified.
macOSPartialDesktop AppPublic host/UI generation, lifecycle, accessibility, packaging, signing/notarization and a sample are verified.
WindowsPartialDesktop UIPublic host/UI generation, lifecycle, accessibility, MSIX/signing metadata and a sample are verified.
LinuxPartialRoadmapA supported UI/runtime adapter, accessibility, distribution formats and a representative application are verified.
Edge and serverPartial; bounded TCP/TLS/listener and HTTPS operations, fixture replay, aggregate deadlines, caller-selected providers, loopback browser execution and the admitted native libcurl adapter have hosted-green evidence. A cross-compiled Windows branch is not physical Windows execution.Language Network I/O, Network Services, HTTPS Runtime, HTTPS I/O, bounded POST, Project ManifestLive browser service adapters, multi-engine evidence, HTTP/3, cross-platform libcurl provisioning, DNS policy, structured async services, observability, deployment and load/conformance tests are verified.
PluginsPartialPlugin ManifestCapability-limited loading, lifecycle, compatibility, resource limits, packaging and hostile-plugin tests are verified.

Agent economics, review, and operations

RequirementStatusEvidence ownerComplete when
Token-budgeted semantic contextPartial; bounded standalone and authenticated Project context use retained typed indexes without requiring full graph transfer. Compact CLI/service views replay losslessly. Additive model-text v2 saves 14–18% of measured tokens on two large graphs and 11% on an HTTP task context; small views grow 5–7%.Agent Context v2, compact projection measurements, Economics, Workspace ImageExact model-token budgets, broader semantic edges, persistent indexing and representative measured savings are verified.
Impact analysis before modificationPartialSemantic Impact, Workspace ImageRepository-wide call/type/contract/test/schema/target/capability consumers are complete and incremental.
Typed holes and compiler-generated repairsPartial; installed SPX-S103 catalog/plans, typed Candidate holes and their admitted repair routes have hosted-green evidence; plans remain authority-free and do not rank or apply arbitrary repairs.Diagnostic Repair, Installed Fix Plan, Candidate HolesGeneral obligations and composable sound repairs are generated, ranked, reviewed and replay-verified.
Proof-carrying patchesPartialPatch Evidence v2General semantic claims, tests, targets, capability deltas, provenance and compatibility are independently verified before commit.
Project-bound assurance reportsPartial; deterministic source and Project/ProgramRoot assurance reports derive audited AST/HIR obligations and explicitly selected held static architecture claims, with independent source-bound replay.Assurance Manifest v1, Project Assurance Manifest v1; workspace project_assurance_manifest and projections assurance_manifest::project_cli gatesBroader proof backends, architecture predicates, target evidence and policy integration retain their own completion requirements.
Semantic human reviewPartialSemantic ReviewComplete repository-wide behavioral, API, security, memory, target, migration and unsafe summaries are evidence-backed.
Graph-derived documentationPartial; checked module documentation, generated library/shapes catalogs, bounded topic/diagnostic help and version-matched installed guidance are implemented. Their hosted-green tests do not make the bounded shapes a complete grammar or node catalogue.Documentation Projection, Guided CLI Help, Installed GuidanceDocument whole projects and their use closure, generate bundled agent skills and standard-library catalogs from one complete stable semantic graph document, and expose the projection through editor and workspace sessions.
Unified 1.0 command surfacePartial; unified verify/review/agent/query/package/add/fetch/doc, exact installed guidance/diagnostics/fix-plan adapters, bounded service transports and scripted Agent run/replay are implemented. doctor is dispatched by the shared driver in both binaries; native Rust package building and the full staged-publication hooks remain private-host operations.Unified CLI, Workflow CLI, Installed Guidance, Installed Diagnostics, Fix Plan, Service Transport, Service MCPAdmit remaining verbs, including unadmitted Agent resume/reconcile routes, with their own gates; make the private-host split invisible to promoted workflows and drive editor surfaces from the same catalog.
Editor integration by meaningPartial; saved-source diagnostics, stable-identity navigation, Project-routed context, code lenses, semantic review/rename and bounded Agent/candidate views are implemented. The historical local Extension Host witness retains its original subject and platform; current release evidence is hosted green within admitted editor gates.VS Code Adapter, Unified CLI, VS Code Host Evidence v2Drive the remaining editor surfaces, packaging and manual UI from the same catalog and verify the claimed host/platform breadth. A historical single-platform witness does not establish every possible editor or environment.
Sandboxed builds and dependenciesPartial; exact held Project subjects, generated Cargo inputs, semantic locks and bounded linked builds have hosted-green release evidence. Held source authority and absence of implicit tool execution are not a hermetic OS sandbox.Project Dependencies, Capability Manifest, Offline Lock, Resolver, Source Capsule, Pure Wasm Build, Linked Wasm BuildVerify reproducible acquired inputs, generic package signatures, supported publication and actual least-authority OS sandbox/dependency enforcement.
Debugger, profiler, diagnostics, and operationsPartial; bounded installed static diagnostic inventory and exact identity/provenance explanation have hosted-green evidence. Static presence is not complete runtime reachability, wording, repair knowledge or backend coverage.Architecture, Human Diagnostics, Installed DiagnosticsSource-level debugging/profiling, crash and trace mapping, complete runtime diagnostic semantics and repair guidance, observability and deployment diagnostics cover every backend.

Public-generic TypeScript settlement increment

Status remains partial. The owning settlement specification records immutable module-byte admission, bounded single-call host settlement, full result preflight, sticky release evidence, replay and a bounded native semantic comparison. This is the flat-owned-Bytes host reference caller, not a compiler-derived generic provider, complete four-language proof, browser matrix or hosted promotion. Required Rust-generator and full quality gates must be executed separately before advancing their evidence class.

Public-generic compiled-reference settlement increment

Status remains partial. A compiled C11 reference route now executes in-module allocation, handles, copying and failure settlement under Core Wasm and compares them with the same native corpus. Its raw host calls are not the generated TypeScript public ABI. Clang-compiling the reference fixture is not evidence that Semaprax compiled an admitted generic endpoint. Compiler-derived descriptors/subjects, nested records/all Copy scalars, full consumer/model participation, Rust bridge execution and hosted closure retain their separate requirements.

Final validation product

Completion requires one maintained offline-first product built from a shared SEMAPRAX codebase with web, iOS, Android, macOS, Windows, and Linux clients; native notifications and secure storage; local databases; native or WASI server execution; authentication; background synchronization; a custom accelerated visual; one C library; one JavaScript package; and one WebAssembly component.

Every artifact must be built and exercised in CI or on representative simulators/devices. Platform-specific implementations must be declared rather than hidden behind false portability. No current narrow prototype satisfies this final gate. The v0.4.0 hosted-green release advances the implemented slices without claiming this mature-product completion.