test(semantics): mutate the formal-model signature; separate stage, evidence and blocking claims (B0)

[songoow]

Delivers slice B0 of #4447, the declared head of the Track B chain and the last slice still unstarted. Per the task brief, PR #4631 turned out to be merged into main already (440b002fb), so the domain fixtures are present in my base rather than pending — I did not duplicate them and did not depend on them.

What I found

check_formal_model() was thorough on shape and touched by exactly one test (test_candidate_decisions_are_exhaustive_and_default_to_unknown, which reads two fields of candidate_decisions). The exact key set, the five roles, the consumer hierarchy, the seven relation kinds, the six invariant ids, the per-invariant shape and the four-lane partition were entirely unmutated. The regressions B0 asks for did not exist.

Two real defects fell out of doing the work:

1. A duplicate invariant entry was accepted. The id check and the lane-partition check are both set comparisons, so a repeated entry leaves them unchanged, and every dict check_formal_model builds by id keeps only the last occurrence. A second F1_producer_closedness carrying a weaker statement validated, and nothing recorded which of the two the smoke had walked. Fixed by requiring each id exactly once — a one-line tightening, not a weakened check.

2. The RFC's blocking_next gloss was false. Section 11 described that lane as "Planned blocking checks after M0.5; not claimed by M0". F1, F2 and F4 sit in that lane and all three fail closed today. Measured, not assumed:

Mutation	Actual result
Drop a registered value executor.py::_run_turn writes	turn_result_kind: producer writes unregistered values ['repair_required']
Add a kernel value nobody produces	turn_result_kind: decoder does not produce registered input zzz_never_produced
Remove one context from the SOURCE_SURFACES declaration	SOURCE_SURFACES: contexts must name every defining module exactly once

Each exits the smoke non-zero, and by I10 the smoke runs on the pull-request path. The RFC text is what changed here — the lane name still records the milestone that owns the check, and the blocking claim moved to its own column, so the two readings stop being one sentence.

What each regression proves

tests/architecture/test_semantic_formal_model.py — new file, not an append to test_semantic_vocabulary_drift.py, which three open PRs already collide at. 26 single mutations plus 5 structural tests. Every mutation asserts the checker fails closed naming its own rule; a mutation that fails for an unrelated reason proves nothing and would rot into a test that only asserts "something raised".

Group	Cases
Signature	missing key, extra key, schema drift, dropped universe
Roles / hierarchy	dropped role, dropped subrole from role_hierarchy, emptied hierarchy, hierarchy reparented to owner
Relations	dropped relation kind (persists, which F6 quantifies over), extra relation kind
Invariant entries	missing invariant, duplicated id, unknown stage, empty statement, empty evidence, missing domain, extra field
Four lanes	id in two lanes, lane disagrees with enforcement, dropped lane
Stage vs walked domain	unproved claims verified members, advisory claims verified members, widened domain
Boundary / candidates	empty proof-boundary claim, dropped boundary class, default not unknown

Plus test_metadata_shape_is_not_an_executed_proof, which pins the B0 exit condition in executable form: a validated block asserts only that each obligation declares a stage, a non-empty evidence boundary and a domain the smoke recomputes from the registry — never that the obligation holds.

What RFC text changed and why

Both mirrors, same rows (docs-governance-smoke.py passes; verified 45 headings, 2 ledger entries and 5 decision rows in each).

• Section 11 lane table gains Implementation stage and Blocks a pull request today as separate columns, with the correction note. Measured vs. claimed, above.
• Section 5 gains "Four separate readings of one obligation row" — schema validation, implementation stage, evidence status, blocking behaviour — stating for each what it can and cannot say, and pointing at the new test file. The domain table now carries stage and blocking beside the verified / registered counts. I2 and I11–I14 each gained an explicit stage / evidence / blocking sentence.
• Schema table: formal_model is now described as schema validation only; enforcement_policy is described as a milestone label, not a blocking claim.
• Appendix A ledger entry dated 2026-09-17, and Appendix B decision row dated 2026-09-17 with alternatives (renaming the lane — rejected, it would lose the milestone mapping and collapse the readings the other way; adding a blocks_today field — rejected, one more declared field a reader could mistake for a measurement). Both mirrors.

