Bounded Semantic Patch v2

Status: versioned bounded reference; the completion matrix owns product status.

Audience: agent and tool authors, plus compiler contributors.

Semantic Patch v2 is an additive, single-file transaction format for exact identity-scoped source changes. Schema-less patches retain the v1 behavior and the legacy rename domain: explicitly identified functions and resources only.

Frozen grammar

The first non-comment v2 instruction is exactly:

schema semaprax.semantic-patch.v2

It is followed by one base, zero or more operations, and optional requirements:

base <sha256-revision>
rename <function-or-resource-id> to <identifier>
rename-member owner <record-or-variant-case-id> member <field-id> to <identifier>
rename-case owner <variant-id> case <case-id> to <identifier>
replace-call-type-argument expression <expression-id> template <template-id> old-instance <instance-id> index <canonical-u32> from <i64|bool> to <i64|bool>
require no-new-effects

Unknown schemas, a v2 operation without the schema line, a schema line after another instruction, duplicate bases/requirements/selectors, non-canonical indices, conflicts, and overlapping source spans reject before staging.

Identity and transaction contract

All selectors resolve against the same verified pre-edit AST/HIR. Record fields are addressed by (record ID, field ID), payload fields by (case ID, field ID), cases by (variant ID, case ID), and generic arguments by the complete expression/template/old-instance/index/from tuple. Member and case owners and targets must have explicit persistent IDs. Compiler-owned Option/Result declarations and automatic identities are outside the writable domain.

Construction and record-update grammar has no shorthand, so only the exact resolved label changes. Record and variant pattern shorthand is expanded from { old } to { new: old }; the binding name, ValueId, and every Place root remain unchanged. Every edit is computed before any text changes, applied in reverse byte order, parsed and verified once, and committed through the existing authenticated A0 staging/held-handle/final-reparse path.

The mandatory post-HIR semantic-delta gate compares Graph meaning after removing only the exact admitted display-name fields, exact addressed call instance/type arguments, and exact selected old/new materialized instance declarations. All other declaration IDs, owner/index/type facts, binding names and IDs, places, layouts, call facts, and CleanupPlan bytes must remain equal. Generic edits must produce the grouped final argument vector and derived instance, and no other reachable instance may change. The Graph lattice maximum remains v14, lower-schema programs remain v10-v13, and CleanupPlan selection is unchanged.

Stable diagnostics

• SPX-G106: duplicate, conflicting, no-op, or overlapping v2 edit.
• SPX-G107: wrong owner/kind/persistence domain or compiler-owned identity.
• SPX-G108: stale generic-call tuple, source/HIR index mismatch, or excessive post-HIR semantic delta.
• Existing v1 parse, name, stale-revision, effect, verification, and A0 I/O diagnostics retain their codes and behavior.

The direct single-file apply route also rejects a schema-less rename whose candidate revision equals its base as SPX-G106, before creating a staging file. A source whose retained permissions are read-only rejects as SPX-I205; atomic replacement never turns read-only input into write authority.

Threat model and nonclaims

The source snapshot, lock, staging handle, sibling paths, final source reparse, and atomic rename retain the A0 transaction checks. Failed and stale operations leave source unchanged. The patch file itself is trusted input: A0 authenticates the source and stage, not a concurrently replaced read_to_string(patch_path); callers that require patch provenance must snapshot/authenticate it externally.

The separate Semantic Impact v1 command can run this same pre-state semantic preflight over owned source/patch buffers and report a candidate revision without committing it. That preview's digest binds the exact patch bytes it processed, but it does not authenticate the continuing patch path or widen Patch v2's operation, Graph, CleanupPlan, or commit scope.

The separate Semantic Review v1 command embeds one complete, nontruncated canonical Impact v1 report for Patch v2 and classifies each authored operation across seven fixed sections. Review is read-only and adds no Patch v2 operation, flag, Context, target execution, verifier/proof artifact, provenance authentication, or A0 authority.

The separate Semantic Patch Evidence v1 capsule binds that unchanged Review/Impact evidence and can be independently replayed. Only the opt-in patch-with-evidence route requires replay before staging. Additive Target Evidence v1 and Evidence v2 bind compiler projections without adding Patch operations, target execution, authority, or multi-file scope. Only the evidence routes gate A0 staging; ordinary patch and Patch v2 bytes, selectors, operation meaning, and trusted patch-path nonclaim are unchanged. The capsule is neither authenticated provenance nor reusable commit authorization.

The separate Diagnostic Repair v1 tranche defines an isolated Semantic Patch v3 with exactly one canonical three-line assign-function-id operation. V3 does not compose with or widen v2, and Impact v1 rejects every syntactically valid, canonical v3 as SPX-G110 before semantic selector interpretation; malformed or noncanonical v3 remains SPX-G101.

This milestone does not add construction/update shorthand, full type renames, aggregate/resource generic arguments, generic-template-to-generic-template composition, transitive generic instance materialization, multi-file commits, Graph v15, or a new CleanupPlan schema. The admitted v14 resolver materializes generic instances only from monomorphic source calls, so the bounded reachable delta is the directly selected old/new instance set.

Evidence

tests/semantic/patch_v2.rs covers schema confusion, legacy v1 success, noncanonical exact spans, every member use site (declaration, construction, update, projection, flat/nested record and variant patterns), shorthand binding identity, case/payload changes, same-name owner isolation, a single mixed atomic batch, two indices on one call, unrelated same-instance calls, every tuple dimension, automatic/compiler-owned/wrong-kind/cross-owner targets, collisions, and no-write failures. The mixed transaction's canonical post-edit revision KAT is sha256:f2f344c5a19591dfde2aa65ffd21918464be0848f526d6a59b977af9394805a7. Its exact old/new call-instance KATs are semaprax.function-instance.v1:14:generic.marker:2:3:i644:bool and semaprax.function-instance.v1:14:generic.marker:2:4:bool3:i64. The focused suite also applies a v2 call patch and executes the changed source under Clang -O0/-O2 and Node/Wasm (256 re-entries). The focused suite is 9/9. The exact f95d243 full matrix is hosted green in run 31401200449 attempt 2, including Ubuntu job 93505622044; the lock-reconciled isolated runtime is green in Wasmtime job 93505622110.

Focused gates:

cargo test --locked -p semaprax --all-features --test semantic patch_v2::
cargo test --locked -p semaprax --all-features --test semantic patch::
cargo test --locked -p semaprax --all-features --test language generic_functions::
cargo test --locked -p semaprax --all-features --test cleanup_backends executable_generic_function::
cargo clippy --locked --workspace --all-targets --all-features -- -D warnings

The separate Semantic Workspace Transaction v1 may embed an exact canonical Patch v2 string for one changed managed file. That composition does not change this single-file grammar, preflight, KATs, authority, provenance nonclaim, or semantic-delta gate and adds no cross-file Patch meaning.

Semantic Workspace Patch Evidence v1 independently rebuilds the same child preflight and binds its existing Patch/Review/Evidence-v1 digests. The outer capsule changes no Patch-v2 bytes, operation, authority, or single-file semantic-delta boundary.