docs(semantics): govern vocabulary convergence by proof stage - #4453
huangruiteng merged 5 commits into
Conversation
…, and add a target state A fourth review of the M0 slice found three gaps in the RFC rather than in the guard. The RFC said repository-wide while the inventory root and every literal scan read loopx/ only; Section 3 now says so and lists apps/ and examples/ as non-goals. Merging twelve upstream commits staled the committed inventory, and replaying the scanner over the last twenty upstream merges showed eight would do the same, so Section 10 records the merge-order hazard and the interim regenerate rule, and Section 12 gains Q9 for the maintainers' policy choice. The plan had ratchets but no definition of done; Section 11 gains a target-state table and Section 12 gains Q10 (Turn vocabulary end state) and Q11 (identifier-counted retirement budgets). SOURCE_SURFACES is recorded as bounded-context reuse of one name, not a fork, in Section 5 and in the registry note, so nobody lowers the budget by renaming it. No code path, budget, or anchor changes. The premerge planner keeps python3 on purpose: every fleet command is spelled that way and the runner smoke asserts the text; the interpreter requirement is documented in Section 10 instead. (cherry picked from commit 2099ea39e288a471d090da128cdcc6747174dc0a) Signed-off-by: song <liusongstep@gmail.com>
…1 on an M0.5 slice The RFC used producer and consumer nineteen times without defining either, Q2 and Q10 waited on a producer check the document never specified, scope existed only as a preview paragraph, and Section 1 still said the smoke ran on every premerge and fleet run after Section 10 made the pytest sweep the obligation. Section 5 gains a roles table (owner, producer, interpreter, pass-through) with one check per role, the fixed production forms, and which tiers must list producers; the schema table gains scope, producers, and compatibility_only. Section 2 gains I11 to I14, each marked enforced from M0.5 so the M0 smoke is not claimed to do what it does not. Section 9 gains three M0.5 rows including the expected first failure on skip. Section 11 gains the M0.5 milestone and M1 now gates on it. Q2 and Q10 point at I12 instead of an undefined check. Both language versions move together; docs governance, the drift smoke, and the architecture tests stay green. No code, registry value, or budget changed. (cherry picked from commit a8bf889c7bd3dd1ccd9ffb230482aba7d6e46276) Signed-off-by: song <liusongstep@gmail.com>
Signed-off-by: song <liusongstep@gmail.com>
Signed-off-by: song <liusongstep@gmail.com>
Signed-off-by: song <liusongstep@gmail.com>
f951e98 to
554248b
Compare
huangruiteng
left a comment
huangruiteng
left a comment
There was a problem hiding this comment.
动机
词汇收敛现在有几套规则：注册表里的词表/关系/预算、drift smoke 的字面量扫描、RFC 第 9 节的证据表。缺的那一块是**"这条性质现在到底强制不强制"**：RFC 里已经按 M0/M0.5/M1 标了阶段，但那只是一张散文表，没有任何机器可读副本。后果是把"计划要强制"读成"已经证明"——F1/F2/F4/F6 会被当成已经成立的性质来引用，M1 的合并门看起来像是已经满足。这个 PR 把车道写进 registry 并让 smoke 校验，方向我认可：它让"未证明"可以被 CI 拒绝，而不是靠评审者记性。
改动思路
loopx/semantics/vocabulary_v0.json新增formal_model：有限全域（vocabularies/values/sites/scopes/roles）、角色与role_hierarchy（consumer = [interpreter, pass_through]）、七种关系、F1–F6 不变式（每条带 statement/evidence/enforcement）、proof_boundary（established/bounded/unproved）与enforcement_policy四条车道。examples/semantic-vocabulary-drift-smoke.py新增check_formal_model与三组硬编码常量，并把formal_model加进REGISTRY_KEYS。- RFC（英文 + zh-CN 镜像）补上角色/作用域、I11–I14、两条车道的执行模型、M0.5 切片与新的证据行。
- 顺带在 registry 的
multi_value_forks语义里加multi_value_forks_note，写明 SOURCE_SURFACES 的 4 个 fork 属于有界上下文复用，必须靠 M0.5 的 scope 声明减少，不许靠重命名。
具体改动
docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md（+342/-3）与.zh-CN.md（+266/-4）：:424 registry 契约表新增formal_model一行，:641 起"两条车道"执行模型，:665-668 车道表，:543 的变异行要求删掉不变式/角色/关系即失败。examples/semantic-vocabulary-drift-smoke.py（+68）：:52FORMAL_MODEL_KEYS、:68FORMAL_ENFORCEMENT、:69FORMAL_POLICY_KEYS、:159唯一调用点、:193check_formal_model、:222-231划分与阶段一致性断言。loopx/semantics/vocabulary_v0.json（+93）：:14起formal_model，:33起enforcement_policy（blocking_now=F5 / blocking_next=F1,F2,F4 / advisory=F3 / unproved=F6），:760multi_value_forks_note。
关键内容讲解
- 车道是可校验的，不是散文。
:222要求四条车道恰好划分 F1–F6 各一次，:231再要求每条不变式自己的enforcement与所在车道一致。我把enforcement_policy.blocking_now清空后 smoke 立刻失败：formal_model enforcement_policy must partition all invariants exactly once；恢复后git status干净。这条探针正是"未证明不能被报成 passed"的守门人。 - 没有另建权威。
formal_model不复述词表、不复制预算锚点：它引用 F1–F6 的声明式不变式，proof_boundary.unproved明确列出all_producers_are_found、persistence_reader_compatibility等尚未证明的命题；registry schema_version 未变，也没有新增 CLI 面。M0.5 的scope/producers/生产形式扫描只被声明为路线图，没有提前落地实现。 - 验证证据：
examples/semantic-vocabulary-drift-smoke.py→ ok；scripts/generate_semantic_inventory.py --check→ semantic inventory up to date；pytest -q tests/architecture/test_semantic_inventory.py tests/architecture/test_semantic_vocabulary_drift.py→ 20 passed；4 个改动文件的 public boundary scan 干净。
对主干的风险
P3（车道表有两份手写副本）。RFC :665-668 的车道表与 registry 的 enforcement_policy（vocabulary_v0.json:33）是同一份"哪条性质当前阻塞"的知识，但没有机器比较：smoke 只校验 registry 自洽，不读 RFC 表格。把 F4 从 blocking_next 挪到 advisory 时若只改 registry，RFC 会静默过期，而评审者通常先读 RFC。最小修法：在 smoke 里加一条一致性检查（解析 RFC 表格的 lane→invariant 映射，或让表格由 registry 生成），并补一个"只改 RFC 某一行"的负例。
P3（m1 是允许写入但无法使用的值）。FORMAL_ENFORCEMENT（:68）允许 m1，但 stage_for_policy（:223）只有 m0/m0_5/advisory/unproved 四条车道。因此任何按枚举写成 enforcement="m1" 的不变式必然触发 partition 失败，而报错说的是"划分不完整"，作者会误以为漏写 id。最小修法：删掉 m1（M1 落地时再连同车道一起加），或在车道表与 RFC 中补一行说明 M1 尚未启用。
P3（新的 ratchet 没进既有 mutation 参数化）。tests/architecture/test_semantic_vocabulary_drift.py:43 仍然只参数化 ["twin_budget", "twin_root", "scan_root"]，formal_model 的形状只被 smoke 自身断言保护。最小修法：把 formal_model 加进该参数化，或加一条同形用例（把 F5 移出 blocking_now），断言失败信息点名具体车道。
其余残余风险：本轮只有本地等价验证——packet 上没有 CI rollup 可读（checks.total=0），所以"远程 CI 绿"未被证实。multi_value_forks_note 只是文字理由，不会立即降低 SOURCE_SURFACES 的 fork 计数（作者也明写要等 M0.5 的 scope 声明），这是有意的保守选择。本 PR 不改 runtime、quota、todo、权限或任何用户可见行为，合并后除架构预算车道外没有回滚面。
我的整体评价
APPROVE。它把"这条性质现在强制 / 计划强制 / 只是建议 / 尚未证明"从 RFC 散文变成可被 CI 拒绝的 registry 契约，并且没有顺手把 M0.5 的字段提前实现，规模与主题是配的（762 行里 608 行是规范文档与中文镜像，93 行声明数据，68 行校验）。三条发现都是局部可修的低风险项：车道表的两份副本、m1 死值、以及新 ratchet 没进 mutation 参数化；它们影响的是将来这次改动自身的可维护性，不改变本 PR 该不该合并的判断，也不引入新的状态或权限。不阻塞合并。
English verdict: APPROVE at 554248b. The PR turns the vocabulary-convergence rules into a machine-checkable contract: loopx/semantics/vocabulary_v0.json gains a formal_model (finite universes, roles, role hierarchy, relations, invariants F1-F6, proof boundary, and a four-lane enforcement policy) and the drift smoke gains check_formal_model, which asserts that every invariant appears in exactly one lane and that the lane agrees with its own enforcement stage. I verified the new ratchet by mutation: emptying enforcement_policy.blocking_now fails the smoke with "formal_model enforcement_policy must partition all invariants exactly once", and the file was restored clean. Validation at this head: drift smoke ok, generate_semantic_inventory.py --check up to date, 20 passed in tests/architecture/test_semantic_inventory.py + test_semantic_vocabulary_drift.py, and the public/private boundary scan is clean on all four changed files. The change adds no runtime behavior, no new CLI surface and no state; M0.5 fields stay declared-only. Non-blocking findings: the RFC lane table (lines 665-668) and the registry enforcement_policy are two hand-written copies with no machine comparison (P3); FORMAL_ENFORCEMENT admits m1 while stage_for_policy has no m1 lane, so that value can be written but never validated (P3); and the new formal-model ratchet is not in the existing mutation parametrization at tests/architecture/test_semantic_vocabulary_drift.py:43 (P3).
2 participants
Refs #4447 — semantic-convergence tracking issue. This PR covers the design/schema follow-up; M0.5–M4 remain tracked there.
Summary
Following merged PR #4433, this PR adds the bilingual formal model, Consumer role hierarchy, proof-stage metadata and convergence roadmap. The smoke validates metadata structure and consistency; producer/consumer data-flow analysis remains future work.
The registry now records the finite semantic signature, the proof boundary, and four enforcement lanes:
blocking_now: projection totality already enforced by M0;blocking_next: producer closedness, canonical-value liveness, and scope separation planned for M0.5;advisory: consumer-domain evidence reported without blocking ordinary consumer edits;unproved: persistence/version compatibility explicitly remains unproven.The RFC's English and Chinese mirrors now contain the mathematical model, the two-track roadmap, phase dependencies, and exit evidence. The drift smoke validates the formal model shape and requires every formal invariant to appear exactly once in an enforcement lane.
Included prior implementation
The M0 registry, inventory, PR-path smoke, tracked-source boundaries and premerge coverage preservation are already in main through #4433. This continuation includes the remaining RFC refinements and formal metadata, rather than re-delivering M0.
Validation
Tested revision:
554248b2834ee052ba00b488c1b1d5da0c636f1dRun state:
finishedAfter rebase, premerge selected 11 checks: all passed, 0 failures, 0 manual holds.
The 19-check premerge and 20-test results below are earlier pre-rebase validation; they are not a fresh full-suite claim for the current revision.
loopx canary premerge --from-git-diff --git-diff-base upstream/main --format jsonpython3.11 examples/semantic-vocabulary-drift-smoke.pypython3.11 scripts/generate_semantic_inventory.py --checkpython3.11 examples/docs-governance-smoke.pypython3.11 -m pytest -q tests/architecture/test_semantic_inventory.py tests/architecture/test_semantic_vocabulary_drift.pyFormal-model mutation check: removing an enforcement-lane invariant is rejected.
Scope and follow-up
This PR does not claim to implement whole-program producer/consumer data-flow analysis or persistence compatibility proof. Those remain staged M0.5/M1/M2 work in the RFC and are intentionally not immediate blockers for unrelated consumer edits.
中文说明
关联总追踪 Issue #4447。本 PR 在已合并的 #4433 上补充中英 RFC、Consumer 上位角色与子角色、形式模型及分级路线图；smoke 校验的是元数据结构与分组一致性。M0.5 的生产者/作用域分析、消费者角色报告和持久化兼容验证仍未完成，后续按 issue 中的独立任务推进，本 PR 不关闭总追踪 issue。
当前 head 在 rebase 后通过 11 项 premerge 检查；上方 19 项 premerge 和 20 项测试是此前版本的验证记录。