Deliberately left undone

The grounding gap the 2026-09-17 domain entry named is still open, and I have said so in Appendix A rather than implying B0 closed it: moving an invariant's enforcement and its policy lane together stays internally self-consistent, so a coordinated two-field edit can still downgrade a check with no test failing. Closing it needs the lane derived from the code that runs rather than declared beside it. B0 narrows the gap to a coordinated edit and documents the residue; it does not close it.

Validation

$ python3 examples/semantic-vocabulary-drift-smoke.py
semantic-vocabulary-drift-smoke: ok
  coverage=vocabularies:26/26,owner_symbols:51/51,literal_scan_fields:1/1,projections:1/1,relations:9/9,schema_versions:1/1
  ...
  formal_domain=F1:6/26,F2:6/26,F3:0/26,F4:4/4,F5:1/1,F6:0/0 (verified/registered)
  formal_domain_bounds: kernel_with_producers=6/6 cross_runtime_unverified=20/20 producer_scan_reach=436/1207_files projections=1/1 scope_declarations=1 declared_contexts=4/4
EXIT=0

$ python3 examples/docs-governance-smoke.py
docs-governance-smoke ok
EXIT=0

$ /tmp/loopx-pr3668-venv/bin/python -m pytest tests/architecture/ -q
366 passed in 145.48s (0:02:25)

$ PYTHONPATH=. /tmp/loopx-pr3668-venv/bin/python -c "import sys; sys.argv=['loopx','canary','premerge','--from-git-diff']; from loopx.cli import main; raise SystemExit(main())"
## Risk Profile Smokes — ok: true, selected_checks: 8, executed_checks: 8, failures: 0
## Public Boundary — ok: true, selected_checks: 1, executed_checks: 1, failures: 0
EXIT=0

