Skip to content

docs(semantics): define relative completeness boundary - #4457

Closed
songoow wants to merge 8 commits into
loopx-project:mainfrom
songoow:codex/semantic-vocabulary-proof-boundary
Closed

songoow wants to merge 8 commits into
loopx-project:mainfrom
songoow:codex/semantic-vocabulary-proof-boundary

Conversation

@songoow

@songoow songoow commented Sep 15, 2026 •

Copy link
Copy Markdown
Collaborator

Problem and behavior

Semantic completeness claims need a declared value universe and a bounded proof domain. This change makes the registry and bilingual RFC use L for source sites, U(v) for ambient runtime values and S(v) for admitted values. Production is defined before membership is checked, so producer closedness is not tautological.

The formal model gains a closed, advisory candidate-disposition vocabulary with unknown as its default. The drift smoke checks the label/default contract; this metadata supplies neither per-candidate storage nor automatic product enforcement. Each RFC language contains one canonical candidate-decision section.

Dependency and review scope

This is the foundation of the coordinated semantic chain: #4457 → #4459 → #4480. Both successor branches now contain this exact prerequisite. Land and review the foundation before its dependents; #4360 and #4482 remain separate feature branches.

Validation

Tested revision: d12be19c5666c7cd3ed61fc57571dc93eeee3d3b

  • 21 inventory/drift tests plus 4 Turn-lane fence tests passed; the isolated unbound-channel case also passed. The shared fixture correction from fix(runtime): discover Python interpreters without fixed minor lists #4482 is reused with commit attribution. Docs governance passed on the combined candidate.
  • Verified one candidate section per language, consistent domain notation and public-safe changes.
  • The exact five-PR integration candidate d8c8988b35a40d7f9784462967d3b14391d6ce75 passed 467 Python tests and 187 plugin tests, plus Ruff, kernel mypy, plugin typechecking/build and lifecycle/docs smokes. This is composition evidence, not main delivery or an independent approval.

No runtime permission, scheduling, schema enforcement stage or semantic budget is widened. Remote CI and fresh-head reviews remain required.

Signed-off-by: song <liusongstep@gmail.com>
Signed-off-by: song <liusongstep@gmail.com>

@huangruiteng huangruiteng left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

动机

semantic-vocabulary-convergence-v0 的 M0 契约里,"完备"是一个没有写边界的词:RFC 与注册表只写了生产者闭包 Produced(v) ⊆ Val(v),没有说明这个结论只在哪个语言片段、哪一层值域上成立。读者(以及按契约工作的 agent)很容易把"M0 检查通过"读成"任意动态 Python/TypeScript 的数据流与行为等价已被证明",而后者对一般程序不可判定。本 PR 把边界写清楚:区分环境值域 U(v)、注册允许集合 S(v)、实际产生集合 P(v),给出 P(v) ⊆ S(v) ⊆ U(v);把 unknown 定义成显式的失败关闭证据状态;再给"候选处理"一个封闭且穷尽的决策枚举(默认 unknown)。同时它修正 producer closedness 的陈述,并在注册表里落地为 formal_model.candidate_decisions 与 proof_boundary.unknown,由既有漂移 smoke 与新增回归测试守住。评审 head:9b71c5c62b98bc3217b81891fdddc829a493ed00,5 文件 +270/-16。

改动思路

  • 归属正确:没有新模块,改动落在既有 owner —— loopx/semantics/vocabulary_v0.json(契约与证明账本)与 examples/semantic-vocabulary-drift-smoke.py(结构校验),两份镜像文档同步更新;这与仓库里 registry + 漂移 smoke 的既有分工一致。
  • 类型化优先:七项 disposition 是封闭枚举(candidate_decisions.values,写入时按字典序排序),default 必须是 unknown,键集合被 smoke 断言为恰好 {values, default, meaning};proof_boundary 增加 unknown 分类,与既有 established/bounded/unproved 并列。
  • 失败关闭:默认 unknown 表示"证据不足不能当复用",新增回归测试把 default 改成 reuse_existing 后断言 smoke 抛 Drift。
  • 只做契约与校验,不做分析器:作者明确不声称实现全程序生产者/消费者分析、持久化兼容证明或行为等价证明,符合"M0 只对有界载体成立"的定位。
  • 正例路径:候选进入 → formal_model.candidate_decisions 声明集合与默认值 → 漂移 smoke 校验结构 → 新增测试校验"默认值退化"这一负例。

具体改动

