docs(.ccr V8): 2026-09-23 四条裁定 + 一条文字修正落地（§〇.6 为变更源） - #165
Merged
Merged
Conversation
维护者裁定四条 + 文字修正一条，逐条落进规格。本档为提案档，零实现。 **裁-1 `checker` = 外部工具钩子（定死）** - 语义 = `checker = <external checker identity>`；**不是可求值声明** - 加 `checkerRef` / `validatorRef` 防误读句 + 理由（一旦 Core 理解/执行 checker 内部逻辑， Constraint / Rule / 推理语义就会从侧门重新回来） - 落点：§五 5.2（原「本文按工具钩子读」的悬置段 → 定案）· 待裁 **新-10 收口** · §七.3 立 **v2-反例 ③**（含可观测判据：identity 指向不存在工具 ⇒ 加载仍须成功，否则说明 Core 已在求值它） **裁-2 CCR-4 选 (乙)：删 v1 旧承诺** - 删「有限文件表示无限结构」（随自由项代数 #2 + 规则闭包 #6 一并失去承载，故不再宣称） - 定案表述 = 「`.ccr` 本身有限，但 relation universe 是开放的」= **open-ended（外延开放）**， **不是** v1 的 **internally infinite（内部指称无限）** - 落点：§二 S-1d 整行重写 · S-2 连带 · §五 标题+5.1 · §六 6.3 补句 · 待裁 **新-9 收口** **裁-3 三个反例：退休两条 · 继承一条 · 另设 v2 反例** - 退休「无限递归关系」「非格关系」——**各带「为什么失去测试力」留痕**（不是静默删） - 继承「矛盾事实共存」，性质改述为 **`CCR stores relations, not truth closure`** - **另设 3 条 v2 反例**（本文导出）：拼写差异造两种 relation · RelationDomain 塞 solver/fixed point/proof rules · Core 不得求值 checker - ⚠ 写成「退休两条 + 保留一条 + 另设」，**不是**「v2 以后只剩一个反例」 - 落点：§七.2 重写为留痕节 · §七.3 另设 · 待裁 **新-11 收口** **裁-4 两项沿用（内容加厚）** - 版本标识形态 = `V8` / `V8.x` / `V8-<suffix>`；**身份必须显式进 magic/version**——不许靠「解析失败大概不是这个版本」自证 - 后端：**读 relations ≠ 执行 CCR inference**（`.coi` 拆出后更重要，更没有理由让 CCR reader 演变成推理机） - 落点：§九 C-1 / C-2 · 待裁 1 收窄（命名已定 / 编码未定）· §十四 **U-12 收口** **文修-1 全文禁「`.ccr` 表示无限结构」** - 唯一合法表述（原文逐字）：**`.ccr` stores a finite set of relations in an open, extensible relational universe.** - §〇.7 全文清点：**11 处** ⇒ 改写 4 · 保留 7（保留项全是**原文引用**或**数学 domain 的性质**； domain 的无界 ≠ `.ccr` 的指称无界，正是裁-2 要区分的那对） - §十五 自我约束新增第 5 条（长期效力） **裁-4 引入 `.coi` 的连带更新** - C-2 增补：`.coi` = optimization knowledge（`.ccr` = relation storage）；落地程度实核 = `develop@origin` 上**无任何 `.coi` 文件**，现存设计档 + 同日计划档 ⇒ `[已设计未实现]` - **C-10 标为「条件性消解」**——依据是 `.coi` 设计档 §〇.1 **自己给出的结论**（该档**直接引用了本档 C-10**， 并判定「`.coi` 把 opt_meta 整节搬出 `.ccr` 后，C-10 从『改名问题』降级为『不存在问题』」）； 处置建议随之改为「等 `opt_meta` 搬出」，**不再走「V8 侧改名」**（避免迁移期出现第三种叫法） - §十一.3 新增 `.coi` 联动行 · §十四 新增 **U-18**（该档未逐条对账） - 编号不重排：C-6…C-9 序号与内容一字未动（重排会让已引用编号指错对象） **基线换成当前 tip 重核**（本仓纪律：复核任何清单的第一步 = 把声明基线换成当前基线） - `develop@origin` 已从 `0eb1efd3` 前进到 **`90d8a5cd`**（PR #163，**130 文件 / +5750 −1948**） - 实测：本文锚定的 **14 个代码/CI/判据文件在两修订间逐字节相同**；2 处**已变动**的设计文档引用 （`materialization-space.md:784/:786/:846` · `execution-mapping-design.md` 执行域×14/`:640`/`:1613`） 按新 tip 逐行重读、**落点不变** ⇒ **全部锚点在今日 tip 上仍成立**（§八.0 第 5 条） - ⇒ 锚点强度由「对 `0eb1efd3` 有效」升为「对今日 `develop@origin` 有效」 三态计数：**A = 9 / 7 / 21**（已设计未实现 +3 全为 `.coi`；提案 +2 为 §七 的来源声明）· **B = 46** （§八 四表一行未动，机械重数 ✓）。表格结构：35 张表逐行 pipe 数校验通过 （忽略转义 `\|` 的 2 处假阳）。**无编译、无测试执行**（本批纯文档）。
dslsdzc
added a commit
that referenced
this pull request
Sep 23, 2026
* docs(.ccr V8): §十一.4 落纸——`.coi` 档 ↔ 本档对账（12 项：命中 3 · 接缝 4 · 对齐 5）+ U-18 已核
按 lead 指示把对账结果落进本档。判据 = **两档之间不得有第二份权威**（「`.ccr` 里到底有哪些面」只能一处说了算）。
- 新增 **§十一.4**：对账表 **12 项**，逐项给「`.coi` 档说法（带行号）| 本档说法（带节号）| 判定」
- ✅ **对齐 5**：relation metadata（该档明确让渡权威）· `RelationDomain` vs 执行域（两档独立同构）·
「格」（该档引本档为权威）· `.ccr`→`.coi` 依赖方向 · 串表
- 🟠 **接缝 4**：字符串/符号面粒度 · 面数口径（该档 6 行按段 vs 本档 4 面按语义）· 两套溯源机制 ·
`cache-semantics.md` 条款 1–7
- 🔴 **第一类命中 3**（**只登记不裁决**，已转维护者）
- 按 lead 要求写清**三件事**：
① **读数范围**（已读 §〇 / §一 / §四 #1#2#4 / §五 全节 / §9.1 / §15.3 + 各节标题；
未读 §六–§八 / §十–§十四 / §十六–§廿六）+「**本表不声称全档穷尽**」声明
—— 这句是**这张表能被信的前提**，必须留
② 命中的**判定依据**：**同一件事两处措辞、都自洽、读者会各引各的**（**不是「谁错」**）
③ **命中 3 单独标出**：**引文逐字准确 ✓ 但引的是本档已撤回的建议**——该档引本档 `42bc97cf` 版 C-10
的「核实结论 3」；本档已于 `dc19982b` 改为「等 `opt_meta` 搬出、**不再走 V8 侧改名**」
⇒ 失效形态 = **「引文准确 + 引用陈旧」**，**不得与「引错对象」混入同一档**
- 新增 **§11.4.2 两条反向约束（本档接收 → 落在 V8 落地批的约束面）**：
**C-11a** `.ccr` 不得含对 `.coi` 的引用（禁 sidecar 指针/期望哈希/「需配套」标记位；load 不得因 `.coi` 缺失而失败）·
**C-11b** `.coi` 私有串表与 `.ccr` intern 池**分离**（判据 = `.coi` 串表增删不改 `.ccr` 任何字节）
- **§十四 U-18 由「未核」改为「已核 + 3 条命中待裁」**
- ⚠ **未改** U-17 及任何与命中 1/2 相关的既有内容（等维护者裁，同批落，避免造出第三种说法）；
⚠ **未动** `.coi` 档（它已在 develop 上，改它要开新 PR）
顺带修复：上一编辑曾误删 `## 十二、三态计数与自查` 标题，已复原并复核 15 个 `##` 齐全。
三态计数不变（A = 9 / 7 / 21 · B = 46）；**38 张表逐行 pipe 校验 0 失配**。零源码改动。无编译、无测试。
* docs(.coi): C-10 引用同步——上引 V8 规格「核实结论 3」的建议已被该档撤回（本轮对账产出·第二半）
本笔**只加一条同步注，零实质内容改动**（`8 insertions(+), 0 deletions(-)`）。
- **落点**：§〇.1 引「V8 规格 §九 C-10」及其「我的核实结论 3」那处**旁边**（引文块与 📌 块之间），
即该引用**紧邻**位置——不在别处另起一节
- **内容**：该建议已由 V8 规格档 **`dc19982b`** 撤回——**不再走「V8 侧改名」**，
改为「**等 `.coi` 把 `opt_meta` 整节搬出 `.ccr`**」；
**撤回理由 = 改名与搬迁同时做，会在迁移期引入第三种叫法**
- **明写对本档结论无影响**：下方「本文展开——`.coi` 如何消解 C-10」的结论**不受影响**
（它本来就是根因级处置）；**仅「V8 侧那条建议」作废**，本档实质内容无需改动
- **为什么与 §11.4 同批落**：这是**同一轮对账的产出**，拆成两个 PR 会**让引用漂移继续活着**——
本档读者仍会看到一条**已被撤回的建议**
（该失效形态已由 V8 规格档 §十一.4 命中 3 登记为「**引文准确 + 引用陈旧**」，
与「引错对象」**不同档**）
⚠ **未动**本档任何实质内容——命中 1（`.ccr` 是否只装 target-independent）与命中 2（类型/接口面归属）
仍**等维护者裁**，现在动它们会**造出第三种说法**。
无编译、无测试（纯文档）。
* docs(.ccr V8): 裁-5 落地——命中 1/2 收口（target-independence 约束 + TYPE/IFACE 性质）
维护者 2026-09-23 对 §11.4 的**命中 1 / 命中 2** 作出裁定。本笔只落这两条命中的处置；**命中 1/2 以外内容未动**。
**裁定原文（逐字，四条）**
1. **CCR 禁止 target-specific relation。**
2. **target-specific optimization knowledge → COI。**
3. **target 本身的 capability/topology/semantics → Target Model。**
4. **TYPE/IFACE 属于 Core 的通用语义 relation domain；关系进 CCR，合法性由 checker 负责。**
**落点（逐条对应；凡本文展开处已标）**
- **§〇.6 新增裁-5**：裁定原文逐字 + 落点表 + 两条连带效果
- **§五 5.1**（命中 1）：加 **target-independence 约束**（裁定第 1 条）+ **三分流表**（第 2 / 3 条）；
判据形状新增第 4 条（机械钉子）——⚠ 明写该钉子的方向**取决于下方 (甲)/(乙) 裁决**
- **§三 3.3**（命中 2）：TYPE/IFACE 性质按裁定改写（原「不得读成 RelationDomain 雏形」**已由裁定取代**）；
并保留「**现行载体** vs **V8 归属**」两分，**两者不得互推**
- §11.4.1 两条命中各加「✅ 已裁」块 · §11.4 计数块末记三条命中的收口状态
- §十四 **U-17 结项** · **U-18 更新**（三条命中均已收口）· §12.2 新增自查行 24
**本文在落点内新登记的两条待确认项（均未自行裁决）**
① **裁-5 第 3 条的档名对齐**：裁定写「**Target Model**」；`.coi` 档 §5.3 把同类内容记作
「硬件能力描述 → HIT 表 / hw-map / `CapabilityDomain`」（`:581`）与「**canonical target model**」（`:582`）
⇒ **疑似同一物**，**标为疑似**，待维护者确认后再统一档名。
② 🔴 **`locatedAt(x, r12)` 与「禁止 target-specific」的关系**：v2 原文**自己的** relation 例含 `locatedAt(x, r12)`
（`r12` 是**目标寄存器**），而 `.coi` §5.2「分配决策（var → 物理寄存器）」行（`:568`）把同类信息判为
**优化知识、应迁 `.coi`** ⇒ **两处同向指向**「寄存器位置这类信息应出 `.ccr`」。
两种读法：**(甲)** 该约束只针对**优化类关系**，结构性的 `locatedAt` 不受限；**(乙)** 严格字面 ⇒ v2 原文该例须撤。
**本文按 (甲) 读并标为展开**；**(乙) 若成立，§三 3.2 的 v2 原文引例需维护者同批处置**——**本文不自行处置引例**。
**连带（本文展开）**
- 裁-5 第 1 条**同时坐实** `.coi` 档 §5.1 的前提（「`.ccr` 只装 target-independent」**现在是裁定、不再是默认**）
⇒ **该档无需改动**
- 命中 2 的处置方向 = **「V8 侧补明性质」**，**不是**「让 `.coi` 改」（该档 `:558`/`:559` 与裁定一致）
**自检**
- 本笔只动一个文件：**`1 file changed, 102+/8−`**（`.coi` 档**未动**）
- **★推前判据** `jj diff --from develop@origin --to @` = **2 files, 180+/9−**
（原 78+/1−；涨幅 **+102/+8 = 本笔**，**对上上面列出的 8 处落点**）
- 三态计数 **10 / 7 / 21**（已实现 +1 = §三 3.3 新写的现状断言，**已按本档规矩补 `file:line`**）
- 表格 **39 张**逐行 pipe 校验 **0 失配**
- 无编译、无测试（纯文档）
* docs(.ccr V8): 裁-5 落点内「Target Model」档名收口（本批 lead 裁定）
§11.4 计数块末登记的待确认项 ①（裁-5 第 3 条的档名对齐）由 **本批 lead 裁定**收口。
**裁定内容（非维护者原话，出处分级如下）**
- **档名：统一用「Target Model」**（lead 裁定，2026-09-23）
- **`.coi` 档 §5.3 那两行（`:581` 硬件能力描述 · `:582` canonical target model）不冲突、不改**——
它们在 `.coi` 档里是**非目标（non-goal）表述**：该档原文非目标清单列有「a canonical target model」
**本文落纸前的独立核验（不凭转述）**
- `.coi:664` = `- a canonical target model;`，**确在非目标清单内**（§七 原文 §4 段）；
- 该档 `:1009` 自注更直接写明「**原文 §4 明列 `.coi` 不是 canonical target model**」⇒ **lead 的读法有出处** ✓
⇒ 与裁-5 第 3 条是**同一件事的两面**：**`.ccr` 不装 · `.coi` 不是 · 另有 Target Model 承担**。
**改动（2 处）**
1. **§五 5.1**：原「⚠ 第 3 条的档名**待对齐**（本文登记，不裁决）」→ **「✅ 已裁」**，
含档名统一、`.coi` 那两行的非目标性质、以及「**`.coi` 档不得改动**（它那两行本来就对）」；
并明写**本文此后一律用「Target Model」**（不再写「疑似 = canonical target model」）。
2. **§11.4 计数块末**：待确认项 **2 条 → 1 条**（① 已裁；② `locatedAt(x,r12)` 的 (甲)/(乙) 仍**维护者裁定中**，
本文**暂按 (甲) 读并保留「本文展开」标注**，见 §五 5.1 的 🔴 登记）。§十四 U-18 尾部的指针同步为「余下 1 条」。
**未动**：`.coi` 档（本笔 **1 file changed**）· ② 的 (甲) 读法与标注 · 命中 3 · 任何命中 1/2 以外的内容。
**自检**
- 本笔：**1 file changed, 13+/9−**（全在 V8 档）
- **★推前判据** `jj diff --from develop@origin --to @` = **2 files, 184+/9−**（原 180+/9−；净 **+4**）
—— 净涨幅 **+4** = §五 那处注净增 3 行 + 计数块净增 1 行，**对得上**（本笔的 13+/9− 中多数是被改写的、原属上一笔的新增行）
- 三态计数 **10 / 7 / 21**（未变）· 表格 **39 张 0 失配**
- 无编译、无测试（纯文档）
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
内容
.ccrV8 规格档（docs/maintainer/design/ccr-v8-open-relational-lattice.md）落地维护者 2026-09-23 的四条裁定 + 一条文字修正。本档为提案档（零实现）——全文除[已实现]标注的现状锚点外无仓库对应物。本 PR 只含增量（1 file, 302+/62−）：
## 〇.6为变更源节，逐条给 原文 · 语义 · 落点 · 影响面。前序 v1（b704f068）与 v2 重写（42bc97cf）已由 #162 squash 合入（d81918b9），故本分支直接基于develop@origin，不含那两笔的谱系。四条裁定 + 一条文字修正的落点
checker= 外部工具钩子（定死，不是可求值声明）：checker = <external checker identity>，Core 只知道「这个 relation domain 的额外合法性检查交给谁」；加checkerRef/validatorRef防误读句 + 理由（一旦 Core 理解/执行 checker 内部逻辑，Constraint、Rule、推理语义从侧门回来）.ccr本身有限，但 relation universe 是开放的」= open-ended，不是 internally infiniteV8/V8.x/V8-<suffix>+ 身份必须显式进 magic/version（不许靠「解析失败大概不是这个版本」自证）；后端 读 relations ≠ 执行 CCR inference.ccr表示无限结构」退休两条反例的留痕方式（非静默删）
§七.2 是一张留痕表，每条的「为什么失去测试力」栏即留痕本体：
analyzer/result handle句柄）。CCR stores relations, not truth closure（v1 版测「冲突分类/四值」，v2 版测「不做真值闭包」⇒ 判据不得再写成四值形态）。checker（可观测判据：identity 换成指向不存在的工具 ⇒ 加载仍须成功，否则说明 Core 已在求值它）。全文「无限」清点 = 11 处（改 4 · 留 7）
规则先定死、后取数：凡把「无限 / 无界」归给
.ccr自身能力的句子 ⇒ 改写；v1/v2 原文引用与数学 domain 的性质两类保留。D = ℕ无最大元 / 「无界域必须能声明」）——后者正是裁-2 要区分的那对（domain 的无界 ≠.ccr的指称无界）.ccr自身能力留下唯一合法英文表述（此后本档沿用）：
⭐ 基线已换成当前 tip 重核
原稿声明基线 =
0eb1efd3，该修订已不是 tip（develop@origin现为90d8a5cd，PR #163，130 文件 / +5750 −1948）。按本仓纪律「复核任何清单的第一步 = 把它的声明基线换成当前基线」重核：file:line在今日 tip 上原样成立materialization-space.md（:784/:786/:846）·execution-mapping-design.md（执行域×14 /:640/:1613）——按新 tip 逐行重读，四处落点全不变⇒ 锚点强度由「对
0eb1efd3有效」升为「对今日develop@origin有效」（§八.0 第 5 条）。裁-4 引入
.coi的连带更新.coi= optimization knowledge（.ccr= relation storage）；落地程度实核 =develop@origin上无任何.coi文件，现存设计档 + 同日计划档 ⇒[已设计未实现].coi设计档 §〇.1 自己给出的结论（该档直接引用了本档 C-10，并判定「.coi把opt_meta整节搬出.ccr之后，C-10 从『改名问题』降级为『不存在问题』」）；处置建议随之改为「等opt_meta搬出」，不再走「V8 侧改名」（避免迁移期出现第三种叫法）.coi联动行 · §十四 新增 U-18（该档未逐条对账）三态计数
A = 9 / 7 / 21（已实现 / 已设计未实现 / 提案；已设计未实现 +3 全为
.coi，提案 +2 为 §七 来源声明）· B = 46（§八 四表一行未动，机械重数 ✓）自检
\|经复核为假阳）jj diff --from develop@origin --to @= 1 file, 302+/62−