Note for the reviewer: origin/main advanced to 001c6daf2 while I worked. The three PRs merged there (#4659, #4657, #4653) touch support_control*.py, the interaction-pattern catalog and the change-window fixture — disjoint from every path in this diff, so no rebase was needed and none of the four gates above is affected.

Worktree: /home/ubuntu/loopx-b0, branch codex/b0-formal-model-reconciliation, two commits split by reviewer logic (tests / docs), both DCO signed off.

Refs #4447 (B0)

🤖 Generated with Claude Code

[huangruiteng]

Reviewed exact head: 6671bc3c22a915652a5ea5b918caa2b33e920a9d (base main @ 440b002fb, merge base unchanged since 2026-09-17T14:27:33Z).

动机

这是 #4447 Track B 的 B0 切片，审阅框架是仓库自己的 RFC docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md（第 5 节、第 11 节、附录 A）。

作者指出的是一个可测量的文档不一致：第 11 节的层级表把 blocking_next 注解为"planned blocking checks after M0.5; not claimed by M0"。这句话在该层级被命名时成立，但在 M0.5b 交付之后就变成错的——check_producers 与 check_scope_declarations 都由 smoke 的 main()（经 check_inventory）调用，按 I10，这个 smoke 在每个跑 Python 测试的 PR 上失败即关闭。于是"实施阶段"和"今天是否阻断合并"这两件事被同一张表的同一句散文混在一起。

第二个问题是同类风险的另一面：check_formal_model 是唯一守着 formal_model 这块规范性元数据的检查器，但此前只有一个测试触及它，而且只读了 candidate_decisions 的两个字段。键集合、五个角色、consumer 层级、七种关系边、六个不变量 ID、逐条不变量的形状、四层划分——全部删掉也能绿。元数据被校验过，就容易被读成"已被证明"；而校验器本身无人守护。

改动思路

作者没有重命名 blocking_next（那会丢掉"哪个里程碑拥有这项检查"的信息），也没有给 formal_model 加 blocks_today 布尔字段（那只会再多一个可被误读为"测量值"的声明字段）。他选择把一条义务行的四种读法拆开陈述——schema 校验、实施阶段、证据状态、实际阻断行为——并明确"只有 main() 里的代码决定什么会拦住合并"。

对第 4 种读法，他补的是测试而不是宣称：26 条单点突变，每条只改一处，断言检查器失败即关闭并指名那一条规则；再加 4 条把关键结构钉住的直接断言。并且他真的做了一次突变实验，找到了一个逃逸案例：重复的不变量条目（id 集合与层级划分都是集合，重复项不会改变它们，而检查器按 id 建的 dict 只保留最后一次出现）能被接受，于是新增了一条 fail-closed 规则。

具体改动

examples/semantic-vocabulary-drift-smoke.py（+8/-3）：唯一的行为改动。原来的 {item.get("id") for item in invariants} == FORMAL_INVARIANTS 被拆成三步：先要求是 list，再要求 id 集合相等，再要求 len(invariant_ids) == len(set(invariant_ids))。这是一条真实的收紧，不是措辞调整。

tests/architecture/test_semantic_formal_model.py（新增 311 行）：MUTATIONS 表是 (mutation, match) 对，match 字符串直接绑定检查器的报错文本；另有基线、重复条目、"层级与阶段一致"、"形状不等于已执行的证明"四条直接断言。文件用 runpy.run_path 加载 smoke 并深拷贝 registry，不重写任何规则。

两份 RFC 镜像（+138/-23 与 +111/-24）：I2、I11–I14 各加上实施阶段、证据边界、今天是否阻断三件事；第 5 节新增"同一条义务行的四种读法"表格；第 11 节层级表拆成"实施阶段"与"今天是否阻断 PR"两列，并在正文里说明为什么保留旧层级名；附录 A 新增执行账本条目，明确写出未解决的部分（把 enforcement 与层级一起改动仍能降级检查，B0 只把缺口收窄到一次协同编辑，没有关闭它）。

对主干的风险

风险面很窄且方向正确：产品运行时、CLI、持久化、权限边界都不涉及，唯一的运行时行为变化是让一个此前会静默通过的畸形 registry 变成失败。

我独立做了两件事，而不是只读 CI：

1. 验证突变测试确实绑住规则，而不只是"能通过"。把 require(set(model) == FORMAL_MODEL_KEYS, ...) 放宽为 >=，test_formal_model_mutation_fails_closed[extra_key] 立刻变红；把新增的唯一性 require 换成 True，[duplicated_invariant_id] 与 test_duplicate_invariant_entry_cannot_restate_an_obligation 立刻变红。两次实验都在审阅用 worktree 内完成，随后 git checkout 还原，git status 干净。
2. 验证文档里"今天即阻断"的事实主张。直接在 registry 层面删掉一个 SOURCE_SURFACES 声明上下文，check_scope_declarations 抛出 SOURCE_SURFACES: contexts must name every defining module exactly once——与 RFC 引用的报错逐字一致；check_scope_declarations 确实由 check_inventory 调用，而 check_inventory 在 main() 里。I10 也成立：tests/architecture/test_semantic_vocabulary_drift.py 以子进程运行 smoke 并断言 returncode == 0，该文件由 python-tests.yml 的 pytest -q 收集。

验证结果：突变测试文件 31 passed；tests/architecture 全量 366 passed（91.20s）；smoke 打印 ok，formal_domain=F1:6/26,F2:6/26,F3:0/26,F4:4/4,F5:1/1,F6:0/0，与 RFC 表格逐行吻合。

非阻塞的两点（均已在 PR 正文中披露，不构成阻断）：

• P3：match 字符串与检查器报错文本耦合。改一条报错文案会同时让对应突变用例以"未匹配"失败。失败方向是响的（红而非绿），代价是改动时的连带修改成本；文件 docstring 已经把 match 定义为契约的一部分。
• P3：把某条不变量的 enforcement 阶段与它所在的 policy lane 一起改，仍然可以降级检查而不触发任何测试——这正是作者在附录 A "Not addressed here" 里主动写下的残留。关闭它需要层级由实际运行的代码推导，属于另一片工作，B0 只把缺口收窄到一次协同编辑。

我的整体评价

APPROVE。这是一个"用测量代替宣称"的切片：它先证明旧注释已经为假，再证明校验器几乎无人守护，然后只用一条 fail-closed 规则和一组单点突变把两件事钉住，并且把没关掉的缺口写在账本里而不是留在正文的暗示里。文档层面的改动方向与我读到的实际代码一致，我没有找到把声明写强于代码的地方。

我另外确认这不是 PR farming：songoow 在同一条 #4447 链上已有 8 个已合并切片，本次三个 PR（4661 / 4662 / 4663）是 B0、Track A、B5 三个不同切片，不是同一形状的重复提交。

English verdict: APPROVE - PR #4661 at head 6671bc3; the lane table's blocking claim is corrected and the formal-model signature is now guarded by 26 single-mutation regressions plus one real fail-closed rule (duplicate invariant ids), validated locally (31 passed for the new file, 366 passed for tests/architecture, smoke ok) and independently reproduced by weakening two checker rules and by dropping a declared scope context.

[huangruiteng]

Merge-readiness qualification — #4661 @ 6671bc3c22a915652a5ea5b918caa2b33e920a9d

结果：not ready，但只剩一项，且不是代码问题。

loopx pr-review --repo huangruiteng/loopx --check-merge-readiness 4661@6671bc3c22a915652a5ea5b918caa2b33e920a9d
→ ready=false
  blocking_reasons: merge_state_requires_update
  merge_state: BEHIND
  review_decision: APPROVED
  checks: 24/24 success（含必需检查 Sign-off、merge-gate）
  review_threads: total 0, unresolved 0
  authority: grants_merge_authority=false,
             admin_bypass_overrides_this_gate=false

唯一阻塞项可以精确对到 main 上生效的 ruleset protect main（ruleset id 18121976）：

阻塞项	触发规则	需要的动作
merge_state_requires_update（BEHIND）	strict_required_status_checks_policy: true —— head 必须包含 main 的最新提交	更新本分支（作者 rebase 或合并 main，维护者也可用 “Update branch”）

该 exact head 的评审结论（APPROVE）与全部必需检查都已就绪，所以更新分支之后需要重新做的是对新的 head 重新评审并重跑门，而不是重新讨论本 PR 的设计。

更新分支时请注意同一 ruleset 的另外两条规则

• dismiss_stale_reviews_on_push: true —— 推入新 commit 会废止旧审批，所以更新分支后必须在新 head 上重新评审。
• require_last_push_approval: true —— 推入更新的那个人不能提供计入的审批。因此这次更新最好由作者本人完成：如果由维护者推入，则本轮维护者的审批将无法计入，PR 反而会被卡在 REVIEW_REQUIRED（本仓库的 test(manager-context): guard receiver isolation and successive requests #4640 正是这种情形）。

本轮做了什么、没做什么

• 读取了该 exact head 的审批状态、检查结论与 review thread 摘要，并运行了上面的合并门命令；结论与 PR 正文的证据一致。
• 没有合并，也没有使用 admin bypass（门返回 admin_bypass_overrides_this_gate=false）。
• 门必须在合并前对未变化的 head 重新运行；本 head 一旦变动即 restart_review_and_rerun_gate。

English verdict: APPROVE - PR #4661 at head 6671bc3; the review conclusion and all required checks are green at this exact head, and merge readiness is blocked only by merge_state_requires_update (strict required status checks, ruleset protect main), which the author should resolve by updating the branch before the gate is re-run.