Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
67 changes: 67 additions & 0 deletions docs/architecture/rfcs/semantic-vocabulary-convergence-v0.md
Original file line number Diff line number Diff line change
Expand Up @@ -1123,6 +1123,72 @@ introduce a competing target state.

## Appendix A: Execution ledger (non-normative)

### 2026-09-17 — Per-value meaning for the `cross_runtime` tier

Non-normative for the model; it adds no invariant and changes no existing
check's verdict. What changes is that every registered value now says what
produces it.

- Coverage moves from 68 of 149 values to 149 of 149. The 68 were the whole
kernel tier, documented by #4625 (the four canonical Turn vocabularies) and
#4626 (`effective_action` and `lease_action`). The 81 added here are the
whole `cross_runtime` tier, 20 vocabularies.
- The tracking issue described this remainder as "117 values". That count was
taken before #4626 merged: 117 is everything #4625 did not cover, which then
still included `effective_action` (32) and `lease_action` (4). Both are
kernel-tier and already documented, so the work actually outstanding was
81 values. The registry is the measurement, not the issue text.
- **What a note is required to say:** which condition produces the value — what
has to be true at runtime for the code to choose it. Not a restatement of the
identifier, and not only the disposition that follows. The three sets of notes
that existed at M0 recorded disposition, which is why a reader still had to
reconstruct control flow from the generated rule table; that is the failure
mode being closed. That is the bar review holds a note to; it is not a bar a
test can decide, and the ratchet below does not claim to.
- Where the producing condition cannot be established, the note says so and names
the evidence that would settle it, in the form `Unresolved: … Missing
evidence: …`. Two of the 81 are in that state as measured here, and neither is
guessed at: `settlement_failure_kind.cancelled` is declared in both owners and
admitted by the decoders but selected by no branch under `loopx/`, exercised
only by tests that fabricate it, and carries no `compatibility_only`
declaration saying it is reserved; `todo_decision_scope_kind.other` is an
accepted member with no producer, no fallback — a kind outside the set is
rejected, not coerced to it — and no documented rule for when an author should
choose it.
- A related boundary the notes now state rather than hide: several
`cross_runtime` values are **author-declared and only membership-validated**,
not selected by any branch. All four `goal_amendment_class` values, all of
`todo_decision_scope_kind` and `todo_decision_scope_granularity`, and
`delivery_outcome.primary_goal_outcome` are in this class. Their notes say who
declares the value and against what criterion, cite where that criterion is
normative, and say plainly that no code branch selects it. This is a real
property of the tier, and it is the reason `cross_runtime` declares no
producers and sits outside F1/F2.
- The ratchet is a new file, `tests/architecture/test_cross_runtime_value_notes.py`,
rather than an addition to the end of `test_semantic_vocabulary_drift.py`,
where the kernel-tier ratchet lives and where several open branches already
collide. It derives its population from the registry, so a new `cross_runtime`
vocabulary is covered without editing the test. It fails a value with no
`value_notes` entry, an entry that is blank or whitespace, and an unresolved
marker that does not name its missing evidence; a further test fails if a
vocabulary is ever registered under a tier neither ratchet walks.
- **Two gates the first revision of that file carried were removed under
review**, and the review is right. A character floor plus a count of
non-stopword words claimed to catch a note that only restates its own
identifier: a word count cannot show that a note names the producing
condition, and what it reliably changes is to reward padding. A budget pinning
the unresolved count at 2 claimed to stop "unresolved" becoming the cheap
default: a cap on honesty buys the smaller count by pressuring the next author
to invent a producing condition rather than record that the evidence is
missing, which is the outcome the evidence rules exist to prevent. Both
obligations remain real and both stay with review; the test now asserts only
what it can decide from the registry.
- Not addressed here: the notes are prose, and nothing checks them for truth.
Nothing verifies that a stated producing condition was ever right, or still
matches the code after the code moves. For the `cross_runtime` tier there is
no producer scan to check it against, which is the same gap F1/F2's domain
bounds already disclose.

### 2026-09-17 — Formula, role and enforcement claims separated; formal signature mutated