关键内容讲解

  1. loopx/semantics/vocabulary_v0.json:36-47 新增 formal_model.candidate_decisions:values 是七个 disposition(排序后写入,顺序被 smoke 强制),default: "unknown",meaning 说明 unknown 是失败关闭的证据状态;:130-133 的 proof_boundary.unknown 增加两条(动态生产/消费路径、未分类候选)。:77 把 F1_producer_closedness 的陈述从 Produced(v) ⊆ Val(v) 改成 Produced(v) ⊆ S(v) ⊆ U(v);:18 的 universes.values 从 Val(v): values admitted by vocabulary v 改成 U(v)/S(v) 两分;:67-68 的 produces/consumes 关系改为 × U。
  2. examples/semantic-vocabulary-drift-smoke.py:242-249:check_formal_model 增加四段 require(键集合恰好、values 等于排序后的全集、default == "unknown"、meaning 非空),:250-256 把证明边界键集合放宽为四项;:52-55 的 FORMAL_MODEL_KEYS 同步加入 candidate_decisions,:70-79 的 FORMAL_CANDIDATE_DECISIONS 是判定的唯一来源。
  3. tests/architecture/test_semantic_vocabulary_drift.py:68-84:新测试断言默认值与集合,并篡改 default 后断言 Drift 消息匹配 default unresolved candidates,覆盖"默认值退化"这条负例。
  4. 两份镜像各新增一节 Soundness, relative completeness, and candidate decisions(docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md:407、…zh-CN.md:331),叙述 P ⊆ S ⊆ U、Sound/Complete 定义、dispositions 与 same_concept 不被自动提升为定理;:525 与 :645 的索引/反例表同步提到 candidate decisions。

实测(head 9b71c5c62):examples/semantic-vocabulary-drift-smoke.py → ok;scripts/generate_semantic_inventory.py --check → up to date;pytest -q tests/architecture/test_semantic_inventory.py tests/architecture/test_semantic_vocabulary_drift.py → 21 passed;examples/docs-governance-smoke.py → ok;把该 head 合入当前 main 9719dc0d(merge ref 97e4072f0)后复跑清单检查 → 仍然 up to date。

对主干的风险

