From 9e6dc84c5a0b38ba69cc6f398c01376e88ad9b6b Mon Sep 17 00:00:00 2001 From: song Date: Tue, 15 Sep 2026 22:34:55 +0800 Subject: [PATCH 1/9] docs(semantics): define relative completeness boundary Signed-off-by: song --- .../semantic-vocabulary-convergence-v0.md | 106 +++++++++++++++++- ...emantic-vocabulary-convergence-v0.zh-CN.md | 89 ++++++++++++++- examples/semantic-vocabulary-drift-smoke.py | 23 +++- loopx/semantics/vocabulary_v0.json | 40 ++++++- .../test_semantic_vocabulary_drift.py | 20 ++++ 5 files changed, 266 insertions(+), 12 deletions(-) diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md index 51564280a3..833afd46a8 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md @@ -404,6 +404,108 @@ edges are modelled. The registry stores this proof boundary in implicit pass. +### Soundness, relative completeness, and candidate decisions + +The word *complete* is scoped here. Let `U(v)` be the ambient runtime value +space for a vocabulary, `S(v)` its registered admitted set, `P(v)` the values +actually produced, and `O(v)` the values observed by the scanner. The producer +obligation is meaningful only when production is defined over `U(v)`: + +```text +P(v) ⊆ S(v) ⊆ U(v) +``` + +Defining `P(v)` as a subset of `S(v)` in advance would make the first +inclusion tautological. M0 currently establishes only bounded claims about +`O(v)` and registered structural carriers. + +For a recognised language fragment `L0` and an exact analyser `A0`, define: + +```text +Sound(A0, property, L0) := A0 accepts c ⇒ property(c) +Complete(A0, property, L0) := property(c) ⇒ A0 accepts c +``` + +The M0 guard can aim at both properties for its fixed carrier and dispatch +forms. It cannot claim either property for arbitrary dynamic Python or +TypeScript. A value flowing through an alias, configuration, reflection, +external input, or unrecognised syntax belongs to `unknown` until a bounded +analysis accounts for it. Unknown is an evidence result, not proof of absence. + +Every candidate change must receive exactly one finite disposition: + +```text +reuse_existing | extend_vocabulary | create_vocabulary | local_only +external_input | compatibility_only | unknown +``` + +This makes the *workflow classification* exhaustive even though the program +analysis is not. `reuse_existing` requires the same slot, compatible scope, +and an equivalent contract. `extend_vocabulary` requires a witness that +reusing an existing value would collapse two states with different required +behaviour. `create_vocabulary` requires a new semantic domain or independently +owned lifecycle. If the evidence cannot decide among these cases, the default +is `unknown`; the agent must not silently treat an unresolved candidate as a +reuse. + +General behavioural equivalence remains undecidable for arbitrary programs, so +`same_concept` is not promoted to a theorem by this schema. It becomes a +blocking property only for a restricted contract with explicit inputs, +outputs, transitions, persistence version and finite test domain. This is the +boundary between a useful proof skeleton and an uncheckable claim of +whole-program semantic convergence. + + +### Soundness, relative completeness, and candidate decisions + +The word *complete* is scoped here. Let `U(v)` be the ambient runtime value +space for vocabulary `v`, `S(v)` its registered admitted set, `P(v)` the values +actually produced, and `O(v)` the values observed by the scanner. The producer +obligation is meaningful only when production is defined over `U(v)`: + +```text +P(v) ⊆ S(v) ⊆ U(v) +``` + +Defining `P(v)` as a subset of `S(v)` in advance would make the first +inclusion tautological. M0 establishes bounded claims about recognised source +forms and registered structural carriers. + +For a recognised language fragment `L0` and an exact analyser `A0`, define: + +```text +Sound(A0, property, L0) := A0 accepts c ⇒ property(c) +Complete(A0, property, L0) := property(c) ⇒ A0 accepts c +``` + +The M0 guard may aim at both properties for its fixed carrier and dispatch +forms. It cannot claim either property for arbitrary dynamic Python or +TypeScript. Values flowing through aliases, configuration, reflection, external +input, or unrecognised syntax are `unknown` until a bounded analysis accounts +for them. Unknown is an evidence result, not proof of absence. + +Every vocabulary candidate has exactly one finite disposition: + +```text +reuse_existing | extend_vocabulary | create_vocabulary | local_only +external_input | compatibility_only | unknown +``` + +`reuse_existing` requires the same slot, compatible scope, and an equivalent +contract. `extend_vocabulary` requires a witness that reusing an existing value +would collapse two states with different required behaviour. `create_vocabulary` +requires a new semantic domain or independently owned lifecycle. If evidence +cannot decide among these cases, the disposition is `unknown`; an unresolved +candidate must not silently become a reuse. + +General behavioural equivalence is undecidable for arbitrary programs, so +`same_concept` is not promoted to a theorem by this schema. It can become a +blocking property only for a restricted contract with explicit inputs, outputs, +transitions, persistence version, and a finite test domain. This is the boundary +between a useful proof skeleton and a claim of whole-program semantic +convergence. + + ### State model and schema `loopx/semantics/vocabulary_v0.json`, `schema_version` @@ -420,7 +522,7 @@ vocabulary key fails the smoke. | `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` | 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.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 | @@ -540,7 +642,7 @@ inventory in the same PR. | 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 | +| 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 | Known limits, stated so the check is not over-trusted: 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 cba3879ca0..ba46812ccd 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md @@ -328,6 +328,91 @@ R ⊆ S × V × Version 将值持久化 `formal_model` 保存这条证明边界；标记为 `unproved` 的性质是显式局限，不能被当作默认通过。 +### 健全性、相对完备性与候选决策 + +这里的“完备”必须带范围。令 `U(v)` 为词表的运行时完整值域，`S(v)` 为注册表允许 +的值集合，`P(v)` 为实际产生的值集合，`O(v)` 为扫描器观察到的值集合。生产义务 +只有在完整值域上定义时才有意义： + +```text +P(v) ⊆ S(v) ⊆ U(v) +``` + +如果预先把 `P(v)` 定义成 `S(v)` 的子集，第一个包含关系就变成恒真命题。M0 当前 +只对 `O(v)` 和已登记的结构载体建立有界结论。 + +对一个受限语法片段 `L0` 和精确分析器 `A0`，定义： + +```text +Sound(A0, property, L0) := A0 接受 c ⇒ property(c) +Complete(A0, property, L0) := property(c) ⇒ A0 接受 c +``` + +M0 守卫可以对固定载体和固定分发形式追求这两个性质，但不能对任意动态 Python 或 +TypeScript 宣称它们成立。值如果经过别名、配置、反射、外部输入或未识别语法流动， +在有界分析覆盖它之前都属于 `unknown`。Unknown 是证据结果，不是“不存在”的证明。 + +每个候选改动必须且只能得到一个有限决策： + +```text +reuse_existing | extend_vocabulary | create_vocabulary | local_only +external_input | compatibility_only | unknown +``` + +这样可以让“流程分类”完备，即使程序分析本身不完备。`reuse_existing` 要求槽位相同、 +作用域兼容、契约等价。`extend_vocabulary` 要求给出反例，证明复用旧值会把两个需要 +不同处理的状态压成一个。`create_vocabulary` 要求出现新的语义定义域或独立 owner 与 +生命周期。如果证据不足以在这些情况之间做决定，默认就是 `unknown`；Agent 不能把 +未解析候选静默当成复用旧词。 + +任意程序的行为等价通常不可判定，因此这个 schema 不会把 `same_concept` 自动提升为 +定理。只有当输入、输出、状态转换、持久化版本和有限测试域都明确时，行为等价才可 +在受限契约内成为阻断条件。这就是可用的证明骨架与“全程序语义收敛已被证明”之间的 +边界。 + + +### 健全性、相对完备性与候选决策 + +这里的“完备”必须带范围。令 `U(v)` 为词表 `v` 的运行时完整值域，`S(v)` 为注册表 +允许的值集合，`P(v)` 为实际产生的值集合，`O(v)` 为扫描器观察到的值集合。生产义务 +只有在完整值域上定义时才有意义： + +```text +P(v) ⊆ S(v) ⊆ U(v) +``` + +如果预先把 `P(v)` 定义成 `S(v)` 的子集，第一个包含关系就会变成恒真命题。M0 +只对已识别的源码形式和已登记的结构载体建立有界结论。 + +对一个受限语法片段 `L0` 和精确分析器 `A0`，定义： + +```text +Sound(A0, property, L0) := A0 接受 c ⇒ property(c) +Complete(A0, property, L0) := property(c) ⇒ A0 接受 c +``` + +M0 守卫可以对固定载体和固定分发形式追求这两个性质，但不能对任意动态 Python 或 +TypeScript 宣称它们成立。值如果经过别名、配置、反射、外部输入或未识别语法流动， +在有界分析覆盖它之前都属于 `unknown`。Unknown 是证据结果，不是“不存在”的证明。 + +每个词表候选必须且只能得到一个有限决策： + +```text +reuse_existing | extend_vocabulary | create_vocabulary | local_only +external_input | compatibility_only | unknown +``` + +`reuse_existing` 要求槽位相同、作用域兼容、契约等价。`extend_vocabulary` 要求给出 +反例，证明复用旧值会把两个需要不同处理的状态压成一个。`create_vocabulary` 要求出现 +新的语义定义域或独立 owner 与生命周期。如果证据不足以在这些情况之间做决定，默认 +就是 `unknown`；未解析候选不能静默当成复用旧词。 + +任意程序的行为等价通常不可判定，因此这个 schema 不会把 `same_concept` 自动提升为 +定理。只有当输入、输出、状态转换、持久化版本和有限测试域都明确时，行为等价才可 +在受限契约内成为阻断条件。这就是可用的证明骨架与“全程序语义收敛已被证明”之间的 +边界。 + + ### 状态模型与 schema `loopx/semantics/vocabulary_v0.json`，`schema_version` 为 @@ -344,7 +429,7 @@ R ⊆ S × V × Version 将值持久化 | `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` | 有限的集合、角色关系与层次、语义义务、候选决策，以及已建立/有界/unknown/未证明的声明 | 漂移 smoke 校验精确 schema、角色层次、候选决策和不变量 ID；属性实施阶段不能冒充已完成证明 | | `formal_model.enforcement_policy` | 当前阻断、下一阶段阻断、建议性和未证明层级 | 每个形式不变量恰好出现一次，且层级与其实施阶段一致 | | `vocabularies..value_notes`、`deprecated_values` | 逐值评审备注；计划删除的值 | 名字必须是已注册值 | | `relations.same_concept` | `vocabulary.value` 成员组 | 每个成员可解析 | @@ -447,7 +532,7 @@ PR 中重新生成清单。 | 有界上下文名字只能靠声明离开分叉预算（M0.5） | 为 `SOURCE_SURFACES` 声明四个上下文；另行只改名其中一处定义而不声明 | 声明把 `multi_value_forks` 降到 3；单独改名不降 | I14；诚实的修法是评审者看得见的注册表修改，改名是不碰注册表的代码改动 | | 上游合并会让已提交清单过期 | 对 `upstream/main` 最近二十个合并提交，在第一父提交与合并结果之间重放扫描器 | 20 次合并中 8 次至少改变一个载体 | 提交快照的实测成本；处理规则见第 10 节与第 12 节 Q9 | -| 形式模型不能静默丢失证明义务 | 从 `formal_model` 删除不变量、角色、关系或证明边界分类 | 漂移 smoke 针对形式模型结构失败 | 该模型是有限契约和证明账本，本身不等于这些性质已经被证明 | +| 形式模型不能静默丢失证明义务 | 从 `formal_model` 删除不变量、角色、候选决策、关系或证明边界分类 | 漂移 smoke 针对形式模型结构失败 | 该模型是有限契约和证明账本，本身不等于这些性质已经被证明 | 已知边界，写明是为了不让这个检查被过度信任： diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py index d01dc46069..2fbc3d90c4 100755 --- a/examples/semantic-vocabulary-drift-smoke.py +++ b/examples/semantic-vocabulary-drift-smoke.py @@ -51,7 +51,7 @@ STATUSES = {"canonical", "legacy", "merge_candidate"} FORMAL_MODEL_KEYS = { "schema_version", "universes", "roles", "role_hierarchy", "relations", "invariants", "proof_boundary", - "enforcement_policy", + "enforcement_policy", "candidate_decisions", } FORMAL_MODEL_SCHEMA_VERSION = "loopx_semantic_formal_model_v0" FORMAL_UNIVERSE_KEYS = {"vocabularies", "values", "sites", "scopes", "roles"} @@ -67,6 +67,15 @@ } FORMAL_ENFORCEMENT = {"m0", "m0_5", "m1", "advisory", "unproved"} FORMAL_POLICY_KEYS = {"blocking_now", "blocking_next", "advisory", "unproved"} +FORMAL_CANDIDATE_DECISIONS = { + "reuse_existing", + "extend_vocabulary", + "create_vocabulary", + "local_only", + "external_input", + "compatibility_only", + "unknown", +} # 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 @@ -230,9 +239,17 @@ def check_formal_model(model: dict[str, Any]) -> None: 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") + candidates = model["candidate_decisions"] + require(set(candidates) == {"values", "default", "meaning"}, + "formal_model candidate_decisions must define values, default, and meaning") + require(candidates["values"] == sorted(FORMAL_CANDIDATE_DECISIONS), + "formal_model candidate_decisions must be a stable exhaustive classification") + require(candidates["default"] == "unknown", + "formal_model candidate_decisions must default unresolved candidates to unknown") + require(candidates["meaning"].strip(), "formal_model candidate_decisions needs a meaning") boundary = model["proof_boundary"] - require(set(boundary) == {"established", "bounded", "unproved"}, - "formal_model proof_boundary must separate established, bounded, and unproved claims") + require(set(boundary) == {"established", "bounded", "unknown", "unproved"}, + "formal_model proof_boundary must separate established, bounded, unknown, 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") diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json index 17558ccd1d..879deb0b3c 100644 --- a/loopx/semantics/vocabulary_v0.json +++ b/loopx/semantics/vocabulary_v0.json @@ -28,13 +28,39 @@ "pass_through" ], "role_hierarchy": { - "consumer": ["interpreter", "pass_through"] + "consumer": [ + "interpreter", + "pass_through" + ] + }, + "candidate_decisions": { + "values": [ + "compatibility_only", + "create_vocabulary", + "extend_vocabulary", + "external_input", + "local_only", + "reuse_existing", + "unknown" + ], + "default": "unknown", + "meaning": "Exhaustive disposition for a vocabulary candidate; unknown is the fail-closed evidence state when the bounded analysis cannot classify it." }, "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"] + "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", @@ -100,6 +126,10 @@ "all_producers_are_found", "same_concept_behavioral_equivalence", "persistence_reader_compatibility" + ], + "unknown": [ + "dynamic_producer_or_consumer_path", + "unclassified_vocabulary_candidate" ] } }, diff --git a/tests/architecture/test_semantic_vocabulary_drift.py b/tests/architecture/test_semantic_vocabulary_drift.py index 50d9434045..2d51dadff7 100644 --- a/tests/architecture/test_semantic_vocabulary_drift.py +++ b/tests/architecture/test_semantic_vocabulary_drift.py @@ -63,3 +63,23 @@ def test_literal_scan_rejects_unknown_value_with_either_quote(suffix: str, quote sources = [smoke["SourceFile"]("loopx/probe" + suffix, suffix, text)] with pytest.raises(smoke["Drift"], match="unregistered_action"): smoke["check_literal_vocabularies"](smoke["load_registry"](), sources) + + +def test_candidate_decisions_are_exhaustive_and_default_to_unknown() -> None: + smoke = runpy.run_path(str(SMOKE)) + registry = smoke["load_registry"]() + candidate_decisions = registry["formal_model"]["candidate_decisions"] + assert candidate_decisions["default"] == "unknown" + assert set(candidate_decisions["values"]) == { + "reuse_existing", + "extend_vocabulary", + "create_vocabulary", + "local_only", + "external_input", + "compatibility_only", + "unknown", + } + + registry["formal_model"]["candidate_decisions"]["default"] = "reuse_existing" + with pytest.raises(smoke["Drift"], match="default unresolved candidates"): + smoke["check_formal_model"](registry["formal_model"]) From 9b71c5c62b98bc3217b81891fdddc829a493ed00 Mon Sep 17 00:00:00 2001 From: song Date: Tue, 15 Sep 2026 22:37:37 +0800 Subject: [PATCH 2/9] docs(semantics): align formal value domains Signed-off-by: song --- loopx/semantics/vocabulary_v0.json | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json index 879deb0b3c..87b4fd258b 100644 --- a/loopx/semantics/vocabulary_v0.json +++ b/loopx/semantics/vocabulary_v0.json @@ -15,7 +15,7 @@ "schema_version": "loopx_semantic_formal_model_v0", "universes": { "vocabularies": "V: registered vocabulary identifiers", - "values": "Val(v): values admitted by vocabulary v", + "values": "U(v): ambient runtime values; S(v): registered admitted values", "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" @@ -64,8 +64,8 @@ }, "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", + "produces": "P ⊆ S × V × U: a site writes or returns a runtime value; it is valid only when the value is in S(v)", + "consumes": "C ⊆ S × V × U: a site accepts or branches on a runtime 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", @@ -74,7 +74,7 @@ "invariants": [ { "id": "F1_producer_closedness", - "statement": "Produced(v) ⊆ Val(v)", + "statement": "Produced(v) ⊆ S(v) ⊆ U(v)", "enforcement": "m0_5", "evidence": "bounded production-form AST scan; unknown dynamic producers are reported, not treated as proven safe" }, From 34e43f1f67d0a7ea30c7e4a3be7e3aab2c4eef56 Mon Sep 17 00:00:00 2001 From: song Date: Tue, 15 Sep 2026 23:33:45 +0800 Subject: [PATCH 3/9] feat(pr-review): surface semantic alignment constraints Signed-off-by: song --- loopx/capabilities/pr_review_queue/README.md | 35 +++++ .../capabilities/pr_review_queue/__init__.py | 2 + .../pr_review_queue/result_check.py | 12 +- .../pr_review_queue/review_contract.py | 132 +++++++++++++++++- loopx/pr_review.py | 2 + tests/capabilities/test_pr_review_contract.py | 45 ++++++ .../test_pr_review_result_check.py | 22 +++ 7 files changed, 246 insertions(+), 4 deletions(-) diff --git a/loopx/capabilities/pr_review_queue/README.md b/loopx/capabilities/pr_review_queue/README.md index 4616b6fb4b..18a0144116 100644 --- a/loopx/capabilities/pr_review_queue/README.md +++ b/loopx/capabilities/pr_review_queue/README.md @@ -309,6 +309,41 @@ progress toward approval by themselves; the reviewer should request the smallest viable fix, deletion, split, or hold when the benefit does not justify the accumulated mechanism. +### Semantic alignment and CI constraint recovery + +Every code review plan carries `semantic_alignment`. It is a lightweight +orientation block, not a demand for whole-program semantic analysis. The agent +must state whether the change has no semantic contract impact or whether it +reuses an existing vocabulary, extends one, creates one, is an external or +compatibility value, or remains `unknown`. A normal code PR may use +`not_applicable` only with a reason that names the checked boundary. + +For semantic or constraint-related changes, read the exact base and head of the +RFC, registry, smoke, and relevant CI files. The current required checks are +`Sign-off` and `merge-gate`; the semantic smoke is currently executed through +the default Python test path, while Full Public Smokes is a post-merge/scheduled +confirmation surface rather than a PR-required check. Green CI proves only the +checks that ran and does not prove whole-program semantic convergence. + +Use this repair map when a check fails: + +| Failure family | What it means | Minimum repair | Do not repair by | +| --- | --- | --- | --- | +| `Sign-off` | One commit in the PR range lacks a valid DCO trailer | Add `Signed-off-by` to every affected commit with `git commit --amend -s` or an equivalent history repair; verify the full range | Signing only the newest commit | +| semantic smoke: unregistered value | A recognised carrier/field form introduced a value outside the registry | Reuse the existing owner value, or add the value with its owner, slot, scope, tests, and RFC evidence | Registering an unrelated string to silence the error | +| semantic smoke: stale inventory | The committed generated map no longer matches the indexed source tree | Stage intended source paths, run `python3.11 scripts/generate_semantic_inventory.py`, then `--check` | Editing counts by hand or including private/untracked files | +| semantic smoke: owner/parity | A defining symbol or Python/TypeScript value set diverged | Restore the single owner or deliberately update both runtime owners with parity evidence | Adding a second silent authority | +| semantic smoke: projection | A source value is unmapped, mapped to the wrong target, or should be rejected explicitly | Update the declared mapping and executable owner together, then test the boundary case | Deleting a source value without compatibility analysis | +| semantic smoke: budget/anchor | Measured debt grew or the guard was weakened | Fix the underlying duplicate/coverage issue and lower a budget only when the measured debt really fell | Raising the budget, narrowing the scan root, or renaming to hide drift | +| `merge-gate` | A required upstream CI job failed, was skipped unexpectedly, or has incomplete qualification | Inspect `needs` and the failing job, fix the owning path, and rerun at the same head | Treating a local smoke as proof that the remote gate is complete | + +For every failure, publish the exact head, affected constraint, observed output, +minimum repair, non-repair that would only hide the signal, rerun command, and +remaining unknown boundary. A dynamic producer or consumer that the bounded +scanner cannot classify is `unknown`; it is not evidence that the value is +absent or safe. Missing semantic evidence is `not_yet_proven` and blocks an +approval for an applicable semantic-alignment row. + The per-actionable-PR `pull_request_review_plan_v1` records the exact target, applicability, required evidence ids, and an initially `unverified` `pull_request_review_result_v1` skeleton. Metadata, labels, file counts, risk diff --git a/loopx/capabilities/pr_review_queue/__init__.py b/loopx/capabilities/pr_review_queue/__init__.py index 387298cc13..d96b806797 100644 --- a/loopx/capabilities/pr_review_queue/__init__.py +++ b/loopx/capabilities/pr_review_queue/__init__.py @@ -13,6 +13,7 @@ build_review_execution_contract, build_review_plan, build_review_template, + build_semantic_alignment_context, ) from .selection_execution import ( exact_head_key, @@ -42,6 +43,7 @@ "build_review_execution_contract", "build_review_plan", "build_review_template", + "build_semantic_alignment_context", "build_scheduling_policy", "DEFAULT_REVIEW_PRIORITY", "classify_scheduling_lane", diff --git a/loopx/capabilities/pr_review_queue/result_check.py b/loopx/capabilities/pr_review_queue/result_check.py index d3daba306a..3050385809 100644 --- a/loopx/capabilities/pr_review_queue/result_check.py +++ b/loopx/capabilities/pr_review_queue/result_check.py @@ -3,7 +3,11 @@ from collections.abc import Mapping from typing import Any -from .review_contract import build_review_execution_contract, build_review_plan +from .review_contract import ( + SEMANTIC_CANDIDATE_DECISIONS, + build_review_execution_contract, + build_review_plan, +) def _missing(value: object) -> bool: @@ -146,6 +150,12 @@ def check_review_result( blockers.append(f"{key}:missing_evidence_detail") if status == "verified": requirement = requirements[key] + if key == "semantic_alignment": + decision = row.get("candidate_decision") + if decision not in SEMANTIC_CANDIDATE_DECISIONS: + blockers.append("semantic_alignment:invalid_candidate_decision") + if decision == "unknown" and row.get("verdict") != "not_yet_proven": + blockers.append("semantic_alignment:unknown_requires_not_yet_proven") _require_fields( blockers, evidence_id=key, diff --git a/loopx/capabilities/pr_review_queue/review_contract.py b/loopx/capabilities/pr_review_queue/review_contract.py index 2b3287ddde..11cd2ab65a 100644 --- a/loopx/capabilities/pr_review_queue/review_contract.py +++ b/loopx/capabilities/pr_review_queue/review_contract.py @@ -4,7 +4,7 @@ from typing import Any # Increment when review requirements change without changing the packet shape. -REVIEW_POLICY_REVISION = 3 +REVIEW_POLICY_REVISION = 4 REQUIRED_FINAL_SECTIONS = [ "动机", @@ -27,6 +27,68 @@ NEGATIVE_PATH_AREAS = CODE_AREAS | BEHAVIORAL_POLICY_AREAS +SEMANTIC_CONTRACT_PATH_PREFIXES = ( + "loopx/semantics/", + "examples/semantic-vocabulary", + "tests/architecture/test_semantic_vocabulary", + "docs/architecture/rfcs/semantic-vocabulary-convergence-v0", + "scripts/generate_semantic_inventory.py", +) +SEMANTIC_CI_CONSTRAINT_PATHS = ( + ".github/workflows/python-tests.yml", + ".github/workflows/dco.yml", + ".github/workflows/full-public-smokes.yml", + ".github/GOVERNANCE.md", + "scripts/ci/review_gate.py", +) +SEMANTIC_CANDIDATE_DECISIONS = ( + "reuse_existing", + "extend_vocabulary", + "create_vocabulary", + "local_only", + "external_input", + "compatibility_only", + "unknown", +) + + +def build_semantic_alignment_context( + files: Sequence[Mapping[str, Any]], +) -> dict[str, Any]: + """Describe when a PR must account for vocabulary and CI constraints. + + This is a routing signal, not a semantic detector. It makes the current + constraint sources visible to the review agent while leaving the final + architecture judgment in the structured evidence block. + """ + paths = [str(item.get("path") or "") for item in files if item.get("path")] + semantic_paths = sorted( + path + for path in paths + if path.startswith(SEMANTIC_CONTRACT_PATH_PREFIXES) + ) + ci_paths = sorted( + path + for path in paths + if path in SEMANTIC_CI_CONSTRAINT_PATHS + ) + return { + "applicable": bool(semantic_paths or ci_paths), + "semantic_contract_paths": semantic_paths, + "ci_constraint_paths": ci_paths, + "source_of_truth": [ + "docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md", + "loopx/semantics/vocabulary_v0.json", + "examples/semantic-vocabulary-drift-smoke.py", + ".github/workflows/python-tests.yml", + ".github/workflows/dco.yml", + ], + "current_required_checks": ["Sign-off", "merge-gate"], + "current_semantic_scope": ( + "M0 structural owner/parity/projection/inventory checks; M0.5 producer and scope checks are planned, not implied by registry metadata." + ), + } + def _as_mapping(value: Any) -> Mapping[str, Any]: return value if isinstance(value, Mapping) else {} @@ -89,12 +151,12 @@ def build_review_template(item: Mapping[str, Any]) -> dict[str, Any]: _section( "对主干的风险", "250-500字", - "Use `failure_analysis`, `walkthroughs.negative`, and `validation_matrix`; trace each finding from triggering state to observed outcome and minimum repair. When `scope_fit` applies, name the active production caller or explicitly record a coverage-only boundary. When `change_proportionality` applies, compare verified problem impact with mechanism and maintenance cost; a resolved implementation blocker does not justify approval when the full exact-head scope remains disproportionate. For opt-in changes, prove disabled-path parity through `default_off_isolation`; do not infer isolation from an absent feature object. Use `authority_semantics` to verify that public protocol names do not claim a broader actor lifecycle or authority model than the implementation provides. Surface typed-state-rule, domain-neutrality, behavior-change-disclosure, and guidance-vs-obligation findings when their evidence applies.", + "Use `failure_analysis`, `walkthroughs.negative`, and `validation_matrix`; trace each finding from triggering state to observed outcome and minimum repair. When `scope_fit` applies, name the active production caller or explicitly record a coverage-only boundary. When `change_proportionality` applies, compare verified problem impact with mechanism and maintenance cost; a resolved implementation blocker does not justify approval when the full exact-head scope remains disproportionate. For opt-in changes, prove disabled-path parity through `default_off_isolation`; do not infer isolation from an absent feature object. Use `authority_semantics` to verify that public protocol names do not claim a broader actor lifecycle or authority model than the implementation provides. When `semantic_alignment` applies, include a concise `### 语义与 CI 对齐` subsection with the affected constraint, failure family, minimum repair, and non-repair that would only hide the signal. Surface typed-state-rule, domain-neutrality, behavior-change-disclosure, and guidance-vs-obligation findings when their evidence applies.", ), _section( "我的整体评价", "150-300字", - "Use `observable_semantics` to report baseline/head comparisons and remaining compatibility gaps; equal decision codes are insufficient. Use `code_volume`, `change_proportionality`, `default_off_isolation`, `authority_semantics`, validation results, residual risk, and exact-head freshness to state the verdict and the evidence needed for re-review.", + "Use `observable_semantics` to report baseline/head comparisons and remaining compatibility gaps; equal decision codes are insufficient. Use `code_volume`, `change_proportionality`, `default_off_isolation`, `authority_semantics`, validation results, residual risk, and exact-head freshness to state the verdict and the evidence needed for re-review. For semantic or constraint-related changes, state whether the PR reuses an existing vocabulary, extends one, creates one, stays local, or remains unknown, and link any required registry/RFC/CI repair.", ), ], "review_order": _review_order(key_files), @@ -187,6 +249,50 @@ def build_review_execution_contract(*, wait_for_ci: bool = True) -> dict[str, An "failure_or_retry_owner", ], }, + { + "evidence_id": "semantic_alignment", + "required_when": "semantic_alignment_required", + "verdict_values": [ + "aligned", + "new_semantics_justified", + "not_applicable", + "not_yet_proven", + ], + "fields": [ + "semantic_surface_classification", + "ci_constraints_considered", + "candidate_decision", + "affected_vocabulary_slot_scope", + "owner_and_reuse_evidence", + "producer_consumer_or_persistence_impact", + "failure_family_and_minimum_repair", + "non_repairs_that_only_hide_drift", + "unknown_or_unproved_boundary", + "validation_commands", + "verdict", + ], + "candidate_decisions": list(SEMANTIC_CANDIDATE_DECISIONS), + "rule": ( + "For every code change, and for changes touching the semantic registry, " + "semantic smoke, semantic RFC, or the required CI constraint paths, " + "make the alignment decision explicit. Read the exact base and head " + "versions of the semantic RFC, registry, smoke, and relevant CI files. " + "Report the current required checks (`Sign-off`, `merge-gate`) and the " + "semantic smoke's actual scope. Classify a candidate as reuse, extension, " + "new vocabulary, local-only, external input, compatibility-only, or " + "unknown. A green CI result proves only the checks that ran; it does not " + "prove whole-program semantic convergence. For a semantic failure, give " + "the minimum repair: update the owner/registry, regenerate inventory, " + "repair the projection, or run the required compatibility evidence. " + "Explicitly reject hiding the failure by renaming a symbol, raising a " + "budget, narrowing the scan root, or registering an unrelated value. " + "If the change is ordinary code with no semantic contract impact, mark " + "`not_applicable` and explain the checked paths and why no new field, " + "slot, producer, consumer domain, projection, or persistence contract " + "was introduced. unknown dynamic paths remain visible and are not " + "treated as proof of absence." + ), + }, { "evidence_id": "repository_reuse", "required_when": "behavior_bearing_change", @@ -847,6 +953,7 @@ def build_review_execution_contract(*, wait_for_ci: bool = True) -> dict[str, An "misleading", "not_yet_proven", ], + "semantic_alignment": ["not_yet_proven"], }, "required_final_sections": REQUIRED_FINAL_SECTIONS, }, @@ -869,6 +976,11 @@ def build_review_execution_contract(*, wait_for_ci: bool = True) -> dict[str, An "or not_yet_proven; correctness, green CI, and resolved earlier " "findings cannot override this gate" ), + "open_pr_unresolved_semantic_alignment": ( + "REQUEST_CHANGES when semantic_alignment is not_yet_proven; " + "the review must identify the affected CI or vocabulary boundary, " + "minimum repair, and any unknown dynamic path" + ), "materially_expanded_rereview": ( "Reset change_proportionality from the original problem and review " "the full exact head; do not inherit an approval trajectory from " @@ -904,6 +1016,16 @@ def build_review_plan(item: Mapping[str, Any]) -> dict[str, Any]: smoke_or_example_only = bool(areas & EXAMPLE_OR_SMOKE_AREAS) and not ( code_change or behavioral_policy_change ) + semantic_context = item.get("semantic_alignment_context") + if not isinstance(semantic_context, Mapping): + semantic_context = build_semantic_alignment_context( + [ + file + for file in _as_sequence(item.get("key_files")) + if isinstance(file, Mapping) + ] + ) + semantic_alignment_required = code_change or bool(semantic_context.get("applicable")) required_evidence = [ "problem_context", "architecture_flow", @@ -935,6 +1057,8 @@ def build_review_plan(item: Mapping[str, Any]) -> dict[str, Any]: required_evidence.append("guidance_vs_obligation") if smoke_or_example_only: required_evidence.append("durable_smoke_value") + if semantic_alignment_required: + required_evidence.append("semantic_alignment") number = item.get("number") head_oid = str(item.get("head_oid") or "").strip() target_key = f"{number}@{head_oid}" if number and head_oid else None @@ -983,6 +1107,8 @@ def build_review_plan(item: Mapping[str, Any]) -> dict[str, Any]: "durable_smoke_value_required": smoke_or_example_only, "duplication_scan_required": smoke_or_example_only, "batch_pattern_scan_required": smoke_or_example_only, + "semantic_alignment_required": semantic_alignment_required, + "semantic_alignment_context": dict(semantic_context), }, "required_evidence_ids": required_evidence, "result_template": { diff --git a/loopx/pr_review.py b/loopx/pr_review.py index c634620130..8aaa15606c 100644 --- a/loopx/pr_review.py +++ b/loopx/pr_review.py @@ -17,6 +17,7 @@ community_feedback_ready, exact_head_key, materialize_review_execution, + build_semantic_alignment_context, normalize_fresh_audit_exact_heads, normalize_review_priority, scheduling_sort_key, @@ -999,6 +1000,7 @@ def _normalize_pr( }, "areas": _area_counts(files), "key_files": files[:10], + "semantic_alignment_context": build_semantic_alignment_context(files), "commit_headlines": _commit_headlines(pr), "checks": checks, "wait_for_ci": wait_for_ci, diff --git a/tests/capabilities/test_pr_review_contract.py b/tests/capabilities/test_pr_review_contract.py index 4d3b987393..f74f936665 100644 --- a/tests/capabilities/test_pr_review_contract.py +++ b/tests/capabilities/test_pr_review_contract.py @@ -81,6 +81,7 @@ def test_execution_contract_owns_deep_review_requirements() -> None: "behavior_change_disclosure", "guidance_vs_obligation", "durable_smoke_value", + "semantic_alignment", } assert requirements["symbol_map"]["item_count"] == { "minimum": 2, @@ -113,6 +114,19 @@ def test_execution_contract_owns_deep_review_requirements() -> None: assert "maintenance_and_migration_cost" in proportionality["fields"] assert "green CI" in proportionality["rule"] assert "original problem" in proportionality["rule"] + semantic = requirements["semantic_alignment"] + assert semantic["required_when"] == "semantic_alignment_required" + assert set(semantic["candidate_decisions"]) == { + "reuse_existing", + "extend_vocabulary", + "create_vocabulary", + "local_only", + "external_input", + "compatibility_only", + "unknown", + } + assert "raising a budget" in semantic["rule"] + assert "unknown dynamic paths" in semantic["rule"] isolation = requirements["default_off_isolation"] assert isolation["required_when"] == "behavior_bearing_change" assert isolation["verdict_values"] == [ @@ -148,6 +162,7 @@ def test_execution_contract_owns_deep_review_requirements() -> None: "change_proportionality": ["disproportionate", "not_yet_proven"], "default_off_isolation": ["not_isolated", "not_yet_proven"], "authority_semantics": ["misleading", "not_yet_proven"], + "semantic_alignment": ["not_yet_proven"], } assert contract["finding_contract"]["findings_first"] is True verdict = contract["verdict_policy"] @@ -329,6 +344,36 @@ def test_non_behavior_review_keeps_existing_coverage_policy(area: str) -> None: assert "repository_reuse" not in plan["required_evidence_ids"] +def test_code_review_requires_semantic_alignment_even_when_no_known_path_matches() -> None: + plan = build_review_plan(_item(areas={"product_runtime": 1})) + + assert plan["applicability"]["semantic_alignment_required"] is True + assert "semantic_alignment" in plan["required_evidence_ids"] + context = plan["applicability"]["semantic_alignment_context"] + assert context["applicable"] is False + assert context["current_required_checks"] == ["Sign-off", "merge-gate"] + + +def test_semantic_alignment_context_marks_registry_and_constraint_paths() -> None: + from loopx.capabilities.pr_review_queue import build_semantic_alignment_context + + context = build_semantic_alignment_context( + [ + {"path": "loopx/semantics/vocabulary_v0.json"}, + {"path": ".github/workflows/python-tests.yml"}, + {"path": "docs/README.md"}, + ] + ) + + assert context["applicable"] is True + assert context["semantic_contract_paths"] == [ + "loopx/semantics/vocabulary_v0.json" + ] + assert context["ci_constraint_paths"] == [ + ".github/workflows/python-tests.yml" + ] + + def test_reuse_evidence_compares_semantics_beyond_the_diff() -> None: contract = build_agent_response_contract()["review_execution_contract"] reuse = next( diff --git a/tests/capabilities/test_pr_review_result_check.py b/tests/capabilities/test_pr_review_result_check.py index 6c7b3d131e..e381403916 100644 --- a/tests/capabilities/test_pr_review_result_check.py +++ b/tests/capabilities/test_pr_review_result_check.py @@ -38,6 +38,8 @@ def _review(): ) if "verdict_values" in requirement: row["verdict"] = requirement["verdict_values"][0] + if key == "semantic_alignment": + row["candidate_decision"] = "local_only" if "items_field" in requirement: item_fields = requirement.get("item_fields", []) if "required_cases" in requirement: @@ -78,6 +80,26 @@ def test_result_check_is_not_semantic_or_merge_authority(): assert not checked["external_writes_performed"] +@pytest.mark.parametrize( + ("candidate_decision", "verdict", "blocker"), + [ + ("made_up", "aligned", "semantic_alignment:invalid_candidate_decision"), + ("unknown", "aligned", "semantic_alignment:unknown_requires_not_yet_proven"), + ], +) +def test_semantic_alignment_cannot_hide_unknown_or_invalid_candidate( + candidate_decision: str, verdict: str, blocker: str +) -> None: + packet, result = _review() + row = result["evidence"]["semantic_alignment"] + row["candidate_decision"] = candidate_decision + row["verdict"] = verdict + checked = check_review_result(packet, result) + + assert blocker in checked["approval_blockers"] + assert not checked["approval_consistent"] + + @pytest.mark.parametrize( "kind", ["missing", "unverified", "empty", "blocking", "finding", "unknown_verdict"] ) From 92f9e36c6b7de38d8163cbad87153f468df62248 Mon Sep 17 00:00:00 2001 From: song Date: Tue, 15 Sep 2026 23:34:43 +0800 Subject: [PATCH 4/9] chore(semantics): refresh inventory for review contract Signed-off-by: song --- loopx/semantics/inventory_v0.json | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/loopx/semantics/inventory_v0.json b/loopx/semantics/inventory_v0.json index d5620542d4..2455b90c15 100644 --- a/loopx/semantics/inventory_v0.json +++ b/loopx/semantics/inventory_v0.json @@ -238,6 +238,9 @@ {"name": "BEHAVIORAL_POLICY_AREAS", "module": "loopx/capabilities/pr_review_queue/review_contract.py", "container": "set", "values": ["public_entry_or_policy", "agent_instruction_surface"]}, {"name": "CODE_AREAS", "module": "loopx/capabilities/pr_review_queue/review_contract.py", "container": "set", "values": ["product_runtime", "app_or_ui_surface", "ci_or_release", "build_or_config"]}, {"name": "REQUIRED_FINAL_SECTIONS", "module": "loopx/capabilities/pr_review_queue/review_contract.py", "container": "list", "values": ["动机", "改动思路", "具体改动", "对主干的风险", "我的整体评价"]}, + {"name": "SEMANTIC_CANDIDATE_DECISIONS", "module": "loopx/capabilities/pr_review_queue/review_contract.py", "container": "tuple", "values": ["reuse_existing", "extend_vocabulary", "create_vocabulary", "local_only", "external_input", "compatibility_only", "unknown"]}, + {"name": "SEMANTIC_CI_CONSTRAINT_PATHS", "module": "loopx/capabilities/pr_review_queue/review_contract.py", "container": "tuple", "values": [".github/workflows/python-tests.yml", ".github/workflows/dco.yml", ".github/workflows/full-public-smokes.yml", ".github/GOVERNANCE.md", "scripts/ci/review_gate.py"]}, + {"name": "SEMANTIC_CONTRACT_PATH_PREFIXES", "module": "loopx/capabilities/pr_review_queue/review_contract.py", "container": "tuple", "values": ["loopx/semantics/", "examples/semantic-vocabulary", "tests/architecture/test_semantic_vocabulary", "docs/architecture/rfcs/semantic-vocabulary-convergence-v0", "scripts/generate_semantic_inventory.py"]}, {"name": "CAPABILITY_ORIGINS", "module": "loopx/capabilities/registry.py", "container": "frozenset", "values": ["builtin", "extension"]}, {"name": "CAPABILITY_VISIBILITIES", "module": "loopx/capabilities/registry.py", "container": "frozenset", "values": ["public", "internal"]}, {"name": "REQUIRED_CAPABILITY_FIELDS", "module": "loopx/capabilities/registry.py", "container": "tuple", "values": ["id", "title", "status", "user_value", "next_real_step"]}, @@ -904,7 +907,7 @@ "summary": { "source_files": 1175, "python_enums": 103, - "python_closed_sets": 495, + "python_closed_sets": 498, "python_literal_aliases": 8, "typescript_const_arrays": 40, "named_string_constants": 2031, From 6902499cff279147ac1c23dec9bae6455e78ad15 Mon Sep 17 00:00:00 2001 From: song Date: Wed, 16 Sep 2026 00:17:51 +0800 Subject: [PATCH 5/9] fix(pr-review): scope semantic evidence to affected contracts Signed-off-by: song --- examples/pr-review-command-smoke.py | 2 + .../capabilities/pr_review_queue/__init__.py | 2 - .../pr_review_queue/result_check.py | 30 +++- .../pr_review_queue/review_contract.py | 144 ++++++------------ loopx/pr_review.py | 2 - loopx/semantics/inventory_v0.json | 4 +- skills/loopx-pr-review/SKILL.md | 2 +- tests/capabilities/test_pr_review_contract.py | 48 +++--- .../test_pr_review_result_check.py | 128 +++++++++++++++- 9 files changed, 222 insertions(+), 140 deletions(-) diff --git a/examples/pr-review-command-smoke.py b/examples/pr-review-command-smoke.py index f61375bc5a..6e0bbd1129 100644 --- a/examples/pr-review-command-smoke.py +++ b/examples/pr-review-command-smoke.py @@ -910,6 +910,7 @@ def fake_run_gh_json(args: list[str], *, cwd: Path | None = None) -> object: "behavior_change_disclosure", "guidance_vs_obligation", "durable_smoke_value", + "semantic_alignment", }, requirements assert requirements["symbol_map"]["item_count"] == {"minimum": 2, "maximum": 5} assert "caller_evidence" in requirements["symbol_map"]["item_fields"] @@ -966,6 +967,7 @@ def fake_run_gh_json(args: list[str], *, cwd: Path | None = None) -> object: "change_proportionality": ["disproportionate", "not_yet_proven"], "default_off_isolation": ["not_isolated", "not_yet_proven"], "authority_semantics": ["misleading", "not_yet_proven"], + "semantic_alignment": ["not_yet_proven", "violated"], } assert execution["finding_contract"]["findings_first"] is True first_plan = first["review_plan"] diff --git a/loopx/capabilities/pr_review_queue/__init__.py b/loopx/capabilities/pr_review_queue/__init__.py index d96b806797..387298cc13 100644 --- a/loopx/capabilities/pr_review_queue/__init__.py +++ b/loopx/capabilities/pr_review_queue/__init__.py @@ -13,7 +13,6 @@ build_review_execution_contract, build_review_plan, build_review_template, - build_semantic_alignment_context, ) from .selection_execution import ( exact_head_key, @@ -43,7 +42,6 @@ "build_review_execution_contract", "build_review_plan", "build_review_template", - "build_semantic_alignment_context", "build_scheduling_policy", "DEFAULT_REVIEW_PRIORITY", "classify_scheduling_lane", diff --git a/loopx/capabilities/pr_review_queue/result_check.py b/loopx/capabilities/pr_review_queue/result_check.py index 3050385809..92b246bfe5 100644 --- a/loopx/capabilities/pr_review_queue/result_check.py +++ b/loopx/capabilities/pr_review_queue/result_check.py @@ -135,7 +135,11 @@ def check_review_result( if not isinstance(evidence, Mapping): evidence = {} errors.append("evidence_not_object") - for key in plan["required_evidence_ids"]: + evidence_ids = list(plan["required_evidence_ids"]) + # Contract findings supplied for docs-only reviews still constrain approval. + if "semantic_alignment" in evidence and "semantic_alignment" not in evidence_ids: + evidence_ids.append("semantic_alignment") + for key in evidence_ids: row = evidence.get(key) if not isinstance(row, Mapping): blockers.append(f"{key}:missing") @@ -152,16 +156,34 @@ def check_review_result( requirement = requirements[key] if key == "semantic_alignment": decision = row.get("candidate_decision") - if decision not in SEMANTIC_CANDIDATE_DECISIONS: + verdict = row.get("verdict") + if (verdict != "not_applicable" or decision is not None) and ( + decision not in SEMANTIC_CANDIDATE_DECISIONS + ): blockers.append("semantic_alignment:invalid_candidate_decision") - if decision == "unknown" and row.get("verdict") != "not_yet_proven": - blockers.append("semantic_alignment:unknown_requires_not_yet_proven") + if decision == "unknown" and verdict not in ( + "advisory", "not_yet_proven", "violated" + ): + blockers.append("semantic_alignment:unknown_cannot_claim_alignment") + if verdict == "not_applicable" and decision in ( + "extend_vocabulary", "create_vocabulary", "compatibility_only" + ): + blockers.append("semantic_alignment:contract_change_requires_evidence") _require_fields( blockers, evidence_id=key, value=row, fields=requirement.get("fields"), ) + fields_by_verdict = requirement.get("fields_by_verdict", {}) + verdict = row.get("verdict") + if isinstance(verdict, str): + _require_fields( + blockers, + evidence_id=key, + value=row, + fields=fields_by_verdict.get(verdict), + ) items = _require_items( blockers, evidence_id=key, diff --git a/loopx/capabilities/pr_review_queue/review_contract.py b/loopx/capabilities/pr_review_queue/review_contract.py index 11cd2ab65a..ac107176ae 100644 --- a/loopx/capabilities/pr_review_queue/review_contract.py +++ b/loopx/capabilities/pr_review_queue/review_contract.py @@ -4,7 +4,7 @@ from typing import Any # Increment when review requirements change without changing the packet shape. -REVIEW_POLICY_REVISION = 4 +REVIEW_POLICY_REVISION = 5 REQUIRED_FINAL_SECTIONS = [ "动机", @@ -27,20 +27,6 @@ NEGATIVE_PATH_AREAS = CODE_AREAS | BEHAVIORAL_POLICY_AREAS -SEMANTIC_CONTRACT_PATH_PREFIXES = ( - "loopx/semantics/", - "examples/semantic-vocabulary", - "tests/architecture/test_semantic_vocabulary", - "docs/architecture/rfcs/semantic-vocabulary-convergence-v0", - "scripts/generate_semantic_inventory.py", -) -SEMANTIC_CI_CONSTRAINT_PATHS = ( - ".github/workflows/python-tests.yml", - ".github/workflows/dco.yml", - ".github/workflows/full-public-smokes.yml", - ".github/GOVERNANCE.md", - "scripts/ci/review_gate.py", -) SEMANTIC_CANDIDATE_DECISIONS = ( "reuse_existing", "extend_vocabulary", @@ -52,44 +38,6 @@ ) -def build_semantic_alignment_context( - files: Sequence[Mapping[str, Any]], -) -> dict[str, Any]: - """Describe when a PR must account for vocabulary and CI constraints. - - This is a routing signal, not a semantic detector. It makes the current - constraint sources visible to the review agent while leaving the final - architecture judgment in the structured evidence block. - """ - paths = [str(item.get("path") or "") for item in files if item.get("path")] - semantic_paths = sorted( - path - for path in paths - if path.startswith(SEMANTIC_CONTRACT_PATH_PREFIXES) - ) - ci_paths = sorted( - path - for path in paths - if path in SEMANTIC_CI_CONSTRAINT_PATHS - ) - return { - "applicable": bool(semantic_paths or ci_paths), - "semantic_contract_paths": semantic_paths, - "ci_constraint_paths": ci_paths, - "source_of_truth": [ - "docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md", - "loopx/semantics/vocabulary_v0.json", - "examples/semantic-vocabulary-drift-smoke.py", - ".github/workflows/python-tests.yml", - ".github/workflows/dco.yml", - ], - "current_required_checks": ["Sign-off", "merge-gate"], - "current_semantic_scope": ( - "M0 structural owner/parity/projection/inventory checks; M0.5 producer and scope checks are planned, not implied by registry metadata." - ), - } - - def _as_mapping(value: Any) -> Mapping[str, Any]: return value if isinstance(value, Mapping) else {} @@ -151,7 +99,7 @@ def build_review_template(item: Mapping[str, Any]) -> dict[str, Any]: _section( "对主干的风险", "250-500字", - "Use `failure_analysis`, `walkthroughs.negative`, and `validation_matrix`; trace each finding from triggering state to observed outcome and minimum repair. When `scope_fit` applies, name the active production caller or explicitly record a coverage-only boundary. When `change_proportionality` applies, compare verified problem impact with mechanism and maintenance cost; a resolved implementation blocker does not justify approval when the full exact-head scope remains disproportionate. For opt-in changes, prove disabled-path parity through `default_off_isolation`; do not infer isolation from an absent feature object. Use `authority_semantics` to verify that public protocol names do not claim a broader actor lifecycle or authority model than the implementation provides. When `semantic_alignment` applies, include a concise `### 语义与 CI 对齐` subsection with the affected constraint, failure family, minimum repair, and non-repair that would only hide the signal. Surface typed-state-rule, domain-neutrality, behavior-change-disclosure, and guidance-vs-obligation findings when their evidence applies.", + "Use `failure_analysis`, `walkthroughs.negative`, and `validation_matrix`; trace each finding from triggering state to observed outcome and minimum repair. When `scope_fit` applies, name the active production caller or explicitly record a coverage-only boundary. When `change_proportionality` applies, compare verified problem impact with mechanism and maintenance cost; a resolved implementation blocker does not justify approval when the full exact-head scope remains disproportionate. For opt-in changes, prove disabled-path parity through `default_off_isolation`; do not infer isolation from an absent feature object. Use `authority_semantics` to verify that public protocol names do not claim a broader actor lifecycle or authority model than the implementation provides. For a `semantic_alignment` contract impact or finding, include a concise `### 语义与 CI 对齐` subsection; ordinary `not_applicable` triage needs no separate subsection. For a blocker, name the current obligation, triggering change, observed evidence, minimum repair and rerun command. Surface typed-state-rule, domain-neutrality, behavior-change-disclosure, and guidance-vs-obligation findings when their evidence applies.", ), _section( "我的整体评价", @@ -256,41 +204,46 @@ def build_review_execution_contract(*, wait_for_ci: bool = True) -> dict[str, An "aligned", "new_semantics_justified", "not_applicable", + "advisory", "not_yet_proven", + "violated", ], - "fields": [ - "semantic_surface_classification", - "ci_constraints_considered", - "candidate_decision", - "affected_vocabulary_slot_scope", - "owner_and_reuse_evidence", - "producer_consumer_or_persistence_impact", - "failure_family_and_minimum_repair", - "non_repairs_that_only_hide_drift", - "unknown_or_unproved_boundary", - "validation_commands", - "verdict", - ], + "fields": ["checked_scope", "impact_reason", "verdict"], + "fields_by_verdict": { + "not_applicable": [], + "aligned": ["candidate_decision", "affected_contract", "evidence_refs"], + "new_semantics_justified": ["candidate_decision", "affected_contract", "evidence_refs"], + "advisory": ["candidate_decision", "analysis_limit"], + "not_yet_proven": [ + "candidate_decision", "affected_contract", "trigger", + "observed_evidence", "minimum_repair", "validation_commands", + ], + "violated": [ + "candidate_decision", "affected_contract", "trigger", + "observed_evidence", "minimum_repair", "validation_commands", + ], + }, "candidate_decisions": list(SEMANTIC_CANDIDATE_DECISIONS), "rule": ( - "For every code change, and for changes touching the semantic registry, " - "semantic smoke, semantic RFC, or the required CI constraint paths, " - "make the alignment decision explicit. Read the exact base and head " - "versions of the semantic RFC, registry, smoke, and relevant CI files. " - "Report the current required checks (`Sign-off`, `merge-gate`) and the " - "semantic smoke's actual scope. Classify a candidate as reuse, extension, " - "new vocabulary, local-only, external input, compatibility-only, or " - "unknown. A green CI result proves only the checks that ran; it does not " - "prove whole-program semantic convergence. For a semantic failure, give " - "the minimum repair: update the owner/registry, regenerate inventory, " - "repair the projection, or run the required compatibility evidence. " - "Explicitly reject hiding the failure by renaming a symbol, raising a " - "budget, narrowing the scan root, or registering an unrelated value. " - "If the change is ordinary code with no semantic contract impact, mark " - "`not_applicable` and explain the checked paths and why no new field, " - "slot, producer, consumer domain, projection, or persistence contract " - "was introduced. unknown dynamic paths remain visible and are not " - "treated as proof of absence." + "Start with bounded triage of the full diff and relevant definitions/callers. " + "Record checked_scope and impact_reason. If no shared contract is affected, " + "use not_applicable and stop; no candidate_decision or full RFC read is required. " + "File previews and unchanged registry paths do not prove absence of impact. " + "For shared values, owners, consumers, projections or persistence changes, " + "read only affected base/head contracts and reuse repository_reuse, " + "observable_semantics and validation_matrix evidence through evidence_refs. " + "Resolve CI obligations from the target repository's current policy; " + "observed check names alone do not establish which checks are required. " + "unknown due solely to bounded analysis is advisory: state analysis_limit " + "and why no affected current obligation lacks required evidence. It is not " + "proof of safety. Use not_yet_proven for missing required evidence on an " + "affected current contract, or violated for a concrete violation. Both block " + "approval and must name the contract, PR trigger, observed evidence, minimum " + "repair and rerun command. Advisory cannot override a required CI failure " + "or concrete blocking finding. Do not promote future/advisory RFC properties " + "to current obligations. Reject hiding a failure by renaming a symbol, " + "raising a budget, narrowing the scan root or registering an unrelated value. " + "Docs-only reviews may supply this same row when contract impact is found." ), }, { @@ -953,7 +906,7 @@ def build_review_execution_contract(*, wait_for_ci: bool = True) -> dict[str, An "misleading", "not_yet_proven", ], - "semantic_alignment": ["not_yet_proven"], + "semantic_alignment": ["not_yet_proven", "violated"], }, "required_final_sections": REQUIRED_FINAL_SECTIONS, }, @@ -977,9 +930,10 @@ def build_review_execution_contract(*, wait_for_ci: bool = True) -> dict[str, An "findings cannot override this gate" ), "open_pr_unresolved_semantic_alignment": ( - "REQUEST_CHANGES when semantic_alignment is not_yet_proven; " - "the review must identify the affected CI or vocabulary boundary, " - "minimum repair, and any unknown dynamic path" + "REQUEST_CHANGES for semantic_alignment not_yet_proven or violated: " + "name the affected current contract, PR trigger, observed evidence, " + "minimum repair and rerun command. A bounded-analysis advisory alone " + "does not block approval or override other required checks." ), "materially_expanded_rereview": ( "Reset change_proportionality from the original problem and review " @@ -1016,16 +970,7 @@ def build_review_plan(item: Mapping[str, Any]) -> dict[str, Any]: smoke_or_example_only = bool(areas & EXAMPLE_OR_SMOKE_AREAS) and not ( code_change or behavioral_policy_change ) - semantic_context = item.get("semantic_alignment_context") - if not isinstance(semantic_context, Mapping): - semantic_context = build_semantic_alignment_context( - [ - file - for file in _as_sequence(item.get("key_files")) - if isinstance(file, Mapping) - ] - ) - semantic_alignment_required = code_change or bool(semantic_context.get("applicable")) + semantic_alignment_required = behavior_bearing_change required_evidence = [ "problem_context", "architecture_flow", @@ -1108,7 +1053,6 @@ def build_review_plan(item: Mapping[str, Any]) -> dict[str, Any]: "duplication_scan_required": smoke_or_example_only, "batch_pattern_scan_required": smoke_or_example_only, "semantic_alignment_required": semantic_alignment_required, - "semantic_alignment_context": dict(semantic_context), }, "required_evidence_ids": required_evidence, "result_template": { diff --git a/loopx/pr_review.py b/loopx/pr_review.py index 8aaa15606c..c634620130 100644 --- a/loopx/pr_review.py +++ b/loopx/pr_review.py @@ -17,7 +17,6 @@ community_feedback_ready, exact_head_key, materialize_review_execution, - build_semantic_alignment_context, normalize_fresh_audit_exact_heads, normalize_review_priority, scheduling_sort_key, @@ -1000,7 +999,6 @@ def _normalize_pr( }, "areas": _area_counts(files), "key_files": files[:10], - "semantic_alignment_context": build_semantic_alignment_context(files), "commit_headlines": _commit_headlines(pr), "checks": checks, "wait_for_ci": wait_for_ci, diff --git a/loopx/semantics/inventory_v0.json b/loopx/semantics/inventory_v0.json index a3c8f7a538..6174790c25 100644 --- a/loopx/semantics/inventory_v0.json +++ b/loopx/semantics/inventory_v0.json @@ -239,8 +239,6 @@ {"name": "CODE_AREAS", "module": "loopx/capabilities/pr_review_queue/review_contract.py", "container": "set", "values": ["product_runtime", "app_or_ui_surface", "ci_or_release", "build_or_config"]}, {"name": "REQUIRED_FINAL_SECTIONS", "module": "loopx/capabilities/pr_review_queue/review_contract.py", "container": "list", "values": ["动机", "改动思路", "具体改动", "对主干的风险", "我的整体评价"]}, {"name": "SEMANTIC_CANDIDATE_DECISIONS", "module": "loopx/capabilities/pr_review_queue/review_contract.py", "container": "tuple", "values": ["reuse_existing", "extend_vocabulary", "create_vocabulary", "local_only", "external_input", "compatibility_only", "unknown"]}, - {"name": "SEMANTIC_CI_CONSTRAINT_PATHS", "module": "loopx/capabilities/pr_review_queue/review_contract.py", "container": "tuple", "values": [".github/workflows/python-tests.yml", ".github/workflows/dco.yml", ".github/workflows/full-public-smokes.yml", ".github/GOVERNANCE.md", "scripts/ci/review_gate.py"]}, - {"name": "SEMANTIC_CONTRACT_PATH_PREFIXES", "module": "loopx/capabilities/pr_review_queue/review_contract.py", "container": "tuple", "values": ["loopx/semantics/", "examples/semantic-vocabulary", "tests/architecture/test_semantic_vocabulary", "docs/architecture/rfcs/semantic-vocabulary-convergence-v0", "scripts/generate_semantic_inventory.py"]}, {"name": "CAPABILITY_ORIGINS", "module": "loopx/capabilities/registry.py", "container": "frozenset", "values": ["builtin", "extension"]}, {"name": "CAPABILITY_VISIBILITIES", "module": "loopx/capabilities/registry.py", "container": "frozenset", "values": ["public", "internal"]}, {"name": "REQUIRED_CAPABILITY_FIELDS", "module": "loopx/capabilities/registry.py", "container": "tuple", "values": ["id", "title", "status", "user_value", "next_real_step"]}, @@ -907,7 +905,7 @@ "summary": { "source_files": 1176, "python_enums": 103, - "python_closed_sets": 498, + "python_closed_sets": 496, "python_literal_aliases": 8, "typescript_const_arrays": 40, "named_string_constants": 2031, diff --git a/skills/loopx-pr-review/SKILL.md b/skills/loopx-pr-review/SKILL.md index 0569a5984a..3916f077fd 100644 --- a/skills/loopx-pr-review/SKILL.md +++ b/skills/loopx-pr-review/SKILL.md @@ -47,7 +47,7 @@ Do not pipe the only copy through `jq`. When an exhaustive request has `result_completeness.complete=false`, rerun with its `recommended_limit` before reviewing. -Require execution `policy_revision == 3`; a schema name alone is insufficient. +Require execution `policy_revision == 5`; a schema name alone is insufficient. If missing or unequal, do not publish APPROVE; a conservative REQUEST_CHANGES is allowed only when it names the incompatible-policy evidence gap. Do not retain expired temporary worktree overrides. Honor explicit runtime pins, but report diff --git a/tests/capabilities/test_pr_review_contract.py b/tests/capabilities/test_pr_review_contract.py index f74f936665..5b4873150d 100644 --- a/tests/capabilities/test_pr_review_contract.py +++ b/tests/capabilities/test_pr_review_contract.py @@ -126,7 +126,10 @@ def test_execution_contract_owns_deep_review_requirements() -> None: "unknown", } assert "raising a budget" in semantic["rule"] - assert "unknown dynamic paths" in semantic["rule"] + assert semantic["fields"] == ["checked_scope", "impact_reason", "verdict"] + assert semantic["fields_by_verdict"]["not_applicable"] == [] + assert "analysis_limit" in semantic["fields_by_verdict"]["advisory"] + assert "minimum_repair" in semantic["fields_by_verdict"]["not_yet_proven"] isolation = requirements["default_off_isolation"] assert isolation["required_when"] == "behavior_bearing_change" assert isolation["verdict_values"] == [ @@ -162,7 +165,7 @@ def test_execution_contract_owns_deep_review_requirements() -> None: "change_proportionality": ["disproportionate", "not_yet_proven"], "default_off_isolation": ["not_isolated", "not_yet_proven"], "authority_semantics": ["misleading", "not_yet_proven"], - "semantic_alignment": ["not_yet_proven"], + "semantic_alignment": ["not_yet_proven", "violated"], } assert contract["finding_contract"]["findings_first"] is True verdict = contract["verdict_policy"] @@ -344,34 +347,35 @@ def test_non_behavior_review_keeps_existing_coverage_policy(area: str) -> None: assert "repository_reuse" not in plan["required_evidence_ids"] -def test_code_review_requires_semantic_alignment_even_when_no_known_path_matches() -> None: +def test_code_review_requires_only_semantic_triage_before_contract_impact_is_known() -> None: plan = build_review_plan(_item(areas={"product_runtime": 1})) assert plan["applicability"]["semantic_alignment_required"] is True assert "semantic_alignment" in plan["required_evidence_ids"] - context = plan["applicability"]["semantic_alignment_context"] - assert context["applicable"] is False - assert context["current_required_checks"] == ["Sign-off", "merge-gate"] + assert "semantic_alignment_context" not in plan["applicability"] -def test_semantic_alignment_context_marks_registry_and_constraint_paths() -> None: - from loopx.capabilities.pr_review_queue import build_semantic_alignment_context - - context = build_semantic_alignment_context( - [ - {"path": "loopx/semantics/vocabulary_v0.json"}, - {"path": ".github/workflows/python-tests.yml"}, - {"path": "docs/README.md"}, - ] +@pytest.mark.parametrize("repo", ["huangruiteng/loopx", "example/service"]) +def test_semantic_triage_does_not_inject_repository_facts_or_infer_from_preview(repo: str) -> None: + item = _item(areas={"product_runtime": 1}) + item["repository"] = repo + item["key_files"] = [{"path": f"src/file_{i}.py"} for i in range(10)] + plan = build_review_plan(item) + item["key_files"].append({"path": "loopx/semantics/vocabulary_v0.json"}) + assert build_review_plan(item) == plan + semantic = next( + row for row in build_agent_response_contract()["review_execution_contract"]["evidence_requirements"] + if row["evidence_id"] == "semantic_alignment" ) + assert "Sign-off" not in json.dumps(semantic) + assert "merge-gate" not in json.dumps(semantic) + assert "loopx/semantics" not in json.dumps(semantic) - assert context["applicable"] is True - assert context["semantic_contract_paths"] == [ - "loopx/semantics/vocabulary_v0.json" - ] - assert context["ci_constraint_paths"] == [ - ".github/workflows/python-tests.yml" - ] + +def test_generated_inventory_does_not_create_a_detailed_review_obligation() -> None: + item = _item(areas={"public_docs": 1}) + item["key_files"] = [{"path": "loopx/semantics/inventory_v0.json"}] + assert "semantic_alignment" not in build_review_plan(item)["required_evidence_ids"] def test_reuse_evidence_compares_semantics_beyond_the_diff() -> None: diff --git a/tests/capabilities/test_pr_review_result_check.py b/tests/capabilities/test_pr_review_result_check.py index e381403916..b889f4765e 100644 --- a/tests/capabilities/test_pr_review_result_check.py +++ b/tests/capabilities/test_pr_review_result_check.py @@ -39,7 +39,11 @@ def _review(): if "verdict_values" in requirement: row["verdict"] = requirement["verdict_values"][0] if key == "semantic_alignment": - row["candidate_decision"] = "local_only" + row.update( + checked_scope="Changed helper and its callers; no shared state writes.", + impact_reason="Local formatting only; no shared contract changes.", + verdict="not_applicable", + ) if "items_field" in requirement: item_fields = requirement.get("item_fields", []) if "required_cases" in requirement: @@ -84,7 +88,10 @@ def test_result_check_is_not_semantic_or_merge_authority(): ("candidate_decision", "verdict", "blocker"), [ ("made_up", "aligned", "semantic_alignment:invalid_candidate_decision"), - ("unknown", "aligned", "semantic_alignment:unknown_requires_not_yet_proven"), + ("unknown", "aligned", "semantic_alignment:unknown_cannot_claim_alignment"), + ("unknown", "not_applicable", "semantic_alignment:unknown_cannot_claim_alignment"), + ("extend_vocabulary", "not_applicable", "semantic_alignment:contract_change_requires_evidence"), + ("create_vocabulary", "not_applicable", "semantic_alignment:contract_change_requires_evidence"), ], ) def test_semantic_alignment_cannot_hide_unknown_or_invalid_candidate( @@ -100,6 +107,91 @@ def test_semantic_alignment_cannot_hide_unknown_or_invalid_candidate( assert not checked["approval_consistent"] +def test_no_candidate_exits_after_scope_and_reason() -> None: + packet, result = _review() + result["evidence"]["semantic_alignment"] = { + "status": "verified", + "checked_scope": "Formatting helper and unchanged callers.", + "impact_reason": "No shared field, state value or persistence change.", + "verdict": "not_applicable", + } + assert check_review_result(packet, result)["approval_consistent"] + + +@pytest.mark.parametrize("missing", ["checked_scope", "impact_reason"]) +def test_no_impact_still_needs_a_bounded_reason(missing: str) -> None: + packet, result = _review() + del result["evidence"]["semantic_alignment"][missing] + assert not check_review_result(packet, result)["approval_consistent"] + + +@pytest.mark.parametrize("verdict", ["aligned", "new_semantics_justified"]) +def test_contract_change_reuses_existing_review_evidence(verdict: str) -> None: + packet, result = _review() + row = result["evidence"]["semantic_alignment"] + row.update( + verdict=verdict, + candidate_decision="extend_vocabulary", + affected_contract="TaskState shared enum and reader compatibility.", + evidence_refs=["repository_reuse", "observable_semantics", "validation_matrix"], + ) + assert check_review_result(packet, result)["approval_consistent"] + del row["affected_contract"] + assert not check_review_result(packet, result)["approval_consistent"] + + +def test_scanner_blind_spot_is_reported_without_claiming_safety_or_blocking() -> None: + packet, result = _review() + row = result["evidence"]["semantic_alignment"] + row.update( + verdict="advisory", + candidate_decision="unknown", + impact_reason="Existing required checks pass; no changed contract lacks required evidence.", + analysis_limit="Unchanged external pass-through is outside the bounded scanner.", + ) + assert check_review_result(packet, result)["approval_consistent"] + del row["analysis_limit"] + assert not check_review_result(packet, result)["approval_consistent"] + + +@pytest.mark.parametrize("verdict", ["not_yet_proven", "violated"]) +def test_contract_blocker_requires_actionable_repair(verdict: str) -> None: + packet, result = _review() + row = result["evidence"]["semantic_alignment"] + row.update( + verdict=verdict, + candidate_decision="compatibility_only", + affected_contract="Persisted TaskState values must remain readable.", + trigger="PR deletes a persisted enum member.", + observed_evidence="Old-state readback is missing or fails in validation_matrix.", + minimum_repair="Restore decoding or add a tested migration.", + validation_commands="pytest tests/test_state_readback.py", + ) + assert not check_review_result(packet, result)["approval_consistent"] + result["verdict"] = "REQUEST_CHANGES" + assert check_review_result(packet, result)["ok"] + del row["minimum_repair"] + assert "semantic_alignment:missing_field:minimum_repair" in ( + check_review_result(packet, result)["approval_blockers"] + ) + + +def test_advisory_cannot_override_a_concrete_blocking_finding() -> None: + packet, result = _review() + result["evidence"]["semantic_alignment"].update( + verdict="advisory", candidate_decision="unknown", analysis_limit="Scanner limit." + ) + result["findings"] = [{"severity": "P2", "blocking": True}] + assert not check_review_result(packet, result)["approval_consistent"] + + +def test_optional_semantic_evidence_cannot_hide_a_docs_contract_violation() -> None: + packet, result = _review() + packet["pull_requests"][0]["areas"] = {"public_docs": 1} + result["evidence"]["semantic_alignment"].update(verdict="violated") + assert not check_review_result(packet, result)["approval_consistent"] + + @pytest.mark.parametrize( "kind", ["missing", "unverified", "empty", "blocking", "finding", "unknown_verdict"] ) @@ -245,10 +337,34 @@ def test_inventory_only_head_cannot_certify_a_new_review() -> None: check_review_result(packet, result) -def test_public_cli_check_has_no_github_or_checkpoint_effects( - tmp_path, monkeypatch, capsys +@pytest.mark.parametrize( + ("semantic_verdict", "expected_exit"), + [("not_applicable", 0), ("new_semantics_justified", 0), ("advisory", 0), + ("not_yet_proven", 1), ("violated", 1)], +) +def test_public_cli_checks_semantic_boundaries_without_github_or_checkpoint_effects( + tmp_path, monkeypatch, capsys, semantic_verdict: str, expected_exit: int ): packet, result = _review() + semantic = result["evidence"]["semantic_alignment"] + semantic["verdict"] = semantic_verdict + if semantic_verdict == "new_semantics_justified": + semantic.update( + candidate_decision="extend_vocabulary", + affected_contract="Shared TaskState enum.", + evidence_refs=["repository_reuse", "observable_semantics", "validation_matrix"], + ) + elif semantic_verdict == "advisory": + semantic.update(candidate_decision="unknown", analysis_limit="Dynamic pass-through.") + elif semantic_verdict in ("not_yet_proven", "violated"): + semantic.update( + candidate_decision="compatibility_only", + affected_contract="Persisted TaskState compatibility.", + trigger="Deleted state member.", + observed_evidence="Old-state readback is missing or fails.", + minimum_repair="Restore decoding or validate migration.", + validation_commands="pytest tests/test_state_readback.py", + ) packet_path, result_path = tmp_path / "packet.json", tmp_path / "result.json" packet_path.write_text(json.dumps(packet)) result_path.write_text(json.dumps(result)) @@ -266,8 +382,8 @@ def test_public_cli_check_has_no_github_or_checkpoint_effects( "--packet", str(packet_path), ] - assert main(argv) == 0 - assert json.loads(capsys.readouterr().out)["approval_consistent"] + assert main(argv) == expected_exit + assert json.loads(capsys.readouterr().out)["approval_consistent"] is (expected_exit == 0) assert {p.name: p.read_bytes() for p in tmp_path.iterdir()} == before result["evidence"]["failure_analysis"]["status"] = "unverified" result_path.write_text(json.dumps(result)) From 940f5183927bcd1ce8b16ef89009317e2285fa0f Mon Sep 17 00:00:00 2001 From: song Date: Wed, 16 Sep 2026 00:18:04 +0800 Subject: [PATCH 6/9] docs(pr-review): define semantic triage and repair boundaries Signed-off-by: song --- .../semantic-vocabulary-convergence-v0.md | 13 ++++ ...emantic-vocabulary-convergence-v0.zh-CN.md | 9 +++ loopx/capabilities/pr_review_queue/README.md | 75 ++++++++++++++----- 3 files changed, 78 insertions(+), 19 deletions(-) diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md index 51564280a3..bfc064ed41 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md @@ -674,6 +674,19 @@ 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. +PR review preserves these lanes. Ordinary changes record their checked scope and +reason, then exit semantic review when no shared contract is affected. Detailed +evidence is limited to affected contracts and may reference existing review +evidence. A scanner blind spot is advisory; missing required validation for a +contract affected by this PR, or a concrete violation, blocks approval with the +contract, triggering change, observed evidence, minimum repair and rerun command. +The global F6 proof gap does not itself block unrelated work or excuse a missing +compatibility check required by the changed contract. See the +[review evidence contract](../../../loopx/capabilities/pr_review_queue/README.md#semantic-alignment-and-ci-constraint-recovery) +for the executable verdict shapes. Model performance remains an empirical +question: compare matched tasks/model/budgets, counting tokens, time, independently +accepted completions, false blocks and missed defects before claiming a benefit. + The phases are therefore: 1. **M0:** keep the current structural guard and make its proof boundary 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 cba3879ca0..b2b3c9ba45 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md @@ -560,6 +560,15 @@ planner 条目则有意保留 `python3`。 测试覆盖已识别形式后，才可移到阻断层。这样既严格防止静默破坏，也允许不完整的分析 为无关改动提供信息而不阻断它们。 +PR review 保留这些层级。普通改动记录检查范围和理由，无共享契约影响就结束语义 +审查。详细证据只针对受影响契约，可以引用已有审查证据。扫描器盲区仅作建议性 +报告；本次修改影响的契约缺少必需验证，或存在明确违规，才以契约、触发修改、 +观察证据、最小修复和复验命令阻断批准。F6 的全局证明缺口本身不阻断无关改动， +也不能用来豁免被修改契约要求的兼容性检查。可执行的结论结构见 +[review 证据契约](../../../loopx/capabilities/pr_review_queue/README.md#semantic-alignment-and-ci-constraint-recovery)。 +模型表现仍需实测：固定任务、模型与预算，比较 token、耗时、独立验收成功率、 +误阻塞和漏检，之后才能声称带来收益。 + 阶段顺序如下： 1. **M0：** 保留当前结构守卫，并明确其证明边界。 diff --git a/loopx/capabilities/pr_review_queue/README.md b/loopx/capabilities/pr_review_queue/README.md index 18a0144116..e1957af855 100644 --- a/loopx/capabilities/pr_review_queue/README.md +++ b/loopx/capabilities/pr_review_queue/README.md @@ -311,19 +311,39 @@ the accumulated mechanism. ### Semantic alignment and CI constraint recovery -Every code review plan carries `semantic_alignment`. It is a lightweight -orientation block, not a demand for whole-program semantic analysis. The agent -must state whether the change has no semantic contract impact or whether it -reuses an existing vocabulary, extends one, creates one, is an external or -compatibility value, or remains `unknown`. A normal code PR may use -`not_applicable` only with a reason that names the checked boundary. - -For semantic or constraint-related changes, read the exact base and head of the -RFC, registry, smoke, and relevant CI files. The current required checks are -`Sign-off` and `merge-gate`; the semantic smoke is currently executed through -the default Python test path, while Full Public Smokes is a post-merge/scheduled -confirmation surface rather than a PR-required check. Green CI proves only the -checks that ran and does not prove whole-program semantic convergence. +Policy revision 5 replaces the universal detailed semantic review with bounded +triage for code and behavior-bearing policy changes. The required row starts +with `checked_scope`, `impact_reason`, and `verdict` (plus the standard evidence +`status`). Review the full diff and relevant definitions/callers, then stop at +`not_applicable` if no shared contract is affected. No candidate value, separate +report subsection, full RFC read, or hypothetical repair is needed on this path. +A changed-file preview or an unchanged registry alone cannot establish no impact. + +| Verdict | Additional evidence | Approval effect | +| --- | --- | --- | +| `not_applicable` | None; scope and reason explain the absence of shared contract impact | No semantic blocker | +| `aligned` / `new_semantics_justified` | `candidate_decision`, `affected_contract`, `evidence_refs` to existing review evidence | No semantic blocker | +| `advisory` | `candidate_decision`, `analysis_limit`; the impact reason explains why no affected current obligation lacks required evidence | Reports a bounded-analysis gap, without claiming safety or blocking on that gap alone | +| `not_yet_proven` / `violated` | `candidate_decision`, `affected_contract`, `trigger`, `observed_evidence`, `minimum_repair`, `validation_commands` | Blocks approval for an affected current obligation with missing required evidence or a concrete violation | + +For shared states, owners, consumer domains, projections or persistence changes, +read only the affected base/head contracts. Reuse `repository_reuse`, +`observable_semantics`, and `validation_matrix` evidence instead of repeating +it. Docs-only reviews may supply the same row when they find contract impact; +a supplied row is checked even when not required by the plan. A generated +inventory change alone does not require a detailed semantic review. + +The generic capability does not infer impact from repository-specific paths or +inject a repository's check names into another repository's packet. Resolve +obligations from the target repository's current policy and use the existing +validation matrix. Observed check runs do not establish which checks are required. +Green CI proves only the checks that ran, not whole-program convergence. + +The repair map below is a **LoopX repository example**, not a policy for every +`--repo`. In LoopX, verify required checks against `.github/GOVERNANCE.md` and the +current CI configuration: `Sign-off` and `merge-gate` are the documented checks; +the semantic smoke runs through Python tests. Full Public Smokes is a +post-merge/scheduled surface. These facts are not copied into generic packets. Use this repair map when a check fails: @@ -337,12 +357,29 @@ Use this repair map when a check fails: | semantic smoke: budget/anchor | Measured debt grew or the guard was weakened | Fix the underlying duplicate/coverage issue and lower a budget only when the measured debt really fell | Raising the budget, narrowing the scan root, or renaming to hide drift | | `merge-gate` | A required upstream CI job failed, was skipped unexpectedly, or has incomplete qualification | Inspect `needs` and the failing job, fix the owning path, and rerun at the same head | Treating a local smoke as proof that the remote gate is complete | -For every failure, publish the exact head, affected constraint, observed output, -minimum repair, non-repair that would only hide the signal, rerun command, and -remaining unknown boundary. A dynamic producer or consumer that the bounded -scanner cannot classify is `unknown`; it is not evidence that the value is -absent or safe. Missing semantic evidence is `not_yet_proven` and blocks an -approval for an applicable semantic-alignment row. +A blocker must connect the exact-head change to an existing obligation and a +replayable failure or missing required validation. An untraceable dynamic value +alone is an `advisory`, not `not_yet_proven` and not proof of safety. Removing a +persisted value without required old-state readback is `not_yet_proven`; a failed +required projection check is `violated`. Neither can be downgraded to advisory +to bypass CI or a concrete blocking finding. Do not turn future or advisory RFC +properties into current merge obligations. Result checking validates declared +consistency, not the truth of a reviewer's classification. + +**中文边界：** 普通改动只填检查范围、影响理由与结论，无共享契约影响时用 +`not_applicable` 结束，无需虚构候选值或补齐整张证据表。影响共享状态、owner、 +消费者、投影或持久化时，按受影响契约检查并引用已有证据。扫描器能力不足用 +`advisory` 报告；本次修改缺少现行契约要求的验证用 `not_yet_proven`，明确违规用 +`violated`，后二者阻断批准并给出契约、触发修改、观察证据、最小修复与复验命令。 +其他仓库使用自己的 CI 与契约规则，不能继承 LoopX 的检查名。 + +A matched model evaluation should preselect ordinary edits, legal contract +extensions, and real contract defects; fix tasks, model/version, tools, seeds +where supported, and total budgets across policies. Count review and repair +within that budget. Compare independently accepted completions, tokens, elapsed +time, false blocks and missed defects; report uncertainty and repeat stochastic +runs. Deterministic consistency fixtures establish the boundary, not model +benchmark uplift or non-regression. The per-actionable-PR `pull_request_review_plan_v1` records the exact target, applicability, required evidence ids, and an initially `unverified` From 732acf0ee9dd36ba3ff2b8d92e33bdb841cd168e Mon Sep 17 00:00:00 2001 From: song Date: Wed, 16 Sep 2026 07:44:52 +0800 Subject: [PATCH 7/9] docs(development): use uv for current-checkout validation Signed-off-by: song --- CONTRIBUTING.md | 30 ++++----- .../semantic-vocabulary-convergence-v0.md | 29 +++++---- ...emantic-vocabulary-convergence-v0.zh-CN.md | 25 +++---- docs/development/testing-and-quality.md | 65 ++++++++++++++++--- examples/semantic-vocabulary-drift-smoke.py | 2 +- loopx/capabilities/pr_review_queue/README.md | 2 +- scripts/generate_semantic_inventory.py | 8 +-- 7 files changed, 102 insertions(+), 59 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b5b6dfea87..5e2c09ce79 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -79,26 +79,20 @@ Before adding or consolidating a public smoke, use the bilingual [good smoke guide](docs/development/good-smokes.md) to define its durable invariant, independent oracle, cadence, and public-safe fixture boundary. -Install and verify the checkout: +For source development, run commands from the repository or dedicated worktree +root with `uv`. It manages a compatible Python and installs the current checkout +in the project environment, keeping checks separate from a globally installed +LoopX release. See the [local validation commands](docs/development/testing-and-quality.md#local-validation-environment--本地验证环境) +for environment, lockfile, and CI boundaries. ```bash -git clone https://github.com/huangruiteng/loopx ~/loopx -~/loopx/scripts/install-local.sh -export PATH="$HOME/.local/bin:$PATH" -loopx doctor -loopx demo -``` - -Common focused checks: - -```bash -python -m pip install -e ".[test]" -python -m ruff check tests loopx/canary loopx/control_plane loopx/domain_packs loopx/presentation -python -m mypy -python examples/control_plane/cli-output-budget-regression-smoke.py -python -m pytest -q -loopx canary premerge --from-git-diff -loopx check --scan-path loopx/ --scan-path tests/ --scan-path examples/ --scan-path docs/ +uv sync --extra test +uv run --extra test python -m ruff check tests loopx/canary loopx/control_plane loopx/domain_packs loopx/presentation +uv run --extra test python -m mypy +uv run --extra test python examples/control_plane/cli-output-budget-regression-smoke.py +uv run --extra test python -m pytest -q +uv run --extra test loopx canary premerge --from-git-diff +uv run --extra test loopx check --scan-path loopx/ --scan-path tests/ --scan-path examples/ --scan-path docs/ git diff --check ``` diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md index bfc064ed41..efc98f7e1b 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md @@ -516,9 +516,9 @@ inventory in the same PR. | Claim | Test or evidence | Required result | Boundary / exclusions | | --- | --- | --- | --- | -| Registry and inventory match the code at baseline | `python3.11 examples/semantic-vocabulary-drift-smoke.py` | `ok` with coverage, ratchet, budget, and twin report | Proves parity for registered vocabularies and mapped carriers only | -| Inventory is fresh | `python3.11 scripts/generate_semantic_inventory.py --check` | exit 0 | Structural map only | -| Scanner classification rules | `pytest tests/architecture/test_semantic_inventory.py` | pass | Fixture repository; rules from this RFC, not from output | +| Registry and inventory match the code at baseline | `uv run --extra test loopx canary smoke-suite --script semantic-vocabulary-drift-smoke.py` | `ok` with coverage, ratchet, budget, and twin report | Proves parity for registered vocabularies and mapped carriers only | +| Inventory is fresh | `uv run python scripts/generate_semantic_inventory.py --check` | exit 0 | Structural map only | +| Scanner classification rules | `uv run --extra test python -m pytest tests/architecture/test_semantic_inventory.py` | pass | Fixture repository; rules from this RFC, not from output | | A widened `effective_action` set fails closed in Python | Add an unregistered literal via `==`, membership, or conditional expression | Failure names the value and file | Mutation exercise; not a committed test | | A widened `effective_action` set fails closed in TypeScript | Add an unregistered literal via `===` or a ternary | Same | Same | | A forked constant fails closed | Redefine `TURN_ENVELOPE_SCHEMA_VERSION` or `HANDOFF_MODES` in a non-owner module, regenerate the inventory | Failure lists the extra defining module or the fork budget | Same | @@ -529,10 +529,10 @@ inventory in the same PR. | A multi-value collision cannot grow | Define one closed-set name in two modules with divergent values, or with equal values, and regenerate | `multi_value_forks` or `multi_value_twins` fails naming the new name | Mutation exercise; not a committed test | | The registry cannot relax its own ratchet | Lower any `coverage_floor` count, raise any `inventory_ratchets` budget, or raise a retirement budget, in the same diff that removes the coverage it counts | `COVERAGE_ANCHOR`, `BUDGET_ANCHOR`, or `RETIREMENT_ANCHOR` fails naming the anchored value | Mutation exercise; moving an anchor is a code edit a reviewer sees | | A tightened budget cannot drift back to a stale anchor | Lower a registry budget without touching the anchor | Failure says the registry value and the anchor differ | Equality, not `<=`; the fix is to lower the anchor in the same diff | -| The smoke is on the pull-request path | `pytest tests/architecture/test_semantic_vocabulary_drift.py` | pass; the test is collected by the default `pytest -q` sweep in `python-tests.yml` | The fleet and premerge surfaces are not the obligation (I10) | -| Premerge selects the smoke for a `loopx/` diff | `loopx canary premerge --changed-file loopx/control_plane/turn_driver/loop_controller.py` | the plan lists `examples/semantic-vocabulary-drift-smoke.py` under `repo-architecture-budget` | Selection is by trigger hint; the pytest wrapper is the guarantee | -| 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 | +| The smoke is on the pull-request path | `uv run --extra test python -m pytest tests/architecture/test_semantic_vocabulary_drift.py` | pass; the test is collected by the default `pytest -q` sweep in `python-tests.yml` | The fleet and premerge surfaces are not the obligation (I10) | +| Premerge selects the smoke for a `loopx/` diff | `uv run --extra test loopx canary premerge --changed-file loopx/control_plane/turn_driver/loop_controller.py` | the plan lists `examples/semantic-vocabulary-drift-smoke.py` under `repo-architecture-budget` | Selection is by trigger hint; the pytest wrapper is the guarantee | +| Measurement covers both carrier shapes and filters local naming | `uv run --extra test python -m 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 | `uv run --extra test python -m 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 `uv run --extra test 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 | @@ -601,13 +601,14 @@ 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. +**Interpreter and checkout.** Run the commands above from the target worktree +with `uv run`; Python compatibility comes from `pyproject.toml` (`>=3.11`), +and the imported LoopX must come from this checkout. Canary normalizes displayed +`python3` commands to `sys.executable`, the interpreter that launched LoopX. +A global installation may scan a different release snapshot even when its Python +is compatible. See [local validation](../../development/testing-and-quality.md#local-validation-environment--本地验证环境) +for setup, interpreter/source readback, and lockfile boundaries. Historical +receipts below retain the commands actually executed. ## 11. Normative delivery plan 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 b2b3c9ba45..c129648857 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md @@ -423,9 +423,9 @@ PR 中重新生成清单。 | 声明 | 测试或证据 | 要求结果 | 边界 / 排除 | | --- | --- | --- | --- | -| 基线上注册表与清单和代码一致 | `python3.11 examples/semantic-vocabulary-drift-smoke.py` | `ok` 并输出覆盖、棘轮、预算与孪生报告 | 只证明已注册词表与已映射载体的一致性 | -| 清单新鲜 | `python3.11 scripts/generate_semantic_inventory.py --check` | 退出码 0 | 仅结构性映射 | -| 扫描器分类规则 | `pytest tests/architecture/test_semantic_inventory.py` | 通过 | 夹具仓库；规则来自本 RFC 而非输出 | +| 基线上注册表与清单和代码一致 | `uv run --extra test loopx canary smoke-suite --script semantic-vocabulary-drift-smoke.py` | `ok` 并输出覆盖、棘轮、预算与孪生报告 | 只证明已注册词表与已映射载体的一致性 | +| 清单新鲜 | `uv run python scripts/generate_semantic_inventory.py --check` | 退出码 0 | 仅结构性映射 | +| 扫描器分类规则 | `uv run --extra test python -m pytest tests/architecture/test_semantic_inventory.py` | 通过 | 夹具仓库；规则来自本 RFC 而非输出 | | Python 侧扩宽 `effective_action` 时失败关闭 | 通过 `==`、成员测试或条件表达式加一个未注册字面量 | 失败文本命名该值与文件 | 突变练习；非提交测试 | | TypeScript 侧扩宽 `effective_action` 时失败关闭 | 通过 `===` 或三元表达式加一个未注册字面量 | 同上 | 同上 | | 分叉常量时失败关闭 | 在非 owner 模块重定义 `TURN_ENVELOPE_SCHEMA_VERSION` 或 `HANDOFF_MODES`，重新生成清单 | 失败列出多出的定义模块或分叉预算 | 同上 | @@ -436,10 +436,10 @@ PR 中重新生成清单。 | 多值冲突不能增长 | 让一个闭集名在两个模块中以不同值集定义，或以相同值集定义，并重新生成 | `multi_value_forks` 或 `multi_value_twins` 失败并命名新名字 | 突变练习；非提交测试 | | 注册表不能放松自己的棘轮 | 在同一 diff 中调低任一 `coverage_floor` 计数、调高任一 `inventory_ratchets` 预算或退休预算，同时删掉它所统计的覆盖 | `COVERAGE_ANCHOR`、`BUDGET_ANCHOR` 或 `RETIREMENT_ANCHOR` 失败并命名被锚定的值 | 突变练习；挪动锚点是一次评审者可见的代码修改 | | 已收紧的预算不能漂回过期锚点 | 只调低注册表预算而不动锚点 | 失败文本指出注册表值与锚点不等 | 用相等而非 `<=`；修法是同 diff 调低锚点 | -| smoke 在 PR 路径上 | `pytest tests/architecture/test_semantic_vocabulary_drift.py` | 通过；该测试被 `python-tests.yml` 的默认 `pytest -q` 扫描收集 | 舰队与 premerge 表面不是义务（I10） | -| premerge 会为 `loopx/` 的 diff 选中该 smoke | `loopx canary premerge --changed-file loopx/control_plane/turn_driver/loop_controller.py` | 计划在 `repo-architecture-budget` 下列出 `examples/semantic-vocabulary-drift-smoke.py` | 选择靠触发词；pytest 包装才是保证 | -| 度量覆盖两种载体形状并过滤局部命名 | `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` 既有环境失败除外 | +| smoke 在 PR 路径上 | `uv run --extra test python -m pytest tests/architecture/test_semantic_vocabulary_drift.py` | 通过；该测试被 `python-tests.yml` 的默认 `pytest -q` 扫描收集 | 舰队与 premerge 表面不是义务（I10） | +| premerge 会为 `loopx/` 的 diff 选中该 smoke | `uv run --extra test loopx canary premerge --changed-file loopx/control_plane/turn_driver/loop_controller.py` | 计划在 `repo-architecture-budget` 下列出 `examples/semantic-vocabulary-drift-smoke.py` | 选择靠触发词；pytest 包装才是保证 | +| 度量覆盖两种载体形状并过滤局部命名 | `uv run --extra test python -m pytest tests/architecture/test_semantic_inventory.py` | 通过，含冲突与模块局部约定两组夹具 | 规则来自本 RFC 而非扫描输出 | +| 两处 owner 修正不改变行为 | `uv run --extra test python -m 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` 与 `uv run --extra test 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 失败；只被比较的值不算已携带 | @@ -496,11 +496,12 @@ heartbeat/quota 覆盖。quick 与 deep 档位的上限不变。 `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`。 +**解释器与源码。** 在目标 worktree 根目录通过 `uv run` 执行上面的命令。 +Python 兼容范围来自 `pyproject.toml`（`>=3.11`），导入的 LoopX 必须来自当前源码。 +Canary 将显示为 `python3` 的命令转换为启动 LoopX 的 `sys.executable`；全局安装 +即使 Python 版本兼容，也可能扫描另一份发布快照。安装、解释器／源码读回及锁文件 +边界见[本地验证环境](../../development/testing-and-quality.md#local-validation-environment--本地验证环境)。 +下方历史证据保留实际执行过的命令。 ## 11. 规范性交付计划 diff --git a/docs/development/testing-and-quality.md b/docs/development/testing-and-quality.md index 2661bdea1d..c1fb7ab83e 100644 --- a/docs/development/testing-and-quality.md +++ b/docs/development/testing-and-quality.md @@ -331,22 +331,69 @@ negative 或 mutation-style 断言，并让各 provider 复用同一 envelope 经 review 的兼容理由，不得削弱或删除已有维度。禁止复制生产文本、标识、路径、日志、 凭据或私有快照。PR 验证证据需报告 fixture schema、语义维度、provider arms 与有意差异。 -Install the test dependencies once: +### Local Validation Environment / 本地验证环境 + +Run from the repository or dedicated worktree root with `uv`. The project's +`requires-python` declares Python `>=3.11`; it does not require an executable +named `python3.11`. `uv` selects a compatible interpreter, creates `.venv`, and +installs the checkout with the selected extras. Interpreter downloads depend on +uv's download settings and network access. A system `python3` may be too old, +and a global `loopx` may resolve to a different installed source tree. + +在仓库或独立 worktree 根目录使用 `uv`。`pyproject.toml` 要求 Python `>=3.11`， +无需依赖名为 `python3.11` 的命令。uv 选择兼容解释器，在 `.venv` 中安装当前源码 +与测试依赖；能否自动下载 Python 取决于下载配置与网络。系统 `python3` 可能过旧， +全局 `loopx` 也可能指向另一个已安装版本。 ```bash -python -m pip install -e ".[test]" +uv sync --extra test +uv run --extra test python -m ruff check tests loopx/canary loopx/control_plane loopx/domain_packs loopx/presentation +uv run --extra test python -m mypy +uv run --extra test python examples/control_plane/cli-output-budget-regression-smoke.py +uv run --extra test python -m pytest -q +uv run --extra test loopx canary premerge --from-git-diff +# For a fork whose PR base is upstream/main, use this instead: +uv run --extra test loopx canary premerge --from-git-diff --git-diff-base upstream/main +# Run one semantic smoke or check its generated inventory: +uv run --extra test loopx canary smoke-suite --script semantic-vocabulary-drift-smoke.py +uv run python scripts/generate_semantic_inventory.py --check +git diff --check ``` -Run the fast repository gate: +Confirm the interpreter and imported checkout when diagnosing a mismatch: ```bash -python -m ruff check tests loopx/canary loopx/control_plane loopx/domain_packs loopx/presentation -python -m mypy -python examples/control_plane/cli-output-budget-regression-smoke.py -python -m pytest -q -git diff --check +uv run python -c "import sys, loopx; print(sys.executable); print(loopx.__file__)" ``` +Canary executes Python checks with the interpreter that launched LoopX +(`sys.executable`). Its displayed `python3` command is not a second interpreter +selection. Keep subprocesses on `sys.executable`; use `uv run` at the developer +entrypoint. Avoid `uvx loopx` or `uv run --no-project` when validating this +checkout, and change into the intended worktree before running Git-based checks. +An activated compatible environment remains a supported alternative: install +with `python -m pip install -e ".[test]"`, then use that environment's Python +and LoopX commands directly. + +Canary 使用启动 LoopX 的 `sys.executable` 执行 Python 检查，显示的 `python3` +不是重新选择解释器。子进程继续复用 `sys.executable`，只在开发入口使用 `uv run`。 +检查当前源码时不要改用 `uvx loopx` 或 `uv run --no-project`；Git diff 检查前先进入 +目标 worktree。已有兼容虚拟环境也可用 `python -m pip install -e ".[test]"` 安装源码， +随后直接使用该环境的命令。 + +The repository does not currently track `.python-version` or `uv.lock`. `uv` +creates a local lockfile during resolution; keep that generated file out of +unrelated PRs. Introducing a shared lock or interpreter pin is a separate +repository policy change. Do not claim identical environments from +`requires-python` alone, or use `--locked` before a reviewed lockfile exists. +CI keeps its explicit Python versions and pinned/hash-checked installation +paths. Historical validation receipts keep the commands that actually ran. + +当前仓库未跟踪 `.python-version` 或 `uv.lock`。uv 解析依赖时生成的本地锁文件不要 +混入无关 PR；共享锁文件与解释器版本固定应单独评审。最低版本要求不等于环境完全 +可复现，没有已评审锁文件时也不使用 `--locked`。CI 保留显式 Python 版本与固定依赖／ +哈希校验的安装路径，历史验证记录保留实际执行过的命令。 + `.github/workflows/python-tests.yml` runs this fast lane for relevant Python pull requests. It intentionally excludes provider-backed evaluation and the full smoke catalog, so ordinary iteration does not depend on credentials, @@ -377,7 +424,7 @@ Sonar 只复用同一次 run 的 XML，不重复测试、不跨 run 取产物。 Sonar，测试 job 不接收 Sonar secret。触发范围取原有两套 workflow 的并集；纯前端 PR 使用前述豁免，Sonar 配置变更仍全量运行，包括没有 token 的 fork。 -Reproduce one shard locally with `python -m pytest -q -n 2 --splits 4 --group 1 +Reproduce one shard locally with `uv run --extra test python -m pytest -q -n 2 --splits 4 --group 1 --splitting-algorithm least_duration --cov=loopx`. Omit the split arguments to run the complete suite locally. 全量本地测试仍省略分片参数即可。 diff --git a/examples/semantic-vocabulary-drift-smoke.py b/examples/semantic-vocabulary-drift-smoke.py index d01dc46069..6e19e58a5a 100755 --- a/examples/semantic-vocabulary-drift-smoke.py +++ b/examples/semantic-vocabulary-drift-smoke.py @@ -450,7 +450,7 @@ def check_inventory(registry: dict[str, Any], sources: list[SourceFile]) -> tupl committed = inventory_path.read_text(encoding="utf-8") inventory = build_inventory(REPO_ROOT, sources=sources) require(inventory["schema_version"] == INVENTORY_SCHEMA_VERSION, "inventory schema drift") - require(render_inventory(inventory) == committed, f"{registry['inventory']} is stale; run python3.11 scripts/generate_semantic_inventory.py and commit the result") + require(render_inventory(inventory) == committed, f"{registry['inventory']} is stale; from the repository root run uv run python scripts/generate_semantic_inventory.py and commit the result") ratchets = registry["inventory_ratchets"] summary = inventory["summary"] parts = [] diff --git a/loopx/capabilities/pr_review_queue/README.md b/loopx/capabilities/pr_review_queue/README.md index e1957af855..9ed96ef5b7 100644 --- a/loopx/capabilities/pr_review_queue/README.md +++ b/loopx/capabilities/pr_review_queue/README.md @@ -351,7 +351,7 @@ Use this repair map when a check fails: | --- | --- | --- | --- | | `Sign-off` | One commit in the PR range lacks a valid DCO trailer | Add `Signed-off-by` to every affected commit with `git commit --amend -s` or an equivalent history repair; verify the full range | Signing only the newest commit | | semantic smoke: unregistered value | A recognised carrier/field form introduced a value outside the registry | Reuse the existing owner value, or add the value with its owner, slot, scope, tests, and RFC evidence | Registering an unrelated string to silence the error | -| semantic smoke: stale inventory | The committed generated map no longer matches the indexed source tree | Stage intended source paths, run `python3.11 scripts/generate_semantic_inventory.py`, then `--check` | Editing counts by hand or including private/untracked files | +| semantic smoke: stale inventory | The committed generated map no longer matches the indexed source tree | Stage intended source paths, run `uv run python scripts/generate_semantic_inventory.py`, then `--check` | Editing counts by hand or including private/untracked files | | semantic smoke: owner/parity | A defining symbol or Python/TypeScript value set diverged | Restore the single owner or deliberately update both runtime owners with parity evidence | Adding a second silent authority | | semantic smoke: projection | A source value is unmapped, mapped to the wrong target, or should be rejected explicitly | Update the declared mapping and executable owner together, then test the boundary case | Deleting a source value without compatibility analysis | | semantic smoke: budget/anchor | Measured debt grew or the guard was weakened | Fix the underlying duplicate/coverage issue and lower a budget only when the measured debt really fell | Raising the budget, narrowing the scan root, or renaming to hide drift | diff --git a/scripts/generate_semantic_inventory.py b/scripts/generate_semantic_inventory.py index ca254b2e24..c7da0ff5d3 100755 --- a/scripts/generate_semantic_inventory.py +++ b/scripts/generate_semantic_inventory.py @@ -2,9 +2,9 @@ """Generate or check the repository-wide semantic inventory. Usage: - python3.11 scripts/generate_semantic_inventory.py # rewrite inventory_v0.json - python3.11 scripts/generate_semantic_inventory.py --check # exit 1 when the file is stale - python3.11 scripts/generate_semantic_inventory.py --report # print advisory consumer ranking + uv run python scripts/generate_semantic_inventory.py # rewrite inventory_v0.json + uv run python scripts/generate_semantic_inventory.py --check # exit 1 when the file is stale + uv run python scripts/generate_semantic_inventory.py --report # print advisory consumer ranking """ from __future__ import annotations @@ -51,7 +51,7 @@ def main() -> int: if args.check: print( f"stale semantic inventory: {INVENTORY_PATH.relative_to(ROOT)}; " - "run scripts/generate_semantic_inventory.py and commit the result", + "from the repository root run uv run python scripts/generate_semantic_inventory.py and commit the result", file=sys.stderr, ) return 1 From e32659fa965372f69d2b8a079f0fb3cbef189c17 Mon Sep 17 00:00:00 2001 From: song Date: Wed, 16 Sep 2026 08:31:45 +0800 Subject: [PATCH 8/9] fix(semantics): unify proof domains and candidate guidance Signed-off-by: song --- .../semantic-vocabulary-convergence-v0.md | 93 ++++++------------- ...emantic-vocabulary-convergence-v0.zh-CN.md | 77 +++++---------- loopx/semantics/vocabulary_v0.json | 20 ++-- 3 files changed, 61 insertions(+), 129 deletions(-) diff --git a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md index 833afd46a8..796567f743 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md @@ -363,28 +363,29 @@ whose listed symbol is a journal or receipt writer marks the vocabulary ### 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: +`V` be the set of registered vocabularies, `L` the source sites, `U(v)` the +ambient runtime values, and `S(v)` the registered admitted values of vocabulary +`v`. Production and consumption range over `U(v)` before validation. 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 +D ⊆ L × V defines +P ⊆ L × V × U(v) produces +C ⊆ L × V × U(v) consumes or branches on +I ⊆ L × V × V interprets one vocabulary as another +T ⊆ L × V passes through without changing meaning +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) ⊆ Val(v)`. A recognised producer +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. -3. **Consumer domain closedness:** `Accepted(c) ⊆ Val(v)`, unless the consumer +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. @@ -432,7 +433,7 @@ TypeScript. A value flowing through an alias, configuration, reflection, external input, or unrecognised syntax belongs to `unknown` until a bounded analysis accounts for it. Unknown is an evidence result, not proof of absence. -Every candidate change must receive exactly one finite disposition: +Advisory candidate triage uses one finite disposition: ```text reuse_existing | extend_vocabulary | create_vocabulary | local_only @@ -440,8 +441,11 @@ external_input | compatibility_only | unknown ``` This makes the *workflow classification* exhaustive even though the program -analysis is not. `reuse_existing` requires the same slot, compatible scope, -and an equivalent contract. `extend_vocabulary` requires a witness that +analysis is not. The registry stores the allowed labels and default, not +per-candidate decisions; this metadata does not enforce candidate handling in +product code. The drift smoke validates the label contract only. +`reuse_existing` requires the same slot, compatible scope, and an equivalent +contract. `extend_vocabulary` requires a witness that reusing an existing value would collapse two states with different required behaviour. `create_vocabulary` requires a new semantic domain or independently owned lifecycle. If the evidence cannot decide among these cases, the default @@ -456,56 +460,6 @@ boundary between a useful proof skeleton and an uncheckable claim of whole-program semantic convergence. -### Soundness, relative completeness, and candidate decisions - -The word *complete* is scoped here. Let `U(v)` be the ambient runtime value -space for vocabulary `v`, `S(v)` its registered admitted set, `P(v)` the values -actually produced, and `O(v)` the values observed by the scanner. The producer -obligation is meaningful only when production is defined over `U(v)`: - -```text -P(v) ⊆ S(v) ⊆ U(v) -``` - -Defining `P(v)` as a subset of `S(v)` in advance would make the first -inclusion tautological. M0 establishes bounded claims about recognised source -forms and registered structural carriers. - -For a recognised language fragment `L0` and an exact analyser `A0`, define: - -```text -Sound(A0, property, L0) := A0 accepts c ⇒ property(c) -Complete(A0, property, L0) := property(c) ⇒ A0 accepts c -``` - -The M0 guard may aim at both properties for its fixed carrier and dispatch -forms. It cannot claim either property for arbitrary dynamic Python or -TypeScript. Values flowing through aliases, configuration, reflection, external -input, or unrecognised syntax are `unknown` until a bounded analysis accounts -for them. Unknown is an evidence result, not proof of absence. - -Every vocabulary candidate has exactly one finite disposition: - -```text -reuse_existing | extend_vocabulary | create_vocabulary | local_only -external_input | compatibility_only | unknown -``` - -`reuse_existing` requires the same slot, compatible scope, and an equivalent -contract. `extend_vocabulary` requires a witness that reusing an existing value -would collapse two states with different required behaviour. `create_vocabulary` -requires a new semantic domain or independently owned lifecycle. If evidence -cannot decide among these cases, the disposition is `unknown`; an unresolved -candidate must not silently become a reuse. - -General behavioural equivalence is undecidable for arbitrary programs, so -`same_concept` is not promoted to a theorem by this schema. It can become a -blocking property only for a restricted contract with explicit inputs, outputs, -transitions, persistence version, and a finite test domain. This is the boundary -between a useful proof skeleton and a claim of whole-program semantic -convergence. - - ### State model and schema `loopx/semantics/vocabulary_v0.json`, `schema_version` @@ -870,6 +824,15 @@ introduce a competing target state. ## Appendix A: Execution ledger (non-normative) +### 2026-09-16 — Review consistency repair + +- Keep one candidate-decision section per language. +- Use `L` for source sites, `U(v)` for ambient values and `S(v)` for admitted + values throughout the registry and narrative. Production is not admitted by definition. +- Clarify candidate dispositions as advisory metadata; no per-candidate runtime + store or enforcement is delivered by this schema. + + ### 2026-09-15 — M0 opened with the RFC - **Baseline:** `1dc6ad8d8` 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 ba46812ccd..4fd2b3ba70 100644 --- a/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md +++ b/docs/architecture/rfcs/semantic-vocabulary-convergence-v0.zh-CN.md @@ -298,25 +298,26 @@ M0.5 之后新增或删除值时；`cross_module` 只在晋升后（Q8）。持 ### 形式模型与证明边界 -注册表是更大程序语义的有限规格。令 `V` 为已注册词表集合，`Val(v)` 为词表 -`v` 允许的值集合，`S` 为源码位点集合。模型记录的是关系，而不只是名称： +注册表是更大程序语义的有限规格。令 `V` 为已注册词表集合，`L` 为源码位点集合， +`U(v)` 为词表 `v` 的环境运行时值空间，`S(v)` 为注册允许集合。生产与消费先在 +`U(v)` 上定义，再验证是否属于允许集合。模型记录的是关系，而不只是名称： ```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 将值持久化 +D ⊆ L × V 定义词表 +P ⊆ L × V × U(v) 生产值 +C ⊆ L × V × U(v) 消费或据值分支 +I ⊆ L × V × V 将一个词表解释为另一个词表 +T ⊆ L × V 不改变含义地透传 +G ⊆ V × V × (S(v_source) ⇀ S(v_target) ∪ {reject}) 做投影 +R ⊆ L × V × Version 将值持久化 ``` 最低语义义务如下： -1. **生产闭包：** `Produced(v) ⊆ Val(v)`。被识别的生产者不能写入注册集合之外的值。 +1. **生产闭包：** `Produced(v) ⊆ S(v) ⊆ U(v)`。被识别的生产者不能写入注册集合之外的值。 2. **规范值存活：** `Canonical(v) ⊆ Produced(v) ∪ CompatibilityOnly(v)`。只被比较、 没有生产来源的值是死值或兼容值，不能是 canonical。 -3. **消费者定义域闭包：** `Accepted(c) ⊆ Val(v)`，除非消费者显式声明外部定义域或部分定义域。 +3. **消费者定义域闭包：** `Accepted(c) ⊆ S(v)`，除非消费者显式声明外部定义域或部分定义域。 4. **作用域分离：** 只有声明作用域相交时，同名冲突才是语义冲突。拼写本身不能证明等价。 5. **投影全性：** 每个源值都必须映射到目标值，或显式映射为 `reject`。 6. **持久化兼容性：** 持久化词表改变时，必须保持所有读者可读，或声明带版本的迁移。 @@ -352,7 +353,7 @@ M0 守卫可以对固定载体和固定分发形式追求这两个性质，但 TypeScript 宣称它们成立。值如果经过别名、配置、反射、外部输入或未识别语法流动， 在有界分析覆盖它之前都属于 `unknown`。Unknown 是证据结果，不是“不存在”的证明。 -每个候选改动必须且只能得到一个有限决策： +建议性的候选分类使用一个有限决策： ```text reuse_existing | extend_vocabulary | create_vocabulary | local_only @@ -370,48 +371,8 @@ external_input | compatibility_only | unknown 在受限契约内成为阻断条件。这就是可用的证明骨架与“全程序语义收敛已被证明”之间的 边界。 - -### 健全性、相对完备性与候选决策 - -这里的“完备”必须带范围。令 `U(v)` 为词表 `v` 的运行时完整值域，`S(v)` 为注册表 -允许的值集合，`P(v)` 为实际产生的值集合，`O(v)` 为扫描器观察到的值集合。生产义务 -只有在完整值域上定义时才有意义： - -```text -P(v) ⊆ S(v) ⊆ U(v) -``` - -如果预先把 `P(v)` 定义成 `S(v)` 的子集，第一个包含关系就会变成恒真命题。M0 -只对已识别的源码形式和已登记的结构载体建立有界结论。 - -对一个受限语法片段 `L0` 和精确分析器 `A0`，定义： - -```text -Sound(A0, property, L0) := A0 接受 c ⇒ property(c) -Complete(A0, property, L0) := property(c) ⇒ A0 接受 c -``` - -M0 守卫可以对固定载体和固定分发形式追求这两个性质，但不能对任意动态 Python 或 -TypeScript 宣称它们成立。值如果经过别名、配置、反射、外部输入或未识别语法流动， -在有界分析覆盖它之前都属于 `unknown`。Unknown 是证据结果，不是“不存在”的证明。 - -每个词表候选必须且只能得到一个有限决策： - -```text -reuse_existing | extend_vocabulary | create_vocabulary | local_only -external_input | compatibility_only | unknown -``` - -`reuse_existing` 要求槽位相同、作用域兼容、契约等价。`extend_vocabulary` 要求给出 -反例，证明复用旧值会把两个需要不同处理的状态压成一个。`create_vocabulary` 要求出现 -新的语义定义域或独立 owner 与生命周期。如果证据不足以在这些情况之间做决定，默认 -就是 `unknown`；未解析候选不能静默当成复用旧词。 - -任意程序的行为等价通常不可判定，因此这个 schema 不会把 `same_concept` 自动提升为 -定理。只有当输入、输出、状态转换、持久化版本和有限测试域都明确时，行为等价才可 -在受限契约内成为阻断条件。这就是可用的证明骨架与“全程序语义收敛已被证明”之间的 -边界。 - +候选处置在此仅为建议性元数据。注册表只保存允许标签与默认值，不存储逐候选决策， +也不在产品代码中强制执行候选处理；漂移 smoke 只验证标签合同。 ### 状态模型与 schema @@ -713,6 +674,14 @@ planner 条目则有意保留 `python3`。 ## 附录 A：执行账本（非规范） +### 2026-09-16 — 评审一致性修复 + +- 每种语言只保留一个候选决策小节。 +- 注册表与叙述统一使用源码位点 `L`、环境值空间 `U(v)` 和允许集合 `S(v)`， + 不把生产值预先定义为合法值。 +- 明确候选处置为建议性元数据；本 schema 不交付逐候选运行时存储或执行门禁。 + + ### 2026-09-15 — 随 RFC 开启 M0 - **基线：** `1dc6ad8d8` diff --git a/loopx/semantics/vocabulary_v0.json b/loopx/semantics/vocabulary_v0.json index 87b4fd258b..7d0adb2956 100644 --- a/loopx/semantics/vocabulary_v0.json +++ b/loopx/semantics/vocabulary_v0.json @@ -16,7 +16,7 @@ "universes": { "vocabularies": "V: registered vocabulary identifiers", "values": "U(v): ambient runtime values; S(v): registered admitted values", - "sites": "S: source locations that define, produce, consume, interpret, pass through, project, or persist values", + "sites": "L: 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" }, @@ -44,7 +44,7 @@ "unknown" ], "default": "unknown", - "meaning": "Exhaustive disposition for a vocabulary candidate; unknown is the fail-closed evidence state when the bounded analysis cannot classify it." + "meaning": "Advisory vocabulary-candidate disposition labels and default; no per-candidate storage or runtime enforcement is implied. Unknown records unresolved bounded evidence, not proof of safety." }, "enforcement_policy": { "blocking_now": [ @@ -63,13 +63,13 @@ ] }, "relations": { - "defines": "D ⊆ S × V: a site defines a vocabulary carrier", - "produces": "P ⊆ S × V × U: a site writes or returns a runtime value; it is valid only when the value is in S(v)", - "consumes": "C ⊆ S × V × U: a site accepts or branches on a runtime 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" + "defines": "D ⊆ L × V: a site defines a vocabulary carrier", + "produces": "P ⊆ L × V × U(v): a site writes or returns a runtime value; it is valid only when the value is in S(v)", + "consumes": "C ⊆ L × V × U(v): a site accepts or branches on a runtime value", + "interprets": "I ⊆ L × V × V: a site maps one vocabulary into another", + "passes_through": "T ⊆ L × V: a site serializes, persists, forwards, or displays without changing meaning", + "projects": "G ⊆ V × V × (S(v_source) ⇀ S(v_target) ∪ {reject}): a declared projection between registered admitted sets", + "persists": "R ⊆ L × V × Version: a site writes a value to a durable representation" }, "invariants": [ { @@ -86,7 +86,7 @@ }, { "id": "F3_consumer_domain_closedness", - "statement": "Accepted(c) ⊆ Val(v), unless the consumer declares an external or partial domain", + "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" }, From d12be19c5666c7cd3ed61fc57571dc93eeee3d3b Mon Sep 17 00:00:00 2001 From: song Date: Wed, 16 Sep 2026 08:36:16 +0800 Subject: [PATCH 9/9] test(chat): isolate unbound channel fixture from installed runtime Signed-off-by: song (cherry picked from commit db58562bf8db078504006f02af6f8a10f3863849) Signed-off-by: song --- tests/test_manager_channel_binding.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/test_manager_channel_binding.py b/tests/test_manager_channel_binding.py index eab42ede18..5d4b896fd8 100644 --- a/tests/test_manager_channel_binding.py +++ b/tests/test_manager_channel_binding.py @@ -420,9 +420,12 @@ def test_the_channel_quotes_the_session_mode_instead_of_deriving_it(): assert binding["session_status"] == "busy" -def test_a_channel_without_a_session_reads_as_unbound(): +def test_a_channel_without_a_session_reads_as_unbound(monkeypatch): """A ready managed endpoint is not evidence that the channel is bound.""" + monkeypatch.setattr( + host_binding, "dsh_runtime_importable", lambda *args, **kwargs: True + ) binding = manager_channel_binding({"DEEPSEEK_API_KEY": "fixture"}) assert binding["available"] is True