Normative for the enforcement-lane wording; the checks are unchanged except for
Expand Down Expand Up @@ -1373,6 +1439,7 @@ result on the current tree; what changes is what the invariants claim.
| 2026-09-16 | B1 rename invariance: add the name-keyed divergence advisory; state the limit it does not close | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B1; PR review pending | Keying the budget on value sets (rejected: `CONFIDENCE_LEVELS` and `EDGE_CASE_COMPLEXITIES` share `high/low/medium` with different meanings); a committed name ledger (rejected at M0: Q9 retired the committed census). The advisory lists surviving forks by name; it was first described as catching a one-sided rename, which measurement disproved, so both mirrors state the limit as it behaves | 9 |
| 2026-09-17 | B0: state schema validation, implementation stage, evidence status and blocking behaviour separately for I2/I11-I14 and the enforcement lanes; require each formal invariant id exactly once | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B0; PR review pending | Rename the `blocking_next` lane to match its behaviour (rejected: the lane name is the milestone that owns the check, and renaming it would lose that and collapse the two readings the other way); add a `blocks_today` boolean to `formal_model` (rejected: it would be one more declared field a reader could mistake for a measurement, and the fact is a property of the smoke's `main()`, which no registry edit can change); leave the lane gloss and note the gap in the ledger only (rejected: the gloss is the sentence a reviewer quotes) | 2, 5, 11, Appendix A, Appendix B |
| 2026-09-17 | Bound F1/F2 to the kernel tier and the scan reach, restate F4 as scope enumeration completeness, and give every obligation a derived `domain` | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447); **kernel-maintainer approval required, not yet given** | Leave the unconditional statements and record the gap in prose only (rejected: the statement was stronger than `validate_production`'s own docstring); restate F4 as per-context value-set disjointness (rejected: refuted by the repo's own data, since `scope_declarations` exists to permit legitimate same-name reuse); widen the scan so the unconditional claim becomes true (rejected: a separate change with its own risk) | 5, 9, Appendix B, Appendix C |
| 2026-09-17 | Document every `cross_runtime` value with the condition that produces it, taking per-value coverage from 68/149 to 149/149, and ratchet it in a separate test file | Implementation, Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) Track A; PR review pending | Append to the kernel ratchet at the end of `test_semantic_vocabulary_drift.py` (rejected: three open PRs already collide on that tail, and a same-diff rule is exactly what a merge there loses); infer a meaning for the two values with no producer (rejected by the evidence rules: a guessed note is indistinguishable from a verified one once it is in the table); document only the values a branch selects (rejected: it would leave the author-declared values looking undocumented rather than declared, which is the more useful fact); enforce the "not a restatement" bar with a character floor plus a non-stopword word count, and cap the unresolved count at 2 (both rejected under review: a word count cannot show that a note names the producing condition and only rewards padding, and a budget on honesty pressures the next author to invent a condition rather than record missing evidence) | Appendix A, Appendix B |

## Appendix C: Evidence registry

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -906,6 +906,53 @@ PR review 保留这些层级。普通改动记录检查范围和理由,无共

## 附录 A:执行账本(非规范)

### 2026-09-17 — `cross_runtime` 层的逐值含义

对形式模型非规范:不新增任何不变量,也不改变任何既有检查的结论。改变的是每个
已注册值现在都写明了什么条件产生它。

- 覆盖率从 149 个值中的 68 个升到 149/149。原有的 68 个就是整个 kernel 层,由
#4625(四个规范 Turn 词表)与 #4626(`effective_action` 与 `lease_action`)
补齐。本次新增的 81 个是整个 `cross_runtime` 层,共 20 个词表。
- 跟踪 issue 把这批剩余描述为“117 个值”。那是 #4626 合并之前的计数:117 是
#4625 未覆盖的全部,其中当时仍包含 `effective_action`(32 个)与
`lease_action`(4 个)。这两个都属 kernel 层且已补齐,所以真正待办的是 81 个。
以注册表为准,而不是以 issue 文本为准。
- **一条备注必须写什么:** 什么条件产生这个值——运行时要成立什么,代码才会选它。
不是把标识符换个说法,也不只是它随后的处置。M0 时仅有的三组备注记的都是处置,
这正是读者仍须从生成的规则表里反推控制流的原因;要闭合的就是这个失效模式。
这是评审据以衡量一条备注的标准;它不是测试能判定的标准,下面的棘轮也不声称能判定。
- 当产生条件无法确定时,备注就如实写明,并点名什么证据可以了结它,形式为
`Unresolved: … Missing evidence: …`。按本次实测,81 个中有 2 个处于此状态,且都
没有臆测:`settlement_failure_kind.cancelled` 在两个 owner 中都有声明、
解码器也接受,但 `loopx/` 下没有任何分支选它,只有伪造它的测试用到,且没有
`compatibility_only` 声明说明它是保留值;`todo_decision_scope_kind.other`
是一个被接受的成员,却没有生产者、也不是兜底——集合外的 kind 会被拒绝而不是
归并到它——并且没有任何文档说明作者何时该选它。
- 备注同时写明而非隐藏了一条相关边界:若干 `cross_runtime` 值是
**由作者声明、仅做成员校验** 的,没有任何分支选择它们。四个
`goal_amendment_class` 值、`todo_decision_scope_kind` 与
`todo_decision_scope_granularity` 的全部值,以及
`delivery_outcome.primary_goal_outcome` 都属此类。它们的备注写明由谁声明、
依据什么判据、该判据在哪里是规范性的,并直说没有代码分支选它。这是该层的真实
性质,也正是 `cross_runtime` 不声明 producers、处在 F1/F2 之外的原因。
- 本次的棘轮是一个新文件
`tests/architecture/test_cross_runtime_value_notes.py`,而不是追加到
`test_semantic_vocabulary_drift.py` 末尾——kernel 层棘轮在那里,且已有多个未合分支
在该处冲突。它从注册表推导自己的作用集合,因此新增一个 `cross_runtime` 词表无需
改测试即被覆盖。没有 `value_notes` 条目、条目为空白或仅空格、以及未点名缺失证据的
unresolved 标记,都会失败;另有一条测试会在某个词表被登记到两个棘轮都不走的层时
失败。
- **该文件初版带的两道闸门在评审中被移除**,评审是对的。字符下限加非停用词计数声称
能抓住“只是复述自身标识符”的备注:词数无法说明一条备注写出了产生条件,它可靠改变
的只是奖励灌水。把未解析数量钉在 2 的预算声称能阻止 “unresolved” 变成省事的默认
答案:给诚实设上限,换来的小数字来自逼迫下一位作者编造一个产生条件,而不是如实
记下证据缺失——而那正是证据规则要防的结果。两项义务都真实存在,也都留给评审;测试
现在只断言它能从注册表判定的东西。
- 本次未处理:备注是散文,没有任何机制检查其真伪。没有任何机制保证所述的产生条件曾经
成立,或在代码移动之后仍然成立。对 `cross_runtime` 层而言并不存在可供比对的
producer 扫描,这与 F1/F2 的值域边界已经披露的是同一个缺口。

