Graph-operational programme: requirement and evidence ledger
September 10, 2026 · View on GitHub
Audience: compiler contributors, agent builders, and programme reviewers.
Status: full programme remains Partial. This ledger preserves the complete
requested objective: canonical human .spx source, persistent derived semantic
workspaces, typed intentions and candidate overlays, independently replayed
source materialization, and separate publication authority. Completing a
bounded image, query protocol, or append-parameter operation does not complete
that objective.
The completion matrix owns product status. This ledger preserves the full programme requirements, not a replacement product denominator. The implemented v0.4.0 slices and their admitted regression corpus are HOSTED GREEN under the release baseline. Earlier writing-session labels are superseded; completed release checks are maintenance obligations, not unexecuted backlog.
Partial means an implemented bounded mechanism still leaves part of the stated mature-product requirement open. Missing means the requested integrated mechanism has not been implemented; a related utility is not a substitute. Neither a green release nor an authority-free report promotes an unpublished package, a private API or a broader target/provider claim. The exact-subject archived executions retain their original counts, platforms, measurements and limitations. They are historical witnesses, not the current release's evidence ceiling. No new comparative model trial, physical device run or general performance result is inferred.
Evidence owners
| Key | Source, specification, and executable evidence |
|---|---|
| Image | image.rs, Image v1, image evidence, CLI evidence |
| Facets | image_facets.rs, Facets v1, facet evidence |
| Concrete generic-function navigation | Function Instances v1; source-template-bound retained-instance pages and exact instance facets, callers and closure relationships, implemented; no new instantiation or execution |
| Generic template rename | Generic Template Rename v1; explicit stable-ID display rename with exact retained concrete-instance/type-argument and normalized checked-HIR preservation through full Project replay, implemented; no generic signature evolution, external compatibility or execution |
| Protocol | image_transport.rs, Image Agent Protocol v1, protocol evidence |
| Candidate | candidate module, intent constructors, Candidates v1, candidate evidence |
| Candidate protocol | candidate transport, Candidate Protocol v2, protocol evidence |
| Holes | draft module, Typed Holes v1, hole evidence |
| Signature mapping | signature engine, Signature Evolution v1, Owned Result Wrap v1; the result lane wraps one exact whole owning Bytes/String result in an existing visible one-field owning record and migrates authenticated local body callers, implemented |
| Computed signature arguments | Argument Expressions v1; explicit scalar and stable-ID Copy nominal computations over staged original parameters, caller-local annotations and rebuilt checked-signature admission, implemented |
| Expression changes | expression module, Expression Change v1, expression evidence |
| Immutable lexical bindings | Lexical Binding Constructor v1; scoped initializer reuse through ordinary candidate admission, implemented |
| Compiler-owned byte calls | Builtin Call Constructor v1; stable-ID selection of the existing byte/string operation inventories, including the exact rooted owning String view, shared schemas/discovery and complete source replay, implemented; direct authenticated field places are implemented by Field Place Constructor v1 |
| Contract changes | intent module, Contract Change v1, candidate evidence |
| Rebase | rebase module, Candidate Rebase v1, rebase evidence |
| Declaration creation | function declaration module, type declaration module, Declaration Change v1, function evidence, type evidence |
| Extraction | extraction module, Extraction v1, Owning Capture Extraction v1, Copy evidence, owning evidence; one exact local whole Bytes/String owner can transfer through a fresh helper boundary, implemented |
| Recovery | recovery module, Recovery v1, recovery evidence |
| Typed-hole restart recovery | draft recovery module, Draft Recovery v1, library evidence, v5 evidence |
| Self-contained draft recovery | Draft Archive v1; canonical original sources plus valid history and pending selectors, source-independent library restore, startup-only historical host restore and current-base RPC restore, implemented |
| Durable typed drafts | Draft Persistence v1, v5 Archive Store Protocol; shared immutable archive store with independent typed replay, explicit persist/load commands, closed startup-policy v6 selection, and automatic optional retention checkpoint after a successful draft/archive-store, implemented |
| Draft semantic rebase | Draft Rebase v1; checked-history rebase, source-region conflicts and authenticated remapping of pending body/expression/contract holes, without implicit completion, implemented |
| Draft semantic merge | Draft Merge v1; common-base history merge, opposing-write checks, independent pending-selector rebinding and bounded union without inferred completion, implemented |
| Candidate archive persistence | Archive v1, immutable Archive Store, CLI, v5 Archive Store Protocol; independently rebuilt original source and exact complete history, with optional automatic post-store retention checkpoint through distinct startup-held roots, implemented |
| Startup archive recovery | Workspace Archive Recovery; host-only historical candidate retention with live authentication and unchanged approval boundary |
| Declaration moves | movement module, Declaration Move v1 |
| Nominal declaration rename | Nominal Rename v1; shared authenticated occurrence planning for explicit source records/variants, full candidate replay and conservative nominal rebase, implemented |
| Member rename | Member Rename v1; shared cross-file occurrence planning for explicit record fields, variant cases and payload fields, full source replay and conservative owner-shape conflicts, implemented |
| Aggregate-member changes | field migration, Record Field Change v1, Variant Case Change v1; the variant lane appends one owning Bytes case under exact checked shape/TypeFacts replay, implemented, while String variants remain unsupported |
| HIR relationships | relationship facets, HIR Relationships v1 |
| Declaration dependencies | shared index, Dependencies v1; lazy immutable-image access and caller indexes shared with candidate deltas, implemented |
| Compact declaration navigation | Dependency Navigation v1; bounded summaries and reference-bound sites/callers/calls/members pages over the shared index, implemented |
| Cross-session function references | Function Reference v1; canonical exact-image function/facet selectors with source provenance, fresh summary/handle resolution after an identical rebuild, closed v5 reads and detached batch support. Candidate Function Reference Rebind v1 independently derives one candidate's base/final images and conservatively returns a fresh exact destination selector for a surviving unique explicit stable identity; no protocol route or compatibility inference, implemented. |
| Candidate tests | test planning/execution, Candidate Tests v1, Test Protocol v3 |
| Candidate diagnostics | attempt/repair module, Candidate Diagnostics v1 |
| Managed publication | publication bridge, Candidate Publication v1 |
| Image lifecycle | image_store.rs, Image Store v1 |
| Semantic deltas | delta.rs, Semantic Delta v1 |
| Contract deltas | Contract Delta v1; whole-candidate predicate and static callable-dependency comparisons, exact replay and v5 chunks, implemented |
| Ownership deltas | Ownership Delta v1; checked nominal members and available type facts alongside signatures, structural inventories and complete ordered loan/cleanup comparisons with exact replay, implemented |
| Candidate ABI deltas | Candidate ABI Delta v1; manifest-selected callable signatures, reachable concrete nominal shapes and retained native/Wasm structural projections with exact replay, implemented; compatibility, runtime, deployment and external consumers remain explicitly unassessed |
| Cleanup dependencies | Cleanup Dependencies v1; reverse type/case/field selection over actual retained inventory/cleanup/loan facts, original plan coordinates and candidate before/after review, implemented |
| Artifact deltas | Artifact Delta v1; actual base/candidate Web/npm, OpenAPI and C source file and stable export comparisons after full replay, under the existing build grant, implemented |
| Candidate artifact boundary evidence | Candidate Analysis Artifact Evidence v1; exact candidate coverage plus one independently replayed selected pathless carrier delta, changing only generated artifacts to partial; library and v5 build-granted chunk evidence implemented |
| Candidate runtime boundary evidence | Candidate Analysis Runtime Evidence v1; exact candidate coverage plus one independently replayed, policy-bounded reference-interpreter test closure, changing only runtime environment to partial; library evidence implemented |
| Candidate function facets | Candidate Function Facets v1; final-candidate compact summaries and all nine existing HIR facet pages with candidate-bound handles and cursors, implemented |
| Diagnostic protocol | Diagnostic Protocol v4 |
| Integrated managed workflow | Workflow v1, authored scenario |
| Focused canonical-Git execution evidence | Execution Evidence v1; exact subject 474c481bf3c3561c144e077f0000460f61af55f2 passed the locked/offline local three-test selection with authenticated SHA-1/SHA-256 economics exports; managed, generated-client, MCP, target-runtime, hosted and completion dimensions remain unselected or unclaimed |
| Same-subject Phase 0 aggregate evidence | Phase 0 Evidence v2 records the last reviewed executed aggregate: 86 passing rows at its exact historical subject. Phase 0 Evidence v3 now authors one recursively authenticated selection of the canonical-Git, generated client/MCP, three-language supported product workflow, pinned packaged TypeScript MCP, real Visual Studio Code host and independent Python MCP SDK components. V3 remains unrun; managed ACTIVE, exact tag, remote/later head, hosted cross-platform, target runtime, full quality and programme completion remain unclaimed. |
| Frontend reuse | Frontend Cache v1, incremental.rs |
| Checked semantic reuse | Semantic Cache v1, authored cases; exact synthetic module HIR plus exact monomorphic free-function HIR under complete environment equality within one compiler process; every semantic gate still reruns, implemented |
| Persistent checked-module reuse | Persistent Cache v1, authenticated store; private complete codec, compiler-file/key binding before decoding, source reparse and warm full-Project replay |
| Live frontend reuse | Workspace Frontend Cache v1, cached session cases; exact authenticated source loading and transactional cache adoption |
| Parallel image reads | Parallel Reads v1, batch cases; embedding-host scoped workers, not a concurrent stdio server |
| Parallel retained reads | Parallel Retained Reads v1; selected immutable candidate/draft/attempt inputs, shared sequential payload handlers and implemented parity evidence |
| Host-selected protocol batches | Parallel Read Protocol v1; explicit v7 startup worker selection, unchanged aggregate wire caps, generated schemas/clients and MCP method selection, implemented |
| Retained session subjects | Retained Subjects v1; bounded deterministic candidate/draft/rejected-attempt handles and registry-local associations, explicitly outside immutable batches, implemented |
| Checked hole-fill suggestions | Fill Suggestions v1; exact type/effect-guided place/call enumeration with ordinary source fill replay, no retained previews or intent/runtime-contract proof, implemented |
| Integrated canonical Git workflow | Git Workflow v1, real-provider scenarios; exact local subject evidence passed SHA-1, SHA-256 and stale-ref cases, with broader provider/platform evidence still open |
| Supported product workflow | Product Workflow v1, Response Accountability v1, Packaged TypeScript Workflow SDK v1, Candidate Test Tasks v1, and Phase 1 Product Workflow Evidence v1; exact-subject local evidence passed the complete Python, Rust, and explicitly provisioned TypeScript compositions over isolated local Unix bare SHA-256 repositories, including ten closed hostile transitions. Later focused work adds closed SDK failures and per-call authority/blind-spot transcripts, one installed zero-authority TypeScript package whose raw-v5 review/separate-publication gate passed and whose pinned-MCP equivalent is implemented, and a session-scoped cancellable candidate-test task selected through v5/MCP and the editor controller. This is one bounded scalar workflow only; the editor task path has real Extension Host evidence for exact subject 3fccd30b861d48c9d404eb2698fa2eff510569af alone, and general intentions and ownership, broader cross-platform, target-runtime, full-quality integration and programme scope remain open |
| Expression holes | Expression Holes v1 |
| Contract expression holes | Contract Expression Holes v1; source-replayed pre/postcondition subtree changes, shared draft/recovery lifecycle and v5 discovery, implemented |
| Typed repair change | Diagnostic Change v1 |
| Static protocol conformance | Static Protocol Conformance v1, static_protocol.rs |
| Interface implementation | Interface Change v1, interface.rs |
| Conformance discovery | Image Protocol Conformance v1; source-bound sidecar and v4 query/catalogue integration |
| Typed discovery | Agent Discovery v5; runtime-selected request/envelope schemas, typed outer client parameters and explicitly opaque compiler-report schemas |
| Typed responses | Typed Response Clients v1; exact local subject evidence executes Python, Rust and provisioned TypeScript response consumers for the selected bounded schemas; heterogeneous compiler reports remain open |
| Typed requests | Typed Request Clients v1 and Client/MCP Evidence v2; one exact local subject executes Python, offline compiled Rust and provisioned TypeScript request construction against real compiler admission, including an exact hostile unbound-place rejection; packaged SDK and exhaustive generated-method coverage remain open |
| Compact hole navigation | Hole Navigation v1; typed summaries and context-bound scope/call/obligation/constructor pages for all three hole kinds, implemented; full contexts and pending-state authority unchanged |
| Unified workspace protocol | Workspace Protocol v5, startup CLI |
| MCP integration | MCP Adapter v1, Client/MCP Evidence v2, Packaged TypeScript Workflow SDK v1, and Phase 0 Evidence v2; one exact local subject passes the authored adapter/stdio gates and an independent provisioned Python mcp SDK 1.27.0 interoperability profile including bounded catalogue paging and notification nonexecution. The packaged TypeScript workflow now owns a pinned-MCP transport and real review/separate-publication MCP gate, implemented. Full MCP certification, HTTP and broader cross-platform scope remain open |
| Editor source review | Source Review v1, VS Code Adapter v1, and focused host evidence; exact local subject 2888f84f123b7caa44aa6807388d98f851d4beaf executes the compiler-backed typed rename, verified virtual diff and dirty-buffer invalidation without saved-source writes. Packaging, manual UI, minimum-version and broader cross-platform scope remain open |
| Editor typed holes | VS Code Adapter v1; three-kind hole planning, compact facets, explicit checked-suggestion selection into bound fill scratches and separate completion, implemented; editor-host execution remains open |
| Editor diagnostic repair | VS Code Adapter v1; separate rejected attempts, exact-byte report inspection and explicit compiler repair selectors, implemented with mock controller regressions; richer repair UX and actual editor-host execution remain open |
| Draft expression discovery | Draft Expression Catalogue v1; last-valid body/contract selection after fills, exact draft bindings, typed v5 discovery and editor integration, implemented; no implicit candidate release |
| Protocol source commit | Source Commit Protocol v5; independently selected startup authority and exact approval |
| Target/artifact queries | Target and Artifact Projections v1, OpenAPI Artifacts v1 and C Artifacts v1; actual pathless source-bound carrier construction and replay |
| Canonical Git publication | Git Publication v1, explicit host CLI |
| Store | project_revision_store.rs, Store v1, Windows-entry v1, store evidence |
| Analysis | workspace_analysis.rs, Workspace Analysis v1; retained six-family typed indexes and existing Context/Impact/Review |
| Existing mutation | semantic workspace operations, Operations v1, operation evidence; Project rename and rename evidence |
| Existing evidence | patch evidence, workspace change, target evidence, their versioned specifications and focused suites |
| Economics | agent_economics.rs, Agent Context Economics v1, economics evidence |
These owners identify the implemented v0.4.0 surfaces and their executable regression contracts. Their release evidence is HOSTED GREEN within the stated profiles. Each remaining requirement below concerns broader functionality or support, not merely the presence of a source file or a historical local run.
Phase 1: fast semantic workspace
| Requirement | Status and remaining evidence |
|---|---|
| Persistent, content-addressed derived HIR and graph snapshots | Partial; implemented. A separate authenticated store now retains complete checked module HIR, synthetic inputs, canonical sources and graph projections. Fresh processes can decode only after MAC and compiler-file checks, then reparse source and require zero-resolver full-Project replay with exact graph equality. Ordinary Image Store remains cold. The admitted cross-process, corruption and recovery regressions are HOSTED GREEN. Broader profile support, measured performance and complete session/checkpoint recovery remain open. |
| Identity binds compiler, graph/HIR compatibility, manifest, ordered paths/digests and profiles | Partial; implemented. Image identity stays unchanged. Persistent envelopes additionally bind exact compiler executable bytes, codec/header compatibility, host width/endianness/platform and the complete source/manifest/HIR payload. This requires an immutable static installation from exec and protected host key custody; it does not attest loaded code, dynamic libraries or a hostile same-principal process. Cross-build rejection cases still require execution. |
| Derived, deletable, rebuildable, Git-excluded, revision-bound; no graph-only meaning | Implemented Image/Store boundaries. Image replay reconstructs from admitted source revision; .semaprax-images/ is ignored. Still require integrated cache deletion/recovery/corruption and stale-source lifecycle evidence. |
| Incremental invalidation/rechecking | Partial implemented. Exact synthetic AST, imported stubs and manifest context govern checked-module reuse, including explicitly restored caches. Changed modules may reuse exact monomorphic free-function HIR only under complete environment/signature/contract/span equality; full source, HIR and Project-wide gates rerun. A separate caller-owned Target Cache v1 reuses exact scalar-Web, pathless native-C11 and pathless npm carriers after independent replay. Persistent load reparses original source and rebuilds graph/indexes while reusing HIR. Generic/class-method semantic reuse, broader/cross-process target work, and measured performance beyond the admitted equivalence corpus remain missing. |
| Expanded symbol and reverse indexes | Partial; implemented. Stable-ID lookup and six-family indexes exist; the shared immutable-image dependency index adds source-bound field/type/case use sites and local/cross-file direct caller closure, exposed through a read-only v5 query and reused by candidate deltas. General package/artifact consumers and measured index benefits remain open. |
| Capability-negotiated discovery | Partial; implemented. Host-selected read-only v1, candidate-only v2, fixed-policy test v3 and diagnostic v4 remain preserved. Additive v5 combines optional candidate/diagnostic/test/pathless-build capabilities and a separately attached startup-approved Git commit host. Artifact filesystem materialization and request-driven elevation remain absent. |
| Compact summaries/references/facet expansion | Partial; implemented. Function facets and declaration-dependency summaries expose revision-bound handles and paginated detail. Generic-function navigation adds source-template-bound retained instances with exact instance facets, caller identities and entry/test closure joins without inventing instantiations or execution evidence. Dependency pages add source-bound caller relevance reasons and bind page size/output limits without embedding complete reports in summaries. Candidate-bound dependency pages reuse those four views over changed and introduced declarations with history-isolated handles/cursors and no retained derived image. Typed-hole summaries add exact-context references and bounded scope/call/obligation/constructor pages while retaining full prior proof contexts separately. A live v5 retained-subject inventory now recovers bounded candidate/draft/rejected-attempt references and registry-local associations without replaying their reports; it stays outside immutable batches. Exact-revision function references carry one stable-ID/facet selector and resolve against an identical rebuilt image; a conservative rebind can export a fresh destination selector only when separately admitted images preserve one unique explicit stable identity and exact source/module provenance. It classifies provenance change without inferring ancestry or semantic compatibility. Type/candidate/draft references, cursor continuation, optional advisory ranking and measured task-level context improvement remain open. |
| Diagnostics/repair metadata retained with the workspace | Partial. Existing compiler diagnostics and repair discovery are separate; invalid source does not produce an admitted Image. Missing integrated symbol-linked diagnostic/repair inventory and incremental refresh. |
Phase 2: candidate model
| Requirement | Status and remaining evidence |
|---|---|
| Immutable overlays against one immutable base, branching and discard | Candidate implemented. Applying returns a new value; siblings retain their base, dropping discards. Candidate-only v2 retains bounded candidate/draft registries and exposes discard. Explicit draft capsules now recover pending selectors, filled-hole lineage, branch ancestry and prior valid history through source replay, retaining no complete candidate until completion. Successful image/candidate/draft store receipts share one authority-neutral deterministic retention checkpoint contract. An explicit private-root Retention Registry now persists consecutive checkpoint/plan pairs and a CAS current-generation cursor through held descriptors, without restoring subjects or applying GC. An opt-in v5 embedding session can hold the coordinator and accept typed post-store receipts; v5 also has an optional startup-held archive-store route with post-store checkpointing. General branch/session checkpointing, separately authorized eviction and complete recovered branch lifecycle remain open. |
| Versioned Semantic Change IR and mandatory constraints | Partial, Candidate implemented for all eleven requested operation classes, including replayed diagnostic repair and static protocol implementation. Base revision, exact identity additions/relocations, exports, effects, permits, exact contract inventory changes and profile/core-target preservation are checked in that slice. General interface behavior, broader constraints and complete semantic-delta proof remain open. |
| Typed expression/declaration constructors | Partial; implemented. Candidate constructors cover bounded scalar/parameter/operator/call expressions, stable-ID record and variant construction with explicit direct-scalar generic arguments, authenticated Option/Result cases, record-field value projection, direct field places with authenticated nominal roots, subset record updates with base-first evaluation, exhaustive variant value matching with exact-owner typed staging and arm-local payload bindings, monomorphic function declarations with limited ownership modes and stable-ID Copy nominal parameters/returns, and explicit monomorphic record/variant declaration creation with checked resource-free data fields. Fields can select direct scalar/String/Bytes types or already visible nominal owners; no new import or borrowed/resource storage is introduced. Field places compose with compiler-owned byte calls under the existing direct owned-field borrow profile, without staging a root temporary. Catalogue/hole discovery exposes bindings, checked templates, field/case owners and compiler provenance; full candidate replay, exact added identity inventories and checked type facts own admission. Nested/named generic arguments, general nested borrowing, general/ownership-aware patterns, generic/resource type creation, and general declarations remain missing. Bounded place/direct-call hole suggestions now use exact type/effect prefilters followed by ordinary full fill replay, dropping preview drafts; broader constructor search, runtime contract/intent proof and measured guidance effectiveness remain open. |
| Ephemeral typed holes | Partial; implemented. Body, body-expression and contract-expression holes expose checked lexical context, expected type/ownership and last-valid proof facts. Filling performs complete candidate admission and remaps surviving selections; unresolved drafts cannot materialize. Contract holes distinguish phase/predicate/subtree, enforce pure predicates and coexist with body regions. Explicit recovery rebuilds prior valid history and re-creates pending holes under exact draft/capsule identities. Recursive incomplete declarations, general incomplete-state diagnostics, next-expression liveness guidance and evidence for that broader scope remain open. |
| Candidate ID, base/candidate revisions, semantic/source-diff digests, validation/diagnostics/gates | Partial, Candidate implemented. Complete candidates carry digests, diffs, validation facts and gates. V4 adds bounded rejected-attempt lifecycle and repair discovery without invalid source/image access. General incomplete-state diagnostics remain missing. |
| Candidate comparison, targeted validation and exact semantic replay | Partial. Original comparison is descriptive target overlap; additive read-only merge preview performs full merge replay in both orders, reports admission/rejection, and compares actual accepted canonical source without retaining a candidate. Source is formatted, reparsed and rebuilt with complete Project admission. General semantic compatibility decisions, intended-delta verification across general transformations, selective invalidation/validation and executed preview evidence remain open. |
The additive literal constructors cover bounded owned string contents and explicit fixed byte arrays through ordinary source replay. The scalar literal extension adds exact character and finite IEEE encodings to recursive expressions and both signature-default forms, completing the eight built-in Copy scalars while leaving record defaults, diagnostic repair and computed argument selectors on their explicit narrower grammars. Both extensions are implemented; source ownership/provenance and target admission remain unchanged, and repeat arrays and general constructor search remain outside their scope. The existing seven String intrinsics are also selectable through compiler-owned typed builtin calls, with exact parameter ownership and separate byte/string evidence owners. Discovery and eligible declaration movement share those identities. This extension does not widen String target profiles, source imports or runtime authority.
Phase 3: all eleven requested operations
All eleven requested classes now have bounded implemented slices. This counts represented operation classes, not completed general operations, runtime interface support, passing tests or completion-matrix promotions. Each row keeps its broader requirement open.
| Operation | Present scope and remaining requirement |
|---|---|
rename_declaration | Partial; implemented. Candidate supports explicit non-main functions, source record/variant display renames and explicit record fields/variant cases/payload fields through the shared authenticated Operations occurrence collector. A generic template rename authenticates the retained source/HIR template and preserves the exact bounded concrete-instance identities, type arguments and normalized checked HIR while migrating stable-ID-bound local typed calls. Cross-file member labels migrate while stable identities and import aliases remain unchanged. Generic/owned nominal shapes retain ordinary source/profile admission; unsupported reference pairs fail closed. Generic signature evolution, interface and other declaration renames, broader reference forms, complete merge normalization and evidence for that broader scope remain open. |
change_function_signature | Partial; implemented. Scalar append and ordered mapping include hygienic parameter display renaming, checked nominal Copy record/variant retention/reordering/removal, direct Bytes and checked resource-free String/nominal owner retention/reordering, exact existing borrow str and borrow Slice<u8> retention/reordering, fresh aliases derived from an authenticated original borrowed view, and fresh scalar or stable-ID Copy nominal parameters computed from staged original arguments. A borrowed alias derives its exact type/root from one retained borrow str or borrow Slice<u8> source and reuses that original left-to-right staged argument; ordinary loan/provenance replay still decides admission. One closed owner-view lane replaces a mixed set of one through eight distinct exact owning Bytes/String parameters with borrow Slice<u8>/borrow str only when each checked provider owner has one sole matching unprojected bytes_as_slice/string_as_str body use and contracts have no owner root. A separate result lane wraps one exact whole owning Bytes/String result in an existing visible monomorphic resource-free one-field owning record, constructs it once at provider result commit, and makes every authenticated local body caller project/move that field. Complete source/HIR authentication precedes mutation. Every caller stages all old arguments left to right and retains ordinary caller cleanup; full replay owns changed loan boundaries, lifetimes and target admission. Contracts, entrypoints, manifest exports and zero local callers remain excluded from the local intention. A separate read-only package proposal migrates one authenticated cross-package own Bytes argument to borrow Slice<u8> from a bare staged owner and requires complete candidate-era package replay; it does not discover consumers, write source or assess compatibility. Provider and caller type bindings are resolved independently. Exact rebuilt HIR TypeFacts govern new named eligibility, retained facts govern original parameters, and nominal identities participate in rebase conflicts. Other owners and original borrowed views cannot be dropped or duplicated. Projected/temporary/escaping String views, standalone internal-String conversion, nominal owner conversion, new independent roots, borrow Bytes, general result conversion, borrowed nominal/storage migration and dependent declarations remain missing. |
replace_expression | Partial; implemented. Body-expression selection uses actual revision-scoped HIR identity and unambiguous canonical AST provenance; replacement uses authenticated lexical scope, expected-type/ownership checks and full Project admission. A separate replace_contract_expression intention supports pre/postcondition subtrees with exact requested-source reconstruction and conservative rebase, leaving body-only behavior unchanged. Generic/synthetic selections, general typed constructors and evidence for that broader scope remain open. |
replace_function_body | Partial, Candidate implemented: bounded typed constructors for explicit monomorphic non-main functions followed by full source admission. General body/control/data/ownership shapes remain. |
extract_function | Partial; implemented. Actual HIR expression selection, immutable scalar and checked Sized Copy nominal capture/result derivation, whole-root capture for field reads, fresh caller-selected function identity, in-place call substitution and exact source replay. A narrow ownership lane authenticates one exact whole body-local own Bytes or bare owning String binding with one unconditional consuming occurrence, transfers it at the original expression position into an owning helper parameter, and may publish an already-supported whole owned result. Parameters, projections, shared/borrowed roots, multiple or conditional uses, contracts, entrypoints, exports, internal owning storage and external consumers fail closed. A nested-block lane separately retains internal resource-free owners inside their original lexical cleanup boundary under a fresh helper root. Nominal values and bindings use retained compiler TypeFacts under the existing shared type/byte bounds. General owned/borrowed/mutable captures, borrowed/shared results, resources, unsafe-boundary relocation and general control/data forms remain excluded. |
add_declaration | Partial; implemented. Typed monomorphic function append and explicit monomorphic record/variant creation in an anchor's module with global identity/namespace checks and exact invariant extension. New data types bind every owner/case/field identity and admit direct scalar/String/Bytes fields or existing stable-ID nominal fields through checked sized/resource-free facts. Nominal field dependencies participate in intermediate rebase checks; later intentions can evolve and use those types. Function creation composes with local owning nominal helpers and bare String signatures through requested-mode and rebuilt HIR checks. Copy nominal signatures retain direct-scalar local generic instances and authenticated prelude types; owning nominal parameters are monomorphic, sized, non-Copy and resource-free with cleanup. Imports and target profiles remain unchanged. General declaration kinds, generic/resource type creation, broader borrowing modes, recursive construction and placement remain open. |
move_declaration | Partial, focused local evidence. Explicit monomorphic scalar, String and checked resource-free data planning preserves identity, migrates stable-ID call/type import bindings and aggregate syntax, and replays exact source plus rebuilt semantic identities. Internal owned byte work uses authenticated compiler operations without new staging. An owning nongeneric resource-free nominal can move across modules through one exact stable-ID type import; callable imports exposing owned nominal arguments, fixed exports, borrowed signatures, generic source-type imports and audit-bearing relocation remain excluded. |
implement_interface | Partial; implemented. Compiler-derived required-member discovery and a typed mapping bind an explicit monomorphic record to an exact Project protocol and eligible existing functions. An optional destination module imports cross-module receiver, protocol and function dependencies through stable IDs and deterministic bounded aliases; protocol imports are static-conformance-only and remain outside runtime HIR/Graph/operation sidecars. Exact member coverage/signature matching and canonical source replay are checked. Conservative rebase and same-root merge retain an admitted intention only while the exact compiler-owned receiver, protocol, method, selected-function, destination and import facts remain unchanged and the implementation identity and receiver/protocol pair remain vacant; full replay still decides admission. General interface contracts, generic/owned receiver forms, behavioral compatibility, runtime witnesses and dynamic dispatch remain missing. |
add_record_field | Partial; implemented. Appends one inert i64/bool/i32/u8/usize field to an existing checked sized resource-free record, including owned storage beyond flat Bytes when ordinary source admission permits it. A narrower lane appends a bounded owning string or freshly copied Bytes field to an originally Copy, drop-free record with an authenticated constructor and no target record patterns, then requires the exact Copy-to-needs-drop checked transition. It preserves old initializer order and field identities and revalidates complete Project/layout/loan/cleanup/target admission. Generic/class/variant targets, owning pattern migration, public ABI compatibility and general record evolution remain open. |
add_contract | Partial; implemented. Append one typed requires/ensures predicate to an explicit monomorphic non-main function, preserving prior predicates and exact other invariants with full Project admission. General declaration contracts, proof of runtime satisfaction and external compatibility remain open. |
repair_diagnostic | Partial; implemented. Existing ID repair remains separate. Candidate Diagnostics and v4 retain rejected attempts; typed wire rederives integer-literal retagging and direct owned-byte field borrow repairs and preserves them in replayable history. Byte-field repair requires actual SPX-T266 rejection and complete candidate admission without weakening source borrowing rules. Selectors bind the exact predecessor and reject rebase/reminting. General repair classes remain missing. |
change/catalog <target> now provides candidate-bound constructor discovery
in candidate-only v2 for supported intention classes. Unsupported
targets expose no operations; each payload still requires full admission.
Discovery of fully proven legal transitions remains open; this catalogue does
not advertise the aspirational table above. Existing hygienic generation is related typed
synthesis, not an implementation of the missing change operations.
Phase 4: generalized impact, facets and evidence
| Required facet family | Present evidence and remaining work |
|---|---|
| Contracts | Partial; implemented. Facets expose actual pre/postcondition expressions. Whole-candidate Contract Delta compares ordered predicates and their static callable dependencies with exact candidate replay and source provenance, including helper changes behind unchanged predicates. General invariant dependency graphs, logical implication/satisfaction, runtime behavior and evidence for that broader scope remain missing. |
| Ownership | Partial; implemented. Facets expose parameter modes and structural slots. Whole-candidate Ownership Delta compares checked ownership signatures, complete structural inventories and retained instance facts with exact source replay. General creation/transfer/settlement relationships, runtime liveness and evidence for that broader scope remain missing. |
| Cleanup | Partial; implemented. Facets reuse complete ordered CleanupPlan projection. Ownership Delta compares whole-candidate loan and cleanup plans without rewriting their vectors or claiming behavioral equivalence. Cleanup Dependencies adds reverse source type/case/field selection over retained storage shapes, cleanup and loan plan facts with original coordinates, an image-local lazy index, and candidate before/after review through the same collector. General lifetime/alias reasoning, broader expression-to-obligation queries, physical execution and evidence for that broader scope remain missing. |
| Data access | Partial; implemented. Function facets expose actual ValueId reads/writes, field projections and consumption-context facts with provenance. A shared lazy index supports bounded reverse field/type/case queries and candidate relationship deltas. Whole-value leaf expansion, general alias analysis, runtime liveness and evidence for that broader scope remain missing. |
| Interfaces | Partial; implemented source-sidecar conformance facts and v4 protocol/conformance / candidate/interface-catalog discovery. The additive whole-candidate Interface Delta compares complete affected-member inventories, bound functions and static-call dependencies with exact candidate replay; v5 exposes chunks. Implementations may choose an exact Project destination and import receiver, protocol and implementation functions through deterministic static-only dependencies. Facts bind source revisions and stable receiver/protocol/member/function identities; protocol imports remain outside runtime HIR/Graph and add no dispatch edges. Generic/owned receiver admission, dynamic dispatch and evidence for that broader scope remain missing. |
| Tests | Partial; implemented Candidate Tests selects relevance from exact transitive test-root HIR calls with conservative fallback for non-call facts; explicit execution runs the full declared interpreter test closure. Dynamic coverage, multi-root selection and native/Wasm evidence remain missing. |
| Targets | Partial; implemented. V5 image/target-admission derives actual native-C11/Core-Wasm emission and structural validation facts for complete entry/test closures and checks selected-function membership. The caller-owned Target Cache v1 retains and independently replays exact scalar-Web, pathless native-C11 and pathless npm carriers without weakening Project admission; C and npm hits invoke no emitter/generator. Whole-closure failure is not blamed on one function. Runtime execution, persistent/cross-process reuse, general declaration-level diagnosis, broader targets and package-profile coverage remain missing. |
| Artifacts | Partial; implemented. Web/npm projections build and replay existing pathless carriers; OpenAPI adds actual per-source documents and C adds real linked native source with exact header prototypes or explicit exclusions. Shared renderers and complete Project source replay preserve ordinary admission, native linkage and status conventions. All bind files, source inputs and manifest export identities. Artifact Delta compares actual base/candidate file inventories and exports after complete candidate replay, separating content from carrier metadata. V5 requires the existing build grant and returns chunks, not materialized files. Rust carriers, compiled C libraries/public FFI, broader schema admission, installed consumer relationships, generalized consumer migration, artifact filesystem authority and evidence for that broader scope remain missing. |
| Packages | Partial; implemented Package Semantic Graph. Exact source-capsule replay supplies coordinate-qualified interface, import and cross-package call relationships with revision-bound consumer queries. Explicit host attachment exposes a separate immutable package subject, never an inferred Project dependency. Candidate Package Consumer Replay independently authenticates an explicit candidate-era provider report/source/capsule and projects only that final-candidate source onto its known imports and static call sites. Package Consumer Migration v1 accepts one exact caller-supplied baseline corpus and one Copy-scalar signature append, reconstructs canonical proposed consumer sources, rebuilds provider evidence, and requires candidate-era replay before returning the authority-free proposal. Installed-consumer discovery, writes/publication, owning migration, compatibility, whole-Project package association and general cross-package migration remain missing. |
| Analysis boundaries | Partial; implemented Analysis Coverage plus its candidate projection: exact retained image or final-candidate input and declared interface-import facts alongside explicit deployment, generated provenance, external API behavior, runtime and consumer blind spots. A fixed source-bound ledger distinguishes absent deployment, generator and external/deployed-runtime evidence from absence of the underlying contracts. Candidate Analysis Evidence composes one explicit authenticated candidate-era package corpus and changes only external consumers to partial. Artifact and runtime evidence separately change only their authenticated areas to partial. Closed caller declarations can change deployment configuration to partial for exact candidate/export-bound key shapes, or change exactly one of generated-file provenance and external API behavior to partial through bounded blind-spot declarations. The generated-file form binds retained source bytes to an opaque generator token/digest without execution; the API form binds complete manifest exports or an explicit stable subset to operation/schema digests without endpoints or provider observation. A bounded bundle independently replays all three owning declarations and advances exactly deployment configuration, generated-file provenance and external API behavior to partial while preserving every other coverage fact and nonclaim. Coverage Change v1 reconstructs the immutable base candidate and independently authenticates optional exact base/final bundles through those three owners, categorizing real attached-evidence advance/regression/same-status drift while keeping runtime and external consumers source-only invariants and completeness/compatibility unassessed. Environment Review independently composes that bundle with the complete canonical source review and exact source/Project/Workspace/graph joins. Environment Consumer Review additionally joins one host-attached authenticated candidate-era package graph and advances only the external-consumer area to partial; its bounded inventory may be empty and never implies completeness or compatibility. External API Contract Delta compares exact base/candidate declared inventories and digest facets while leaving compatibility not_assessed. V5 exposes the pre-existing reports through bounded candidate queries, closed schemas, generated clients and MCP discovery; the coverage-change report remains library-only and all execution remains unrun. No ambient external-input ingestion, installed discovery, native/Wasm or deployed execution, environment/network/provider observation, generator execution, materialization/deployment proof, runtime/API conformance, compatibility proof or completeness percentage. |
| Unsafe boundaries | Partial; implemented HIR Relationships projection machinery. Current Project admission excludes unsafe-bearing sources, so its public unsafe inventory remains empty. Active unsafe-source coverage, transitive dependency/exposure analysis, broader import-bearing Project admission and candidate deltas remain missing. |
| Diagnostics | Partial; implemented Symbol Diagnostics joins session-retained rejected attempts to their exact predecessor and intention target, with actually admitted repair classes and report-bound continuations. It never treats a rejection as a checked image or attributes its spans to verified HIR. General diagnostic causality, retained compiler warning inventories, broader repairs remain missing. The implemented regression corpus is HOSTED GREEN. |
Each generalized fact must bind source provenance, stable identity, revision, edge kind, reason, evidence owner and authoritative/descriptive/advisory class. Current Facets labels descriptive validated-HIR projections and source revisions; this does not establish the missing families or their independent replay. LoanPlan vectors remain proof data, not runtime liveness authority.
Cross-file candidate-aware impact is Partial: Candidate pairs base and
candidate six-family Impact reports. Additive Impact Navigation
provides candidate/query-bound compact summaries and exact ordered pages over
the final candidate artifact without expanding truncated rows. Semantic Delta adds release-tested selected
declaration before/after facts, function facets, reverse field accesses, test
relevance and whole-closure target artifacts with exact recomputation. This
narrows the missing delta work above; package/artifact families, broader interface admission,
behavioral equivalence and runtime coverage remain open.
Source/semantic-diff binding and exact candidate replay passed for the bounded
474c481b Git-workflow fixture; generalized facet coverage remains incomplete. That historical fixture's
interpreter request is not the full quality profile. The implemented release
regressions are HOSTED GREEN; generalized policy-selected quality integration
remains an independent requirement.
Evidence-bound materialization through separate
commit authority is Partial in existing A0/managed Workspace routes and
Partial for candidates through a separately implemented managed Workspace
bridge. It replays under the existing lock before ACTIVE publication and leaves
original raw Git paths unchanged. A separate host route constructs canonical
Git objects and publishes a branch by expected-old ref update in an explicitly
selected Unix bare SHA1 or SHA256 repository; the bounded local fixture executed
both formats. SHA1
adds exact staged-object readback and a SHA256 observed/prepared-content binding,
without collision-detection or modern SHA1 integrity claims. Broader hosts and
checkout integration remain missing; a capsule cannot publish
itself or select that authority. V5 can invoke this fixed authority only when the
host attached it and approved an exact candidate before the first request.
Review/export first, then restore/commit in a separate host-approved session;
there is no in-session RPC or later-startup approval shortcut.
Protocol, generated integrations and candidate lifecycle
| Requested surface | Current status |
|---|---|
protocol/capabilities, protocol/schemas | Implemented Protocol. Host-selected capabilities and catalogue-driven request/success/error envelopes. Additive protocol/constructor-schemas supplies self-contained closed typed-expression/intent/change schemas. V5 adds runtime-selected schemas and typed clients with concrete candidate comparison/reconciliation/catalog/test-plan and frontend-work payloads. Client generation rejects unsupported validation assertions and includes only response-reachable documents. Heterogeneous candidate/HIR report interiors remain missing. |
workspace/open, workspace/status, workspace/refresh-preview, workspace/refresh, query/catalog | Implemented. Host binds the manifest; requests cannot select a new path. V5 preview discovers the currently observed revision without replacing state. Cold and opt-in frontend/checked-module cache refresh authenticate the same source set with exact expected image/new Project revisions, retain candidate handles and clear incomplete drafts/attempts only after successful bounded response preparation. Failed refresh preserves session/cache state; general incremental rechecking and measured reuse remain open. |
protocol/conformance, candidate/interface-catalog | Implemented additive v4 read-only source-sidecar queries and candidate-bound static required-member discovery. Existing v1–v3 method sets and runtime Graph contracts remain unchanged; no runtime interface or publication authority is granted. |
change/catalog, validation/catalog | Implemented candidate-only v2. Target-specific constructor discovery and independent candidate replay are available; arbitrary payload validity requires apply. General legal-transition discovery and execution routes remain open. |
| Read-only, candidate-only, source-commit, build-enabled, test-enabled, artifact-materialization-enabled sessions | V5 composes host-selected read-only/candidate/diagnostic/test/pathless-build capabilities and optionally startup-approved fixed Git publication. Older profiles remain unchanged. No artifact filesystem materialization, arbitrary tool execution or request authority elevation is granted. |
| Version-matched agent instructions | Implemented catalogue-derived instructions cover only methods granted by the selected v5 host policy and preserve older profile instructions. The admitted instruction/client regression corpus is HOSTED GREEN; broader instruction and SDK scope remains open. |
| TypeScript, Python, Rust clients | V5 authors typed TypeScript/Python/Rust request parameters, enum choices, builders and result decoders from runtime-selected catalogues, with one domain-separated client-contract revision across all three languages. Earlier exact-subject local evidence executes Python, offline compiled Rust and provisioned strict TypeScript 5.8.3/Node request/response consumers with hostile depth/work cases. Phase 1 Product Workflow Evidence v1 additionally executes the complete bounded review/publish composition through all three generated clients. Packaged TypeScript Workflow SDK v1 executes one installed package over the selected TypeScript review/publish profile. All-language generation remains deterministic; other heterogeneous compiler reports, exhaustive generated-method admission, complete typed payloads, broader packaged SDKs and ergonomics remain open. |
| Optional MCP/editor adapters | Partial. Exact-subject local evidence passes the pinned 2025-11-25 in-process MCP contract and actual stdio child. Separate exact subject 2888f84f123b7caa44aa6807388d98f851d4beaf executes the saved-source adapter inside a selected local Visual Studio Code 1.135.0 Extension Host against a freshly built compiler. Additive candidate-test task tools and editor Run/Cancel commands now implement one bounded cooperative lifecycle with source/epoch invalidation and all-false authority; focused Rust compilation and Node controller evidence pass, and exact subject 3fccd30b861d48c9d404eb2698fa2eff510569af ran that task path, the supplementary-character diagnostic range, diagnostic retention/clearing, and project-routed navigation inside a selected local Visual Studio Code 1.136.1 Extension Host. The client frames remain authored Rust JSON rather than an independent MCP SDK/conformance client. MCP Tasks/HTTP, manual UI/accessibility, VSIX/Marketplace, typed-hole/repair host paths, minimum-version, hosted and cross-platform evidence remain missing. |
| Machine-readable operation catalogue | Universal Semantic Query v1 adds a locally exercised core available_operations result for the sole Universal Semantic Transaction v1 rename, derived from the same eligibility classifier used by validation and bound to one canonical workspace revision. Existing read-query and target-specific constructor catalogues remain separate; no v5/CLI/MCP/LSP exposure or general change catalogue is claimed. |
candidate/open, candidate/apply-intent | Candidate library and candidate-only v2 methods implemented; bounded immutable registry with no publication authority. |
candidate/query, candidate/validate, candidate/impact | Implemented v2 methods: bounded report chunks, complete independent replay and six-family impact. Additive v5 candidate dependency navigation exposes compact sites/callers/calls/members; Impact Navigation pages the final candidate artifact's affected/edge/frontier arrays with exact query and truncation bindings. A candidate-only deployment-contract read binds exact canonical declaration bytes and returns bounded regenerated analysis chunks through generated clients/MCP without environment authority. These reads retain no derived image or omitted impact. General incomplete-candidate validation and generalized impact remain open. |
candidate/test | The library and explicitly host-selected v3 route require exact candidate replay before fixed-policy execution of the full declared interpreter test closure. The bounded product-workflow evidence executes and independently repeats that exact fixture report; static relevance is not coverage, and native/Wasm, broader candidate tests and policy-selected full gates remain separate. |
candidate/compare, candidate/discard | Descriptive library and v2 lifecycle methods implemented. Semantic compatibility proof remains missing. |
candidate/commit | Partial separate host bridges to managed ACTIVE and canonical Git branch publication, each with exact candidate approval/replay. The Git adapter admits Unix bare SHA1/SHA256 repositories and never rewrites raw checkouts. V5 adds candidate/commit only with separately attached fixed authority and exact startup approval, consumed on invocation; success/uncertainty is terminal for that commit host. The bounded product-workflow evidence executes three generated-client publications through isolated local Unix bare SHA-256 repositories, including real post-ref result loss. Ordinary checkout integration, SHA-1 workflow composition, broader Git interoperability, hosted/cross-platform providers and physical durability remain missing. |
Phase 5: multi-agent operation
| Requirement | Status and remaining evidence |
|---|---|
| Semantic rebase/merge | Partial; implemented Rebase. Stable-ID target/dependency conflict classification, introduced-identity collision checks, display-normalized call facts, canonical source replay and same-root history merge cover supported intentions. Imported callable dependencies now conflict on concurrent signature, effect or contract drift. Draft Rebase carries checked history and pending body/expression/contract holes to an admitted destination; Draft Merge combines common-base histories and independently rebinds pending inventories. Additive v2 drafts retain authenticated filled-hole events and bounded rebase/merge ancestry through recovery and v5 transport without implicitly completing sibling holes. General ownership-sensitive reconciliation, behavioral interface equivalence, cross-manifest merging and measured parallel-agent evidence remain open. |
| Conflict cases | Focused Rebase cases are implemented: unrelated body/display rename, body/postcondition revalidation, competing signature conflicts, deleted call dependencies, and exact static-interface receiver/protocol/member/function/pair/identity drift. Preserve the released matrix and expand to all intended operations and preserve expected-expression remapping before claiming full coverage. |
| Candidate branching | Partial in-memory immutable siblings and bounded candidate-only v2 registry. Complete histories and unfinished drafts have release-tested self-contained source archives and typed entry points to a host-selected immutable content-addressed store. Startup policy can restore explicitly selected candidates and drafts. Draft archives reconstruct pending selectors and valid history after the original checkout changes or disappears, while preserving explicit completion and historical startup fences. Sibling drafts can explicitly merge compatible histories and pending selections without inferring completion from another branch. Automatic durable branch registries, complete branch lifecycle recovery and evidence for that broader scope remain missing. |
| Parallel read-only requests | Partial; implemented. The embedding-host batch API uses at most four scoped workers for sixteen selected immutable image/discovery/candidate/draft/diagnostic reads, restores input order and authenticates held source before/after the entire joined batch. Explicit startup-selected workspace/read-batch exposes the same engine through NDJSON and MCP with generated schemas/clients, unchanged 64 KiB request and 1 MiB aggregate response caps, and source authentication even for all-error inner batches. It detaches only request-selected subjects and shares pure sequential report handlers; no registry mutation, refresh, test execution, build or commit authority enters workers. Candidate test tasks are a separate one-worker lifecycle and never enter read batches. Validation and source-only repair/archive replay keep their ordinary bounds, with no total CPU/RSS guarantee. Outer stdio requests remain sequential; general concurrent transport scheduling and measured isolation/throughput evidence beyond the admitted corpus remain missing. |
| Session recovery and content-addressed candidate persistence | Partial; implemented. Self-contained candidate archives retain canonical original sources plus complete-history capsules and persist through an explicit private immutable store. CLI host-policy v3 restores historical candidates before frames; separate host-policy v5 can select the authenticated semantic cache store. Self-contained draft archives add original-source reconstruction and ordinary pending-hole replay without importing contexts or candidate/approval registry entries. Explicit typed store APIs, persist/load commands and host-policy v6 now retain and select these drafts. A separate immutable metadata store publishes authenticated retention checkpoint/plan pairs; the Retention Registry chains successful typed store receipts through an exact private-root CAS cursor and recovers the selected metadata generation under held-directory identity. The opt-in Retention Host Lifecycle holds that startup-selected root identity and advances mixed successful image/candidate/draft receipts while representing stale, failed, uncertain and poisoned registry outcomes without rolling back the subject-store fact. Retention Protocol Session v1 holds that coordinator under a once-only v5 embedding-host selection. An optional distinct startup-held candidate archive-store route persists an exact retained complete candidate and automatically supplies its successful typed receipt to that coordinator; request frames select neither root, and registry outcomes never change store success. It neither makes subjects current nor applies GC. Host historical draft restore remains startup-only and same-manifest; frame restore requires the current original base. The separate automatic candidate/draft lifecycle implements host-library checkpoint composition. General branch/session checkpoints, pending-validation recovery, GC execution and authority recovery remain open. .semaprax-candidates/ is Git-excluded. |
| Manual edits and stale recovery | Partial held-input absorbing invalidation, exact base rejection and library rebase onto a separately admitted revision. V5 reloads through cold, source-exact frontend, or explicitly selected checked-module reuse and preserves historical candidates; explicit startup archives recover complete candidates and drafts after original source removal/edits without making them current. Draft Rebase can move pending work onto a selected current candidate before filling. Drafts/attempts still clear on refresh, so historical draft recovery uses explicit archive startup. Authenticated cross-process checked-HIR reuse is implemented. Complete session recovery, broader incremental rechecking and measured recovery benchmarks remain open. |
Required twelve-step signature demonstration
| Step | Current evidence or outstanding gate |
|---|---|
| 1. Open immutable Project snapshot | Passed in the exact local Git-workflow subject; broader current-head preservation gates remain open. |
| 2. Select explicit stable-ID function | Passed for the fixture's explicit calculator.add selection; general selection evidence remains broader. |
| 3. Change signature | Passed for the bounded reorder/rename/append scalar mapping; general evolution remains open. |
| 4. Migrate every authenticated caller | Passed for the fixture's three local/application/test callers with left-to-right staging; no external/dynamic migration claim. |
| 5. Preserve stable ID and exported identity | Passed for the fixture's declaration and manifest checks; external ABI compatibility is not implied. |
| 6. Prove no new effects/capabilities | Passed for the scalar, effect-free fixture; this is not a general proof. Conflict and publication hostile controls are recorded separately. |
| 7. Revalidate contracts/ownership/cleanup | Passed for rebuilt predicates, exact modes and empty scalar cleanup inventory; resource ownership remains open. |
| 8. Run affected tests | The explicit candidate interpreter-test request passed inside the exact local workflow; broader target/test gates remain open. |
| 9. Verify native/Wasm admission | C11 emission and structural Core-Wasm admission passed inside the workflow; target runtime execution remains open. |
| 10. Return semantic impact and human source diff | Impact, source differences and semantic-delta replay passed for the exact fixture; generalized facets remain open. |
| 11. Reject or semantically rebase concurrent source change | Sibling merge, competing signature rejection and real stale-ref preflight passed; manual refresh/rebase, mid-CAS race and general reconciliation remain open. |
| 12. Commit only through separate authority | Separate startup-approved SHA-1/SHA-256 Git publication, committed-object inspection, wrong approval and terminal reuse controls passed locally. Separate local managed-generation evidence also published and authenticated ACTIVE while preserving raw source; a single integrated general publication path, broader Git and platform evidence remain open. |
An integrated canonical Git scenario is authored in
tests/project_graph_operational_git_workflow_v1.rs: real v5 requests select a
cross-file signature change, merge an unrelated sibling, reject competing
signatures, review exact source/delta evidence, invoke the explicit interpreter
test policy, and export/replay the complete candidate. Separate startup-approved
sessions then use the actual bare Git SHA1/SHA256 process provider, compare
committed source objects and reject wrong approval or a stale fixed ref base.
The scalar fixture checks preserved pre/postconditions, effects, exports and
empty owned cleanup; it does not establish general resource behavior. Native
and Wasm evidence is compiler emission/structural validation, not target execution.
The scenario has focused exact-commit runners and machine-readable evidence
contracts. Execution Evidence v1
selects the two real-provider scenarios plus the nonignored real stale-ref
preflight and requires both format-specific economics artifacts. The
reviewed local bundle
records all three selected tests passing for exact subject
474c481bf3c3561c144e077f0000460f61af55f2. Execution Evidence
v2 additionally selects a real
post-CAS result-loss case, four managed-publication boundary regressions, and
the integrated managed workflow. Its reviewed local exact-subject bundle passes
all nine selected rows; the Phase 0 v2 aggregate passes all 86 selected rows;
generated clients, MCP, hosted CI and native/Wasm runtime remain independent
dimensions. Therefore neither tranche completes the general demonstration.
An integrated managed-generation precursor is executed by the v2 runner in
tests/project_graph_operational_workflow_v1.rs: it combines signature migration,
unrelated merge, competing-signature rejection, deltas, explicit test policy and
separate managed publication with stale rejection. It passed locally at the
recorded exact subject and deliberately
leaves canonical raw Git source unchanged. The demonstration is not complete
until one integrated executable scenario
covers all twelve steps, including the separate commit boundary and its hostile
cases, with evidence tied to the exact commit and required target matrix.
Guardrails and evaluation gates
All phases retain canonical human source and ordinary Git review; persistent
public @id declarations; exact-base intentions; canonical source diffs;
source-to-intended-candidate replay; cache/daemon-independent rebuilds;
deterministic authoritative output; manual-edit invalidation or verified
rebase; host-selected least authority; evidence/review distinct from commit;
and no ambient filesystem/network authority in semantic reasoning. Existing
A0 and managed ACTIVE publication semantics remain distinct.
Prohibited shortcuts remain explicit: canonical graph databases in Git; arbitrary agent writes to graph fields; unrepresentable graph-only states; hidden cache mutations; approval inferred from proof/review; authoritative ML relevance ranking; daemon-required compilation; and graph diffs replacing human-readable source review. Optional deterministic ranking must stay advisory and outside source/graph identity, proof and commit decisions.
Economics provides offline bytes/lexical-unit/relevance evidence only; its small corpus produced context larger than source. Still missing are measured end-to-end workloads comparing source-first and semantic workflows across: model tokens, tool calls, invalid attempts, stale recovery, correctness, validation cost and human review time. Add warm/cold/persistent/incremental and multi-agent conflict/recovery cases; bind corpus, compiler, prompts/models, source revisions and correctness/coverage criteria. Run generated-client, protocol preservation, hostile-image/candidate, backend and policy-selected quality gates before any completion or comparative productivity assertion.
An additive task-economics observation is authored inside the integrated twelve-step Git workflow, with deterministic per-format export and a separate exact-commit envelope contract. It records exact semantic protocol traffic, review-material sizes, scripted control rejections, validation/replay/test operation counts, target-admission row counts and the twelve asserted criteria. It explicitly records stale recoveries as zero and leaves model tokens, external agent tool calls, elapsed validation cost and human review time unobserved. It is infrastructure for the missing comparison, not benchmark results or a productivity claim.
The separate paired comparison harness emits a canonical contract for one available task/lane/trial tuple and a deterministic complete 18-row matrix over the current available lanes. The matrix binds one exact plan/head and the SHA-256 digest of every independently generated trial contract. Neither command invokes an agent or validator or emits an observation. The pinned Zero lane remains explicitly external and unrun; the full observation corpus and every comparative claim remain open.
An authority-free normalized observation API now accepts exact caller-supplied
paired records that embed and authenticate the existing observation-v1 bytes.
It checks closed metric, artifact-reference, acceptance and paired-binding
inventories and emits deterministic descriptive deltas only for matching
outcomes; absent Zero and mismatched outcomes remain not_assessed, and
superiority is never inferred. V5 exposes a smaller envelope-safe
agent/task-comparison query through generated clients and MCP. The compiler
does not invoke agents, tools, validators, reviewers or artifact readers, so
this closes observation ingestion rather than the still-missing executed
comparison.