阻塞项 1(P1,新增小节在两份镜像里各重复了一次)。 EN 文档中同一标题出现两次:docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md:407 与 :459(第二份接在 ### State model and schema 之前),两份都由同一个 commit 9e6dc84c5 加入;ZH 同样重复(…zh-CN.md:331 与 :374)。两份文字已经漂移:EN 一处是 M0 currently establishes only bounded claims about O(v) and registered structural carriers,另一处是 M0 establishes bounded claims about recognised source forms and registered structural carriers;the default is unknown 对 the disposition is unknown。ZH 对应 M0 当前只对 O(v)… 对 M0 只对已识别的源码形式…。契约文档里同一节出现两种措辞,读者无法判断哪一份是规范文本,而且约 100 行纯重复把 diff 放大了一倍。最小修复:每份镜像各删掉一份副本(留哪份都行),删完自检没有第二处同标题。

阻塞项 2(P1,值域改写只做了一半,Val 成了未定义符号)。 commit 9b71c5c62 把注册表值域改成 U/S(vocabulary_v0.json:18、:67-68、:77),但同一份文件里 :71 的 relations.projects 仍是 G ⊆ V × V × (Val ⇀ Val ∪ {reject})、:89 的 F3_consumer_domain_closedness 仍是 Accepted(c) ⊆ Val(v);两份 RFC 的叙述小节也照旧把 Val(v) 定义成 admitted values 并写着 Produced(v) ⊆ Val(v)(…v0.md:366-387、…zh-CN.md:301-319)——而这正是新小节要纠正的说法("Defining P(v) as a subset of S(v) in advance would make the first inclusion tautological")。结果是同一套文档里并存两种值域记法,且 Val 在 universes 中已无定义。最小修复:二选一——在 universes 里显式写 Val(v) := S(v) 作为别名,并让 projects/F3/旧叙述都指向它;或把 projects、F3 与旧叙述一并改写为 S(v),只保留一个已定义符号。

P3(文档自身惯例未跟上):该 RFC 有按评审轮次追加的变更日志(…v0.md:1001 起的 dated 小节),本 PR 新增一整节却没有对应条目,建议补一条并写入本轮结论。

P3(新枚举没有消费点):candidate_decisions 目前只有漂移 smoke 与新增测试在读,产品代码没有消费点。如果这些 disposition 要真的约束候选处理,请在 RFC 里写清"每个候选的 disposition 记录在哪里"(现在没有对应 schema);否则明确标成 advisory,避免读者把它当成已生效闸门。

其余核对:无运行时、权限、调度或默认行为变化(formal_model 是契约与证明账本,smoke 是只读结构校验);两份镜像与注册表的三处引用一致;未发现凭证、私有路径、raw 证据或本地绝对路径进入仓库。

我的整体评价

REQUEST_CHANGES。方向本身正确,而且正是这份契约该做的事:把"完备"限定在固定载体与语言片段 L0 上、把 unknown 变成失败关闭的证据状态、给候选处理一个封闭枚举,并且只用既有 owner(注册表 + 漂移 smoke + 一个回归测试)落地,没有新模块、新能力或新权威。类型化部分做得扎实:键集合、排序、默认值、meaning 都由 smoke 断言,负例测试确实能拦下"默认值退化"。要解除阻塞只需两处一致性修复:① 每份镜像删掉重复的那一节;② 把 Val 与 S/U 统一(显式别名或彻底改写),让同一份契约只有一个值域记法。两处都不涉及设计取舍;改完在新 head 上重跑四条自报命令即可,我会在新 head 上重新评审。本轮不做合并动作。

English verdict: REQUEST_CHANGES at 9b71c5c62b98bc3217b81891fdddc829a493ed00. The direction is right and the typing is solid: completeness is scoped to a fixed carrier and language fragment, an unresolved candidate becomes the fail-closed unknown evidence state, and formal_model.candidate_decisions is a closed sorted enum whose key set, ordering, default and meaning are all asserted by the existing drift smoke, plus a new regression test that catches a non-unknown default. Verified at this exact head: drift smoke ok, generate_semantic_inventory.py --check up to date, docs-governance smoke ok, pytest tests/architecture/test_semantic_inventory.py tests/architecture/test_semantic_vocabulary_drift.py 21 passed, and the inventory check is still clean on the merge tree with current main 9719dc0d (merge ref 97e4072f0), so the #4454/#4360 counter trap does not apply here. Two blocking consistency defects: the new section was pasted twice in both mirrors (EN 407 and 459, ZH 331 and 374) with already drifting wording, and the value-domain migration is half done - the registry universes no longer defines Val, while relations.projects:71, F3_consumer_domain_closedness:89 and the older narrative at …v0.md:366-387 still use Val(v) and the very Produced(v) ⊆ Val(v) statement this PR sets out to correct. Both fixes are mechanical; re-run the four self-reported commands on the new head and I will re-review it. No merge performed in this round.

Signed-off-by: song <liusongstep@gmail.com>
Signed-off-by: song <liusongstep@gmail.com>
@songoow

songoow commented Sep 16, 2026

Copy link
Copy Markdown
Collaborator Author

Review and maintenance follow-up at e32659fa965372f69d2b8a079f0fb3cbef189c17.

  • Removed the duplicate candidate-decision section from each RFC language.
  • Unified the registry and both narratives: L for source sites, U(v) for ambient values, S(v) for admitted values. Production/consumption are defined over the ambient domain before membership is checked; projection and consumer obligations no longer reference an undefined Val.
  • Marked candidate dispositions as advisory label/default metadata, with no implied per-candidate store or product enforcement, and recorded the contract repair in both execution ledgers.
  • Synced main edcddc7aa. Validation: 21 inventory/drift tests, docs governance, exact single-section/domain consistency checks, public-boundary scan and diff checks passed. The changes remove 68 net lines and add no new runtime mechanism or text-snapshot test.

The branch is independently MERGEABLE against current main. #4480 also changes the same semantic contract; reconcile its source/registry changes after this documentation layer lands. New-head review is required; no merge performed.

Signed-off-by: song <liusongstep@gmail.com>
Signed-off-by: song <liusongstep@gmail.com>
Signed-off-by: song <liusongstep@gmail.com>
(cherry picked from commit db58562)
Signed-off-by: song <liusongstep@gmail.com>

@huangruiteng huangruiteng left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

裁定(exact head d12be19c5666c7cd3ed61fc57571dc93eeee3d3b)

前一轮的两个 blocker(双语镜像重复章节、Val(v) 半迁移)在本 head 上已核实修复,语义部分我认为可以接受。但当前 head 不可合并,而且原因恰好来自一个与本主题无关的夹带 hunk,因此本次给 REQUEST_CHANGES,只差一次 rebase。

需要处理的两点

P2(阻断合并)tests/test_manager_channel_binding.py:423-432:这个 hunk 已与主干重复,并且是全分支唯一冲突点。

触发:把当前 head 合到 main。证据:git merge-tree --write-tree --name-only origin/main HEAD 只报 tests/test_manager_channel_binding.py 一处 CONFLICT;而 origin/main(08f0e08d6)第 464-480 行已经通过 #4483/#4492 落地了等价的 monkeypatch.setattr(host_binding, "dsh_runtime_importable", ...),并且还额外声明了 LOOPX_MANAGER_ENDPOINT: dsh。也就是说这次“测试隔离修复”对“定义相对完备性边界”这个目标并非必需,却让 PR 直接卡在冲突上。最小修复:rebase 到最新 main 并保留 main 版本(即丢弃该 hunk);如果确实需要这处隔离修复,请另开一个独立 PR。回归验证:rebase 后 pytest tests/test_manager_channel_binding.py -q 与 python examples/semantic-vocabulary-drift-smoke.py。

P3(非阻断,需重跑)windows-powershell 红。

CI run 35043622418 里 windows-powershell 失败于 tests/control_plane/test_effect_runtime_integration.py::test_coordination_runtime_shadow_bootstrap_crosses_python_typescript_boundary(assert 'replayed' == 'applied'),进而让 merge-gate 失败。这个文件与本次 diff 没有交集;我在 macOS 上复跑该文件 43 passed 未能复现;包含本 PR 全部提交的 #4459 其 windows-powershell 通过,main@34e511e 也通过。因此我判断这是跨平台偶发失败而不是本改动引入——但合并前必须把它重跑成绿。若稳定复现,请按其真实来源(shadow bootstrap 的幂等判定)另开 issue/PR,不要在本 PR 内夹带修复。

动机

RFC 里“完备(complete)”这个词此前没有作用域。注册表用单一 Val(v) 同时充当默认值域和允许集合,于是 Produced(v) ⊆ Val(v) 在生产本就定义在 Val(v) 上时变成恒真命题;proof_boundary 也只有 established/bounded/unproved 三档,任何“扫描通过”的结论都可能被读成证明。对后续 M0.5/M1 的语义守卫来说,这会持续放大成本:每加一条生产者规则,都要先回头纠正域定义,而“测试全绿”会掩盖这种定义层的错误。作者的做法是把值域显式拆开(U(v) 环境运行时值、S(v) 注册允许值、L 源码位点),把生产义务写成 Produced(v) ⊆ S(v) ⊆ U(v),并新增 unknown 证明边界与候选处置闭集。只补一句“完备是相对的”是不够的:注册表与 smoke 断言仍会接受旧范式。改动影响的是读 RFC 的评审者、以及消费 loopx/semantics/vocabulary_v0.json 的 drift smoke 与 inventory 生成器;非目标也说得清楚——不引入逐候选存储、不做运行时强制、不把 same_concept 提升为定理。

改动思路

架构流很简单:loopx/semantics/vocabulary_v0.json::formal_model 是权威输入,examples/semantic-vocabulary-drift-smoke.py::check_formal_model 是唯一裁决者,tests/architecture/test_semantic_vocabulary_drift.py 用 runpy 直接调用同一个函数做回归。head 上这条链被收紧为:candidate_decisions 必须恰好是 values/default/meaning 三键、values 必须等于排序后的闭集、default 必须是 unknown,proof_boundary 必须含 unknown。正路是 smoke 打印 ok 摘要(coverage=vocabularies:26/26, relations:9/9, twins=43/43),反路是任何一处漂移直接抛 Drift 并以非 0 退出。

复用的是已有 owner,而不是新造一层:注册表存范式、smoke 校范式、测试锁回归,没有新模块、没有新 capability、也没有第二个权威。候选处置落在注册表内部,只有 values/default/meaning 三个只读字段,meaning 明确写着不落地逐候选存储与运行时强制——这一点很关键,因为它避免了“先建抽象”的指责。相对基线,universes.values 由 Val(v) 拆为 U(v)/S(v),6 条 relations 全部改写为 L/U(v)/S(v) 形式,F1/F3 陈述同步更新,vocabularies 段与 coverage_floor 未动——这是一次在同一域内的范式修正,没有顺手扩大范围。

具体改动

逐段核对 base..head(236+/47-,6 文件):

  • 文档 146+/27-:双语 RFC 各新增一节 Soundness, relative completeness, and candidate decisions / 健全性、相对完备性与候选决策,包含 P(v) ⊆ S(v) ⊆ U(v)、Sound/Complete 定义、7 值候选闭集与 same_concept 的限制;附录台账补 2026-09-16 — Review consistency repair。我确认两个镜像各只剩一处同名章节、rg -n 'Val\(' docs loopx examples tests 全仓 0 命中,上一轮的两项 blocker 均已落实。
  • 注册表数据 46+/16-(含纯缩进重排):新增 candidate_decisions,proof_boundary 增加 unknown: [dynamic_producer_or_consumer_path, unclassified_vocabulary_candidate],relations/invariants 文本更新。
  • 校验与测试 44+/4-:smoke 新增 FORMAL_CANDIDATE_DECISIONS 常量与 5 条 require;架构测试新增 1 个正负例用例;另有 1 处与本主题无关的测试隔离 hunk(见上文 P2)。
  • 生产运行时代码 0 行:loopx/**/*.py 未被修改。

关键代码讲解

  1. loopx/semantics/vocabulary_v0.json:36 formal_model.candidate_decisions:声明 7 值闭集、default: "unknown" 与 advisory 语义。它是静态数据,被 check_formal_model 读取;关键不变量是“闭集 + 默认未决”,防止未解析候选被静默当成复用旧词。
  2. examples/semantic-vocabulary-drift-smoke.py:202 check_formal_model:唯一裁决点。新增断言包括 set(candidates) == {"values","default","meaning"}、candidates["values"] == sorted(FORMAL_CANDIDATE_DECISIONS)、candidates["default"] == "unknown",并把证明边界收紧为 {established, bounded, unknown, unproved}。失败即抛 Drift,无静默降级。
  3. tests/architecture/test_semantic_vocabulary_drift.py:68 test_candidate_decisions_are_exhaustive_and_default_to_unknown:正例断言闭集,负例把 default 改成 reuse_existing 后要求命中 Drift("default unresolved candidates"),把“会被拒绝”固定成回归契约。
  4. docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md:408 新增章节:把证明骨架与“全程序语义收敛已被证明”划清边界,并说明 unknown 是证据结果而非不存在证明。
  5. tests/test_manager_channel_binding.py:423 test_a_channel_without_a_session_reads_as_unbound:本次唯一的非主题改动,也是唯一的合并冲突来源。

对主干的风险

最强回归场景不是语义错误,而是不可合并:head 与 main 在 tests/test_manager_channel_binding.py 冲突,同时 merge-gate 因 windows-powershell 偶发失败被拒。触发状态是 main 在 #4483/#4492 改了同一个测试函数,而本 PR 夹带了功能等价但文本不同的 hunk;许可路径是这个 hunk 本身,所以最小修复就是丢弃它。影响面限于该 PR 的合并流程与仓库测试文件,不触达产品运行路径。

语义侧我认为风险已收敛:改动只增键、只收紧断言,没有持久化格式迁移,inventory_v0.json 与生成器一致,注册表读取端只有仓库内 smoke 与测试,没有外部消费者或跨版本读取方。反路(default 非 unknown、缺 unknown 边界)在负例中被显式验证会失败。真实边界与 mock 限制我也记录一下:本地在 macOS 上跑的是真实 smoke 与真实测试文件,但 windows-powershell 的 native 失败没能复现,其归因只能依赖间接证据(#4459 与 main 的同一作业为绿)。

另有一条非阻断观察:G ⊆ V × V × (S(v_source) ⇀ S(v_target) ∪ {reject}) 的偏函数与并集优先级在书写上有歧义,旧版 (Val ⇀ Val ∪ {reject}) 同样如此。建议在 M1 细化时加括号或脚注,本次不构成阻断。

我的整体评价

按 exact head 对比:语义部分从“Val(v) 混淆域 + 恒真义务”变为“U(v)/S(v) 分离 + 相对完备性 + unknown 边界 + 候选闭集”,并把旧范式从“可接受”变为“会被拒绝”,这是意图内的契约收紧而非漂移;observable_semantics 判定为 intentional_change_validated。repository_reuse 判定为 reused(沿用注册表 + smoke + 测试这一组既有 owner,无并行实现,无第二权威);change_proportionality 判定为 proportionate(生产机制成本为零,唯一越界项是那 4 行测试 hunk);authority_semantics 为 aligned(candidate_decisions 明确排除存储与运行时强制,不会让读者误判授权)。验证证据:semantic-vocabulary-drift-smoke.py ok、pytest tests/architecture/test_semantic_vocabulary_drift.py tests/architecture/test_semantic_inventory.py tests/test_manager_channel_binding.py 41 passed、generate_semantic_inventory.py --check up to date。

结论:语义内容我已没有 blocker,但因为当前 head 无法合并(唯一冲突来自应被丢弃的测试 hunk),且必需检查 windows-powershell/merge-gate 为红,本次给 REQUEST_CHANGES。重新评审只需要一步:rebase 到最新 main、丢弃 tests/test_manager_channel_binding.py 的 hunk、重跑 CI;只要新 head 上这两项转绿,我会直接按内容批准,不需要再改语义部分。

English verdict: REQUEST_CHANGES — both prior blockers are genuinely fixed (Val( is gone repo-wide and each mirror now has a single section), but this exact head cannot merge: the only conflict with main is the off-theme tests/test_manager_channel_binding.py hunk that main already implements via #4483/#4492, and windows-powershell/merge-gate are red from an unrelated, locally unreproducible failure; rebase, drop that hunk, rerun CI and the semantics content is approvable as-is.

Signed-off-by: song <liusongstep@gmail.com>

@huangruiteng huangruiteng left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

动机

主干语义契约里 Val(v) 一个符号同时承担了两件事:候选词汇运行时可能出现的环境值域,以及被采纳进契约的集合。两者合一时,生产者封闭性(producer closedness)变成同义反复——"所有生产出来的值都 ∈ 被采纳集合"只要两集合相同就恒真,于是扫描全绿可以被读成"完备性已证明",而它其实什么也没证明。受影响的调用方不是运行时路径,而是两类人:读语义 RFC 或注册表来推导值域的评审者,以及按这份契约新增生产者规则的贡献者。代价是真实的:这个 PR 到本轮已经消耗了三轮评审,前两轮里有相当一部分花在重新推导值域而不是看语义。

作者给出的 before/after 是:合并基线(08f0e08d6)上只有一个 Val(v)、证明类别是 established/bounded/unproved、没有候选词汇表;head 上拆成 L(源码站点)/U(v)(环境值)/S(v)(被采纳值),义务写成 P(v) ⊆ S(v) ⊆ U(v),证明边界加入第四类 unknown,并新增一份封闭的七值候选处置词表,默认值是 unknown。

为什么最近的更小修法不够:把边界写进散文而不拆值域,等于保留那个恒真式,只是加了一段说明;只拆值域而不加 unknown,则"没有证据"仍然只能被记成"未证明存在",而这两件事在候选处置上必须区分;只改 RFC 不动注册表,则唯一的裁决者(drift smoke)仍然检查不到这条规则,语义会立刻漂回文档。所以这次的最小可行动作就是"注册表数据 + smoke 断言 + 一条测试",作者也正是这么做的。

改动思路

权威状态仍在原地:loopx/semantics/vocabulary_v0.json::formal_model 声明值域、角色关系、义务、proof_boundary 与新增的 candidate_decisions;examples/semantic-vocabulary-drift-smoke.py::check_formal_model 是唯一裁决者,测试文件通过同一个函数复用同一条规则。没有新模块、没有第二权威、没有持久化字段。

正路径是:读注册表 → check_formal_model 校验值域、关系、义务、证明边界与候选处置词表(键必须恰为 values/default/meaning,值集必须等于排序后的封闭集,默认值必须是 unknown)→ check_inventory 重新渲染语义清单并要求与提交文件一致 → smoke 打印 ok → tests/architecture/test_semantic_vocabulary_drift.py 在默认 pytest -q 扫描中冻结这条契约 → docs-governance-smoke.py 校验中英 RFC 镜像。任一对不上,smoke 抛 Drift 并以非零退出,没有静默回落。

与既有实现的比较:主干上表达同类语义的还有 loopx/semantics/inventory_v0.json(由生成器再生成的 carrier 报告,不承载 admitted-value 语义),以及 RFC 自身;本 PR 是扩展这三件套而不是另起一处,这一点是它最值得保留的地方。七值处置词表被声明为 advisory,meaning 明确否认了"逐候选存储"和"运行时强制",RFC 也保留了 per-candidate 处理属于后续工作这一边界,因此它没有把分类能力伪装成新的权威或 actor 生命周期。

具体改动

5 个文件、+232/−46(相对 merge base 08f0e08d6):两版 RFC(英文 93 个变更行、中文 80 个)、loopx/semantics/vocabulary_v0.json(62)、examples/semantic-vocabulary-drift-smoke.py(23)、tests/architecture/test_semantic_vocabulary_drift.py(20)。没有任何 loopx/**/*.py 产品运行时代码被修改,唯一的可执行行为是 smoke 对形式模型的 fail-closed 裁决。

关键代码讲解

formal_model.candidate_decisions(loopx/semantics/vocabulary_v0.json:36):封闭的七值候选处置词表与它的 unknown 默认值。改动前"没有记录处置的候选"根本没有标签;现在值集固定为 compatibility_only / create_vocabulary / extend_vocabulary / external_input / local_only / reuse_existing / unknown,且 meaning 显式声明不存储、不强制。关键不变量是默认值必须是 unknown:一个未解析的候选不能被静默算成"复用既有词汇"。

check_formal_model(examples/semantic-vocabulary-drift-smoke.py:202):形式模型的唯一裁决者。它除了原先的值域/关系/义务检查,现在额外要求 candidate_decisions 的三个键、排序后的封闭值集、default == unknown,以及证明边界里存在 unknown。任何偏离都以具名理由抛 Drift,所以"未解析"再也不能被读成"已证明不存在"。

test_candidate_decisions_are_exhaustive_and_default_to_unknown(tests/architecture/test_semantic_vocabulary_drift.py:68):把正例(七值封闭集)与反例(把内存副本的 default 改成 reuse_existing,要求 smoke 必须失败)都冻结下来。它跑在默认 pytest -q 扫描里,所以这条规则不依赖 canary 才被检查;磁盘上的注册表不会被反例改动。

对主干的风险

P2(阻断)— 这个 head 相对当前主干已经不携带任何内容。 把 exact head 合入 origin/main(079643038)是一次内容空操作:git merge-tree --write-tree origin/main <head> 得出的树与 origin/main 的树完全相等(两者都是 113f4dc133458e64fc504aa1e6e3bda0b124917e),真实执行 git merge --no-commit --no-ff 也报告 Automatic merge went well 且暂存区为空。原因是这条改动要交付的那块地基已经通过已合并的依赖项 #4459 落在主干上,主干此后又往前走了一步。

相对主干,这个分支只剩"更旧":loopx/semantics/vocabulary_v0.json 与 tests/architecture/test_semantic_vocabulary_drift.py 逐字节相同,而两版 RFC 会丢掉主干已有的 Interpreter and checkout 段落及其指向本地验证文档的链接、主干已经改为 uv run 的命令拼写,以及主干保留的 PR review lanes 段落;smoke 那一行也会把修复提示退回成旧的 python3.11 scripts/generate_semantic_inventory.py。所以接受这个 head 只会产生一个空合并提交,同时把这条已交付的地基记在一个过期的 head 上。最小修法:按"已被 #4459 取代"关闭这条 PR(并在 #4480 里改以主干为基线),或者 rebase 到当前主干、删掉上述四处被取代的文本,再重跑 drift smoke、tests/architecture/test_semantic_vocabulary_drift.py、tests/architecture/test_semantic_inventory.py、scripts/generate_semantic_inventory.py --check 与 examples/docs-governance-smoke.py,让被评审的增量重新变成真实增量。没有任何仓库检查能发现"内容冗余的分支",可复现的检查就是上面那两条 merge 命令。

上一轮的阻断项已修复。 全仓 rg 'Val\(' 命中数为 0;两种语言的 RFC 各只剩一节候选处置小节;python examples/semantic-vocabulary-drift-smoke.py 输出 ok(coverage=vocabularies:26/26、owner_symbols:46/46、relations:9/9),pytest tests/architecture/test_semantic_vocabulary_drift.py tests/architecture/test_semantic_inventory.py 21 项通过,scripts/generate_semantic_inventory.py --check 退出码 0,examples/docs-governance-smoke.py 通过。

残余风险与证据边界。 本次没有取用远程 CI:本轮解析出的评审策略是 wait_for_ci=false,明确要求评审者不抓取、不轮询 CI,因此上一轮提到的 windows-powershell 观察属于另一个 head,本轮不据此判断。proof_boundary 那一半契约我只通过仓库自带测试确认,没有自己做独立的 mutation 对照;我做的是候选处置默认值的对照。另外"内容冗余"这个结论绑定在 origin/main 为 079643038 这个事实上,如果任何合并决定之前主干又移动了,这两条合并检查需要重跑。

我的整体评价

我独立复现了观测语义,而不是只读 diff:在 exact head 上跑真实的 smoke 得到 ok,且 coverage 明细与作者声明一致;把注册表的 formal_model.candidate_decisions.default 从 unknown 改成 reuse_existing 后,smoke 以退出码 1 失败并给出具名理由 formal_model candidate_decisions must default unresolved candidates to unknown,还原后 smoke 重新为 ok、工作区干净。这个方向是对的:值域拆分、unknown 作为证据结论而非缺失证明、以及把裁决留在既有的 smoke 里,都符合"类型化契约优先于散文规则""复用既有 owner"的要求;语义层面我没有发现阻断性问题。

但作为一次变更请求,它已经不再成立:地基已随 #4459 落在主干,合入这个 head 是内容空操作,而分支自身在主干的四处文本上更旧。因此我的结论是 REQUEST_CHANGES,理由不是语义错误,而是"这条 PR 现在没有可交付的增量"——请按取代关闭,或 rebase 后重新界定增量并重跑上面那组验证。下一次评审从新的 exact head 重新开始。

English verdict: REQUEST_CHANGES — exact head 27ef366ecf2bec77e3a4f3157f70b5a2735afe6e of #4457. The semantics themselves are correct and already guarded: the U(v)/S(v)/L split, the four proof-boundary categories and the closed seven-value candidate-disposition vocabulary with default: unknown all hold at this head (drift smoke ok with coverage=vocabularies:26/26, owner_symbols:46/46, relations:9/9; 21 focused architecture tests pass; inventory --check exit 0; docs governance ok; the previous round's duplicated bilingual section and half-migrated Val(v) are gone, with rg 'Val\(' at zero hits). One blocking P2, at the change-request level rather than in the code: merging this exact head into current origin/main (079643038) is a content no-op — git merge-tree --write-tree origin/main <head> returns main's own tree 113f4dc13… and a real git merge --no-commit stages nothing — because the foundation this PR exists to deliver already landed through the merged #4459. Relative to main the branch is only older: the registry and the drift test are byte-identical, while both RFC files would drop main's Interpreter and checkout guidance and its local-validation link, main's uv run spellings and main's PR review lanes paragraph, and the smoke would restore the older python3.11 repair command. Minimum repair: close this PR as superseded (and base #4480 on main), or rebase onto current main, drop the four superseded regions and re-run the drift smoke, tests/architecture/test_semantic_vocabulary_drift.py, tests/architecture/test_semantic_inventory.py, scripts/generate_semantic_inventory.py --check and examples/docs-governance-smoke.py. Residual risk: remote CI was intentionally not consulted per this run's resolved policy (wait_for_ci=false), the proof_boundary half was verified only through the repository's own test file, and the redundancy conclusion is bound to origin/main 079643038, so the merge checks must be repeated if main moves before any merge decision.

@songoow

songoow commented Sep 16, 2026

Copy link
Copy Markdown
Collaborator Author

Closing as superseded, on the same basis documented when #4461 was closed.

The review at head 27ef366ec is correct and I independently reproduced its blocking observation: merging this head into current origin/main is a content no-op. git merge-tree --write-tree origin/main 27ef366ec returns main's own tree, and relative to main this branch's loopx/semantics/vocabulary_v0.json and tests/architecture/test_semantic_vocabulary_drift.py are byte-identical. The foundation this PR exists to deliver already landed through the merged dependency #4459.

I re-ran that check after main moved from 079643038 to f4ed58de9, since the redundancy conclusion is bound to a specific main: this head is still a no-op.

I did not take the review's second suggested repair (rebase onto current main and drop the four superseded regions). Dropping main's Interpreter and checkout guidance, main's uv run spellings, main's PR review lanes paragraph and main's newer smoke repair command leaves no increment at all — the branch carries no unique content, so a rebase would produce a PR with nothing left to review. Closing is the only repair that lands the work on a non-stale head.

No source branch was deleted, no review discussion was removed, and no change was reverted. The semantic content of this PR is present in main and remains guarded by the drift smoke and the architecture tests it introduced. #4480 carries the ongoing M0.5 work and is being rebased onto current main separately.

@songoow

songoow commented Sep 16, 2026

Copy link
Copy Markdown
Collaborator Author

Superseded by the merged #4459; content no-op against current main as verified above. Branch and discussion preserved.

@songoow songoow closed this Sep 16, 2026
@songoow
songoow deleted the codex/semantic-vocabulary-proof-boundary branch September 16, 2026 05:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants