diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md index 8982c8a18c..581a73af80 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md @@ -4,7 +4,7 @@ - **Delivery maturity:** Partial (M0 registry, computed inventory, and drift smoke ship with this RFC) - **Authors / owners:** LoopX contributors; control-plane kernel maintainers own approval - **Created:** 2026-09-15 -- **Last normative revision:** 2026-09-16 +- **Last normative revision:** 2026-09-17 - **Implementation baseline:** `1dc6ad8d8` - **Related contracts:** `loopx/semantics/vocabulary_v0.json`, `loopx/semantics/inventory.py`, @@ -524,22 +524,57 @@ G ⊆ V × V × (S(v_source) ⇀ S(v_target) ∪ {reject}) projects R ⊆ L × V × Version persists a value durably ``` -The minimum semantic obligations are: - -1. **Producer closedness:** `Produced(v) ⊆ S(v) ⊆ U(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. +Each obligation is stated over the domain it is actually checked on, not over +`V`. `Kernel(V) ⊆ V` is the `tier: kernel` subset, the only tier that declares +producers; `Produced_scan(v)` is the production the fixed forms observe inside +the code-owned scan reach; `ScopeDeclarations` are the forked names the registry +declares as bounded contexts. + +1. **Producer closedness (kernel tier):** `∀v ∈ Kernel(V): Produced_scan(v) ⊆ + S(v) ⊆ U(v)`. A recognised producer cannot write a value outside the + registered set. Production outside the scan reach, and the whole + `cross_runtime` tier, is unverified rather than proven closed. +2. **Canonical liveness (kernel tier):** `∀v ∈ Kernel(V): Canonical(v) ⊆ + Produced_scan(v) ∪ CompatibilityOnly(v)`. A value that is only compared is + dead or compatibility-only, never canonical. The `cross_runtime` tier + declares no producers, so liveness there is unverified. 3. **Consumer domain closedness:** `Accepted(c) ⊆ S(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. +4. **Scope enumeration completeness:** `∀n ∈ ScopeDeclarations`, the declared + context owner modules are exactly the modules defining `n`, one context per + module, and every context owner symbol is `n`. Scope is declared and never + inferred, so "a collision is a conflict only when the declared scopes + overlap" is the *definition* of a semantic conflict and cannot be violated; + the checkable obligation is that a declaration enumerates every defining + module. Spelling alone still 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. +Each obligation records the set it quantifies over in +`formal_model.invariants[].domain`, and the smoke derives both sizes from the +registry rather than trusting the declared numbers: + +| Obligation | Quantifies over | Verified / registered | Evidence bound | +| --- | --- | --- | --- | +| F1, F2 | `vocabularies[tier=kernel].producers` | 6 / 26 | producer scan reach | +| F3 | `vocabularies[*]` | 0 / 26 | inventory only | +| F4 | `scope_declarations[*].contexts` | 4 / 4 | declared defining modules | +| F5 | `projections[*]` | 1 / 1 | executable owner function | +| F6 | `persists_edges[*]` | 0 / 0 | unmodelled | + +`verified` is the sub-domain the enforcement stage walks; `registered` is the +whole population of the same unit. An advisory or unproved stage walks nothing, +so its `verified` count must be zero, and an enforced stage may not declare an +empty domain. The selector and the evidence bound of each obligation are pinned +by `FORMAL_DOMAIN_ANCHOR` in the smoke on the `COVERAGE_ANCHOR` pattern (I5), so +an invariant cannot widen the set it claims through a registry edit alone. The +producer scan reach is measured on every run instead of pinned, because its +denominator moves with any new module; the smoke prints the current ratio, the +unresolved-site total, and the share of that total no wider scan could ever +resolve (E21). + These are different proof obligations. M0 establishes owner-set equality, cross-runtime parity, the declared executable projection, and inventory computed from the current tracked tree. Fixed literal forms and closed-set carriers provide bounded evidence, @@ -624,6 +659,7 @@ vocabulary key fails the smoke. | `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 source site or executable input witness (I12, I13) | | `vocabularies..compatibility_only` (M0.5) | values retained for persisted readers or a legacy typed caller interface | 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, candidate decisions, and established/bounded/unknown/unproved claims | Exact schema, role hierarchy, candidate decisions, and invariant ids are checked by the drift smoke; enforcement stages cannot be mistaken for completed proofs | +| `formal_model.invariants[].domain` | the set the obligation quantifies over: `quantifies_over` selector, `verified` and `registered` sizes, `evidence_bound` | Selector and bound are code-owned names pinned per invariant by `FORMAL_DOMAIN_ANCHOR`; both sizes are derived from the registry and must equal the declared ones; an advisory or unproved stage must declare `verified: 0`, an enforced stage a non-empty domain | | `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 | @@ -754,6 +790,8 @@ on the next full-tree scan; genuine shared-contract changes still need review. | A bounded-context name leaves only the semantic fork budget by declaration (M0.5a) | Declare `SOURCE_SURFACES` with its four contexts; separately, rename one definition without declaring | Raw `multi_value_forks` stays 4, `multi_value_forks_semantic` is 3; a rename alone changes neither semantic accounting nor declaration | I14; the honest fix is a registry edit a reviewer sees, the rename is not a repair | | Historical committed snapshots could become stale across merges | 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 | Historical cost motivating Q9; current checks compute the combined tree without a committed snapshot | | The formal model cannot silently lose a proof obligation | Remove an invariant, role, relation, candidate decision, 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 | +| An obligation cannot claim a domain nobody counts | `uv run --extra test python -m pytest tests/architecture/test_semantic_vocabulary_drift.py -k domain` | Dropping `domain`, inflating `verified` or `registered`, inventing a selector, claiming an unanchored selector or an out-of-stage evidence bound, and an advisory invariant claiming verified members each fail closed | The sizes are derived from the registry, so the check grounds the declared domain in registry data; it does not prove the obligation over that domain | +| F1/F2 quantify over exactly what the producer check walks | Same test module: compare `check_producers`' predicate with the declared F1/F2 domain | The vocabularies with `producers` are exactly the `kernel` tier, 6 of 26; the other 20 are all `cross_runtime` | The scan reach bounds the claim further and is reported, not pinned | Known limits, stated so the check is not over-trusted: @@ -1033,6 +1071,33 @@ introduce a competing target state. ## Appendix A: Execution ledger (non-normative) +### 2026-09-17 — Invariant statements bounded to their verified domains + +Normative; requires kernel-maintainer approval. No check changes its pass/fail +result on the current tree; what changes is what the invariants claim. + +- F1 and F2 were unconditional over `V` while `check_producers` skipped every + vocabulary without `producers` — 20 of 26, the entire `cross_runtime` tier. + Both are now stated over `Kernel(V)` and over `Produced_scan(v)`, the + production observed inside the code-owned scan reach, which is 432 of 1203 + tracked `loopx/**/*.{py,ts}` files. `validate_production`'s own docstring + already disclaimed whole-program closedness; the statements now agree with it. +- F4 was `conflict := collision ∧ scope_overlap`, a definition that cannot be + violated because scope is declared and never inferred. It is restated as the + enumeration-completeness property `check_scope_declarations` really enforces. +- Every obligation gains `domain` (`quantifies_over`, `verified`, `registered`, + `evidence_bound`). Both sizes are derived from the registry on each run, and + the selector/bound pair is pinned per invariant by `FORMAL_DOMAIN_ANCHOR`, so + an invariant cannot widen the set it claims through a data-only edit. +- The report prints the domain sizes, the scan reach, and how many unresolved + producer sites can never become evidence (15 of 41). +- The `continue` comment in `check_producers` said the skipped vocabularies were + "other kernel families". They are not kernel at all; the comment is corrected. +- Not addressed here: `check_formal_model` still accepts an internally + consistent false claim, because moving an invariant's `enforcement` and its + policy lane together stays self-consistent. That grounding gap is separate. + + ### 2026-09-16 — B2 pilot: one re-export hop bound in the Python producer scanner - **Trigger:** after M2 moved the three Turn owners into @@ -1215,6 +1280,7 @@ introduce a competing target state. | 2026-09-16 | Q9: compute the full inventory on demand; retire the committed census | Implementation for [maintainer feedback](https://github.com/huangruiteng/loopx/pull/4360#issuecomment-5692062394); PR review pending | Committed snapshot with post-merge regeneration; diff-only scan rejected | 1, I6, 3, 5, 9, 10, 12 | | 2026-09-16 | B2: bind one unrenamed re-export hop in the Python producer scanner | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2; PR review pending | Require every consumer to import the owner module (fragile; failed silently in M2); unbounded multi-hop resolution rejected | 5, Appendix A | | 2026-09-16 | B1 rename invariance: add the name-keyed divergence advisory; state the limit it does not close | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B1; PR review pending | Keying the budget on value sets (rejected: `CONFIDENCE_LEVELS` and `EDGE_CASE_COMPLEXITIES` share `high/low/medium` with different meanings); a committed name ledger (rejected at M0: Q9 retired the committed census). The advisory lists surviving forks by name; it was first described as catching a one-sided rename, which measurement disproved, so both mirrors state the limit as it behaves | 9 | +| 2026-09-17 | Bound F1/F2 to the kernel tier and the scan reach, restate F4 as scope enumeration completeness, and give every obligation a derived `domain` | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447); **kernel-maintainer approval required, not yet given** | Leave the unconditional statements and record the gap in prose only (rejected: the statement was stronger than `validate_production`'s own docstring); restate F4 as per-context value-set disjointness (rejected: refuted by the repo's own data, since `scope_declarations` exists to permit legitimate same-name reuse); widen the scan so the unconditional claim becomes true (rejected: a separate change with its own risk) | 5, 9, Appendix B, Appendix C | ## Appendix C: Evidence registry @@ -1239,6 +1305,9 @@ introduce a competing target state. | 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 | +| E21 | F1/F2 were unconditional but verified over one tier | `3ca868193` | `check_producers`' skip predicate, and the producer scan roots, read from the tree | 6 of 26 vocabularies declare `producers`, exactly the `tier: kernel` ones; the 20 skipped are all `cross_runtime`; the scan reaches 432 of 1203 tracked `loopx/**/*.{py,ts}` files (35.9%), the uncovered bulk being capabilities 285, other control-plane 192, extensions 83 | Counts from the registry and the tracked tree; the reach denominator moves with any new module, so it is reported, not pinned | +| E22 | Fifteen reported unresolved sites can never become evidence | `3ca868193` | smoke report `unresolved_producer_blockers` | 41 unresolved sites, of which `argument_name_only` 10 and `annotation_only` 5 are a field-named keyword argument and a bare declaration; the other 26 are dynamic or interprocedural | Label-keyed; the two labels are code-owned in the scanner, so the floor moves only by a code edit | +| E23 | F4 as written could not be violated | `3ca868193` | read `check_scope_declarations` against the F4 statement | Scope is declared and never inferred, so `conflict := collision ∧ scope_overlap` is a definition; what is enforced is that a declaration names every defining module exactly once, over 1 declaration and 4 contexts | Judgement from reading the check; value-set disjointness across contexts is deliberately *not* the property, because `SOURCE_SURFACES` legitimately reuses one name in four contexts (E19) | | 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 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 defcb781bd..abb3c455ec 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md @@ -4,7 +4,7 @@ - **Delivery maturity：** Partial（M0 的注册表、计算清单与漂移 smoke 随本 RFC 一起交付） - **Authors / owners：** LoopX 贡献者；控制面内核维护者拥有批准权 - **Created：** 2026-09-15 -- **Last normative revision：** 2026-09-16 +- **Last normative revision：** 2026-09-17 - **Implementation baseline：** `1dc6ad8d8` - **Related contracts：** `loopx/semantics/vocabulary_v0.json`、 `loopx/semantics/inventory.py`、 @@ -426,16 +426,45 @@ G ⊆ V × V × (S(v_source) ⇀ S(v_target) ∪ {reject}) 做投影 R ⊆ L × V × Version 将值持久化 ``` -最低语义义务如下： - -1. **生产闭包：** `Produced(v) ⊆ S(v) ⊆ U(v)`。被识别的生产者不能写入注册集合之外的值。 -2. **规范值存活：** `Canonical(v) ⊆ Produced(v) ∪ CompatibilityOnly(v)`。只被比较、 - 没有生产来源的值是死值或兼容值，不能是 canonical。 +每条义务都按它实际被检查的值域陈述，而不是泛指 `V`。`Kernel(V) ⊆ V` 是 +`tier: kernel` 子集，也是唯一声明了 producers 的层；`Produced_scan(v)` 是固定形式 +在代码所有的扫描范围内观察到的生产；`ScopeDeclarations` 是注册表声明为有界上下文 +的那些分叉名字。 + +1. **生产闭包（仅 kernel 层）：** `∀v ∈ Kernel(V): Produced_scan(v) ⊆ S(v) ⊆ U(v)`。 + 被识别的生产者不能写入注册集合之外的值。扫描范围之外的生产，以及整个 + `cross_runtime` 层，是未验证，而不是已证明闭合。 +2. **规范值存活（仅 kernel 层）：** `∀v ∈ Kernel(V): Canonical(v) ⊆ Produced_scan(v) ∪ + CompatibilityOnly(v)`。只被比较、没有生产来源的值是死值或兼容值，不能是 + canonical。`cross_runtime` 层不声明 producers，因此该层的存活性未被验证。 3. **消费者定义域闭包：** `Accepted(c) ⊆ S(v)`，除非消费者显式声明外部定义域或部分定义域。 -4. **作用域分离：** 只有声明作用域相交时，同名冲突才是语义冲突。拼写本身不能证明等价。 +4. **作用域枚举完备性：** `∀n ∈ ScopeDeclarations`，声明的上下文 owner 模块集合 + 恰好等于定义 `n` 的模块集合，每个模块一个上下文，且每个上下文的 owner 符号 + 都是 `n`。作用域是声明的、从不推断，所以“只有声明作用域相交时同名冲突才是 + 语义冲突”是语义冲突的*定义*，不可能被违反；可检查的义务是一份声明必须枚举 + 全部定义模块。拼写本身仍然不能证明等价。 5. **投影全性：** 每个源值都必须映射到目标值，或显式映射为 `reject`。 6. **持久化兼容性：** 持久化词表改变时，必须保持所有读者可读，或声明带版本的迁移。 +每条义务在 `formal_model.invariants[].domain` 中记录它量化的集合，smoke 从注册表 +推导两个规模数字，而不是相信声明值： + +| 义务 | 量化范围 | 已验证 / 已注册 | 证据边界 | +| --- | --- | --- | --- | +| F1、F2 | `vocabularies[tier=kernel].producers` | 6 / 26 | producer 扫描范围 | +| F3 | `vocabularies[*]` | 0 / 26 | 仅清单证据 | +| F4 | `scope_declarations[*].contexts` | 4 / 4 | 声明的定义模块 | +| F5 | `projections[*]` | 1 / 1 | 可执行 owner 函数 | +| F6 | `persists_edges[*]` | 0 / 0 | 未建模 | + +`verified` 是该实施阶段真正走到的子值域，`registered` 是同一单位的全体总数。 +建议性（advisory）与未证明（unproved）阶段什么都不走，因此 `verified` 必须为 0； +已强制阶段则不得声明空值域。每条义务的 selector 与证据边界由 smoke 里的 +`FORMAL_DOMAIN_ANCHOR` 按 `COVERAGE_ANCHOR` 同一模式钉住（I5），因此不可能只改数据 +就扒宽一条不变量所声称的范围。producer 扫描范围本身每次运行现算而不钉住， +因为分母会随任何新模块移动；smoke 会打印当前比值、未解析位点总数，以及其中 +再宽的扫描也永远无法解析的那一部分（E21）。 + 这些是不同的证明义务。M0 已建立 owner 集合相等、跨运行时 parity、声明的可执行投影 和基于当前已跟踪源码树计算的清单。固定字面量形式与闭集载体只提供有界证据，不是全程序证明。M0.5 增加有界的生产者和作用域检查。动态代码中的完整生产者发现、`same_concept` 的行为等价、 @@ -506,6 +535,7 @@ external_input | compatibility_only | unknown | `vocabularies..producers`（M0.5） | 写入该字段的 `path::Symbol` 位点，`kernel` 必填 | 每个位点只写注册值；未列入 `compatibility_only` 的每个值至少有一个源码生产位点或可执行输入见证（I12、I13） | | `vocabularies..compatibility_only`（M0.5） | 为持久化读者或旧类型化调用接口保留的值 | `values` 的子集；零生产位点；每个值带 `value_notes` 理由与退休里程碑 | | `formal_model` | 有限的集合、角色关系与层次、语义义务、候选决策，以及已建立/有界/unknown/未证明的声明 | 漂移 smoke 校验精确 schema、角色层次、候选决策和不变量 ID；属性实施阶段不能冒充已完成证明 | +| `formal_model.invariants[].domain` | 义务量化的集合：`quantifies_over` selector、`verified` 与 `registered` 规模、`evidence_bound` | selector 与证据边界都是代码所有的名字，并由 `FORMAL_DOMAIN_ANCHOR` 逐不变量钉住；两个规模都从注册表推导并必须与声明值相等；advisory 与 unproved 阶段必须声明 `verified: 0`，已强制阶段不得声明空值域 | | `formal_model.enforcement_policy` | 当前阻断、下一阶段阻断、建议性和未证明层级 | 每个形式不变量恰好出现一次，且层级与其实施阶段一致 | | `vocabularies..value_notes`、`deprecated_values` | 逐值评审备注；计划删除的值 | 名字必须是已注册值 | | `relations.same_concept` | `vocabulary.value` 成员组 | 每个成员可解析 | @@ -616,6 +646,8 @@ owner 符号集合的组：`EffectiveAction` 与 `EFFECTIVE_ACTIONS` 是同一 | 历史上的已提交清单会因上游合并而过期 | 对 `upstream/main` 最近二十个合并提交，在第一父提交与合并结果之间重放扫描器 | 20 次合并中 8 次至少改变一个载体 | Q9 的历史动机；当前检查直接计算合并后的全树，不再依赖提交快照 | | 形式模型不能静默丢失证明义务 | 从 `formal_model` 删除不变量、角色、候选决策、关系或证明边界分类 | 漂移 smoke 针对形式模型结构失败 | 该模型是有限契约和证明账本，本身不等于这些性质已经被证明 | +| 义务不能声称一个无人清点的值域 | `uv run --extra test python -m pytest tests/architecture/test_semantic_vocabulary_drift.py -k domain` | 删掉 `domain`、调大 `verified` 或 `registered`、自造 selector、使用未钉住的 selector 或跨阶段的证据边界、以及 advisory 不变量声称已验证成员，逐项失败关闭 | 规模从注册表推导，因此该检查把声明值域接地到注册表数据；它不证明该义务在那个值域上成立 | +| F1/F2 恰好量化 producer 检查真正走到的集合 | 同一测试模块：将 `check_producers` 的谓词与 F1/F2 声明的值域对比 | 声明了 `producers` 的词表恰好是 `kernel` 层，26 中的 6；其余 20 个全部是 `cross_runtime` | 扫描范围进一步约束该声明，它被上报而不被钉住 | 已知边界，写明是为了不让这个检查被过度信任： @@ -839,6 +871,32 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共 ## 附录 A：执行账本（非规范） +### 2026-09-17 — 不变量表述收敛到各自已验证的值域 + +规范性变更；需要内核维护者批准。当前源码树上没有任何检查的通过/失败结果改变， +改变的是这些不变量所声称的内容。 + +- F1 与 F2 原本在 `V` 上无条件成立，而 `check_producers` 会跳过每个没有 + `producers` 的词表——26 个中的 20 个，也就是整个 `cross_runtime` 层。现在两者 + 都改写在 `Kernel(V)` 上，并以 `Produced_scan(v)`（代码所有的扫描范围内观察到的 + 生产）为界，该范围是 1203 个已跟踪 `loopx/**/*.{py,ts}` 文件中的 432 个。 + `validate_production` 自己的 docstring 早已声明不主张全程序闭合性；现在表述与 + 它一致。 +- F4 原本是 `conflict := collision ∧ scope_overlap`，这是一条定义：作用域是声明 + 的、从不推断，因此它不可能被违反。现改写为 `check_scope_declarations` 真正强制 + 的枚举完备性性质。 +- 每条义务新增 `domain`（`quantifies_over`、`verified`、`registered`、 + `evidence_bound`）。两个规模都在每次运行时从注册表推导，selector 与证据边界这一 + 对则由 `FORMAL_DOMAIN_ANCHOR` 逐不变量钉住，因此不可能只改数据就扒宽一条不变量 + 所声称的集合。 +- 报告会打印各值域规模、扫描范围，以及 41 个未解析 producer 位点中永远不可能成为 + 证据的 15 个。 +- `check_producers` 里 `continue` 的注释原本说被跳过的是“其他 kernel 家族”。它们 + 根本不是 kernel；该注释已修正。 +- 本次未处理：`check_formal_model` 仍会接受一个自洽的错误声明，因为同时挪动某条 + 不变量的 `enforcement` 与它的 policy 层级仍然自洽。那个接地缺口是另一件事。 + + ### 2026-09-16 — B2 试点：Python producer 扫描器绑定一跳再导出 - **触发：** M2 把三个 Turn owner 迁入 `turn_contract_generated.py` 后，仍经 @@ -985,6 +1043,7 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共 | 2026-09-16 | Q9：全树按需计算；移除已提交结构清单 | 根据[维护者反馈](https://github.com/huangruiteng/loopx/pull/4360#issuecomment-5692062394)实现，PR 评审待完成 | 取代合并后补再生成；拒绝只扫描 diff | 1、I6、3、5、9、10、12 | | 2026-09-16 | B2：Python producer 扫描器绑定一跳未改名再导出 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B2；PR 评审待完成 | 要求每个消费者都从 owner 模块导入（脆弱；M2 中已静默失效）；拒绝无界多跳解析 | 5、附录 A | | 2026-09-16 | B1 改名不变性：新增按名字归组的分歧报告；写明它未闭合的边界 | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B1；PR 评审待完成 | 把预算改按值集归组（否决：`CONFIDENCE_LEVELS` 与 `EDGE_CASE_COMPLEXITIES` 共享 `high/low/medium` 而含义不同）；提交名字账本（M0 否决：Q9 已退役提交式清单）。该报告列出仍然存在的分叉；初稿称它能抓住单侧改名，实测证否，故两份镜像按真实行为写明边界 | 9 | +| 2026-09-17 | 将 F1/F2 限定在 kernel 层与扫描范围，把 F4 重述为作用域枚举完备性，并给每条义务加上可推导的 `domain` | 实现，Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447)；**需要内核维护者批准，尚未获得** | 保留无条件表述、只在正文记一笔缺口（否决：该表述比 `validate_production` 自己的 docstring 还强）；把 F4 重述为各上下文值集互斥（否决：会被仓库自身数据推翻，`scope_declarations` 恰恰就是为了允许合理的同名复用）；扒宽扫描让无条件声明成立（否决：那是自带风险的另一个变更） | 5、9、附录 B、附录 C | ## 附录 C：证据登记 @@ -1009,6 +1068,9 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共 | 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 门的度量 | +| E21 | F1/F2 写成无条件，但只在一个层上被验证 | `3ca868193` | 从源码树读 `check_producers` 的跳过谓词与 producer 扫描根目录 | 26 个词表中 6 个声明了 `producers`，恰好是 `tier: kernel` 那几个；被跳过的 20 个全部是 `cross_runtime`；扫描触及 1203 个已跟踪 `loopx/**/*.{py,ts}` 中的 432 个（35.9%），未覆盖部分主要是 capabilities 285、其余控制面 192、extensions 83 | 计数来自注册表与已跟踪源码树；分母会随任何新模块移动，所以只上报、不钉住 | +| E22 | 15 个被上报的未解析位点永远不可能成为证据 | `3ca868193` | smoke 报告的 `unresolved_producer_blockers` | 41 个未解析位点，其中 `argument_name_only` 10 个、`annotation_only` 5 个分别是以字段名命名的关键字参数和裸声明；其余 26 个是动态或跨过程的 | 按标签归组；这两个标签在扫描器里由代码持有，因此这个下界只能靠改代码移动 | +| E23 | F4 写法本身不可能被违反 | `3ca868193` | 对照 F4 表述阅读 `check_scope_declarations` | 作用域是声明的、从不推断，所以 `conflict := collision ∧ scope_overlap` 是一条定义；真正被强制的是一份声明必须恰好枚举每个定义模块，范围是 1 份声明、4 个上下文 | 阅读检查后的判断；各上下文值集互斥故意*不*作为该性质，因为 `SOURCE_SURFACES` 正是合理地在四个上下文复用同一个名字（E19） | | E13 | 冲突预算主要在度量局部命名 | `1dc6ad8d8` | 对 `conflicting_values` 与 `same_runtime_forks` 名字应用 `MODULE_LOCAL_CONVENTION` | 18 个冲突中 16 个、25 个分叉中 7 个是模块局部约定；语义子集分别为 2 与 18 | 分类是名字模式，已在扫描器中说明并由夹具测试钉住 | ## 附录 D：被否决或取代的方案 diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py index 058ab08b1c..ebb7382a7d 100755 --- a/examples/semantic-vocabulary-drift-smoke.py +++ b/examples/semantic-vocabulary-drift-smoke.py @@ -16,7 +16,7 @@ import re import sys from pathlib import Path -from typing import Any +from typing import Any, Callable REPO_ROOT = Path(__file__).resolve().parents[1] if str(REPO_ROOT) not in sys.path: @@ -36,6 +36,7 @@ from loopx.semantics.production import ( # noqa: E402 collect_production, validate_production, INPUT_WITNESSES, quota_action_domain, collect_literal_uses, + PRODUCER_FILES, PRODUCER_ROOTS, ) from loopx.semantics.python_production import scan_python_production # noqa: E402 from scripts.generate_semantic_bindings import build_artifacts # noqa: E402 @@ -84,6 +85,59 @@ "F6_persistence_version_compatibility", } FORMAL_ENFORCEMENT = {"m0", "m0_5", "m1", "advisory", "unproved"} +# Each formal invariant names the set it quantifies over. The selector is code +# owned, so registry data cannot invent a domain, and both counts are derived +# from the registry on every run rather than trusted: a declared size that no +# longer matches the tree fails in the same diff that changed the tree. +# ``verified`` is the sub-domain the invariant's enforcement stage actually +# walks; ``registered`` is the whole population of the same unit. An advisory or +# unproved stage walks nothing, so its ``verified`` count must be 0 -- that is +# what those stages mean, and it is checked here instead of asserted in prose. +FORMAL_DOMAIN_KEYS = {"quantifies_over", "verified", "registered", "evidence_bound"} +FORMAL_DOMAIN_SELECTORS: dict[str, Callable[[dict[str, Any]], tuple[int, int]]] = { + # ``check_producers`` walks exactly the vocabularies that declare producers. + # Today that predicate selects the kernel tier and nothing else, so F1/F2 + # quantify over 6 of 26 vocabularies, not over V. + "vocabularies[tier=kernel].producers": lambda registry: ( + sum(1 for entry in registry["vocabularies"].values() + if entry["tier"] == "kernel" and "producers" in entry), + len(registry["vocabularies"]), + ), + "vocabularies[*]": lambda registry: ( + len(registry["vocabularies"]), len(registry["vocabularies"]), + ), + "scope_declarations[*].contexts": lambda registry: ( + sum(len(entry["contexts"]) for entry in registry["scope_declarations"].values()), + sum(len(entry["contexts"]) for entry in registry["scope_declarations"].values()), + ), + "projections[*]": lambda registry: (len(registry["projections"]), len(registry["projections"])), + # No site declares a persists edge, so F6 has an empty domain, not a small one. + "persists_edges[*]": lambda registry: (0, 0), +} +FORMAL_ENFORCED_STAGES = frozenset(FORMAL_ENFORCEMENT - {"advisory", "unproved"}) +# What a verified sub-domain rests on, and which stages may claim it. The first +# three describe evidence something actually walked, so only an enforced stage +# can hold one; the last two say nothing is walked and belong to one stage each. +FORMAL_EVIDENCE_BOUNDS: dict[str, frozenset[str]] = { + "producer_scan_reach": FORMAL_ENFORCED_STAGES, + "declared_defining_modules": FORMAL_ENFORCED_STAGES, + "executable_owner_function": FORMAL_ENFORCED_STAGES, + "inventory_only": frozenset({"advisory"}), + "unmodelled": frozenset({"unproved"}), +} +# Which set each invariant is about, pinned in code for the same reason as +# COVERAGE_ANCHOR and BUDGET_ANCHOR: the registry value must equal the anchor, so +# an invariant cannot quietly widen its own claim by choosing a looser selector +# in a data-only edit. Restating an invariant over a different domain is a +# normative change and edits this literal in the same diff. +FORMAL_DOMAIN_ANCHOR = { + "F1_producer_closedness": ("vocabularies[tier=kernel].producers", "producer_scan_reach"), + "F2_canonical_value_liveness": ("vocabularies[tier=kernel].producers", "producer_scan_reach"), + "F3_consumer_domain_closedness": ("vocabularies[*]", "inventory_only"), + "F4_scope_separation": ("scope_declarations[*].contexts", "declared_defining_modules"), + "F5_projection_totality": ("projections[*]", "executable_owner_function"), + "F6_persistence_version_compatibility": ("persists_edges[*]", "unmodelled"), +} FORMAL_POLICY_KEYS = {"blocking_now", "blocking_next", "advisory", "unproved"} FORMAL_CANDIDATE_DECISIONS = { "reuse_existing", @@ -203,7 +257,6 @@ 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']}") for name, vocabulary in registry["vocabularies"].items(): require(VALUE_SHAPE.match(name) is not None, f"vocabulary name must be lower snake_case: {name}") @@ -259,15 +312,19 @@ def load_registry() -> dict[str, Any]: if scan is not None: require(set(scan) == {"field", "roots", "suffixes"}, f"{name}: literal_scan keys must be field, roots, suffixes") require(VALUE_SHAPE.match(scan["field"]) is not None, f"{name}: literal_scan.field must be an identifier") + # Last: the formal model derives its domain sizes from the sets checked above. + check_formal_model(registry["formal_model"], registry) return registry -def check_formal_model(model: dict[str, Any]) -> None: +def check_formal_model(model: dict[str, Any], registry: 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. + proves every property. Each property carries an enforcement stage, a declared + domain whose size is derived from ``registry`` rather than trusted, and the + proof boundary records what remains unproved. The registry is required, not + optional: a domain nobody counts is the defect this field exists to prevent. """ 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") @@ -279,13 +336,16 @@ def check_formal_model(model: dict[str, Any]) -> None: 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") + require(set(FORMAL_DOMAIN_ANCHOR) == FORMAL_INVARIANTS, + "FORMAL_DOMAIN_ANCHOR must pin a domain for every formal invariant") for item in invariants: - require(set(item) == {"id", "statement", "enforcement", "evidence"}, + require(set(item) == {"id", "statement", "enforcement", "evidence", "domain"}, 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") + check_invariant_domain(item, registry) policy = model["enforcement_policy"] require(set(policy) == FORMAL_POLICY_KEYS, "formal_model enforcement_policy must separate current, next, advisory, and unproved checks") @@ -318,6 +378,56 @@ def check_formal_model(model: dict[str, Any]) -> None: f"formal_model proof_boundary.{key} must contain non-empty claim names") +def check_invariant_domain(invariant: dict[str, Any], registry: dict[str, Any]) -> None: + """Require a declared invariant domain to match the set actually walked. + + An unconditional statement over a domain the checker never visits is the + defect this field exists to catch: the quantifier in ``statement`` has to be + bounded by the set counted here. Both counts are derived from the registry, + so widening the registry without widening the claim -- or the reverse -- is a + one-diff failure rather than silent rot. + """ + name = invariant["id"] + domain = invariant["domain"] + require(isinstance(domain, dict) and set(domain) == FORMAL_DOMAIN_KEYS, + f"formal invariant {name} domain keys must be exactly {sorted(FORMAL_DOMAIN_KEYS)}") + selector = domain["quantifies_over"] + require(selector in FORMAL_DOMAIN_SELECTORS, + f"formal invariant {name} quantifies over an unknown domain {selector!r}; " + f"selectors are code owned, not registry data: {sorted(FORMAL_DOMAIN_SELECTORS)}") + bound = domain["evidence_bound"] + require(bound in FORMAL_EVIDENCE_BOUNDS, + f"formal invariant {name} has an unknown evidence bound {bound!r}; " + f"bounds are code owned: {sorted(FORMAL_EVIDENCE_BOUNDS)}") + require((selector, bound) == FORMAL_DOMAIN_ANCHOR[name], + f"formal invariant {name} declares domain {(selector, bound)} but FORMAL_DOMAIN_ANCHOR " + f"pins {FORMAL_DOMAIN_ANCHOR[name]}; restating an invariant over another domain is a " + "normative change and moves the anchor in the same diff") + stage = invariant["enforcement"] + allowed = FORMAL_EVIDENCE_BOUNDS[bound] + require(stage in allowed, + f"formal invariant {name} claims evidence bound {bound}, which only " + f"{sorted(allowed)} may hold; its stage is {stage}") + require(all(type(domain[key]) is int and domain[key] >= 0 for key in ("verified", "registered")), + f"formal invariant {name} domain sizes must be non-negative integers") + walked, population = FORMAL_DOMAIN_SELECTORS[selector](registry) + require(domain["registered"] == population, + f"formal invariant {name} declares {domain['registered']} registered members of " + f"{selector}; the registry holds {population}") + if stage not in FORMAL_ENFORCED_STAGES: + require(domain["verified"] == 0, + f"formal invariant {name} is {stage} but claims {domain['verified']} verified " + f"members of {selector}; an unenforced stage walks nothing") + else: + require(domain["verified"] == walked, + f"formal invariant {name} claims {domain['verified']} verified members of " + f"{selector}; the {stage} check walks {walked}") + require(domain["verified"] > 0, + f"formal invariant {name} is enforced at {stage} over an empty domain") + require(domain["verified"] <= domain["registered"], + f"formal invariant {name} cannot verify more members than the registry holds") + + def check_coverage_floor(registry: dict[str, Any]) -> str: try: quota_action_domain(registry) @@ -463,6 +573,35 @@ def _producer_literals(field: str, source: SourceFile) -> set[str]: return set().union(*(row.values for row in rows)) +# The blocker labels ``summarise_blockers`` explains as unable to become evidence, +# named once so the report can count them instead of restating the rule. They are +# the floor under the unresolved total, not a backlog anyone can work down. +PERMANENTLY_UNRESOLVABLE_BLOCKERS = ('annotation_only', 'argument_name_only') + + +def blocker_label(site: str) -> str: + return site.rpartition('[')[2].rstrip(']') or 'other' + + +def count_permanently_unresolvable(sites: list[str]) -> int: + """Count reported sites that can never become evidence, however wide the scan.""" + return sum(1 for site in sites if blocker_label(site) in PERMANENTLY_UNRESOLVABLE_BLOCKERS) + + +def producer_scan_reach(sources: list[SourceFile]) -> tuple[int, int]: + """Files the F1/F2 producer scan reaches, out of the tracked ``loopx/`` tree. + + Derived on every run, never pinned in the registry: the denominator moves + with any new module, so a literal here would fail diffs that have nothing to + do with semantics. This reach is the evidence bound F1 and F2 declare, so the + report states it instead of leaving the bound implicit. + """ + scanned = sum(1 for source in sources + if source.path in PRODUCER_FILES + or any(source.path.startswith(root + '/') for root in PRODUCER_ROOTS)) + return scanned, len(sources) + + def summarise_blockers(sites: list[str]) -> str: """Count reported sites by blocker so the total is actionable, not opaque. @@ -473,16 +612,49 @@ def summarise_blockers(sites: list[str]) -> str: counts: dict[str, int] = {} for site in sites: - label = site.rpartition('[')[2].rstrip(']') or 'other' + label = blocker_label(site) counts[label] = counts.get(label, 0) + 1 return ','.join(f"{label}={counts[label]}" for label in sorted(counts)) +def summarise_formal_domains(registry: dict[str, Any], sources: list[SourceFile]) -> str: + """Print how much each formal invariant actually quantifies over. + + The sizes are the ones ``check_invariant_domain`` derived, so the report and + the registry cannot disagree. The scan reach is measured here because it is + a property of the tree rather than of the registry. + """ + invariants = registry['formal_model']['invariants'] + sizes = ','.join( + f"{item['id'].split('_')[0]}:{item['domain']['verified']}/{item['domain']['registered']}" + for item in sorted(invariants, key=lambda item: item['id']) + ) + vocabularies = registry['vocabularies'] + kernel = [name for name, v in vocabularies.items() if v['tier'] == 'kernel'] + cross_runtime = [name for name, v in vocabularies.items() if v['tier'] == 'cross_runtime'] + covered = [name for name in kernel if 'producers' in vocabularies[name]] + unverified = [name for name in cross_runtime if 'producers' not in vocabularies[name]] + scanned, tracked = producer_scan_reach(sources) + projections = len(registry['projections']) + contexts = sum(len(entry['contexts']) for entry in registry['scope_declarations'].values()) + return ( + f"formal_domain={sizes} (verified/registered)\n" + f" formal_domain_bounds: kernel_with_producers={len(covered)}/{len(kernel)}" + f" cross_runtime_unverified={len(unverified)}/{len(cross_runtime)}" + f" producer_scan_reach={scanned}/{tracked}_files" + f" projections={projections}/{projections}" + f" scope_declarations={len(registry['scope_declarations'])} declared_contexts={contexts}/{contexts}" + ) + + def check_producers(registry: dict[str, Any], sources: list[SourceFile]) -> list[str]: unknown: list[str] = [] for name, vocabulary in registry['vocabularies'].items(): if 'producers' not in vocabulary: - continue # Other kernel families retain an explicit M0.5 coverage gap. + # Skipped: the whole cross_runtime tier, which declares no producers. + # F1/F2 therefore hold over the kernel tier only, which is the domain + # the registry's formal_model states -- not an unconditional claim. + continue try: rows = collect_production(REPO_ROOT, vocabulary, sources) field_domain = quota_action_domain(registry) if name == 'effective_action' else None @@ -732,10 +904,13 @@ def main() -> int: print(" " + ratchets) print(" " + " ".join(budgets)) print(" " + twins) - print(f" unresolved_producer_sites={len(unknown_producers)} (not proven safe)") + permanent = count_permanently_unresolvable(unknown_producers) + print(f" unresolved_producer_sites={len(unknown_producers)} (not proven safe; " + f"{permanent} can never become evidence)") print(" unresolved_producer_blockers=" + summarise_blockers(unknown_producers)) uncovered = [name for name, v in registry['vocabularies'].items() if v['tier'] == 'kernel' and 'producers' not in v] print(f" kernel_producer_coverage_pending={','.join(uncovered)}") + print(" " + summarise_formal_domains(registry, sources)) if '--report' in sys.argv[1:]: for site in unknown_producers: print(f" unknown_producer: {site}") diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json index 661b7ca98e..0a96ed3cf9 100644 --- a/loopx/semantics/vocabulary_v0.json +++ b/loopx/semantics/vocabulary_v0.json @@ -13,10 +13,10 @@ "formal_model": { "schema_version": "loopx_semantic_formal_model_v0", "universes": { - "vocabularies": "V: registered vocabulary identifiers", + "vocabularies": "V: registered vocabulary identifiers; Kernel(V) ⊆ V is the tier=kernel subset, the only tier that declares producers", "values": "U(v): ambient runtime values; S(v): registered admitted values", "sites": "L: source locations that define, produce, consume, interpret, pass through, project, or persist values", - "scopes": "Scope: global or bounded_context(context_id)", + "scopes": "Scope: global or bounded_context(context_id); ScopeDeclarations are the forked names the registry declares as bounded contexts", "roles": "Roles assigned to sites; a site may have more than one role only when each edge is explicit" }, "roles": [ @@ -73,39 +73,75 @@ "invariants": [ { "id": "F1_producer_closedness", - "statement": "Produced(v) ⊆ S(v) ⊆ U(v)", + "statement": "∀v ∈ Kernel(V): Produced_scan(v) ⊆ S(v) ⊆ U(v), where Produced_scan(v) is the production the fixed forms observe inside the code-owned scan reach. Production outside that reach, and the whole cross_runtime tier, is unverified rather than proven closed.", "enforcement": "m0_5", - "evidence": "bounded production-form AST scan; unknown dynamic producers are reported, not treated as proven safe" + "evidence": "bounded production-form AST scan over the PRODUCER_ROOTS/PRODUCER_FILES reach in loopx/semantics/production.py; check_producers visits only vocabularies that declare producers, and validate_production claims no whole-program closedness; unresolved dynamic sites are reported, not treated as proven safe", + "domain": { + "quantifies_over": "vocabularies[tier=kernel].producers", + "verified": 6, + "registered": 26, + "evidence_bound": "producer_scan_reach" + } }, { "id": "F2_canonical_value_liveness", - "statement": "Canonical(v) ⊆ Produced(v) ∪ CompatibilityOnly(v)", + "statement": "∀v ∈ Kernel(V): Canonical(v) ⊆ Produced_scan(v) ∪ CompatibilityOnly(v). The cross_runtime tier declares no producers, so liveness there is unverified rather than proven.", "enforcement": "m0_5", - "evidence": "every kernel value has a recognised producer or an explicit compatibility-only reason" + "evidence": "every kernel value has a producer recognised inside the scan reach, an executable input witness, or an explicit compatibility-only reason; a value whose only producer lies outside the reach would be reported as dead, not silently accepted", + "domain": { + "quantifies_over": "vocabularies[tier=kernel].producers", + "verified": 6, + "registered": 26, + "evidence_bound": "producer_scan_reach" + } }, { "id": "F3_consumer_domain_closedness", "statement": "Accepted(c) ⊆ S(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" + "evidence": "consumer and interpreter edges are currently inventory evidence, not complete data-flow proof", + "domain": { + "quantifies_over": "vocabularies[*]", + "verified": 0, + "registered": 26, + "evidence_bound": "inventory_only" + } }, { "id": "F4_scope_separation", - "statement": "A name collision is a semantic conflict only when its declared scopes overlap", + "statement": "∀n ∈ ScopeDeclarations: the declared context owner modules are exactly the modules defining n, one context per module, and every context owner symbol is n. Scope overlap itself is declared, never inferred, so it defines the conflict rather than being checkable against it.", "enforcement": "m0_5", - "evidence": "scope declarations and per-context owners; scope is never inferred from spelling" + "evidence": "check_scope_declarations compares the declared owner modules with the inventory's defining modules for the fork and rejects a partial enumeration; only a declared name leaves the semantic fork budget", + "domain": { + "quantifies_over": "scope_declarations[*].contexts", + "verified": 4, + "registered": 4, + "evidence_bound": "declared_defining_modules" + } }, { "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" + "evidence": "registry mapping is compared with the executable owner function", + "domain": { + "quantifies_over": "projections[*]", + "verified": 1, + "registered": 1, + "evidence_bound": "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" + "evidence": "requires producer, serializer, storage, reader, and migration edges not yet modeled", + "domain": { + "quantifies_over": "persists_edges[*]", + "verified": 0, + "registered": 0, + "evidence_bound": "unmodelled" + } } ], "proof_boundary": { @@ -123,6 +159,7 @@ "unproved": [ "all_runtime_trace_values_are_registered", "all_producers_are_found", + "cross_runtime_producer_closedness", "same_concept_behavioral_equivalence", "persistence_reader_compatibility" ], diff --git a/tests/architecture/test_semantic_vocabulary_drift.py b/tests/architecture/test_semantic_vocabulary_drift.py index 89290bb9a7..d2d71a950d 100644 --- a/tests/architecture/test_semantic_vocabulary_drift.py +++ b/tests/architecture/test_semantic_vocabulary_drift.py @@ -38,6 +38,14 @@ def test_semantic_vocabulary_registry_matches_the_code() -> None: assert completed.stdout.startswith("semantic-vocabulary-drift-smoke: ok"), ( completed.stdout ) + # The domain sizes are part of the report, not only of the registry: a reader + # of the smoke output must see how much each invariant actually covers. + report = completed.stdout + assert "\n formal_domain=F1:" in report, report + for token in ("kernel_with_producers=", "cross_runtime_unverified=", + "producer_scan_reach=", "scope_declarations=", "declared_contexts="): + assert token in report, (token, report) + assert "can never become evidence)" in report, report @pytest.mark.parametrize("mutation", ["twin_budget", "twin_root", "scan_root"]) @@ -82,7 +90,7 @@ def test_candidate_decisions_are_exhaustive_and_default_to_unknown() -> None: registry["formal_model"]["candidate_decisions"]["default"] = "reuse_existing" with pytest.raises(smoke["Drift"], match="default unresolved candidates"): - smoke["check_formal_model"](registry["formal_model"]) + smoke["check_formal_model"](registry["formal_model"], registry) def test_bounded_producer_scan_rejects_unregistered_write() -> None: @@ -434,6 +442,205 @@ def test_remaining_kernel_values_each_carry_a_note(name): assert not undocumented, f'{name}: values with no value_notes entry: {undocumented}' +def _invariant(registry: dict, invariant_id: str) -> dict: + return next(item for item in registry["formal_model"]["invariants"] if item["id"] == invariant_id) + + +def test_f1_f2_domain_names_exactly_the_vocabularies_the_producer_check_walks() -> None: + """The declared domain must be the set ``check_producers`` really visits. + + F1 and F2 were unconditional claims over every vocabulary while the check + skipped 20 of 26. This ties the quantifier in the statement to the predicate + the scanner uses, so widening one without the other fails. + """ + smoke = runpy.run_path(str(SMOKE)) + registry = smoke["load_registry"]() + vocabularies = registry["vocabularies"] + walked = {name for name, entry in vocabularies.items() if "producers" in entry} + assert walked == {name for name, entry in vocabularies.items() if entry["tier"] == "kernel"} + skipped = {entry["tier"] for name, entry in vocabularies.items() if name not in walked} + assert skipped == {"cross_runtime"} + for invariant_id in ("F1_producer_closedness", "F2_canonical_value_liveness"): + domain = _invariant(registry, invariant_id)["domain"] + assert domain["quantifies_over"] == "vocabularies[tier=kernel].producers" + assert domain["verified"] == len(walked) + assert domain["registered"] == len(vocabularies) + assert domain["evidence_bound"] == "producer_scan_reach" + + +@pytest.mark.parametrize("invariant_id", sorted({ + "F1_producer_closedness", + "F2_canonical_value_liveness", + "F3_consumer_domain_closedness", + "F4_scope_separation", + "F5_projection_totality", + "F6_persistence_version_compatibility", +})) +def test_every_invariant_must_declare_a_domain(invariant_id: str) -> None: + smoke = runpy.run_path(str(SMOKE)) + registry = copy.deepcopy(smoke["load_registry"]()) + _invariant(registry, invariant_id).pop("domain") + with pytest.raises(smoke["Drift"], match="invalid shape"): + smoke["check_formal_model"](registry["formal_model"], registry) + + +@pytest.mark.parametrize("invariant_id, field, value", [ + ("F1_producer_closedness", "verified", 26), + ("F1_producer_closedness", "verified", 5), + ("F1_producer_closedness", "registered", 6), + ("F2_canonical_value_liveness", "verified", 26), + ("F4_scope_separation", "verified", 1), + ("F5_projection_totality", "registered", 9), +]) +def test_declared_domain_size_must_match_the_derived_one(invariant_id, field, value) -> None: + """A domain size is counted from the registry, never taken on trust.""" + smoke = runpy.run_path(str(SMOKE)) + registry = copy.deepcopy(smoke["load_registry"]()) + _invariant(registry, invariant_id)["domain"][field] = value + with pytest.raises(smoke["Drift"], match=f"formal invariant {invariant_id}"): + smoke["check_formal_model"](registry["formal_model"], registry) + + +@pytest.mark.parametrize("invariant_id", ["F3_consumer_domain_closedness", "F6_persistence_version_compatibility"]) +def test_an_unenforced_invariant_cannot_claim_verified_members(invariant_id: str) -> None: + """Advisory and unproved stages walk nothing; the count has to say so.""" + smoke = runpy.run_path(str(SMOKE)) + registry = copy.deepcopy(smoke["load_registry"]()) + _invariant(registry, invariant_id)["domain"]["verified"] = 1 + with pytest.raises(smoke["Drift"], match="an unenforced stage walks nothing"): + smoke["check_formal_model"](registry["formal_model"], registry) + + +def test_an_enforced_invariant_cannot_declare_an_empty_domain(monkeypatch) -> None: + """An enforced stage over an empty set is vacuous, not proven.""" + smoke = runpy.run_path(str(SMOKE)) + registry = copy.deepcopy(smoke["load_registry"]()) + # The anchor is what normally forbids this pairing; move it so the emptiness + # rule itself is the one under test. + monkeypatch.setitem( + smoke["check_invariant_domain"].__globals__["FORMAL_DOMAIN_ANCHOR"], + "F4_scope_separation", ("persists_edges[*]", "declared_defining_modules"), + ) + domain = _invariant(registry, "F4_scope_separation")["domain"] + domain["quantifies_over"] = "persists_edges[*]" + domain["verified"] = 0 + domain["registered"] = 0 + with pytest.raises(smoke["Drift"], match="over an empty domain"): + smoke["check_formal_model"](registry["formal_model"], registry) + + +@pytest.mark.parametrize("invariant_id, selector", [ + # Every swap below names a selector the code knows, so only the anchor stops + # an invariant from widening the domain its statement quantifies over. + ("F1_producer_closedness", "vocabularies[*]"), + ("F2_canonical_value_liveness", "vocabularies[*]"), + ("F4_scope_separation", "projections[*]"), + ("F5_projection_totality", "scope_declarations[*].contexts"), +]) +def test_an_invariant_cannot_widen_its_own_domain_by_data_edit(invariant_id, selector) -> None: + smoke = runpy.run_path(str(SMOKE)) + registry = copy.deepcopy(smoke["load_registry"]()) + _invariant(registry, invariant_id)["domain"]["quantifies_over"] = selector + with pytest.raises(smoke["Drift"], match="FORMAL_DOMAIN_ANCHOR pins"): + smoke["check_formal_model"](registry["formal_model"], registry) + + +def test_every_invariant_is_anchored_to_a_domain() -> None: + smoke = runpy.run_path(str(SMOKE)) + anchor = smoke["FORMAL_DOMAIN_ANCHOR"] + assert set(anchor) == smoke["FORMAL_INVARIANTS"] + for selector, bound in anchor.values(): + assert selector in smoke["FORMAL_DOMAIN_SELECTORS"] + assert bound in smoke["FORMAL_EVIDENCE_BOUNDS"] + + +def test_a_domain_selector_cannot_be_invented_by_registry_data() -> None: + smoke = runpy.run_path(str(SMOKE)) + registry = copy.deepcopy(smoke["load_registry"]()) + _invariant(registry, "F1_producer_closedness")["domain"]["quantifies_over"] = "vocabularies[everything]" + with pytest.raises(smoke["Drift"], match="selectors are code owned"): + smoke["check_formal_model"](registry["formal_model"], registry) + + +@pytest.mark.parametrize("invariant_id, bound", [ + ("F1_producer_closedness", "unmodelled"), + ("F1_producer_closedness", "inventory_only"), + ("F3_consumer_domain_closedness", "producer_scan_reach"), + ("F5_projection_totality", "unmodelled"), +]) +def test_an_evidence_bound_cannot_contradict_the_enforcement_stage(monkeypatch, invariant_id, bound) -> None: + """A bound that says nothing was walked cannot sit on an enforced stage, and + a walked-evidence bound cannot sit on an advisory or unproved one.""" + smoke = runpy.run_path(str(SMOKE)) + registry = copy.deepcopy(smoke["load_registry"]()) + anchor = smoke["check_invariant_domain"].__globals__["FORMAL_DOMAIN_ANCHOR"] + monkeypatch.setitem(anchor, invariant_id, (anchor[invariant_id][0], bound)) + _invariant(registry, invariant_id)["domain"]["evidence_bound"] = bound + with pytest.raises(smoke["Drift"], match="evidence bound"): + smoke["check_formal_model"](registry["formal_model"], registry) + + +def test_an_unknown_evidence_bound_is_rejected() -> None: + smoke = runpy.run_path(str(SMOKE)) + registry = copy.deepcopy(smoke["load_registry"]()) + _invariant(registry, "F1_producer_closedness")["domain"]["evidence_bound"] = "trust_me" + with pytest.raises(smoke["Drift"], match="unknown evidence bound"): + smoke["check_formal_model"](registry["formal_model"], registry) + + +@pytest.mark.parametrize("extra", [{"note": "why"}, {}]) +def test_domain_key_set_is_closed(extra: dict) -> None: + smoke = runpy.run_path(str(SMOKE)) + registry = copy.deepcopy(smoke["load_registry"]()) + domain = _invariant(registry, "F5_projection_totality")["domain"] + if extra: + domain.update(extra) + else: + domain.pop("evidence_bound") + with pytest.raises(smoke["Drift"], match="domain keys must be exactly"): + smoke["check_formal_model"](registry["formal_model"], registry) + + +def test_adding_a_vocabulary_forces_the_declared_domain_to_move() -> None: + """The population count is derived, so a registry that grows fails until the + invariant's domain admits it. This is the I6 same-diff rule for a claim.""" + smoke = runpy.run_path(str(SMOKE)) + registry = copy.deepcopy(smoke["load_registry"]()) + registry["vocabularies"]["probe_vocabulary"] = { + "meaning": "probe", "tier": "cross_runtime", "status": "canonical", + "owners": {"python": None, "typescript": None}, "values": ["probe_value"], + } + with pytest.raises(smoke["Drift"], match="the registry holds 27"): + smoke["check_formal_model"](registry["formal_model"], registry) + + +def test_producer_scan_reach_is_measured_not_pinned() -> None: + """F1/F2's evidence bound is a file reach; the report derives it each run.""" + smoke = runpy.run_path(str(SMOKE)) + sources = smoke["load_sources"](REPO_ROOT) + scanned, tracked = smoke["producer_scan_reach"](sources) + assert 0 < scanned < tracked == len(sources) + roots = smoke["PRODUCER_ROOTS"] + files = smoke["PRODUCER_FILES"] + assert scanned == sum( + 1 for source in sources + if source.path in files or any(source.path.startswith(root + "/") for root in roots) + ) + + +def test_permanently_unresolvable_blockers_are_counted_apart() -> None: + """Two blocker labels can never become evidence; the total says how many.""" + smoke = runpy.run_path(str(SMOKE)) + sites = [ + "loopx/a.py::f:1 [argument_name_only]", + "loopx/a.py::f:2 [annotation_only]", + "loopx/a.py::f:3 [call_result]", + "loopx/a.py::f:4 [typescript_dynamic]", + ] + assert smoke["count_permanently_unresolvable"](sites) == 2 + assert set(smoke["PERMANENTLY_UNRESOLVABLE_BLOCKERS"]) == {"annotation_only", "argument_name_only"} + + def test_inventory_report_discloses_budget_slack(monkeypatch): """Budget slack (budget above the measured value) must be disclosed.