diff --git a/docs/maintainer/design/ccr-v8-open-relational-lattice.md b/docs/maintainer/design/ccr-v8-open-relational-lattice.md index 4432986..071e1c9 100644 --- a/docs/maintainer/design/ccr-v8-open-relational-lattice.md +++ b/docs/maintainer/design/ccr-v8-open-relational-lattice.md @@ -204,6 +204,32 @@ jj file show -r docs/maintainer/design/ccr-v8-open-relational-lattic - **落点**：§九 **C-1**（版本：命名形态定死 + 显式身份硬约束）· **C-2**（后端 + `.coi` 分工）· §十 待裁 **1**（收窄：命名已定，编码落点未定）· §十一.3（`.coi` 联动登记）· §十四 **U-12**（已裁决：两条均沿用）。 +#### 裁-5　**命中 1 / 命中 2 的裁定**（**2026-09-23 追加；本版新增**） + +> 本节是 §十一.4 那三条命中的**收口裁定**——裁定原文四条，**逐字转写**。 +> ⚠ **命中 3 不在本裁定范围内**（它已由 §11.4 的第二半——`.coi` 档的 C-10 引用同步——单独处置）。 + +**裁定原文（逐字，四条）**： + +> 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 负责。** + +**落点（逐条对应）**： + +| 裁定条 | 处置 | 落点 | +|---|---|---| +| **第 1 条** | **命中 1 收口**：§五 5.1 的**开放域加 target-independence 约束** | §五 5.1 | +| **第 2 / 3 条** | **三分流**：优化知识 → `.coi`；**target 自身描述 → Target Model**（⚠ **既不进 `.ccr`、也不进 `.coi`**） | §五 5.1 的分流表 | +| **第 4 条** | **命中 2 收口**：**U-17 结项**——TYPE/IFACE **不是**「另一套独立机制」，而是 **Core 的通用语义 relation domain**；**关系进 `.ccr`、合法性由 checker 负责** | §三 3.3 · §十四 U-17 | + +**两条连带效果（本文展开）**： + +1. **`.coi` 档那条边界判据「坐实」**：该档 §5.1 的前提「`.ccr` 只装 target-independent」**自本裁定起是裁定、不再是默认**。 + ⇒ **该档无需改动**（其说法与裁定一致）。 +2. **命中 2 的处置方向确定为「V8 侧补明性质」，不是「让 `.coi` 改」**——该档 `:558`/`:559` 把类型面/接口面列「属于 `.ccr`」**与裁定一致**。 + #### 文修-1　⚠ 文字修正（**全文贯彻**）：不要再说 `.ccr`「表示无限结构」 **原文（逐字；作为本档此后唯一合法的该义表述）**： @@ -535,10 +561,23 @@ Relation Metadata | `argument_shape` | 实参允许面 | **形式未定**（是否引用 EntityRef 的 tag？是否闭集？）⇒ §十 待裁 新-6 | | `value_shape` | value 允许面 | 同上；且须容纳 v2 允许的 **opaque/symbolic value**（§三 3.2） | | `optional refinement/merge` | 本域**可选**提供的 `⪯` / `⊔`（§三 3.4） | **默认缺席**（CCR-5）。⚠ 原文此行把 refinement 与 merge **并写**，两者的关系见 §三 3.4 末 | +- ✅ **性质裁定（2026-09-23，裁-5 第 4 条，原文逐字）**： + + > **TYPE/IFACE 属于 Core 的通用语义 relation domain；关系进 CCR，合法性由 checker 负责。** + + ⇒ **本项原先写的「不得把 TYPE/IFACE 读成 RelationDomain 的雏形」已由裁定改写**： + 它们**不是**「另一套独立机制」，而是 **Core 的通用语义 relation domain** 的一个实例 + （这同时**收口 §十四 U-17**）。 - **[已实现] 现状对照（承重差异）**：现行 `.ccr` **无 relation domain 概念**。 - 现行最接近的「形状声明」是 `TYPE(7)` / `IFACE(8)` 两段（内容构造 = `src/compiler/ccr_types.cr`，D18 解耦）—— - 但那是**编译器的类型判定引擎**的内部表，**不是**开放的 relation domain。 - ⚠ **不得**把 `TYPE`/`IFACE` 读成 RelationDomain 的雏形：前者是**某一实现**的封闭表，后者是**开放**的域声明（§五 5.1）。 + 现行最接近的「形状声明」是 `TYPE(7)` / `IFACE(8)` 两段（内容构造 = `src/compiler/ccr_types.cr`，D18 解耦）。 + ⚠ **「现行载体」与「V8 归属」是两件事，两者都要保留、不得互推**： + 1. **现状**：现行那两段的内容是**编译器的类型判定引擎**的内部表 `[已实现]`——这是**载体事实** + （锚点：`ccr_io.cr:139-140` 段 tag 常量 · 读回 `:1534`→`g_types`/`g_type_terms`/`g_tt_index` · `:1592`→`g_iface_*`； + 内容构造 = `ccr_types.cr`（D18）——逐条见 **§八 A-4 与 B 读侧表**）； + 2. **V8 归属**：按裁-5 第 4 条，它们**属于 Core 的通用语义 relation domain**，**关系进 `.ccr`**， + 而**合法性判定交给 checker**——这是**语义归属**。 + ⇒ ⚠ **注意第 2 点的后半与裁-1 同构**：**「合法性由 checker 负责」= Core 不自行执行合法性检查** + （裁-1：`checker` 是**外部工具钩子**，Core 只存指称、不求值）——两条裁定在这一点上**互相印证**。 ### 3.4 Refinement（**V8 Core 第 4 组件——v2 称「唯一真正值得保留的『格』部分」，但随即自我收窄**） @@ -690,10 +729,46 @@ Relation Metadata 「文件格式不变」这一**检验方式仍然有效**，故本文把它作为 §七.1 主验收的断言（**但承载词按 v2 写**）。 ⚠ **措辞注（裁-2 / 文修-1）**：引文里的「**没有被现有范式封顶**」= **open-ended**（外延开放）， **不是** v1 的 internally infinite ⇒ 本条与 §〇.7 #8 的改写**同向**，**不构成保留「指称无限」的口子**。 +- 🔴 **约束（2026-09-23 维护者裁定，裁-5 第 1 条）——「开放」不等于「什么都装」**： + **`.ccr` 禁止 target-specific relation**（裁定原文逐字）。 + ⇒ §五 标题里的「**开放**」自本裁定起有**确切边界**：开放的是**关系域的名字与个数**， + **不是可装内容的 target 相关性**。⚠ 这一刀**同时坐实** `.coi` 档 §5.1 的前提（「`.ccr` 只装 target-independent」**现在是裁定、不再是默认**）——**该档无需改动**。 +- **三分流（裁-5 第 2 / 3 条，原文逐字）**： + + | 信息类 | 归属 | 依据 | + |---|---|---| + | **target-specific optimization knowledge** | **`.coi`** | 裁-5 第 2 条 | + | **target 本身的 capability / topology / semantics** | **Target Model**——⚠ **既不进 `.ccr`、也不进 `.coi`** | 裁-5 第 3 条 | + | 其余（**target-independent** 的 program relations） | **`.ccr`** | 裁-5 第 1 条的**反面** | + + > ✅ **第 3 条的档名：已裁（本批 lead 裁定，2026-09-23）——统一用「Target Model」**， + > 且 **`.coi` 档 §5.3 那两行（`:581` 硬件能力描述 · `:582` canonical target model）不需要改**： + > 它们在 `.coi` 档里是**非目标（non-goal）表述**——该档原文的非目标清单里就列有 + > 「a canonical target model」（其 `:664`；该档 `:1009` 自注更直接写明「**原文 §4 明列 `.coi` 不是 canonical target model**」）。 + > ⇒ **与裁定是同一件事的两面**：**`.ccr` 不装 · `.coi` 不是 · 另有 Target Model 承担**。 + > ⇒ **本文此后一律用「Target Model」**（不再写「疑似 = canonical target model」）； + > **`.coi` 档不得改动**（它那两行本来就对）。 + + > 🔴 **一处与 v2 原文例子的接口张力（本文登记，不裁决——须维护者确认）**： + > 裁定第 1 条禁的是 **relation** 的 target 相关性，但—— + > - **v2 原文自己的 relation 例含 `locatedAt(x, r12)`**（§三 3.2 逐字引；`r12` 是**目标寄存器**）； + > - **`.coi` 档 §5.2「分配决策（var → 物理寄存器）」行（`:568`）** 明确把「`var_idx` → 物理寄存器」判为 + > **优化知识**、**应迁 `.coi`**（该档 K-2 亦从 `:73` 起论证「它就在 `.ccr` 里」这一现状问题）。 + > + > ⇒ **两处同向指向**：**「寄存器位置」这类信息，按裁定与 `.coi` 的边界分析都应出 `.ccr`**， + > 而它**恰是 v2 原文给出的 relation 例子**。两种读法： + > **(甲)** 该约束**只针对「以目标知识为内容的优化类关系」**，`locatedAt` 这类**结构性**关系不受限； + > **(乙)** 严格按字面 ⇒ `locatedAt(x, r12)` 亦属 target-specific ⇒ **v2 原文该例须撤**。 + > + > **本文按 (甲) 读，并标为展开**（理由：裁-5 第 2/3 条分流的是**优化知识**与**目标自身描述**，不是结构性关系）； + > **若 (乙) 成立，§三 3.2 的该例需维护者同批处置**——**本文不自行处置 v2 原文的引例**。 - **[提案] 判据形状（本文展开）**： 1. 域 `id` = **开放字符串**（无白名单、无枚举）； 2. 新增域后文件版本 / 分节集合**零变化**； - 3. **负向钉子**：源码出现域名的枚举或内建域表 ⇒ 判据红。 + 3. **负向钉子**：源码出现域名的枚举或内建域表 ⇒ 判据红； + 4. 🔴 **新增（裁-5 第 1 条的机械钉子）**：给一个装 **target-specific relation** 的 `.ccr`（如 `locatedAt(x, r12)` 按 (乙) 读） + ⇒ **必须可判定为「违反 target-independence」**（拒载或显式诊断）； + **静默接受 ⇒ 判据红**。⚠ 该钉子的**判据方向取决于上面 (甲)/(乙) 的裁决**，**(甲) 下它不适用**。 ### 5.2 Theory 的降级：模块/包（**#8**） @@ -1365,6 +1440,96 @@ Relation Metadata | `docs/academic/cache-semantics.md`（条款 1–7） | `existence-structure.md` 的条款权威；v1 §十六 16.1 曾把 Cache 降为普通 theory，**该节本版已删**（§二 S-8） | ⚠ **本版变更**：v1 说「条款 1–7 的适用范围收窄为 `theory cache`（**不废除**）」；**v2 没有 `theory cache` 这个 Core 对象了** ⇒ 该收窄表述**失去对象**。**建议改为**：条款 1–7 的适用范围 = 「某个 cache 相关的 relation domain + 其 checker」（⚠ 该 checker 现在有确定语义了——**外部工具**，裁-1）。**登记，不改**；⚠ 这条**属本文展开**，须维护者确认 | | `src/compiler/ccr_io.cr` 头注释 | C-6 的 9 处陈标（含 2 处直指版本闸）+ C-10 的 metadata 撞车 | V8 落地批的**必做前置**（否则读侧真源被陈标遮蔽）；**两条应同批处置**。⚠ **C-10 侧更新**：处置方向**改为「等 `.coi` 搬走 `opt_meta`」，不再走「V8 侧改名」**（见 C-10 第 5 点） | +### 11.4 `.coi` 档 ↔ 本档 **对账**（**2026-09-23 新增**；判据 = **两档之间不得有第二份权威**） + +> **判据（本节的唯一判据）**：**「`.ccr` 里到底有哪些面」只能一处说了算**。 +> 本节逐项对照 `docs/maintainer/design/coi-optimization-knowledge-sidecar.md` 与本档。 +> +> ⚠ **「命中」的定义（必须先读，否则会读成「找茬」）**： +> **同一件事、两处各有一个说法、且两处各自自洽 ⇒ 命中。** +> **命中 ≠ 「谁错」**——它说的是「**读者会各引各的**」：引 `.coi` 得一个结论，引本档得另一个，两引都不算误引。 +> **本节只登记，不裁决**（三条命中已转维护者，见 11.4.1 的待裁问题）。 + +**读数范围（**这张表能被信的前提，必读**）**： + +| | 内容 | +|---|---| +| **已读（逐字）** | 该档 **§〇（术语护栏全节）** · **§一（目的与中心律）** · **§四 #1 / #2 / #4** · **§五（5.1 / 5.2 / 5.3 全节）** · **§9.1** · **§15.3**；另读**各节标题** | +| **未读** | 该档 **§六–§八 · §十–§十四 · §十六–§廿六** | +| ⚠ **声明** | ⇒ **本表不声称全档穷尽。** 未读节内**可能存在本表未覆盖的权威重叠**；引用本表时**不得**据「12 项已对齐/命中」推断「两档已全面对齐」 | + +**对账表（12 项）**： + +| # | 问题 | `.coi` 档的说法（行） | 本档的说法 | 判定 | +|---|---|---|---|---| +| **1** | **`.ccr` 是否只装 target-independent** | `:144`「stores **target-independent** program relations」· `:145`「must remain applicable to any hardware」（**该档原文逐字**） | §一.1「表达 HDFG **及其分析/映射产生**的关系」（**v2 原文逐字**）；§三 3.1 实体例含 `@deploy.gpu0`、tag `target.register`；§五 5.1 域 `id` 全开放 | 🔴 **第一类命中** | +| **2** | **类型面 / 接口面 归谁** | `:553` 表头标「**语义面**」；`:558` 类型面 · `:559` 接口面 **均列「属于 `.ccr`」** | §三 3.3：TYPE/IFACE 是**某一实现的封闭表**，**不得**读成 RelationDomain 雏形；§十四 **U-17：未定** | 🔴 **第一类命中** | +| **3** | **C-10 的处置方向** | `:95` 引本档 C-10 原文；`:96` 引其「核实结论 3」为**建议**；`:102` 给出「`.coi` 搬迁 = 根因级处置」 | **本档已于 `dc19982b` 更新**：处置建议改为「**等 `opt_meta` 搬出**」，并**明确不再走「V8 侧改名」** | 🔴 **第一类命中（引用陈旧，非引错 —— 见 11.4.1 末）** | +| 4 | 字符串 / 符号面 归谁 | `:561` 列「属于 `.ccr`」（`STR`/`SYM` 段） | §三 3.1：**不得**把 `SYM` 段读成本档的 EntityRef；四面清单里**无**「字符串/符号面」 | 🟠 接缝（**粒度不同**） | +| 5 | `.ccr` 有**几个面** | §5.1 = **6 行（按段列）** | §六.1 = **4 面（按语义列）** | 🟠 口径差（与 #4 同根：按段 vs 按语义面） | +| 6 | 溯源机制 | §9.1 记录含 `source_ref` / `source_fingerprint` / `validity`；§9.2 双闸 | §三 3.5 relation metadata 含 `producer` / `epoch` / `evidence_ref` | 🟠 接缝（两套溯源分居两档；**未发现直接冲突**，#11 的单向依赖未被违反） | +| 7 | `cache-semantics.md` 条款 1–7 | §〇.3：「本文**不引用也不修改**它们」 | §十一.3：**提议**收窄为「cache 相关 relation domain + 其 checker」（已标「须维护者确认」） | 🟠 接缝（一档提议改、一档明确不动） | +| 8 | relation metadata（V8） | `:562` 依据 = **「V8 规格 §三 3.5」** | §三 3.5 | ✅ **对齐**（该档**明确让渡**权威） | +| 9 | `RelationDomain` vs 执行域 | `:110`「**`RelationDomain` = V8 的关系域**」；`ExecutionDomain` 归执行映射档 | §〇.4 术语护栏**同款区分** | ✅ **对齐**（两档**独立同构**，互为佐证） | +| 10 | 「格」 | `:125`「`.coi` 不含格承诺（**V8 §三 3.4 已把「格」移出 Core 要求**）」 | §三 3.4 | ✅ **对齐**（该档**引本档为权威**） | +| 11 | `.ccr` → `.coi` 的依赖方向 | §四 #1：`.ccr` **不得**含对 `.coi` 的引用；#2 依赖**单向** | 本档**未覆盖**（四面清单无 `.coi` 引用） | ✅ 对齐（**本档缺项 ⇒ 见 11.4.2 接收**） | +| 12 | 串表 | §15.3：`.coi` **私有**串表，**绝不与 `.ccr` 的 intern 池共享**；判据 = 「`.coi` 串表增删**不改变** `.ccr` 的任何字节」 | §三 3.1 提案的 `name_ni` = STR 段串索引（**在 `.ccr` 池内**） | ✅ 对齐（**且对本档构成约束 ⇒ 见 11.4.2**） | + +**计数**：🔴 **第一类命中 3** · 🟠 **接缝 / 口径差 4** · ✅ **对齐 5** = **12**。 + +> **本版三条命中的收口状态（2026-09-23）**：**命中 1 / 命中 2 → 已由裁-5 裁定**（落点见 §〇.6 与 11.4.1 各自的「已裁」块）； +> **命中 3 → 已由本 PR 的第二半（`.coi` 档 C-10 引用同步）处置**。 +> **仍待确认的只剩 1 条**，且**不是**原三条命中，而是**落点内新发现的接口问题**： +> ① ✅ **已裁（本批 lead 裁定，2026-09-23）**：档名统一用「**Target Model**」；`.coi` §5.3 那两行是**非目标表述**、 +> **与本裁定不冲突、该档不改**——详见 §五 5.1 的该条「已裁」块。 +> ② 🔴 **`locatedAt(x, r12)` 与「禁止 target-specific」的关系**（(甲)/(乙) 两读）—— +> **已转维护者，裁定中**；本文**暂按 (甲) 读并标「本文展开」**，见 §五 5.1 的 🔴 登记。 + +#### 11.4.1 三条第一类命中（**待裁——本节不裁决**） + +**命中 1（最实质，且有工程后果）**：两处**都是维护者原文**，各自自洽，但**读者会各引各的**—— +引 `.coi` 得「`.ccr` 只装 **target-independent**」，引本档得「表达 HDFG **及其分析/映射产生**的关系」（且实体例直接是 `@deploy.gpu0` / `target.register`）。 +**为什么不能只当措辞**：该档把「目标特定优化知识」划归自己（其原文 §3.2），其**部分理由**正是「`.ccr` 只装 target-independent」⇒ 若本档的 `.ccr` 也可装 target-specific relation，**这条边界判据松动**，两档的归属结论可能相反。 +**待裁问题**：`.ccr` **允许**装 target-specific relation 吗？ +（若允许 ⇒ 该档 §5.1/§5.2 的边界需同批重述；若不允许 ⇒ 本档 §五 5.1 的开放域需加 target-independence 约束。） + +> ✅ **已裁（2026-09-23，裁-5 第 1 / 2 / 3 条）**：**走「不允许」那一路**—— +> **CCR 禁止 target-specific relation**；target-specific **优化知识** → `.coi`； +> target **自身的** capability/topology/semantics → **Target Model**（**既不进 `.ccr`、也不进 `.coi`**）。 +> ⇒ **落点 = §五 5.1（加约束 + 三分流表）**，见 §〇.6 裁-5。 +> ⚠ **连带登记的接口张力**：v2 原文的 relation 例含 `locatedAt(x, r12)` ⇒ **该例与「禁止 target-specific」的关系待确认**（§五 5.1 已登记 (甲)/(乙) 两读，**本文按 (甲)**）。 + +**命中 2**：该档 `:558`/`:559` 以「**语义面**」为表头，把**类型面 / 接口面**列「属于 `.ccr`」——**而本档说这事未定**（§十四 U-17）。读者据 `.coi` 可断言「V8 的 `.ccr` 含类型/接口面」，据本档只能说「未定」。 +**待裁问题**：TYPE/IFACE 在 V8 下是**某个 relation domain**、还是**另一套独立机制**？（= U-17 由这处触发） + +> ✅ **已裁（2026-09-23，裁-5 第 4 条，原文逐字）**： + + > **TYPE/IFACE 属于 Core 的通用语义 relation domain；关系进 CCR，合法性由 checker 负责。** + +> ⇒ **处置方向 =「V8 侧补明性质」，不是「让 `.coi` 改」**——该档 `:558`/`:559` 把类型面/接口面列「属于 `.ccr`」 +> **与裁定一致**，**该档无需改动**。 +> ⇒ **落点 = §三 3.3（补性质）+ §十四 U-17（结项）**，见 §〇.6 裁-5。 + +**命中 3 —— ⚠ 性质与上两条不同，须单独看**：**它不是「引文不准」**——该档 §〇.1 `:95` 对本档 C-10 的**引文逐字准确** ✓（连「从『改名问题』降级为『不存在问题』」都对得上）。 +问题是：**它引的是本档已撤回的建议**。 +- 该档 `:96` 引的是本档 C-10「核实结论 3」的**建议**（加限定名 / 承载面决策时改名）——那是本档 **`42bc97cf` 版**的文字； +- 本档已于 **`dc19982b`** 把该点改为「**等 `opt_meta` 搬出；不要再走 V8 侧改名**」（理由：两者同时做会在迁移期引入**第三种叫法**）。 +⇒ **失效形态 = 「引文准确 + 引用陈旧」**，与「引错对象」是**两个不同的失效形态**，**不得混入同一档**（本仓已有「引文行号漂移」与「引文内容错」两类先例，本条属第三类：**被引方自己改了，引用方无从得知**）。 +**待裁问题**：是否由本档出一句**可粘贴的现行结论**交该档作者同步（本档**不动**其文件）。 +> ✅ **同时报一处干净的结果（对账不是只找分歧）**：本档 C-10 的「条件性消解」**是引用而非自创**，且该引用**已逐字核对**——它**不是凭转述站住的**。 + +#### 11.4.2 两条**反向约束**（**本档接收**；落在 V8 落地批的**约束面**上） + +这两条来自 `.coi` 档，但其**受益方/被约束方是 `.ccr`** ⇒ 本档**接收为 V8 落地批的约束**： + +| # | 约束（来源） | 对 V8 落地批的含义 | +|---|---|---| +| **C-11a** | `.ccr` **不得**含对 `.coi` 的引用——禁止 sidecar 指针 / 期望哈希 / 「需配套 `.coi`」标记位；且 `.ccr` 的 `load` **不得**因 `.coi` 缺失或损坏而失败（`.coi` 档 §四 #1） | V8 的四面清单**不得新增**「`.coi` 引用面」；V8 的版本/身份判别式（§九 C-1）**不得**把 `.coi` 的存在性纳入输入 | +| **C-11b** | `.coi` 的串表**绝不与** `.ccr` 的 intern 池共享；判据 = 「`.coi` 串表增删**不改变** `.ccr` 的任何字节」（`.coi` 档 §15.3） | 本档 §三 3.1 的 `name_ni`（STR 段索引）提案**不受影响**（它本就在 `.ccr` 池内）；但 V8 落地批**不得**为省事把两档的串池合并——那会**同时**违反本条与 §九 C-1 的逐字节判据面 | + +> ⚠ **本节与 §十四 U-18 的关系**：U-18 原为「该档未逐条对账」的未核实项，**本节的产出即其核实结果** +> ⇒ U-18 已改为「**已核 + 3 条命中待裁**」。**本节不含对那 3 条的裁决。** + --- ## 十二、三态计数与自查 @@ -1380,7 +1545,7 @@ Relation Metadata | 档 | A（内联标记出现次数） | B（清单行数，**权威口径**） | 说明 | |---|---|---|---| -| 〔已实现〕 | **9** | **46** | B = §八 A/B/C 三表的**数据行**（每条带 `file:line`），**与 v1 同值**（同表同行、基线同一）；**本会话机械重数 ✓**（§12.3） | +| 〔已实现〕 | **10** | **46** | B = §八 A/B/C 三表的**数据行**（每条带 `file:line`），**与 v1 同值**（同表同行、基线同一）；**本会话机械重数 ✓**（§12.3）。⚠ **本修订 +1**（裁-5 落地时在 §三 3.3 新增一处现状断言，**已按规矩补 `file:line`**） | | 〔已设计未实现〕 | **7** | 无成表清单（散落 7 处，见下） | B 档不适用——本档主张不集中在单一清单。⚠ **本修订 +3**（全是 `.coi`：裁-4 引入的新设计档） | | 〔提案〕 | **21** | 其余全部（**默认档**） | A 只数**显式写出**的标记；**未含**默认推断档。⚠ **本修订 +2**（§七 的 7.1/7.3 来源声明） | @@ -1404,7 +1569,7 @@ Relation Metadata **实测读数（本会话 2026-09-23，`f` = 本文件）**： ``` -grep -o '\[已实现\]' $f | wc -l # → 9 +grep -o '\[已实现\]' $f | wc -l # → 10 grep -o '\[已设计未实现\]' $f | wc -l # → 7 grep -o '\[提案\]' $f | wc -l # → 21 ``` @@ -1437,6 +1602,8 @@ grep -o '\[提案\]' $f | wc -l # → 21 | 20 | **裁-4**：版本标识形态定死 + 显式身份；后端「读 relations ≠ 执行 inference」 | §〇.6 裁-4 · §九 C-1 · §九 C-2（+ `.coi`）· §十 待裁 1（收窄）· §十一.3 · §十四 U-12（已裁） | ✅ | | 21 | **文修-1**：全文禁「`.ccr` 表示无限结构」；给出唯一合法英文表述 | §〇.6 文修-1 · **§〇.7（11 处清点：改写 4 / 保留 7）** · §十五 自我约束 5 | ✅ 清点表逐处给判定与理由 | | 22 | **基线换成当前 tip 重核**（复核任何清单的第一步） | §八.0 第 5 条 · §八 标题 · 头部基线块 | ✅ `90d8a5cd`；14 个代码文件逐字节相同 · 2 处文档引用重读落点不变 | +| 23 | **`.coi` 档 ↔ 本档对账**（判据 = 两档之间不得有第二份权威） | **§十一.4**（+ 11.4.1 命中 · 11.4.2 反向约束）· §十四 **U-18 已核** | ✅ **12 项：命中 3 · 接缝 4 · 对齐 5**；含**读数范围 + 「不声称全档穷尽」声明**；命中**只登记不裁决**；命中 3 单列（**引文准确 + 引用陈旧**，不与「引错」同档） | +| 24 | **裁-5 落地：命中 1 / 命中 2 收口** | **§〇.6 裁-5**（裁定原文四条 + 落点表）· **§五 5.1**（target-independence 约束 + 三分流表）· **§三 3.3**（TYPE/IFACE 性质）· §11.4.1 两条「已裁」块 · §十四 **U-17 结项** / U-18 更新 | ✅ 裁定原文**逐字**转写；**命中 1/2 以外内容未动**；⚠ 落点内**新登记两条待确认项**（Target Model 档名对齐 · `locatedAt(x,r12)` 的 (甲)/(乙) 读法）——**均未自行裁决** | ### 12.3 实测读数回填 @@ -1446,7 +1613,7 @@ grep -o '\[提案\]' $f | wc -l # → 21 | 档 | A（实测） | 构成 | |---|---|---| -| 〔已实现〕 | **9** | **4 处方法论自述**（前言「全文除显式标注…」句 · §〇.3 三态表的表头行 · §〇.3 后「本设计的特殊性」说明 · §八 节首「本节全部…」说明）+ **5 处真主张**（§〇.4 术语护栏的 `metadata` 行 · §三 3.1 现状对照 · §三 3.3 现状对照 · §十一.1 表 `2026-09-09-lattice-ir-v7-format.md` 行 · §十一.1 表 `adr-0002` 行）——**本修订未增减** | +| 〔已实现〕 | **10** | **4 处方法论自述**（前言「全文除显式标注…」句 · §〇.3 三态表的表头行 · §〇.3 后「本设计的特殊性」说明 · §八 节首「本节全部…」说明）+ **6 处真主张**（§〇.4 术语护栏的 `metadata` 行 · §三 3.1 现状对照 · **§三 3.3 现状对照 ×2**〔本修订 +1：裁-5 落地时把「TYPE/IFACE 的内容是类型判定引擎内部表」写成了显式现状断言，**已补 `file:line`**〕 · §十一.1 表 `2026-09-09-lattice-ir-v7-format.md` 行 · §十一.1 表 `adr-0002` 行） | | 〔已设计未实现〕 | **7** | 1 处方法论自述（§〇.3 表头行）+ **6 处真主张**（§〇.4 术语护栏的 `格/Lattice` 行 · §关联列表的 `.coi` 行〔**新**〕 · §九 C-2 的 `.coi` 落地程度〔**新**〕 · §九 C-4 · §十一.1 表 `existence-structure.md` 行 · §十一.3 表的 `.coi` 行〔**新**〕） | | 〔提案〕 | **21** | 3 处口径自述（§〇.3 表头行 · 「默认必须是…」句 · 「本设计的特殊性」说明）+ 18 处正文/来源声明/自查/自我约束标记 | @@ -1574,8 +1741,8 @@ grep -o '\[提案\]' $f | wc -l # → 21 | **U-14** | **`@deploy.gpu0` 的 `deploy` 是否属 Core 承认的东西** | v2 例中出现该前缀，但 v2 同时说 tag「**只是工具提示**，而不是 Core ontology」⇒ 「Core 的例子用了它」与「它不是 Core 的」之间的**关系未定** | 语法/编码设计 | | **U-15** | **`existence-structure.md` / `materialization-space.md` 与 v2 有无新冲突** | v2 删了 Core 级格承诺与 theory，**可能**使既有文档里的一些句子失去对象（本文只改了 §十一.3 的 cache 一行，**其余未逐句对账**） | 裁决人；文档批 | | **U-16** | **爆炸半径档（另一位写手）与 v2 的相容性** | 该档**不在 `develop@origin`**，且本文**只读了它的标题、节标题与若干行**（共 272 行），未逐条对账；其侦查语境是 v1 的「取代段表」框架 | 两档作者；V8 落地批 | -| **U-18** | **`.coi` 设计档与本文的相容性**（**本修订新增**） | 本文**只读了该档的节标题、§〇.1 与 K-1/K-3 若干行**（全文 1500+ 行）⇒ **未逐条对账**。已核实的只有两点：① 其 §〇.1 **直接引用了本档 C-10** 并给出「条件性消解」结论（本文据此更新 C-10，**属引用而非自创**）；② 其 **K-3 自述「`.coi` 在本仓零对应物」**与本文实测「`develop@origin` 上无任何 `.coi` 文件」**一致** ✓。⚠ **未核**：其 §五「与 `.ccr` 的边界对照表」是否与本文 §六 的四面清单**有第二份权威** | 两档作者；裁决人 | -| **U-17** | **v2 的「四件事」是否与 v1 的 `type_engine` / `type_terms` 现状构成第三个「域」问题** | ⚠ 本文**未展开**：现行 `TYPE(7)`/`IFACE(8)`（`ccr_types.cr` 构造）在 v2 下应归为**某个 relation domain**、还是**另一套独立机制**，v2 未提，本文亦未核（§三 3.3 只登记了「不得读成雏形」） | 裁决人；承载面设计 | +| ~~**U-18**~~ | ~~`.coi` 设计档与本文的相容性~~ | ✅ **已核（2026-09-23）**——已做**逐项对账**，**见 §十一.4**（该节含**读数范围**与「**不声称全档穷尽**」声明，是这张表能被信的前提）。结果 = **12 项：🔴 第一类命中 3 · 🟠 接缝 4 · ✅ 对齐 5**。**三条命中均已收口**：**命中 1 / 2 由裁-5 裁定**（落点 = §五 5.1 · §三 3.3）· **命中 3 由本批第二半的 `.coi` C-10 引用同步处置**。另：§十一.4.2 已**接收**两条反向约束（C-11a / C-11b）。⚠ **余下 1 条待确认项见 §11.4 计数块末**（`locatedAt(x,r12)` 的 (甲)/(乙) 读法，**维护者裁定中**；Target Model 档名一条**已由 lead 裁定**） | 维护者（该条）；两档作者 | +| ~~**U-17**~~ | ~~v2 的「四件事」是否与 v1 的 `type_engine` / `type_terms` 现状构成第三个「域」问题~~ | ✅ **已裁决（2026-09-23，裁-5 第 4 条）并结项**：原文逐字 = 「**TYPE/IFACE 属于 Core 的通用语义 relation domain；关系进 CCR，合法性由 checker 负责**」⇒ **不是「另一套独立机制」**。落点 = **§三 3.3**（补性质，含「现行载体 vs V8 归属」两分）+ 本行结项。⚠ **连带**：「**合法性由 checker 负责**」与 **裁-1**（`checker` = 外部工具钩子、Core 不求值）**同构、互相印证** | （已收口） | --- diff --git a/docs/maintainer/design/coi-optimization-knowledge-sidecar.md b/docs/maintainer/design/coi-optimization-knowledge-sidecar.md index 4822740..7d34d68 100644 --- a/docs/maintainer/design/coi-optimization-knowledge-sidecar.md +++ b/docs/maintainer/design/coi-optimization-knowledge-sidecar.md @@ -96,6 +96,14 @@ 其「我的核实结论 3」给的是**建议**：「V8 侧的对外名称至少加限定（如 `relation metadata` / `relations.metadata`）， 或在承载面决策时一并改名」。 +> ⚠ **同步（2026-09-23）——上引那条建议已被 V8 规格档撤回**： +> 该档自 **`dc19982b`** 起已把 C-10 的处置**改向**——**不再走「V8 侧改名」**， +> 改为「**等 `.coi` 把 `opt_meta` 整节搬出 `.ccr`**」。 +> **撤回理由**：**改名与搬迁同时做，会在迁移期引入第三种叫法**。 +> ⇒ **仅「V8 侧那条建议」作废**；**下文「本文展开——`.coi` 如何消解 C-10」的结论不受影响** +> （它本来就是根因级处置），**本档实质内容无需改动**。 +> 出处：`docs/maintainer/design/ccr-v8-open-relational-lattice.md` §九 C-10 第 5 点（该档自 `dc19982b` 起）。 + > 📌 **本文展开——`.coi` 如何消解 C-10**： > C-10 的根因不是「两个东西都叫 metadata」，而是**优化参数袋**这个异物**寄居在 `.ccr` 里**—— > 只要它还在 `.ccr` 内，无论怎么改名，`.ccr` 里就永远有两个「元数据」概念需要靠限定词区分。