From 7f6a3138175fffc837f69fcbeb391d242ea65dc7 Mon Sep 17 00:00:00 2001 From: song <22676124+songoow@users.noreply.github.com> Date: Thu, 17 Sep 2026 21:38:58 -0400 Subject: [PATCH 1/3] fix(semantics): key closed-set identity on membership, not source order Collision identity compared `tuple(item["values"])`, which is the order the source happens to list elements in. Swapping three lines inside a `set` literal, membership unchanged, turned a twin into a fork and failed the gate on three budgets at once -- while `divergent_value_sets`, computed from the same inventory, correctly reported no divergence. One scan produced two contradictory answers and the wrong one held the gate. Identity is now membership when every definition of a name is a `set` or `frozenset`, and source order otherwise. The narrowness is the point: `LIFECYCLE_PRIORITY` is a `tuple` defined in two modules whose order *is* the priority, so normalizing every carrier would have replaced a false positive with a false negative. A name carried by mixed containers also stays order-sensitive, which makes the rule a pure relaxation -- it can only merge definitions the old rule split, so no untouched tree starts failing. Enums and `Literal` aliases carry no container and are left order-sensitive; their ordering semantics are not established here. Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: song <22676124+songoow@users.noreply.github.com> --- loopx/semantics/inventory.py | 32 ++++++- tests/architecture/test_semantic_inventory.py | 84 +++++++++++++++++++ 2 files changed, 115 insertions(+), 1 deletion(-) diff --git a/loopx/semantics/inventory.py b/loopx/semantics/inventory.py index b83a6cac08..f88299b1da 100644 --- a/loopx/semantics/inventory.py +++ b/loopx/semantics/inventory.py @@ -221,6 +221,34 @@ def multi_value_carriers( return carriers +# Containers whose element order the language does not preserve. Two definitions +# of the same ``set``/``frozenset`` that list the same members in a different +# order are the same closed set, so reordering one must not invent a fork. +# ``tuple``, ``list`` and ``as const`` arrays are deliberately excluded: a +# carrier like ``LIFECYCLE_PRIORITY`` spends its order as its meaning, and +# normalizing it would hide a real divergence instead of a fake one. +UNORDERED_CONTAINERS = frozenset({"set", "frozenset"}) + + +def _collision_keys(carriers_for_name: list[dict[str, Any]]) -> set[tuple[str, ...]]: + """The distinct value sets one name carries; one key means the name agrees. + + Membership decides identity only when *every* definition of the name is an + unordered container. A name carried by a ``tuple`` in one module and a + ``set`` in another keeps order-sensitive identity, so this can only ever + merge definitions that the old rule split -- it never splits a pair the old + rule merged, and cannot make an untouched tree start failing. + + Carriers with no ``container`` (enums, ``Literal`` aliases, TypeScript + ``as const`` arrays) are ordered by this rule, which reports a reordering + rather than hiding it -- the safe direction while their own ordering + semantics are unestablished here. + """ + if all(item.get("container") in UNORDERED_CONTAINERS for item in carriers_for_name): + return {tuple(sorted(set(item["values"]))) for item in carriers_for_name} + return {tuple(item["values"]) for item in carriers_for_name} + + def multi_value_name_collisions( carriers: list[dict[str, Any]], ) -> tuple[list[dict[str, Any]], list[dict[str, Any]]]: @@ -249,7 +277,9 @@ def multi_value_name_collisions( key=lambda item: item["module"], ) entry: dict[str, Any] = {"name": name, "definitions": definitions} - if len({tuple(item["values"]) for item in definitions}) == 1: + # Keyed off the raw carriers, which still carry ``container``; the + # ``definitions`` entries keep their source order for review. + if len(_collision_keys(carriers_for_name)) == 1: entry["values"] = definitions[0]["values"] entry["modules"] = [item["module"] for item in definitions] twins.append(entry) diff --git a/tests/architecture/test_semantic_inventory.py b/tests/architecture/test_semantic_inventory.py index 96e5151543..3f5a8f3ab6 100644 --- a/tests/architecture/test_semantic_inventory.py +++ b/tests/architecture/test_semantic_inventory.py @@ -17,6 +17,7 @@ import pytest from loopx.semantics.inventory import ( + multi_value_name_collisions, INVENTORY_SCHEMA_VERSION, SourceFile, build_inventory, @@ -387,3 +388,86 @@ def test_typescript_single_quoted_carriers_are_visible(repo: Path) -> None: inventory = build_inventory(repo) assert inventory["typescript_const_arrays"][0]["values"] == ["one", "two"] assert any(item["name"] == "SHARED" for item in inventory["duplicate_definitions"]["same_runtime_forks"]) + + +def _carrier(module: str, values: list[str], container: str = "set") -> dict: + return { + "kind": "python_closed_set", "name": "STATES", "module": module, + "values": values, "container": container, + } + + +def test_reordering_an_unordered_carrier_is_not_a_fork() -> None: + """A ``set`` has no element order, so listing the same members differently + is the same closed set. Before this rule, re-indenting a set literal + manufactured a semantic fork and blocked the gate, while the divergence + report computed from the same inventory correctly saw no divergence -- two + outputs of one scan disagreeing, with the wrong one holding the gate. + """ + twins, forks = multi_value_name_collisions([ + _carrier("loopx/a.py", ["open", "closed"]), + _carrier("loopx/b.py", ["closed", "open"]), + ]) + assert [row["name"] for row in twins] == ["STATES"] + assert forks == [] + # Diagnostics keep source order; only the identity key is normalized. + assert [item["values"] for item in twins[0]["definitions"]] == [ + ["open", "closed"], ["closed", "open"], + ] + + +def test_changing_membership_of_an_unordered_carrier_is_still_a_fork() -> None: + twins, forks = multi_value_name_collisions([ + _carrier("loopx/a.py", ["open", "closed"]), + _carrier("loopx/b.py", ["open", "shut"]), + ]) + assert twins == [] + assert [row["name"] for row in forks] == ["STATES"] + + +def test_reordering_an_ordered_carrier_is_still_a_fork() -> None: + """``tuple`` and ``list`` carriers spend their order as meaning. + + ``LIFECYCLE_PRIORITY`` is a tuple defined in two modules: the order *is* the + priority. Normalizing every carrier to sorted membership would trade a false + positive for a false negative and hide that divergence, so orderedness is + read from the container the source actually used. + """ + for container in ("tuple", "list"): + twins, forks = multi_value_name_collisions([ + _carrier("loopx/a.py", ["first", "second"], container), + _carrier("loopx/b.py", ["second", "first"], container), + ]) + assert twins == [], container + assert [row["name"] for row in forks] == ["STATES"], container + + +def test_a_name_carried_by_mixed_containers_keeps_order_sensitive_identity() -> None: + """Membership decides identity only when every definition is unordered. + + This keeps the rule a pure relaxation: it can only merge definitions the old + rule split, never split a pair it merged, so no untouched tree starts + failing because one side of a name is a tuple. + """ + twins, forks = multi_value_name_collisions([ + _carrier("loopx/a.py", ["open", "closed"], "set"), + _carrier("loopx/b.py", ["open", "closed"], "tuple"), + ]) + assert [row["name"] for row in twins] == ["STATES"] + assert forks == [] + + +def test_a_carrier_without_a_container_stays_order_sensitive() -> None: + """Enums, ``Literal`` aliases and ``as const`` arrays carry no ``container``. + + Their ordering semantics are not established here, so they keep the + reporting behaviour rather than being silently normalized. + """ + twins, forks = multi_value_name_collisions([ + {"kind": "python_enum", "name": "STATES", "module": "loopx/a.py", + "values": ["open", "closed"]}, + {"kind": "python_enum", "name": "STATES", "module": "loopx/b.py", + "values": ["closed", "open"]}, + ]) + assert twins == [] + assert [row["name"] for row in forks] == ["STATES"] From 548b1671dc894fc0fd13dc93b7aa3df833633764 Mon Sep 17 00:00:00 2001 From: song <22676124+songoow@users.noreply.github.com> Date: Thu, 17 Sep 2026 21:38:58 -0400 Subject: [PATCH 2/3] fix(semantics): count F5 as the projections the check actually executes The `projections[*]` selector returned `len(registry["projections"])` for both `verified` and `registered`, while `check_projections` imported exactly one hardcoded projection. A projection whose owner module and function do not exist anywhere in the tree, declared as 2/2, passed the whole smoke and printed `F5:2/2` under the evidence bound `executable_owner_function`. The declaration was counting as its own proof. `verified` now counts only the projections named in `EXECUTED_PROJECTIONS`, which lives in code for the same reason as `COVERAGE_ANCHOR`, and each one's registry `owner` must equal the function the check imports. A registered projection with no executed check raises `registered` without raising `verified`, the way F1 reports 6 of 26, so the gap is reported rather than blocked or hidden. Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: song <22676124+songoow@users.noreply.github.com> --- examples/semantic-vocabulary-drift-smoke.py | 27 ++++++++- .../test_semantic_vocabulary_drift.py | 60 +++++++++++++++++++ 2 files changed, 86 insertions(+), 1 deletion(-) diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py index 0acd64d75f..c1f34306aa 100755 --- a/examples/semantic-vocabulary-drift-smoke.py +++ b/examples/semantic-vocabulary-drift-smoke.py @@ -110,10 +110,28 @@ 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"])), + # ``verified`` counts the projections ``check_projections`` actually imports + # and executes, not the registry's own row count. A registry entry is a + # declaration; counting it as its own evidence let a projection whose owner + # function does not exist report itself verified. An unexecuted entry now + # raises ``registered`` without raising ``verified``, the same way F1 + # reports 6 of 26. + "projections[*]": lambda registry: ( + sum(1 for name in registry["projections"] if name in EXECUTED_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), } +# The projections F5 executes, and the owner each one must name. Pinned in code +# for the same reason as COVERAGE_ANCHOR and FORMAL_DOMAIN_ANCHOR: a data-only +# edit to the registry must not be able to widen what the invariant claims to +# have verified, and the owner string has to stay tied to the function the check +# below imports rather than being prose the registry can restate. +EXECUTED_PROJECTIONS = { + "turn_route_to_loop_disposition": + "loopx/control_plane/turn_driver/turn_contract_generated.py::project_turn_route", +} 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 @@ -708,6 +726,13 @@ def resolve(member: str) -> None: def check_projections(registry: dict[str, Any]) -> None: + for name, owner in EXECUTED_PROJECTIONS.items(): + require(name in registry["projections"], + f"projection {name} is executed by this check but is not registered") + declared = registry["projections"][name].get("owner") + require(declared == owner, + f"projection {name} names owner {declared}; this check executes {owner}, " + "so the registry would be crediting a function it does not run") projection = registry["projections"]["turn_route_to_loop_disposition"] from loopx.control_plane.turn_driver.driver import LoopXTurnRoute from loopx.control_plane.turn_driver.turn_contract_generated import LoopDisposition, project_turn_route diff --git a/tests/architecture/test_semantic_vocabulary_drift.py b/tests/architecture/test_semantic_vocabulary_drift.py index 404d9eee72..9e7b4e40fc 100644 --- a/tests/architecture/test_semantic_vocabulary_drift.py +++ b/tests/architecture/test_semantic_vocabulary_drift.py @@ -718,3 +718,63 @@ def test_inventory_report_discloses_budget_slack(monkeypatch): ) _, line = smoke["check_inventory"](widened, sources) assert "slack=conflicting_values=2" in line, line + + +def _with_unexecuted_projection(registry: dict) -> dict: + registry = copy.deepcopy(registry) + registry["projections"]["unexecuted_probe"] = { + "meaning": "A projection whose owner module and function do not exist.", + "owner": "loopx/semantics/does_not_exist.py::no_such_function", + "mapping": {"a": "b"}, + } + return registry + + +def test_an_unexecuted_projection_cannot_count_itself_as_verified() -> None: + """F5 claims the evidence bound ``executable_owner_function``. + + Before this, ``verified`` was ``len(registry["projections"])`` -- the + registry's own row count standing in for evidence -- while + ``check_projections`` only ever imported one hardcoded projection. Adding a + projection whose owner function does not exist anywhere in the tree passed + the full smoke and reported ``F5:2/2``. A declaration was counting as its + own proof. + """ + smoke = runpy.run_path(str(SMOKE)) + registry = _with_unexecuted_projection(smoke["load_registry"]()) + walked, population = smoke["FORMAL_DOMAIN_SELECTORS"]["projections[*]"](registry) + assert (walked, population) == (1, 2) + + +def test_declaring_an_unexecuted_projection_as_verified_fails() -> None: + smoke = runpy.run_path(str(SMOKE)) + registry = _with_unexecuted_projection(smoke["load_registry"]()) + for invariant in registry["formal_model"]["invariants"]: + if invariant["id"] == "F5_projection_totality": + invariant["domain"]["registered"] = 2 + invariant["domain"]["verified"] = 2 + with pytest.raises(smoke["Drift"], match="claims 2 verified members"): + smoke["check_formal_model"](registry["formal_model"], registry) + + +def test_a_projection_owner_the_check_does_not_run_is_rejected() -> None: + """The owner string must name the function ``check_projections`` imports. + + Otherwise the registry can point at any module while the check keeps + exercising the real one, and the invariant credits a function it never ran. + """ + smoke = runpy.run_path(str(SMOKE)) + registry = copy.deepcopy(smoke["load_registry"]()) + registry["projections"]["turn_route_to_loop_disposition"]["owner"] = ( + "loopx/semantics/elsewhere.py::some_other_function" + ) + with pytest.raises(smoke["Drift"], match="crediting a function it does not run"): + smoke["check_projections"](registry) + + +def test_every_executed_projection_must_be_registered() -> None: + smoke = runpy.run_path(str(SMOKE)) + registry = copy.deepcopy(smoke["load_registry"]()) + del registry["projections"]["turn_route_to_loop_disposition"] + with pytest.raises(smoke["Drift"], match="is not registered"): + smoke["check_projections"](registry) From 5a6ba847b276cbf0fc049f1e7e11b229b6b06941 Mon Sep 17 00:00:00 2001 From: song <22676124+songoow@users.noreply.github.com> Date: Thu, 17 Sep 2026 21:38:58 -0400 Subject: [PATCH 3/3] docs(semantics): record the two corrected measurements in both mirrors Both were reproduced against d8e7af141 before being written, and neither fix relaxes a budget, floor or anchor. Appendix A states what each measurement claimed, what it actually did, and what the correction still does not establish -- F5 walks one projection, and the ordering semantics of enums and `Literal` aliases remain open. Co-Authored-By: Claude Opus 5 (1M context) Signed-off-by: song <22676124+songoow@users.noreply.github.com> --- .../semantic-vocabulary-convergence-v0.md | 42 ++++++++++++++++++- ...emantic-vocabulary-convergence-v0.zh-CN.md | 30 ++++++++++++- 2 files changed, 70 insertions(+), 2 deletions(-) diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md index cf2f8a8312..c16227b1ad 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md @@ -587,7 +587,11 @@ 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 +an invariant cannot widen the set it claims through a registry edit alone. F5's +`verified` count is the number of projections the smoke actually imports and +executes, taken from `EXECUTED_PROJECTIONS` in code, not the registry's own row +count; a registered projection with no executed check raises `registered` +without raising `verified`, the way F1 reports 6 of 26. 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 @@ -1123,6 +1127,42 @@ introduce a competing target state. ## Appendix A: Execution ledger (non-normative) +### 2026-09-17 — Two measurements that contradicted themselves, corrected + +Normative for what F5's `verified` count means and for closed-set collision +identity. No budget, floor or anchor was relaxed; both changes were reproduced +against `d8e7af141` before being written. + +- **A declaration was counting as its own evidence (F5).** The + `projections[*]` selector returned `len(registry["projections"])` for *both* + `verified` and `registered`, while `check_projections` imported exactly one + hardcoded projection. Adding a projection whose owner module and function do + not exist anywhere in the tree, and declaring the domain as 2/2, passed the + whole smoke and printed `F5:2/2` under the evidence bound + `executable_owner_function`. `verified` now counts only the projections named + in `EXECUTED_PROJECTIONS`, which is code, and each one's registry `owner` must + equal the function the check imports. The same injection now either fails + (`claims 2 verified members ... the m0 check walks 1`) or is declared honestly + and prints `F5:1/2`. +- **Reordering a `set` counted as a semantic fork.** Collision identity used + `tuple(item["values"])`, which is source order. Swapping three lines inside a + `set` literal — membership unchanged — turned a twin into a fork and failed + the gate on three budgets at once, while `divergent_value_sets`, computed from + the same inventory, correctly reported no divergence: one scan, two outputs, + and the wrong one held the gate. Identity is now membership when *every* + definition of a name is a `set`/`frozenset`, and source order otherwise. +- **The normalization is deliberately narrow.** `tuple`, `list` and `as const` + carriers keep order-sensitive identity, because `LIFECYCLE_PRIORITY` is a + tuple defined in two modules whose order *is* the priority; normalizing every + carrier would have replaced a false positive with a false negative. A name + carried by mixed containers also stays order-sensitive, which makes the rule a + pure relaxation: it can only merge definitions the old rule split, so no + untouched tree starts failing. +- **What this does not do.** It does not establish the ordering semantics of + enums or `Literal` aliases, which carry no container and are left + order-sensitive; and it does not add a second executed projection. F5 still + walks one. + ### 2026-09-17 — Formula, role and enforcement claims separated; formal signature mutated Normative for the enforcement-lane wording; the checks are unchanged except for 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 be87c33c2d..cbd6b8f5b8 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md @@ -470,7 +470,9 @@ R ⊆ L × V × Version 将值持久化 建议性（advisory）与未证明（unproved）阶段什么都不走，因此 `verified` 必须为 0； 已强制阶段则不得声明空值域。每条义务的 selector 与证据边界由 smoke 里的 `FORMAL_DOMAIN_ANCHOR` 按 `COVERAGE_ANCHOR` 同一模式钉住（I5），因此不可能只改数据 -就扒宽一条不变量所声称的范围。producer 扫描范围本身每次运行现算而不钉住， +就扒宽一条不变量所声称的范围。F5 的 `verified` 取的是 smoke 真正导入并执行的投影 +条数，来自代码里的 `EXECUTED_PROJECTIONS`，而不是注册表自身的行数；已注册但没有 +对应执行检查的投影只抬高 `registered`，不抬高 `verified`，与 F1 报 6/26 同理。producer 扫描范围本身每次运行现算而不钉住， 因为分母会随任何新模块移动；smoke 会打印当前比值、未解析位点总数，以及其中 再宽的扫描也永远无法解析的那一部分（E21）。 @@ -906,6 +908,32 @@ PR review 保留这些层级。普通改动记录检查范围和理由，无共 ## 附录 A：执行账本（非规范） +### 2026-09-17 — 两处自相矛盾的度量已修正 + +对 F5 的 `verified` 含义与闭集碰撞身份是规范性的。没有放松任何预算、下限或锚点； +两处都先在 `d8e7af141` 上复现，再动笔。 + +- **声明把自己当成了证据（F5）。** `projections[*]` selector 的 `verified` 与 + `registered` 都返回 `len(registry["projections"])`，而 `check_projections` 只 + 导入了一个写死的投影。加入一个 owner 模块与函数在整棵树里都不存在的投影，并把 + 值域声明成 2/2，完整 smoke 依然通过，并在证据边界 `executable_owner_function` + 之下打印 `F5:2/2`。现在 `verified` 只统计代码里 `EXECUTED_PROJECTIONS` 点名的 + 投影，且每个投影在注册表里的 `owner` 必须等于检查真正导入的那个函数。同样的注入 + 现在要么失败（`claims 2 verified members ... the m0 check walks 1`），要么如实 + 声明并打印 `F5:1/2`。 +- **重排 `set` 被算成语义分叉。** 碰撞身份用的是 `tuple(item["values"])`，即源码 + 顺序。把一个 `set` 字面量里的三行调换位置——成员完全没变——就会把孪生变成分叉， + 一次触发三个预算失败；而由同一份 inventory 算出的 `divergent_value_sets` 正确 + 地报告没有分歧：一次扫描、两个输出，且挡住 CI 的是错的那个。现在只有当一个名字 + 的**每一个**定义都是 `set`/`frozenset` 时才按成员判定身份，否则仍按源码顺序。 +- **这个归一化是刻意收窄的。** `tuple`、`list` 与 `as const` 载体保持顺序敏感， + 因为 `LIFECYCLE_PRIORITY` 就是一个定义在两个模块里的 tuple，它的顺序就是优先级； + 一刀切归一化等于用一个假阴性换掉一个假阳性。同一名字若由不同容器承载，同样保持 + 顺序敏感——这让该规则成为纯粹的放松：它只会合并旧规则拆开的定义，因此不会让任何 + 未改动的代码树开始失败。 +- **它没有做什么。** 它没有确立 enum 与 `Literal` 别名的顺序语义——这些载体不带 + container，仍按顺序敏感处理；也没有新增第二个可执行投影，F5 仍然只走一个。 + ### 2026-09-17 — 分离公式、角色与强制性声明；对形式签名做突变 强制层级的表述是规范性变更；除新增一条规则外，检查本身不变。#4447 Track B 的 B0 切片。