### 2026-09-17 — 分离公式、角色与强制性声明;对形式签名做突变

强制层级的表述是规范性变更;除新增一条规则外,检查本身不变。#4447 Track B 的 B0 切片。
Expand Down Expand Up @@ -1109,6 +1156,7 @@ PR review 保留这些层级。普通改动记录检查范围和理由,无共
| 2026-09-16 | B1 改名不变性:新增按名字归组的分歧报告;写明它未闭合的边界 | 实现,Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B1;PR 评审待完成 | 把预算改按值集归组(否决:`CONFIDENCE_LEVELS` 与 `EDGE_CASE_COMPLEXITIES` 共享 `high/low/medium` 而含义不同);提交名字账本(M0 否决:Q9 已退役提交式清单)。该报告列出仍然存在的分叉;初稿称它能抓住单侧改名,实测证否,故两份镜像按真实行为写明边界 | 9 |
| 2026-09-17 | B0:为 I2/I11-I14 与各强制层级分别陈述 schema 校验、实施阶段、证据状态与阻断行为;要求每个形式不变量 ID 恰好出现一次 | 实现,Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) B0;PR 评审待完成 | 把 `blocking_next` 层级改名以匹配其行为(否决:层级名字表示拥有该检查的里程碑,改名会丢掉这层含义,并从另一个方向把两种读法重新合并);在 `formal_model` 中加一个 `blocks_today` 布尔字段(否决:那只会多出一个可被读者误当作度量的声明字段,而该事实是 smoke `main()` 的性质,任何注册表修改都改不了它);保留原注解、只在账本里记一笔缺口(否决:评审者引用的正是那句注解) | 2、5、11、附录 A、附录 B |
| 2026-09-17 | 将 F1/F2 限定在 kernel 层与扫描范围,把 F4 重述为作用域枚举完备性,并给每条义务加上可推导的 `domain` | 实现,Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447);**需要内核维护者批准,尚未获得** | 保留无条件表述、只在正文记一笔缺口(否决:该表述比 `validate_production` 自己的 docstring 还强);把 F4 重述为各上下文值集互斥(否决:会被仓库自身数据推翻,`scope_declarations` 恰恰就是为了允许合理的同名复用);扒宽扫描让无条件声明成立(否决:那是自带风险的另一个变更) | 5、9、附录 B、附录 C |
| 2026-09-17 | 为每个 `cross_runtime` 值写明产生它的条件,把逐值覆盖率从 68/149 提到 149/149,并用一个独立测试文件加以棘轮化 | 实现,Refs [#4447](https://github.com/huangruiteng/loopx/issues/4447) Track A;PR 评审待完成 | 追加到 `test_semantic_vocabulary_drift.py` 末尾的 kernel 棘轮(否决:已有三个未合 PR 在该处冲突,而同一 diff 内的规则正是合并时最容易丢失的东西);为两个没有生产者的值推断含义(按证据规则否决:一旦写进表里,臆测的备注与经核实的备注无法区分);只记录由分支选择的值(否决:那会让由作者声明的值看起来像是没写,而“由作者声明”本身才是更有用的事实);用字符下限加非停用词计数来强制“不得只是复述”这条标准,并把未解析数量上限钉在 2(评审中双双否决:词数无法说明一条备注写出了产生条件,只会奖励灌水;而给诚实设预算会逼迫下一位作者编造条件,而不是如实记下证据缺失) | 附录 A、附录 B |

## 附录 C:证据登记

Expand Down
Loading
Loading