From 9e6dc84c5a0b38ba69cc6f398c01376e88ad9b6b Mon Sep 17 00:00:00 2001 From: song Date: Tue, 15 Sep 2026 22:34:55 +0800 Subject: [PATCH 1/4] 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/4] 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 e32659fa965372f69d2b8a079f0fb3cbef189c17 Mon Sep 17 00:00:00 2001 From: song Date: Wed, 16 Sep 2026 08:31:45 +0800 Subject: [PATCH 3/4] 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 4/4] 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