diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md index 17a18ab371..51564280a3 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md @@ -43,7 +43,8 @@ not amend normative sections. string enums, `Literal` aliases, named closed sets, TypeScript `as const` arrays, and every constant name defined in more than one module. A public smoke, `examples/semantic-vocabulary-drift-smoke.py`, checks the code against - both on every premerge and full-public run. A change that widens a + both inside the default `pytest` sweep on every pull request; premerge and + the full-public fleet are additional surfaces (Section 10). A change that widens a vocabulary, forks a constant, adds a carrier, or weakens the registry must edit the registry or regenerate the inventory in the same diff, so the reviewer sees the semantic change as a change. @@ -196,6 +197,29 @@ the TypeScript runtime each own one spelling of the same idea. discovery under `examples/` and the `repo-architecture-budget` premerge profile are additional surfaces, not the obligation: the fleet runs after merge and on a schedule, and premerge selects by changed-path tokens. +- **I11 Roles are distinct.** A vocabulary has one owner, some producers, some + interpreters, and some pass-throughs (Section 5, "Roles of a vocabulary"). + Only the owner defines the set and only producers write values. Mentioning, + comparing, serializing, or displaying a value confers no ownership. An + interpreter or pass-through that starts writing a value has become a + producer and must be registered as one. Enforced from M0.5. +- **I12 Every kernel value is produced.** For a `kernel` vocabulary, every + value not listed under `compatibility_only` has at least one production site + the fixed production forms recognise or a `variable_sourced_values` entry. A + value that is only compared is dead or compatibility-only, never canonical. + `skip` in `effective_action` is the first expected failure. Enforced from + M0.5; at M0 the literal scan accepts a compared value as carried. +- **I13 Producers write registered values only.** A production site that + writes a value outside the registered set fails closed, independently of + whether any consumer compares it. Production is stricter than comparison: a + consumer comparing an unregistered value is dead code, a producer writing one + is protocol drift. Enforced from M0.5; the M0 literal scan covers both forms + together. +- **I14 Scope is declared, not inferred.** A name defined in several modules + is a fork unless the registry declares it `bounded_context` and lists the + contexts and one owner symbol per context. Declared names leave the fork + budget; a rename does not change the budget's meaning and is not a fix. + Enforced from M0.5; at M0 `SOURCE_SURFACES` is counted as a fork and noted. ## 3. Scope and non-goals @@ -214,10 +238,19 @@ the TypeScript runtime each own one spelling of the same idea. - The later milestones that turn `effective_action` into a typed enum, split its three slots, publish the projection through the contract, and retire legacy fields and twins under existing repository rules. +- The scan root is the `loopx/` package. "Repository-wide" in this RFC means + every carrier under `loopx/`, in both runtimes, not every file in the git + tree. The inventory `root` and every `literal_scan.roots` entry say `loopx` + and the smoke reads nothing else. ### Non-goals - Changing any runtime decision, payload shape, or wire format. +- Scanning `apps/` (about 90 TypeScript files on the baseline) or `examples/` + (a dozen `effective_action` assertions in smokes). Those are consumers and + test doubles, not producers; a smoke that asserts an unregistered value is + invisible to M0 and is accepted as such until a milestone widens the root, + which would also raise the merge-order cost in Section 10. - Curating every closed set by hand. The inventory maps all of them; only vocabularies that cross a module or runtime boundary and are dispatched on are curated with owners, values, and relations. @@ -275,6 +308,102 @@ Forbidden alternate authorities: a second registry, a per-module list that restates registered values, or a prose table that claims to be normative for a registered vocabulary. +**Scope of a name (planned for M0.5, not in M0).** The collision rules are +keyed by name, so they cannot tell a fork from four bounded contexts that +happen to reuse one identifier. `SOURCE_SURFACES` is the first case: its four +definitions in `global_risks.py`, `global_todos.py`, `summary_all.py`, and +`pr_review.py` each list the data sources of that one CLI command, and the +value sets are meant to differ. It is counted in `multi_value_forks` today and +must not be "fixed" by renaming, because a rename lowers the number without +changing the code's meaning. M0.5 adds a `scope` field to the registry with at +least `global` and `bounded_context`, lets a bounded-context name be declared +once with its owning contexts, and removes declared names from the fork +budget (I14, the schema rows below, and the M0.5 row in Section 11). Until +then the fork budget is a ceiling that contains this one known +misclassification, recorded in the registry's `inventory_ratchets` note. + +### Roles of a vocabulary + +A module that mentions a value is not its owner, and a vocabulary has more +than one kind of participant. Consumer is the umbrella role for code that reads +or accepts a value; interpreter and pass-through are its two tracked subroles. +The registry distinguishes these roles because the check that makes sense differs +by role: + +| Role | What it does | Registered | Check | +| --- | --- | --- | --- | +| Owner | Defines the closed set as one `module::Symbol` per runtime | Yes, since M0 | I1 to I3 | +| Producer | Writes a value into the field: assignment, dict or object literal, constructor keyword, `return` of a literal inside a listed deciding function, enum member on the owner | Yes for `kernel` vocabularies, from M0.5 | I12, I13 | +| Consumer | Reads or accepts a vocabulary value; this is the umbrella role for interpreters and pass-throughs | Usually no; relation is reported rather than curated | F3 | +| Interpreter | Consumer that branches on or maps the value: `if`, `match`, `switch`, membership test | No; found by the dispatch scan, ranked by `--report` | I2, F3 | +| Pass-through | Consumer that serializes, persists, forwards, or displays the value without changing its meaning | No | F3; persistence also needs F6 evidence | + +Two rules follow. A value with no producer is dead or compatibility-only: +`skip` is compared in `todos/user_gate.py` and written nowhere, so M0 passes +it and M0.5 fails it until it is removed or listed under `compatibility_only`. +Production is stricter than comparison: M0.5 scans production forms on their +own and fails on an unregistered produced value (I13), while the M0 literal +scan keeps catching unregistered comparisons (I2). Interpreters and +pass-throughs are deliberately not registered; otherwise every consumer edit +would touch the registry, the churn Section 6 rejected for consumer counts. +Their relations to a vocabulary are advisory output of `--report`. + +Production forms are fixed in the smoke at M0.5, like the dispatch forms: +Python `x["f"] = "v"`, `f="v"` as a constructor keyword of the envelope or +packet type, `return "v"` inside a function the registry lists as a producer, +and member access on the owner enum; TypeScript `f: "v"` in an object +literal, `x.f = "v"`, and the conditional expression. `variable_sourced_values` +stays for the values a producer builds from a variable the scan cannot follow. +Which vocabularies must list producers: `kernel` at M0.5; `cross_runtime` only +when a value is added or removed after M0.5; `cross_module` only if promoted +(Q8). Persistence is a property the production scan can answer: a producer +whose listed symbol is a journal or receipt writer marks the vocabulary +`persisted`, which is the fact Q2 and Q10 wait on. + +### Formal model and proof boundary + +The registry is a finite specification of a larger program semantics. Let +`V` be the set of registered vocabularies, `Val(v)` the admitted values of a +vocabulary `v`, and `S` the set of source sites. The model records relations, +not just names: + +```text +D ⊆ S × V defines +P ⊆ S × V × Val(v) produces +C ⊆ S × V × Val(v) consumes or branches on +I ⊆ S × V × V interprets one vocabulary as another +T ⊆ S × V passes through without changing meaning +G ⊆ V × V × (Val ⇀ Val ∪ {reject}) projects +R ⊆ S × V × Version persists a value durably +``` + +The minimum semantic obligations are: + +1. **Producer closedness:** `Produced(v) ⊆ Val(v)`. A recognised producer + cannot write a value outside the registered set. +2. **Canonical liveness:** `Canonical(v) ⊆ Produced(v) ∪ CompatibilityOnly(v)`. + A value that is only compared is dead or compatibility-only, never + canonical. +3. **Consumer domain closedness:** `Accepted(c) ⊆ Val(v)`, unless the consumer + explicitly declares an external or partial domain. +4. **Scope separation:** a name collision is a semantic conflict only when the + declared scopes overlap. Spelling alone cannot establish equivalence. +5. **Projection totality:** for every source value, a projection maps to a + target value or explicit `reject`. +6. **Persistence compatibility:** a persisted vocabulary change preserves all + readers or declares a versioned migration. + +These are different proof obligations. M0 establishes owner-set equality, +cross-runtime parity, the declared executable projection, and inventory +freshness. Fixed literal forms and closed-set carriers provide bounded evidence, +not whole-program proof. M0.5 adds bounded producer and scope checks. Producer +discovery over dynamic code, behavioural equivalence of `same_concept`, and +persisted-reader compatibility remain unproved until their source-to-sink +edges are modelled. The registry stores this proof boundary in +`formal_model`; an `unproved` property is an explicit limitation, never an +implicit pass. + + ### State model and schema `loopx/semantics/vocabulary_v0.json`, `schema_version` @@ -288,6 +417,11 @@ vocabulary key fails the smoke. | `vocabularies..tier`, `status` | `kernel`, `cross_runtime`, `cross_module`; `canonical`, `legacy`, `merge_candidate` | Closed enumerations | | `vocabularies..literal_scan` | `field`, roots, suffixes | Every literal the fixed dispatch forms capture is registered; every registered value is captured or variable-sourced (I2) | | `vocabularies..variable_sourced_values` | value to producer module | The producer still contains the quoted value | +| `vocabularies..scope` (M0.5) | `global` or `bounded_context`; a `bounded_context` entry lists `contexts`, each with one owner symbol | Closed enumeration; declared bounded-context names are excluded from `multi_value_forks`; an undeclared multi-module name stays a fork (I14) | +| `vocabularies..producers` (M0.5) | `path::Symbol` sites that write the field, required for `kernel` | Every site writes registered values only; every value not under `compatibility_only` has at least one site or a variable-sourced entry (I12, I13) | +| `vocabularies..compatibility_only` (M0.5) | values kept so readers of persisted records still resolve them | Subset of `values`; zero production sites; each carries a `value_notes` reason and a retirement milestone | +| `formal_model` | finite universes, role relations and hierarchy, semantic obligations, and established/bounded/unproved claims | Exact schema, role hierarchy, and invariant ids are checked by the drift smoke; enforcement stages cannot be mistaken for completed proofs | +| `formal_model.enforcement_policy` | blocking-now, blocking-next, advisory, and unproved lanes | Every formal invariant appears exactly once and its lane agrees with its enforcement stage | | `vocabularies..value_notes`, `deprecated_values` | per-value review notes; values slated for removal | Names must be registered values | | `relations.same_concept` | groups of `vocabulary.value` members | Every member resolves | | `relations.shared_field_names` | one field name, its slots and the vocabulary or values each carries | Every slot resolves | @@ -400,6 +534,13 @@ inventory in the same PR. | Measurement covers both carrier shapes and filters local naming | `pytest tests/architecture/test_semantic_inventory.py` | pass, including the collision and module-local-convention fixtures | Rules come from this RFC, not from scanner output | | No behavior change from the two owner fixes | `pytest tests/test_loopx_turn_transaction.py tests/test_loop_turn_loop_controller.py tests/test_turn_loop_disposition.py tests/test_loopx_turn_managed_step.py tests/control_plane -k authority` and `loopx canary premerge --from-git-diff` | pass | Environment failures already present on `main` are excluded when reproduced on a clean tree | | Docs governance accepts the RFC pair | `python3 examples/docs-governance-smoke.py` | pass | Checks mirror, links, index | +| Retirement budgets count substrings, not identifiers | `goal_boundary` counted with `in file.text` and with `\bgoal_boundary\b` | 35 vs 30 Python modules on the baseline | Known boundary; M3's zero-reader gate needs the identifier count, tracked in Section 12 | +| The module-local convention filter is a code edit | Widen `MODULE_LOCAL_CONVENTION` in `inventory.py` and regenerate | `*_semantic` budgets fall with no code change elsewhere | Known boundary; the regex is in code so the widening is a reviewed diff, and the unfiltered totals stay budgeted | +| A registered value nobody produces fails (M0.5) | Run the production-form scan on the baseline | Fails naming `effective_action` and `skip`; passes after `skip` is removed or listed `compatibility_only` | First expected I12 failure; a compared-only value is not carried | +| A producer of an unregistered value fails (M0.5) | Write `effective_action: "brand_new"` in a listed producer site | Fails naming the site and the value even though no consumer compares it | I13; production is stricter than comparison | +| A bounded-context name leaves the fork budget only by declaration (M0.5) | Declare `SOURCE_SURFACES` with its four contexts; separately, rename one definition without declaring | The declaration lowers `multi_value_forks` to 3; the rename alone does not | I14; the honest fix is a registry edit a reviewer sees, the rename is code without registry change | +| An upstream merge can stale the committed inventory | Replay the scanner over the first parent and the merge of the last twenty `upstream/main` merge commits | 8 of 20 merges change at least one carrier | Measured cost of committing a snapshot; the handling rule is Section 10 and Section 12 Q9 | +| The formal model cannot silently lose a proof obligation | Remove an invariant, role, relation, or proof-boundary category from `formal_model` | The drift smoke fails on the exact formal-model shape | The model is a finite contract and proof ledger; it does not prove the listed properties by itself | Known limits, stated so the check is not over-trusted: @@ -446,16 +587,111 @@ for a diff touching `loopx/control_plane/` alone, and the fleet workflow is deliberately not a PR-required check. A fleet-discovered smoke is not a commit-time check until a required PR job collects it. +**Merge-order hazard.** `inventory_v0.json` is a committed snapshot of the +whole `loopx/` tree, and the smoke fails when the tree and the snapshot differ. +Two pull requests that each add a carrier and each regenerate the inventory are +both green against the `main` they were built on; whichever merges second +leaves `main` with a snapshot missing the first one's entries, and the sweep on +`main` is red until someone regenerates. On the last twenty merges to +`upstream/main`, eight changed at least one carrier, so this is a weekly event, +not a corner case. The first upstream sync of this branch reproduced it: twelve +merged commits added one enum and three closed sets and the check failed +until regenerated. The handling rule is Section 12 Q9; until it is decided, the +rule is that the person who merges a PR after a red `main` regenerates the +inventory in a follow-up commit that touches only `inventory_v0.json`, and the +smoke's failure text names that command. + +**Interpreter.** The smoke, the generator, and the scanner require the +project's Python (`>=3.11` in `pyproject.toml`); `zip(strict=True)` fails on +3.9. Fleet and premerge commands are spelled `python3` by repository convention +and run under the CI interpreter. A macOS system `python3` is 3.9, so local +premerge runs need a 3.11 environment on `PATH`; the docs spell the direct +commands as `python3.11` for that reason, and the planner entry is left as +`python3` on purpose. + ## 11. Normative delivery plan | Milestone | Shipped behavior | Entry gate | Exit evidence | Rollback | | --- | --- | --- | --- | --- | | M0 | Registry with 26 vocabularies and 9 relations, generated inventory with `--check`, drift smoke with fixed dispatch forms and coverage floor, two owner forks removed, RFC index entry | This RFC opened | Section 9 rows green; 20 mutation classes fail closed | Delete the smoke, `loopx/semantics/`, the generator, and its test | -| M1 | `EffectiveAction` typed enum in one owner module; the replay observation and frontier slots split off (Q6); producers and consumers import it; registry `literal_scan` tightened to the enum | M0 merged; owner module chosen (Q3); slot split decided (Q6) | Smoke green; zero bare `effective_action` literals outside the owner; parity fixtures for status/should-run unchanged | Revert to literals; registry keeps the set | +| M0.5 | `scope` with `global` and `bounded_context` and per-context owners; `producers` and `compatibility_only` on `kernel` vocabularies; production-form scan with the two role checks (I12, I13); retirement budgets counted by identifier with all six anchors lowered in one diff (Q11); merge-order rule from Q9 written into Section 10 | M0 merged; Q9 decided or its interim rule accepted | Smoke green with I11 to I14 enforced; `skip` resolved; `multi_value_forks` at 3 by declaration; Section 9 role rows green; `turn_route` persistence answered for Q2 | Remove the three fields and the role checks; budgets return to the M0 anchors | +| M1 | `EffectiveAction` typed enum in one owner module; the replay observation and frontier slots split off (Q6); producers and consumers import it; registry `literal_scan` tightened to the enum | M0.5 merged; owner module chosen (Q3); slot split decided (Q6) | Smoke green; zero bare `effective_action` literals outside the owner; parity fixtures for status/should-run unchanged | Revert to literals; registry keeps the set | | M2 | Route-to-disposition projection, the `decide_loop_disposition` decision table, and the cross-runtime sets published through a shared contract with generated Python and TypeScript bindings, following the coordination contract generator | M1 merged; Q2 and Q7 decided | Generator `--check` and smoke green; `settlement.ts` and `transaction.py` read the generated set | Regenerate from prior contract | | M3 | Per-field retirement of legacy should-run fields, one field per PR, budgets lowered to zero and the field removed | Field has zero external readers proven by producer/reader research | Schema-reduction record per `AGENTS.md`; Appendix B entry | Restore field from the last writer | | M4 | Twin budget lowered with each replacement-first cutover from the migration RFC | Each cutover PR | Budget edit in the same diff | None needed; budget follows code | +A ratchet without a target is a direction, not a plan. The table below is the +state at which this RFC is complete; each row is a registry budget or a +vocabulary property the smoke can check. Rows marked *open* wait on a Section +12 decision and are the reason the plan is a skeleton until those are recorded. + +| Surface | Baseline (`1dc6ad8d8`) | Target when this RFC closes | Reached by | +| --- | --- | --- | --- | +| `effective_action` values | 33 literals, no owner symbol | one enum owner; `skip`, `observe_replay`, `block_replay`, and the two `quota_action_selection_*` codes gone from the decision slot; about 28 values | M1 | +| `effective_action` slots in one envelope | 3 vocabularies under one field name | 1, or a registered union if Q6 keeps the field | M1 (Q6) | +| Turn vocabularies | 3 sets, 28 values, 21 distinct, 7 redundant spellings | 3 sets kept; projection and decision table generated and checked; spellings unchanged unless Q10 sets a merge | M2 (Q2, Q10 *open*) | +| Same-runtime forks, semantic | 18 names | 0 | baseline PRs | +| Conflicting values, semantic | 2 names | 0 | baseline PRs | +| Multi-value forks | 4 (1 misclassified) | 0 after `scope` declares bounded-context names | M0.5 + baseline PRs | +| Multi-value twins | 19 | 0 | baseline PRs | +| Legacy should-run fields | 6 fields, 124 py / 10 ts module mentions | 0 fields | M3, identifier-counted | +| Merge-candidate groups | 32 unreviewed | every group classified; only `same_semantics` groups merged | classification PR, then per-group PRs | +| Control-plane py/ts twins | 43 | follows the TypeScript migration RFC; no target here | M4 | + +### Two-track execution and enforcement lanes + +The roadmap separates repairing existing semantic debt from improving the +measuring apparatus. Track A can proceed without waiting for a design decision: +remove real forks, conflicts, twins, and legacy readers one narrow PR at a time. +Track B improves what the guard can know: scope declarations, bounded producer +analysis, identifier counting, and merge-order handling. Track A reduces the +measured debt; Track B makes that measurement more faithful. M1 and later depend +on Track B where the current measurement is known to be incomplete. + +```text +Track A: baseline debt repairs ───────────────────────────────┐ + ├─> M1 typed slots +Track B: scope + producer model + metric boundaries ──────────┘ │ + ├─> M2 generated projections + ├─> M3 legacy retirement + └─> M4 runtime twin migration +``` + +The formal model uses four enforcement lanes so a difficult property does not +become an accidental merge blocker: + +| Lane | Properties | Current meaning | +| --- | --- | --- | +| `blocking_now` | F5 projection totality | Enforced by the M0 smoke today | +| `blocking_next` | F1 producer closedness, F2 canonical liveness, F4 scope separation | Planned blocking checks after M0.5; not claimed by M0 | +| `advisory` | F3 consumer domain closedness | Reported evidence; it does not block ordinary consumer edits | +| `unproved` | F6 persistence/version compatibility | An explicit proof gap; it cannot be reported as passed | + +The exit condition for a phase is its evidence row, not the existence of a +formula or a registry entry. A property moves from `unproved` to `advisory` only +when a bounded source-to-sink analysis exists, and moves to a blocking lane only +after its false-negative boundary is documented and mutation tests cover the +recognised forms. This keeps the contract strict about silent corruption while +allowing incomplete analyses to remain useful without blocking unrelated work. + +The phases are therefore: + +1. **M0:** keep the current structural guard and make its proof boundary + explicit. +2. **M0.5:** implement `scope`, producer forms for the four Turn kernel + vocabularies, and identifier-based retirement counts. +3. **M1:** split the overloaded `effective_action` slots and introduce one typed + owner after Q3 and Q6 are decided. +4. **M2:** publish the full decision table and both projection hops through a + generated cross-runtime contract. +5. **M3/M4:** retire legacy fields and reduce Python/TypeScript twins only when + their reader and migration evidence is complete. + +This roadmap is normative for dependencies and exit evidence. Issue #4447 may +carry owners, suggested dates, and operational checklists, but it must not +introduce a competing target state. + + ## 12. Open decisions 1. **Registry location.** Owner: kernel maintainers. M0 implements @@ -468,7 +704,13 @@ commit-time check until a required PR job collects it. `wait`), and `stop`, `terminal`, `contract_error` exist on one side only. The `same_concept` relations record the four shared verdicts. Recommendation: keep both, publish the projection in M2, revisit after the - managed-step consumer matures. Needed before M2. + managed-step consumer matures. Needed before M2. The stated reason for + keeping both is that merging would touch persisted Turn records; that + premise is unverified. Before deciding, the M0.5 production-form scan (I12, + Section 5) applied to `turn_route` should establish + whether `turn_route` is ever written to the journal or a receipt, or only + flows in-process; if the latter, the cost of a merge is far lower than this + RFC assumes and Q10 applies. 3. **Owner module for `EffectiveAction`.** The registry declares no owner today because no symbol exists; the literal scan is the only check. Options: `quota/should_run_packet.py` (largest producer), a new @@ -499,6 +741,30 @@ commit-time check until a required PR job collects it. with three or more external consumer modules or a cross-runtime twin must be curated. Recommendation: yes as a review rule now, enforced by the smoke only after a quarter of inventory history exists. Owner: kernel maintainers. +9. **Inventory freshness across merges.** The committed snapshot goes stale + when two carrier-adding PRs merge in sequence (Section 10, eight of the last + twenty upstream merges). Options: (a) branch protection requires the PR to + be up to date with `main`, which removes the hazard and slows every PR; + (b) the merger owns a regenerate-only follow-up commit, which keeps the + snapshot in git history and accepts a red `main` for minutes; (c) the + inventory is not committed and CI generates it for the PR diff only, which + loses `git blame` on carriers. Recommendation: (b) now, (a) if red `main` + exceeds once a week. Owner: repository maintainers. This is an operations + decision, not a code change; it belongs in the tracking issue's decision + list, not its task list. +10. **Target state for the Turn vocabularies.** Section 11's target table + keeps three sets and seven redundant spellings by default because Q2 + recommends keeping both. If the M0.5 production-form scan in Q2 shows `turn_route` is + not persisted, the maintainers should choose between (a) three sets with a + generated projection, the current plan, and (b) a two-phase merge (dual- + write, then retire) to one spelling per concept. Without this decision the + RFC has budgets but no definition of done for its headline problem. + Owner: Turn driver owner. Needed before M2 closes. +11. **Retirement budgets by identifier.** The six legacy-field budgets count + `field in file.text`; `goal_boundary` matches `goal_boundary_repair`. M3's + zero-external-reader gate needs word-boundary counting, which lowers all six + anchors in one diff. Recommendation: do it before the first M3 PR. + Owner: kernel maintainers. ## Appendix A: Execution ledger (non-normative) @@ -599,6 +865,55 @@ commit-time check until a required PR job collects it. departing from the precedent; I10 added; Section 9 gains three rows; Section 10 rewritten from one sentence to a surface table. +### 2026-09-15 — M0 reviewed a fourth time: scope, merge order, target state + +- **Baseline:** `503991dd2` merged; `upstream/main` at `2f84af990`, twelve + commits ahead of the branch. +- **Trigger:** a fourth review asked what the guard's inputs depend on and + what "repository-wide" covers. Merging the twelve upstream commits into a + scratch tree staled the inventory (one enum, three closed sets); replaying + the scanner over the last twenty upstream merges showed eight would have + done the same. The RFC said repository-wide while the inventory root and + every literal scan said `loopx/`; `examples/` holds a dozen + `effective_action` assertions and `apps/` about ninety TypeScript files the + smoke never reads. +- **Also found:** `SOURCE_SURFACES` is four CLI commands each listing its own + data sources, not a fork; the name-keyed rule cannot express that. Retirement + budgets count substrings (35 vs 30 identifier modules for `goal_boundary`). + The plan had budgets but no target state, and its four entry decisions had + no owner deadline. +- **Delivered:** Section 3 fixes the scan root to `loopx/` and names `apps/` + and `examples/` as non-goals; Section 5 previews the M0.5 `scope` field with + `SOURCE_SURFACES` as the first case; Section 9 gains three known-boundary + rows; Section 10 gains the merge-order hazard and interpreter paragraphs; + Section 11 gains the target-state table; Section 12 gains Q9 to Q11 and a + verification note on Q2; the registry's `inventory_ratchets` gains a note on + the misclassified fork. No code or budget changed. +- **Not done on purpose:** the premerge planner keeps `python3`, because every + fleet command is spelled that way and the runner smoke asserts the text; the + interpreter requirement is documented instead. +- **Evidence:** Appendix C, E17 to E20. +- **Effect on normative design:** Section 3 scope narrowed to match the code; + Section 11 now has a definition of done; Section 12 gains three decisions. + +### 2026-09-15 — Role and scope models written into the contract + +- **Trigger:** the RFC used "producer" and "consumer" nineteen times without + defining either, Q2 and Q10 depended on "a producer check" the document + never specified, `scope` existed only as a preview paragraph, and Section 1 + still said the smoke ran "on every premerge and full-public run" after + Section 10 had made the pytest sweep the obligation. +- **Delivered:** Section 5 gains "Roles of a vocabulary" (owner, producer, + interpreter, pass-through) and three schema rows (`scope`, `producers`, + `compatibility_only`); Section 2 gains I11 to I14, each marked as enforced + from M0.5; Section 9 gains three M0.5 rows; Section 11 gains the M0.5 + milestone and M1 now gates on it; Q2 and Q10 point at I12 instead of an + undefined check; Section 1 matches Section 10. No code, registry value, or + budget changed; the M0 smoke does not yet enforce I11 to I14. +- **Effect on normative design:** four invariants added with an explicit + enforcement milestone; the plan gains a definition of "produced" that M3's + zero-reader gate and Q2's persistence question can both use. + ## Appendix B: Decision log | Date | Decision | Owner / approval | Alternatives | Normative sections changed | @@ -624,6 +939,10 @@ commit-time check until a required PR job collects it. | E14 | The smoke was not on the pull-request path | `1dc6ad8d8` + M0 | `loopx canary premerge --changed-file loopx/control_plane/turn_driver/loop_controller.py --changed-file loopx/control_plane/quota/turn_envelope.ts`; `.github/workflows/full-public-smokes.yml` triggers | 32 commands planned, smoke absent; fleet runs on push to `main` and schedule only | Selection by path token; CI wiring read from the workflow files | | E15 | A tightened budget could drift back to its anchor | `1dc6ad8d8` + M0 | `ratchets[key] <= BUDGET_ANCHOR[key]` and `floor[key] >= anchored` in the smoke | any value between the tightened budget and the anchor passed | Code reading; the precedent uses the same comparison | | E16 | Equality closes the stall and the wrapper reaches the sweep | `1dc6ad8d8` + M0 | lower one `inventory_ratchets` entry with the anchor untouched, then `pytest tests/architecture/test_semantic_vocabulary_drift.py` on the clean tree | the mutation fails naming both values; the wrapper passes in about three seconds | Local exercise plus committed test | +| E17 | Upstream merges stale the committed inventory | `upstream/main` `2f84af990`, last 20 first-parent merges | scanner facts of every changed `loopx/**/*.{py,ts}` compared between first parent and merge | 8 of 20 merges change at least one carrier; the branch's own upstream sync added 1 enum and 3 closed sets | Facts-level comparison, equivalent to a full regenerate | +| E18 | Declared scope exceeded the scan root | `503991dd2` + M0 | `literal_scan.roots` and inventory `root` read from the registry; `grep` for `effective_action` dispatch literals under `examples/`; count of `.ts`/`.tsx` under `apps/` | roots are `loopx` only; 12+ assertions in `examples/`; 90 files in `apps/` | Consumers and test doubles, not producers | +| E19 | `SOURCE_SURFACES` is four bounded contexts, not a fork | `503991dd2` | the four `multi_value_forks` definitions read from the inventory | each module lists the data sources of its own CLI command with disjoint values | Judgement from reading the values; the rule cannot make it | +| E20 | Retirement budgets over-count by substring | `503991dd2` | `'goal_boundary' in text` vs `\bgoal_boundary\b` over `loopx/**/*.py` | 35 vs 30 modules | Identifier count is the M3 gate's measure | | E13 | The conflict budget mostly measured local naming | `1dc6ad8d8` | `MODULE_LOCAL_CONVENTION` applied to `conflicting_values` and `same_runtime_forks` names | 16 of 18 conflicts and 7 of 25 forks are module-local conventions; the semantic subsets are 2 and 18 | Classification is a name pattern, documented in the scanner and pinned by a fixture test | ## Appendix D: Rejected or superseded alternatives @@ -662,3 +981,20 @@ projection proven to be a bijection after M2. - One field name can carry several vocabularies inside one envelope; a scan that sees the field cannot see the slot. Record the slots as a relation so the ambiguity is a registered fact, not an accident the registry blesses. +- A committed snapshot of the whole tree makes the guard's input depend on + other people's merges. Measure how often the tree changes under it before + committing it, and write down who regenerates when `main` goes red. +- A name-keyed collision rule needs a way to say "these are different things + that share a name". Without it the honest fix and the dishonest fix (a + rename) lower the same number, and reviewers cannot tell them apart. +- When a document widens its scope faster than the code, the two must be + reconciled in whichever direction is cheaper, but they must match. A scope + claim the scanner does not implement is a false invariant. +- Budgets that only go down describe a direction. Write the target table + before the second milestone, or nobody can say when the work is done. +- A decision that waits on "a check" the RFC never defines is a dangling + reference dressed as prudence. Name the invariant and the milestone that + delivers the check, or the decision has no input and never closes. +- Using a role word (producer, consumer) nineteen times is not defining it. + Until the roles are a table with a check per role, "who writes this value" + is a question every reviewer answers differently. diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md index 10d46ce690..cba3879ca0 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md @@ -37,8 +37,9 @@ RFC 成熟度与交付成熟度彼此独立。带日期的进度条目不修改 以及仓库同意只降不升的预算。生成清单 `inventory_v0.json` 映射 `loopx/` 下 每一个闭集载体：字符串枚举、`Literal` 别名、命名闭集、TypeScript `as const` 数组，以及在多个模块中定义的每个常量名。一支公共 smoke - `examples/semantic-vocabulary-drift-smoke.py` 在每次 premerge 与 full-public - 运行时用两份文件核对代码。任何扩宽词表、分叉常量、新增载体或削弱注册表的 + `examples/semantic-vocabulary-drift-smoke.py` 在每个 PR 的默认 `pytest` 扫描 + 里用两份文件核对代码；premerge 与 full-public 舰队是附加表面（第 10 节）。 + 任何扩宽词表、分叉常量、新增载体或削弱注册表的 改动，必须在同一个 diff 里修改注册表或重新生成清单，评审者因此能把语义 变化当作变化看见。 2. **什么不变。** 运行时行为、线上格式、枚举类本身。每个枚举继续住在自己的 @@ -165,6 +166,23 @@ todos、capabilities 与 TypeScript 运行时各自拥有同一想法的一种 扫描里，因此在每个运行 Python 测试的 PR 上失败即关闭。`examples/` 下的舰队 发现与 `repo-architecture-budget` premerge profile 是附加表面，不是义务： 舰队在合并后和按日程运行，premerge 按改动路径的 token 选择。 +- **I11 角色互异。** 一个词表有一个 owner、若干生产者、若干解释者与若干透传者 + （第 5 节"词表的角色"）。只有 owner 定义集合，只有生产者写入值。提及、 + 比较、序列化或展示一个值不带来任何所有权。开始写入值的解释者或透传者已经 + 变成生产者，必须登记为生产者。自 M0.5 起强制。 +- **I12 每个内核值都被生产。** 对 `kernel` 词表，未列入 `compatibility_only` + 的每个值至少有一个固定生产形式能识别的生产位点，或一条 + `variable_sourced_values`。只被比较的值是死值或兼容值，绝不是 canonical。 + `effective_action` 的 `skip` 是第一个预期失败。自 M0.5 起强制；M0 的字面量 + 扫描把被比较的值当作已携带。 +- **I13 生产者只写注册值。** 写入注册集合之外值的生产位点失败即关闭，与是否 + 有消费者比较它无关。生产比比较更严：消费者比较一个未注册值是死代码，生产 + 者写一个未注册值是协议漂移。自 M0.5 起强制；M0 的字面量扫描把两种形式合在 + 一起覆盖。 +- **I14 作用域靠声明而非推断。** 在多个模块中定义的名字是分叉，除非注册表把它 + 声明为 `bounded_context` 并列出各上下文及每个上下文一个 owner 符号。已声明 + 的名字离开分叉预算；改名不改变预算的含义，不算修复。自 M0.5 起强制；M0 把 + `SOURCE_SURFACES` 计为分叉并加备注。 ## 3. 范围与非目标 @@ -180,10 +198,17 @@ todos、capabilities 与 TypeScript 运行时各自拥有同一想法的一种 版本；六个旧 should-run 字段；控制面孪生数量；清单的分叉与冲突预算。 - 后续里程碑：把 `effective_action` 变成类型化枚举、拆分其三个槽位、通过契约 发布投影、按现有仓库规则退休旧字段与孪生模块。 +- 扫描根是 `loopx/` 包。本 RFC 说的"全仓库"指 `loopx/` 下两个运行时的全部 + 载体，不是 git 树里的每个文件。清单的 `root` 与每条 `literal_scan.roots` + 都写 `loopx`，smoke 不读其他目录。 ### 非目标 - 改变任何运行时决策、载荷形状或线上格式。 +- 扫描 `apps/`（基线约 90 个 TypeScript 文件）或 `examples/`（十余处 smoke 里 + 的 `effective_action` 断言）。它们是消费者与测试替身，不是生产者；一个断言 + 了未注册值的 smoke 对 M0 不可见，在某个里程碑扩根之前接受这一点，扩根也会 + 抬高第 10 节的合并序成本。 - 手工策展每个闭集。清单映射全部闭集；只有跨模块或跨运行时边界并被分发的 词表才带 owner、值与关系进入策展层。 - 取代 `turn_transaction_contract.json` 或 @@ -230,6 +255,79 @@ todos、capabilities 与 TypeScript 运行时各自拥有同一想法的一种 禁止的替代权威：第二份注册表、复述已注册值的模块内列表，或宣称对已注册词表 具有规范性的散文表格。 +**名字的作用域（计划在 M0.5，不在 M0）。** 碰撞规则按名字归组，因此分不清 +"一个分叉"与"四个恰好复用同一标识符的有界上下文"。`SOURCE_SURFACES` 是第一 +个案例：它在 `global_risks.py`、`global_todos.py`、`summary_all.py`、 +`pr_review.py` 的四处定义各自列出那一个 CLI 命令的数据来源，值集本来就该不 +同。它今天被计入 `multi_value_forks`，且不得用改名来"修"，因为改名只让数字 +下降、不改变代码含义。M0.5 给注册表加 `scope` 字段，至少含 `global` 与 +`bounded_context`，允许一个有界上下文名字连同其所属上下文声明一次，并把已 +声明的名字从分叉预算移出（I14、下方 schema 表与第 11 节的 M0.5 行）。在此之 +前分叉预算是一个包含这一处已知误分类的上 +限，记在注册表 `inventory_ratchets` 的备注里。 + +### 词表的角色 + +提及一个值的模块不是它的 owner，一个词表也不止一种参与者。消费者是读取或接受 +值的上位角色，解释者和透传者是它的两个受跟踪子角色。注册表区分这些角色，因为 +对每种角色有意义的检查不同： + +| 角色 | 做什么 | 是否登记 | 检查 | +| --- | --- | --- | --- | +| Owner | 以每个运行时一个 `module::Symbol` 定义闭集 | 是，自 M0 | I1 到 I3 | +| 生产者 | 把值写入字段：赋值、dict 或对象字面量、构造函数关键字、在已登记判定函数内 `return` 字面量、访问 owner 枚举成员 | `kernel` 词表必须，自 M0.5 | I12、I13 | +| 消费者 | 读取或接受词表值；解释者和透传者都属于这个上位角色 | 通常不登记；只报告关系，不做策展 | F3 | +| 解释者 | 消费者的一种，据值分支或映射：`if`、`match`、`switch`、成员测试 | 否；由分发扫描发现，`--report` 排序 | I2、F3 | +| 透传者 | 消费者的一种，序列化、持久化、转发或展示值而不改变其含义 | 否 | F3；涉及持久化时还需 F6 证据 | + +由此得到两条规则。没有生产者的值是死值或兼容值：`skip` 在 `todos/user_gate.py` +被比较却无处写入，M0 放过它，M0.5 让它失败，直到被删除或列入 +`compatibility_only`。生产比比较更严：M0.5 单独扫描生产形式，对未注册的被生产 +值失败（I13），M0 的字面量扫描继续捕获未注册的比较（I2）。解释者与透传者刻意 +不登记；否则每次消费者改动都要碰注册表，正是第 6 节对消费者计数所拒绝的搅动。 +它们与词表的关系是 `--report` 的建议性输出。 + +生产形式在 M0.5 固定在 smoke 里，与分发形式同理：Python 的 `x["f"] = "v"`、 +envelope 或 packet 类型构造函数的关键字 `f="v"`、注册表列为生产者的函数内的 +`return "v"`、对 owner 枚举的成员访问；TypeScript 对象字面量里的 `f: "v"`、 +`x.f = "v"` 与条件表达式。`variable_sourced_values` 保留给生产者从扫描无法跟随 +的变量构造的值。哪些词表必须列生产者：`kernel` 自 M0.5；`cross_runtime` 只在 +M0.5 之后新增或删除值时；`cross_module` 只在晋升后（Q8）。持久化是生产扫描能回 +答的属性：若某个已列生产者符号是 journal 或 receipt 的写方，该词表标为 +`persisted`，这正是 Q2 与 Q10 等待的事实。 + +### 形式模型与证明边界 + +注册表是更大程序语义的有限规格。令 `V` 为已注册词表集合，`Val(v)` 为词表 +`v` 允许的值集合，`S` 为源码位点集合。模型记录的是关系，而不只是名称： + +```text +D ⊆ S × V 定义词表 +P ⊆ S × V × Val(v) 生产值 +C ⊆ S × V × Val(v) 消费或据值分支 +I ⊆ S × V × V 将一个词表解释为另一个词表 +T ⊆ S × V 不改变含义地透传 +G ⊆ V × V × (Val ⇀ Val ∪ {reject}) 做投影 +R ⊆ S × V × Version 将值持久化 +``` + +最低语义义务如下： + +1. **生产闭包：** `Produced(v) ⊆ Val(v)`。被识别的生产者不能写入注册集合之外的值。 +2. **规范值存活：** `Canonical(v) ⊆ Produced(v) ∪ CompatibilityOnly(v)`。只被比较、 + 没有生产来源的值是死值或兼容值，不能是 canonical。 +3. **消费者定义域闭包：** `Accepted(c) ⊆ Val(v)`，除非消费者显式声明外部定义域或部分定义域。 +4. **作用域分离：** 只有声明作用域相交时，同名冲突才是语义冲突。拼写本身不能证明等价。 +5. **投影全性：** 每个源值都必须映射到目标值，或显式映射为 `reject`。 +6. **持久化兼容性：** 持久化词表改变时，必须保持所有读者可读，或声明带版本的迁移。 + +这些是不同的证明义务。M0 已建立 owner 集合相等、跨运行时 parity、声明的可执行投影 +和 inventory 新鲜度。固定字面量形式与闭集载体只提供有界证据，不是全程序证明。M0.5 +增加有界的生产者和作用域检查。动态代码中的完整生产者发现、`same_concept` 的行为等价、 +以及持久化读者兼容性，在建模源码到结果的边之前仍然是未证明状态。注册表通过 +`formal_model` 保存这条证明边界；标记为 `unproved` 的性质是显式局限，不能被当作默认通过。 + + ### 状态模型与 schema `loopx/semantics/vocabulary_v0.json`，`schema_version` 为 @@ -243,6 +341,11 @@ todos、capabilities 与 TypeScript 运行时各自拥有同一想法的一种 | `vocabularies..tier`、`status` | `kernel`、`cross_runtime`、`cross_module`；`canonical`、`legacy`、`merge_candidate` | 封闭枚举 | | `vocabularies..literal_scan` | `field`、根目录、后缀 | 固定分发形式捕获的每个字面量都已注册；每个注册值被捕获或来自变量（I2） | | `vocabularies..variable_sourced_values` | 值到生产者模块 | 生产者仍包含带引号的该值 | +| `vocabularies..scope`（M0.5） | `global` 或 `bounded_context`；`bounded_context` 条目列出 `contexts`，每个含一个 owner 符号 | 封闭枚举；已声明的有界上下文名字从 `multi_value_forks` 排除；未声明的多模块名字仍是分叉（I14） | +| `vocabularies..producers`（M0.5） | 写入该字段的 `path::Symbol` 位点，`kernel` 必填 | 每个位点只写注册值；未列入 `compatibility_only` 的每个值至少有一个位点或一条变量来源条目（I12、I13） | +| `vocabularies..compatibility_only`（M0.5） | 为让已持久化记录的读者仍能解析而保留的值 | `values` 的子集；零生产位点；每个值带 `value_notes` 理由与退休里程碑 | +| `formal_model` | 有限的集合、角色关系与层次、语义义务，以及已建立/有界/未证明的声明 | 漂移 smoke 校验精确 schema、角色层次和不变量 ID；属性实施阶段不能冒充已完成证明 | +| `formal_model.enforcement_policy` | 当前阻断、下一阶段阻断、建议性和未证明层级 | 每个形式不变量恰好出现一次，且层级与其实施阶段一致 | | `vocabularies..value_notes`、`deprecated_values` | 逐值评审备注；计划删除的值 | 名字必须是已注册值 | | `relations.same_concept` | `vocabulary.value` 成员组 | 每个成员可解析 | | `relations.shared_field_names` | 一个字段名、其槽位及各槽位承载的词表或值 | 每个槽位可解析 | @@ -338,6 +441,13 @@ PR 中重新生成清单。 | 度量覆盖两种载体形状并过滤局部命名 | `pytest tests/architecture/test_semantic_inventory.py` | 通过，含冲突与模块局部约定两组夹具 | 规则来自本 RFC 而非扫描输出 | | 两处 owner 修正不改变行为 | `pytest tests/test_loopx_turn_transaction.py tests/test_loop_turn_loop_controller.py tests/test_turn_loop_disposition.py tests/test_loopx_turn_managed_step.py tests/control_plane -k authority` 与 `loopx canary premerge --from-git-diff` | 通过 | 在干净树上可复现的 `main` 既有环境失败除外 | | 文档治理接受这对 RFC | `python3 examples/docs-governance-smoke.py` | 通过 | 检查镜像、链接、索引 | +| 退休预算按子串而非标识符计数 | 分别以 `in file.text` 与 `\bgoal_boundary\b` 统计 `goal_boundary` | 基线上 35 对 30 个 Python 模块 | 已知边界；M3 的零读者门需要标识符计数，见第 12 节 | +| 模块局部约定过滤器是一次代码修改 | 扩宽 `inventory.py` 的 `MODULE_LOCAL_CONVENTION` 并重新生成 | `*_semantic` 预算下降而别处无代码改动 | 已知边界；正则在代码里，扩宽是可评审的 diff，未过滤总数仍在预算内 || 无人生产的注册值失败（M0.5） | 在基线上运行生产形式扫描 | 失败并点名 `effective_action` 与 `skip`；删除 `skip` 或列入 `compatibility_only` 后通过 | 第一个预期的 I12 失败；只被比较的值不算已携带 | +| 生产未注册值失败（M0.5） | 在某个已列生产位点写 `effective_action: "brand_new"` | 即使无消费者比较它也失败，并点名位点与值 | I13；生产比比较更严 | +| 有界上下文名字只能靠声明离开分叉预算（M0.5） | 为 `SOURCE_SURFACES` 声明四个上下文；另行只改名其中一处定义而不声明 | 声明把 `multi_value_forks` 降到 3；单独改名不降 | I14；诚实的修法是评审者看得见的注册表修改，改名是不碰注册表的代码改动 | + +| 上游合并会让已提交清单过期 | 对 `upstream/main` 最近二十个合并提交，在第一父提交与合并结果之间重放扫描器 | 20 次合并中 8 次至少改变一个载体 | 提交快照的实测成本；处理规则见第 10 节与第 12 节 Q9 | +| 形式模型不能静默丢失证明义务 | 从 `formal_model` 删除不变量、角色、关系或证明边界分类 | 漂移 smoke 针对形式模型结构失败 | 该模型是有限契约和证明账本，本身不等于这些性质已经被证明 | 已知边界，写明是为了不让这个检查被过度信任： @@ -376,16 +486,92 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。 工作流被刻意设为非 PR 必需检查。舰队能发现的 smoke 不是提交时检查，除非某个 必需的 PR 作业收集它。 +**合并序风险。** `inventory_v0.json` 是整个 `loopx/` 树的已提交快照，树与快照 +不一致时 smoke 失败。两个各自新增载体、各自正确再生成清单的 PR，对着它们 +各自基于的 `main` 都是绿的；后合并的那个会让 `main` 的快照缺少先合并者的 +条目，`main` 上的扫描在有人再生成之前是红的。对 `upstream/main` 最近二十次 +合并的重放显示有八次至少改变一个载体，所以这是每周会发生的事，不是边角。 +本分支第一次同步上游就复现了它：合入的十二个提交新增一个枚举与三个闭集， +检查失败直到重新生成。处理规则是第 12 节 Q9；在其决定之前的规则是：在 +`main` 变红之后合并 PR 的人负责跟一个只改 `inventory_v0.json` 的再生成提交， +smoke 的失败文本会点名那条命令。 + +**解释器。** smoke、生成器与扫描器要求项目声明的 Python（`pyproject.toml` +中 `>=3.11`）；`zip(strict=True)` 在 3.9 上失败。舰队与 premerge 的命令按仓库 +约定写作 `python3`，在 CI 解释器下运行。macOS 系统 `python3` 是 3.9，本地 +premerge 需要 `PATH` 上有 3.11 环境；文档因此把直接命令写成 `python3.11`， +planner 条目则有意保留 `python3`。 + ## 11. 规范性交付计划 | 里程碑 | 交付行为 | 进入门 | 退出证据 | 回滚 | | --- | --- | --- | --- | --- | | M0 | 含 26 个词表与 9 条关系的注册表、带 `--check` 的生成清单、带固定分发形式与覆盖下限的漂移 smoke、删除两处 owner 分叉、RFC 索引条目 | 本 RFC 开启 | 第 9 节各行全绿；20 类突变失败关闭 | 删除 smoke、`loopx/semantics/`、生成器及其测试 | -| M1 | 单一 owner 模块中的 `EffectiveAction` 类型化枚举；replay observation 与 frontier 槽位拆出（Q6）；生产者与消费者 import 它；注册表 `literal_scan` 收紧到枚举 | M0 合入；owner 模块已定（Q3）；槽位拆分已决（Q6） | smoke 绿；owner 之外零裸 `effective_action` 字面量；status/should-run 的 parity fixture 不变 | 回退为字面量；注册表保留集合 | +| M0.5 | 含 `global` 与 `bounded_context` 及每上下文 owner 的 `scope`；`kernel` 词表上的 `producers` 与 `compatibility_only`；带两条角色检查（I12、I13）的生产形式扫描；退休预算改按标识符计数并在一个 diff 里调低全部六个锚点（Q11）；Q9 的合并序规则写入第 10 节 | M0 合入；Q9 已决或其临时规则被接受 | smoke 在 I11 到 I14 强制下全绿；`skip` 已处理；`multi_value_forks` 靠声明降到 3；第 9 节角色行全绿；为 Q2 回答 `turn_route` 是否持久化 | 删除三个字段与角色检查；预算回到 M0 锚点 | +| M1 | 单一 owner 模块中的 `EffectiveAction` 类型化枚举；replay observation 与 frontier 槽位拆出（Q6）；生产者与消费者 import 它；注册表 `literal_scan` 收紧到枚举 | M0.5 合入；owner 模块已定（Q3）；槽位拆分已决（Q6） | smoke 绿；owner 之外零裸 `effective_action` 字面量；status/should-run 的 parity fixture 不变 | 回退为字面量；注册表保留集合 | | M2 | route 到 disposition 的投影、`decide_loop_disposition` 决策表与跨运行时集合通过共享契约发布，生成 Python 与 TypeScript 绑定，效仿协调契约生成器 | M1 合入；Q2 与 Q7 已决 | 生成器 `--check` 与 smoke 绿；`settlement.ts` 与 `transaction.py` 读取生成集合 | 从上一版契约重新生成 | | M3 | 逐字段退休旧 should-run 字段，每个 PR 一个字段，预算降到零并删除字段 | 经生产者/读者调研证明该字段外部读者为零 | 按 `AGENTS.md` 的 schema 缩减记录；附录 B 条目 | 从最后一个写方恢复字段 | | M4 | 随迁移 RFC 的每次 replacement-first 切换调低孪生预算 | 每个切换 PR | 同 diff 中的预算修改 | 无需；预算跟随代码 | +没有目标的棘轮只是方向，不是计划。下表是本 RFC 完成时的状态；每一行都是一个 +注册表预算或 smoke 可检查的词表属性。标为*未决*的行等待第 12 节的决策，这也 +是计划在那些决策记录之前只是骨架的原因。 + +| 表面 | 基线（`1dc6ad8d8`） | 本 RFC 关闭时的目标 | 由谁达成 | +| --- | --- | --- | --- | +| `effective_action` 取值 | 33 个字面量，无 owner 符号 | 一个枚举 owner；`skip`、`observe_replay`、`block_replay` 与两个 `quota_action_selection_*` 码从判定槽位移出；约 28 值 | M1 | +| 同一 envelope 里的 `effective_action` 槽位 | 一个字段名下 3 套词表 | 1，或在 Q6 保留字段时为一个已注册并集 | M1（Q6） | +| Turn 词表 | 3 套、28 值、21 个不同值、7 个冗余拼法 | 保留 3 套；投影与决策表生成并校验；拼法不变，除非 Q10 决定合并 | M2（Q2、Q10 *未决*） | +| 同运行时分叉（语义） | 18 个名字 | 0 | 基线窄 PR | +| 冲突值（语义） | 2 个名字 | 0 | 基线窄 PR | +| 多值分叉 | 4（1 个误分类） | `scope` 声明有界上下文名字后为 0 | M0.5 + 基线窄 PR | +| 多值孪生 | 19 | 0 | 基线窄 PR | +| 旧 should-run 字段 | 6 个字段，124 py / 10 ts 模块提及 | 0 个字段 | M3，按标识符计数 | +| 合并候选组 | 32 组未评审 | 每组已分类；只合并 `same_semantics` 的组 | 分类表 PR，随后逐组 PR | +| 控制面 py/ts 孪生 | 43 | 跟随 TypeScript 迁移 RFC；本 RFC 不设目标 | M4 | + +### 两条执行轨道与强制层级 + +路线图把修复已有语义债务与完善度量工具分开。轨道 A 不等待设计决策：每个窄 PR +逐步删除真实分叉、冲突、孪生和旧读者。轨道 B 改善守卫能够知道的内容：作用域声明、 +有界生产者分析、标识符计数和合并序处理。轨道 A 降低债务数量，轨道 B 让这个度量更 +接近真实语义。M1 及之后的阶段依赖轨道 B，因为当前度量已知并不完备。 + +```text +轨道 A：修复现有债务 ──────────────────────────────────────┐ + ├─> M1 类型化槽位 +轨道 B：作用域 + 生产者模型 + 度量边界 ─────────────────────┘ │ + ├─> M2 生成式投影 + ├─> M3 旧字段退休 + └─> M4 运行时孪生迁移 +``` + +形式模型使用四个强制层级，避免困难性质意外变成合并阻断： + +| 层级 | 性质 | 当前含义 | +| --- | --- | --- | +| `blocking_now` | F5 投影全性 | 当前 M0 smoke 已强制 | +| `blocking_next` | F1 生产闭包、F2 规范值存活、F4 作用域分离 | M0.5 后计划强制；M0 不宣称已经做到 | +| `advisory` | F3 消费者定义域闭包 | 只报告证据，不阻断普通消费者改动 | +| `unproved` | F6 持久化/版本兼容性 | 明确的证明缺口，不能报告为已通过 | + +阶段完成条件是验收表中的证据，而不是出现一个公式或注册表条目。有界的源码到结果 +分析存在之后，性质才可从 `unproved` 移到 `advisory`；只有记录误报/漏报边界并用突变 +测试覆盖已识别形式后，才可移到阻断层。这样既严格防止静默破坏，也允许不完整的分析 +为无关改动提供信息而不阻断它们。 + +阶段顺序如下： + +1. **M0：** 保留当前结构守卫，并明确其证明边界。 +2. **M0.5：** 为四个 Turn 内核词表实现 `scope`、生产形式和按标识符计算的退休预算。 +3. **M1：** 在 Q3、Q6 决定后拆开过载的 `effective_action` 槽位，并引入一个类型化 owner。 +4. **M2：** 通过生成的跨运行时契约发布完整决策表和两跳投影。 +5. **M3/M4：** 只有在读者与迁移证据完整后，才退休旧字段并减少 Python/TypeScript 孪生。 + +这份路线图对依赖和退出证据具有规范效力。Issue #4447 可以承载 owner、建议日期和 +运维清单，但不能另立一套目标状态。 + + ## 12. 未决决策 1. **注册表位置。** Owner：内核维护者。M0 实现于 `loopx/semantics/`，因为范围是 @@ -396,7 +582,11 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。 投影覆盖全部输入但非单射（`blocked` 与 `wait` 都映到 `wait`），而 `stop`、 `terminal`、`contract_error` 只在一侧存在。`same_concept` 关系记录了四个共享 裁决。建议：两者都保留，M2 发布投影，待 managed-step 消费者成熟后再议。 - M2 前需定。 + M2 前需定。保留两者的理由是合并会触及已持久化的 Turn 记录；这个前提尚未 + 核实。决定之前应先用 M0.5 的生产形式扫描（I12，第 5 节）确认 `turn_route` + 是否曾写入 journal 或 + receipt，还是只在进程内流转；若是后者，合并的代价远低于本 RFC 的假设， + 适用 Q10。 3. **`EffectiveAction` 的 owner 模块。** 注册表今天不声明 owner，因为不存在任何 符号；字面量扫描是唯一检查。选项：`quota/should_run_packet.py`（最大生产者）、 新建 `quota/effective_action.py`，或按迁移 RFC 以 TypeScript `turn_envelope.ts` @@ -419,6 +609,22 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。 8. **从清单到注册表的晋升规则。** 外部消费者模块不少于三个或存在跨运行时孪生 的已映射载体是否必须策展。建议：现在作为评审规则采用，待清单积累一个季度 历史后再由 smoke 强制。Owner：内核维护者。 +9. **跨合并的清单新鲜度。** 两个新增载体的 PR 先后合并时，已提交快照会过期 + （第 10 节；上游最近二十次合并中八次）。选项：(a) 分支保护要求 PR 与 + `main` 同步，根除风险但拖慢所有 PR；(b) 合并者负责一个只再生成的后续提交， + 快照留在 git 历史里，接受 `main` 红几分钟；(c) 清单不入库，CI 只对 PR diff + 生成，失去对载体的 `git blame`。建议：现在用 (b)，若 `main` 变红超过每周 + 一次则改 (a)。Owner：仓库维护者。这是运维决策不是代码改动；应放在跟踪 + issue 的决策清单里，而不是任务清单里。 +10. **Turn 词表的终态。** 第 11 节的目标表默认保留三套与七个冗余拼法，因为 + Q2 建议保留两者。若 Q2 的 M0.5 生产形式扫描表明 `turn_route` 未被持久化，维护者 + 应在 (a) 三套加生成投影（现行计划）与 (b) 两阶段合并（先双写、后退休）到 + 每个概念一种拼法之间选择。没有这个决定，RFC 对其标题问题只有预算、没有 + 完成定义。Owner：Turn driver owner。M2 关闭前需定。 +11. **退休预算按标识符计数。** 六个旧字段预算用 `field in file.text` 统计； + `goal_boundary` 会匹配 `goal_boundary_repair`。M3 的零外部读者门需要词边界 + 计数，这会在一个 diff 里调低全部六个锚点。建议：在第一个 M3 PR 之前做。 + Owner：内核维护者。 ## 附录 A：执行账本（非规范） @@ -502,6 +708,42 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。 - **对规范设计的影响：** I5 改述为相等并说明偏离先例的理由；新增 I10；第 9 节 增三行；第 10 节从一句话改写为表面表格。 +### 2026-09-15 — 第四次评审 M0：范围、合并序、终态 + +- **基线：** 已合入 `503991dd2`；`upstream/main` 在 `2f84af990`，领先分支十二 + 个提交。 +- **触发：** 第四次评审问守卫的输入依赖什么、"全仓库"覆盖什么。把十二个上游 + 提交合入临时树后清单过期（一个枚举、三个闭集）；对上游最近二十次合并重放 + 扫描器，八次会有同样结果。RFC 写全仓库，而清单根与每条字面量扫描都写 + `loopx/`；`examples/` 有十余处 `effective_action` 断言，`apps/` 约九十个 + TypeScript 文件，smoke 从不读取。 +- **同时发现：** `SOURCE_SURFACES` 是四个 CLI 命令各列自己的数据来源，不是分 + 叉；按名归组的规则无法表达这一点。退休预算按子串计数（`goal_boundary` 35 + 对 30 个标识符模块）。计划有预算但没有终态，四个入口决策没有 owner 期限。 +- **交付：** 第 3 节把扫描根固定为 `loopx/` 并把 `apps/` 与 `examples/` 列为 + 非目标；第 5 节预告 M0.5 的 `scope` 字段并以 `SOURCE_SURFACES` 为首例；第 9 + 节增三行已知边界；第 10 节增合并序风险与解释器两段；第 11 节增终态表；第 + 12 节增 Q9 到 Q11 并给 Q2 加核实说明；注册表 `inventory_ratchets` 增一条关于 + 误分类分叉的备注。代码与预算未变。 +- **有意不做：** premerge planner 保留 `python3`，因为舰队所有命令都这样拼写， + runner smoke 也断言了这段文本；改为记录解释器要求。 +- **证据：** 附录 C 的 E17 到 E20。 +- **对规范设计的影响：** 第 3 节范围收窄以匹配代码；第 11 节有了完成定义；第 + 12 节增三条决策。 + +### 2026-09-15 — 角色与作用域模型写入契约 + +- **触发：** RFC 使用"生产者"与"消费者"十九次却从未定义，Q2 与 Q10 依赖一个 + 文中从未说明的"生产者检查"，`scope` 只存在于一段预告，且第 1 节在第 10 节 + 把 pytest 扫描定为义务之后仍写 smoke "在每次 premerge 与 full-public 运行"。 +- **交付：** 第 5 节新增"词表的角色"（owner、生产者、解释者、透传者）与三行 + schema（`scope`、`producers`、`compatibility_only`）；第 2 节新增 I11 到 I14， + 每条标注自 M0.5 起强制；第 9 节新增三行 M0.5 验证；第 11 节新增 M0.5 里程碑， + M1 改为以它为门；Q2 与 Q10 指向 I12 而非未定义的检查；第 1 节与第 10 节一致。 + 代码、注册表值与预算未变；M0 的 smoke 尚未强制 I11 到 I14。 +- **对规范设计的影响：** 新增四条带明确强制里程碑的不变量；计划有了"被生产" + 的定义，M3 的零读者门与 Q2 的持久化问题都能使用它。 + ## 附录 B：决策日志 | 日期 | 决策 | Owner / 批准 | 备选 | 变更的规范章节 | @@ -527,6 +769,10 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。 | E14 | smoke 不在 PR 路径上 | `1dc6ad8d8` + M0 | `loopx canary premerge --changed-file loopx/control_plane/turn_driver/loop_controller.py --changed-file loopx/control_plane/quota/turn_envelope.ts`；`.github/workflows/full-public-smokes.yml` 的触发条件 | 规划 32 条命令，smoke 缺席；舰队只在 push 到 `main` 与日程运行 | 按路径 token 选择；CI 接线读自工作流文件 | | E15 | 已收紧的预算可以漂回锚点 | `1dc6ad8d8` + M0 | smoke 中的 `ratchets[key] <= BUDGET_ANCHOR[key]` 与 `floor[key] >= anchored` | 收紧后的预算与锚点之间的任何值都能通过 | 代码阅读；先例用同样的比较 | | E16 | 相等性关闭停滞，包装进入扫描 | `1dc6ad8d8` + M0 | 只调低一个 `inventory_ratchets` 条目而不动锚点，然后在干净树上跑 `pytest tests/architecture/test_semantic_vocabulary_drift.py` | 突变失败并同时命名两个值；包装约 3 秒通过 | 本地练习加已提交测试 | +| E17 | 上游合并会让已提交清单过期 | `upstream/main` `2f84af990`，最近 20 个 first-parent 合并 | 对每个改动的 `loopx/**/*.{py,ts}` 在第一父提交与合并结果之间比较扫描器事实 | 20 次合并中 8 次至少改变一个载体；本分支自己的上游同步新增 1 个枚举与 3 个闭集 | 事实级比较，等价于完整再生成 | +| E18 | 声明范围超出扫描根 | `503991dd2` + M0 | 从注册表读 `literal_scan.roots` 与清单 `root`；在 `examples/` 下 `grep` `effective_action` 分发字面量；统计 `apps/` 下 `.ts`/`.tsx` | 根只有 `loopx`；`examples/` 12+ 处断言；`apps/` 90 个文件 | 消费者与测试替身，非生产者 | +| E19 | `SOURCE_SURFACES` 是四个有界上下文，不是分叉 | `503991dd2` | 从清单读出四个 `multi_value_forks` 定义 | 每个模块列出自己 CLI 命令的数据来源，值互不相交 | 读值后的判断；规则本身做不出 | +| E20 | 退休预算按子串高估 | `503991dd2` | 对 `loopx/**/*.py` 分别用 `'goal_boundary' in text` 与 `\bgoal_boundary\b` | 35 对 30 个模块 | 标识符计数才是 M3 门的度量 | | E13 | 冲突预算主要在度量局部命名 | `1dc6ad8d8` | 对 `conflicting_values` 与 `same_runtime_forks` 名字应用 `MODULE_LOCAL_CONVENTION` | 18 个冲突中 16 个、25 个分叉中 7 个是模块局部约定；语义子集分别为 2 与 18 | 分类是名字模式，已在扫描器中说明并由夹具测试钉住 | ## 附录 D：被否决或取代的方案 @@ -555,3 +801,15 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。 挪锚点。用相等性比较，两个值就分不开。 - 同一个字段名可以在一个 envelope 里承载多套词表；看得见字段的扫描看不见 槽位。把槽位记为关系，让歧义成为已登记的事实，而不是注册表背书的意外。 +- 整棵树的已提交快照让守卫的输入依赖别人的合并。提交它之前先量一下树在它 + 之下变化的频率，并写下 `main` 变红时由谁再生成。 +- 按名归组的碰撞规则需要一种方式说"这些是共用一个名字的不同东西"。没有它， + 诚实的修法与不诚实的修法（改名）降低的是同一个数字，评审者分不出来。 +- 文档比代码更快地扩大范围时，两者必须朝更便宜的那个方向对齐，但必须一致。 + 扫描器没有实现的范围声明是一条假不变量。 +- 只降不升的预算描述的是方向。在第二个里程碑之前写出目标表，否则没人能说 + 工作何时完成。 +- 等待一个 RFC 从未定义的"检查"的决策，是披着审慎外衣的悬空引用。点名交付 + 该检查的不变量与里程碑，否则决策没有输入，永远关不掉。 +- 用了十九次角色词（生产者、消费者）不等于定义了它。在角色成为一张每行带检查 + 的表之前，"谁写入这个值"是每个评审者答案都不同的问题。 diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py index b5d3367778..d01dc46069 100755 --- a/examples/semantic-vocabulary-drift-smoke.py +++ b/examples/semantic-vocabulary-drift-smoke.py @@ -43,11 +43,30 @@ REGISTRY_KEYS = { "schema_version", "rfc", "inventory", "policy", "coverage_floor", "vocabularies", "relations", "projections", "schema_versions", "retirement_ledger", "dual_runtime_twins", "inventory_ratchets", + "formal_model", } VOCABULARY_KEYS = {"meaning", "tier", "status", "owners", "values"} VOCABULARY_OPTIONAL_KEYS = {"literal_scan", "variable_sourced_values", "value_notes", "deprecated_values"} TIERS = {"kernel", "cross_runtime", "cross_module"} STATUSES = {"canonical", "legacy", "merge_candidate"} +FORMAL_MODEL_KEYS = { + "schema_version", "universes", "roles", "role_hierarchy", "relations", "invariants", "proof_boundary", + "enforcement_policy", +} +FORMAL_MODEL_SCHEMA_VERSION = "loopx_semantic_formal_model_v0" +FORMAL_UNIVERSE_KEYS = {"vocabularies", "values", "sites", "scopes", "roles"} +FORMAL_ROLES = {"owner", "producer", "consumer", "interpreter", "pass_through"} +FORMAL_RELATIONS = {"defines", "produces", "consumes", "interprets", "passes_through", "projects", "persists"} +FORMAL_INVARIANTS = { + "F1_producer_closedness", + "F2_canonical_value_liveness", + "F3_consumer_domain_closedness", + "F4_scope_separation", + "F5_projection_totality", + "F6_persistence_version_compatibility", +} +FORMAL_ENFORCEMENT = {"m0", "m0_5", "m1", "advisory", "unproved"} +FORMAL_POLICY_KEYS = {"blocking_now", "blocking_next", "advisory", "unproved"} # Hard ceiling on the registry's own floors and budgets, kept in code rather than # in the registry so one single-diff edit to ``vocabulary_v0.json`` cannot relax @@ -137,6 +156,7 @@ def load_registry() -> dict[str, Any]: registry = json.loads(REGISTRY_PATH.read_text(encoding="utf-8")) require(set(registry) == REGISTRY_KEYS, f"registry keys must be exactly {sorted(REGISTRY_KEYS)}") require(registry["schema_version"] == REGISTRY_SCHEMA_VERSION, f"registry schema_version must be {REGISTRY_SCHEMA_VERSION}") + check_formal_model(registry["formal_model"]) require((REPO_ROOT / registry["rfc"]).is_file(), f"registry must point at an existing RFC: {registry['rfc']}") require((REPO_ROOT / registry["inventory"]).is_file(), f"registry must point at an existing inventory: {registry['inventory']}") for name, vocabulary in registry["vocabularies"].items(): @@ -170,6 +190,54 @@ def load_registry() -> dict[str, Any]: return registry +def check_formal_model(model: dict[str, Any]) -> None: + """Validate the formal vocabulary model's finite signature and proof ledger. + + This is deliberately a schema check, not a claim that the current scanner + proves every property. Each property carries an enforcement stage and the + proof boundary records what remains unproved. + """ + require(set(model) == FORMAL_MODEL_KEYS, f"formal_model keys must be exactly {sorted(FORMAL_MODEL_KEYS)}") + require(model["schema_version"] == FORMAL_MODEL_SCHEMA_VERSION, "formal_model schema_version drift") + require(set(model["universes"]) == FORMAL_UNIVERSE_KEYS, "formal_model universes must name the declared sets") + require(set(model["roles"]) == FORMAL_ROLES, "formal_model roles must include the consumer role and its subroles") + require(model["role_hierarchy"] == {"consumer": ["interpreter", "pass_through"]}, + "formal_model role_hierarchy must classify interpreter and pass_through as consumers") + require(set(model["relations"]) == FORMAL_RELATIONS, "formal_model relations must be the declared edge kinds") + invariants = model["invariants"] + require(isinstance(invariants, list) and {item.get("id") for item in invariants} == FORMAL_INVARIANTS, + "formal_model invariants must cover exactly F1-F6") + for item in invariants: + require(set(item) == {"id", "statement", "enforcement", "evidence"}, + f"formal invariant {item.get('id')} has an invalid shape") + require(item["enforcement"] in FORMAL_ENFORCEMENT, + f"formal invariant {item['id']} has unknown enforcement stage") + require(item["statement"].strip() and item["evidence"].strip(), + f"formal invariant {item['id']} needs a statement and evidence boundary") + policy = model["enforcement_policy"] + require(set(policy) == FORMAL_POLICY_KEYS, + "formal_model enforcement_policy must separate current, next, advisory, and unproved checks") + policy_ids = [item_id for ids in policy.values() for item_id in ids] + require(set(policy_ids) == FORMAL_INVARIANTS and len(policy_ids) == len(set(policy_ids)), + "formal_model enforcement_policy must partition all invariants exactly once") + stage_for_policy = { + "blocking_now": "m0", + "blocking_next": "m0_5", + "advisory": "advisory", + "unproved": "unproved", + } + stages = {item["id"]: item["enforcement"] for item in invariants} + for policy_name, ids in policy.items(): + require(all(stages[item_id] == stage_for_policy[policy_name] for item_id in ids), + f"formal_model policy lane {policy_name} disagrees with invariant enforcement stage") + boundary = model["proof_boundary"] + require(set(boundary) == {"established", "bounded", "unproved"}, + "formal_model proof_boundary must separate established, bounded, and unproved claims") + for key in boundary: + require(isinstance(boundary[key], list) and all(isinstance(value, str) and value.strip() for value in boundary[key]), + f"formal_model proof_boundary.{key} must contain non-empty claim names") + + def check_coverage_floor(registry: dict[str, Any]) -> str: for vocabulary in registry["vocabularies"].values(): if scan := vocabulary.get("literal_scan"): diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json index f571a16438..17558ccd1d 100644 --- a/loopx/semantics/vocabulary_v0.json +++ b/loopx/semantics/vocabulary_v0.json @@ -11,6 +11,98 @@ "value_shape": "Registered values are lower snake_case tokens (^[a-z][a-z0-9_]*$). The literal scan captures any quoted string so a malformed or versioned spelling is reported, not skipped.", "literal_scan_forms": "The dispatch forms the scan recognises are fixed in the smoke, not in this file: comparison or assignment against a literal (== != === !== : = is), a JS/TS ternary, membership in an inline collection, and a Python conditional expression." }, + "formal_model": { + "schema_version": "loopx_semantic_formal_model_v0", + "universes": { + "vocabularies": "V: registered vocabulary identifiers", + "values": "Val(v): values admitted by vocabulary v", + "sites": "S: source locations that define, produce, consume, interpret, pass through, project, or persist values", + "scopes": "Scope: global or bounded_context(context_id)", + "roles": "Roles assigned to sites; a site may have more than one role only when each edge is explicit" + }, + "roles": [ + "owner", + "producer", + "consumer", + "interpreter", + "pass_through" + ], + "role_hierarchy": { + "consumer": ["interpreter", "pass_through"] + }, + "enforcement_policy": { + "blocking_now": ["F5_projection_totality"], + "blocking_next": ["F1_producer_closedness", "F2_canonical_value_liveness", "F4_scope_separation"], + "advisory": ["F3_consumer_domain_closedness"], + "unproved": ["F6_persistence_version_compatibility"] + }, + "relations": { + "defines": "D ⊆ S × V: a site defines a vocabulary carrier", + "produces": "P ⊆ S × V × Val: a site writes or returns a vocabulary value", + "consumes": "C ⊆ S × V × Val: a site accepts or branches on a value", + "interprets": "I ⊆ S × V × V: a site maps one vocabulary into another", + "passes_through": "T ⊆ S × V: a site serializes, persists, forwards, or displays without changing meaning", + "projects": "G ⊆ V × V × (Val ⇀ Val ∪ {reject}): a declared partial or total projection", + "persists": "R ⊆ S × V × Version: a site writes a value to a durable representation" + }, + "invariants": [ + { + "id": "F1_producer_closedness", + "statement": "Produced(v) ⊆ Val(v)", + "enforcement": "m0_5", + "evidence": "bounded production-form AST scan; unknown dynamic producers are reported, not treated as proven safe" + }, + { + "id": "F2_canonical_value_liveness", + "statement": "Canonical(v) ⊆ Produced(v) ∪ CompatibilityOnly(v)", + "enforcement": "m0_5", + "evidence": "every kernel value has a recognised producer or an explicit compatibility-only reason" + }, + { + "id": "F3_consumer_domain_closedness", + "statement": "Accepted(c) ⊆ Val(v), unless the consumer declares an external or partial domain", + "enforcement": "advisory", + "evidence": "consumer and interpreter edges are currently inventory evidence, not complete data-flow proof" + }, + { + "id": "F4_scope_separation", + "statement": "A name collision is a semantic conflict only when its declared scopes overlap", + "enforcement": "m0_5", + "evidence": "scope declarations and per-context owners; scope is never inferred from spelling" + }, + { + "id": "F5_projection_totality", + "statement": "For every source value, a projection maps to a target value or explicit reject", + "enforcement": "m0", + "evidence": "registry mapping is compared with the executable owner function" + }, + { + "id": "F6_persistence_version_compatibility", + "statement": "A persisted vocabulary change preserves readers or declares a versioned migration", + "enforcement": "unproved", + "evidence": "requires producer, serializer, storage, reader, and migration edges not yet modeled" + } + ], + "proof_boundary": { + "established": [ + "owner_carrier_set_equality", + "cross_runtime_owner_parity", + "declared_projection_mapping", + "inventory_snapshot_freshness" + ], + "bounded": [ + "fixed_literal_forms", + "fixed_closed_set_carriers", + "declared_budget_monotonicity" + ], + "unproved": [ + "all_runtime_trace_values_are_registered", + "all_producers_are_found", + "same_concept_behavioral_equivalence", + "persistence_reader_compatibility" + ] + } + }, "coverage_floor": { "vocabularies": 26, "owner_symbols": 46, @@ -665,6 +757,7 @@ "same_runtime_forks_semantic": 18, "conflicting_values_semantic": 2, "multi_value_meaning": "Enums, named closed sets, Literal aliases, and TypeScript as-const arrays are vocabulary exactly as a NAME = \"value\" constant is, so they get the same collision rule. One name defined in two modules with identical values is a twin; with different values it is a fork.", + "multi_value_forks_note": "The 4 counted forks include SOURCE_SURFACES, whose four definitions are four CLI commands each listing its own data sources; that is bounded-context reuse of one name, not drift. It stays in the budget until M0.5 adds a scope field (RFC Section 5) and must not be removed by renaming.", "semantic_meaning": "same_runtime_forks_semantic and conflicting_values_semantic exclude module-local convention names such as SCHEMA_VERSION, COMMAND, or *_LABEL, which every module legitimately names for itself. The remaining names are shared vocabulary, where a duplicate is real drift rather than local naming; the unfiltered totals stay visible in the generated inventory summary." } }