Skip to content

docs(.ccr V8): 第二版规格——砍成四件事(Entity + Relation + Open Relation Domain + Optional Refinement Algebra) - #162

Merged
dslsdzc merged 2 commits into
developfrom
feature/ccr-v8-spec
Sep 22, 2026
Merged

dslsdzc merged 2 commits into
developfrom
feature/ccr-v8-spec

Conversation

@dslsdzc

@dslsdzc dslsdzc commented Sep 22, 2026

Copy link
Copy Markdown
Owner

这是什么

.ccr 的第二版设计:从"开放关系理论(含 Rule/Constraint/Theory/μν/四值/Query/Bridge)"砍成四件事。

Entity + Relation + Open Relation Domain + Optional Refinement Algebra
CCR = (E, D, R)

其余全部移出 V8 Core:Rule / Fixed Point / Constraint / Proof / Assumption / Query / Mapping / Cache / Time / Execution / Security。

三条最要紧的:

  • Rule 删除——"CCR stores relations, not inference programs"(谁来求值会把整个 V8 拖进一个 relation engine);
  • 全局 complete lattice 删除(维护者原话:"这是目前最危险的过度承诺")——refinement 只要求 preorder/partial order,⊤/⊥ Core 都不要求;
  • 通用 Term 代数删除核心地位——否则会引入 unification / rewriting / normalization。

留痕

不是覆盖,是换版:正文 = 第二版,第一版按父修订 b704f068 读回(实测仍 1234 行、标题 Open Relational Lattice、含八公理节)。§二 是**"删除了什么、为什么":19 条对照(v1 里是什么 / v2 结论 / 理由 / 去处)+ 12 条蕴含删除** + 8 条未改变的 v1 结论(防误读为"全砍")。

一条关键区分

Unknown 是 CCR 的信息状态,不等于 relation domain 的数学 ⊥。

这样不会为了方便实现反过来限制数学空间。

三处仍待维护者裁(本 PR 保留为待裁)

  1. checker = ... 是工具钩子还是可求值声明(若是后者,Constraint 从后门回来);
  2. CCR-4「无界指称」失去承载机制——v1 靠自由项代数 + 规则闭包,两者都砍了;v2 只留"开放 universe 不封顶"(另一个"无界");
  3. v1 那三个反例测试的性质变了(无限递归不再需要表示 / 非格平凡满足 / 矛盾变成"两个关系都存在")。

边界

单文件新增,既有文件零改动;11 项未核实逐条登记;维护者的判断与写手的展开逐处分清。

产物 = docs/maintainer/design/ccr-v8-open-relational-lattice.md(新增单文件,1233 行;
与 existence-structure.md / materialization-space.md 同级)。真源 = /tmp/briefs/ccr-v8-raw.md
(维护者原话逐字,未改动);本文 = 其形式化展开 + 仓库锚定 + 冲突登记。

覆盖:原文 31 节逐节(§二十七 覆盖表机械可查)+ 八条公理 CCR-1…CCR-8(每条三栏:
形式陈述 / 禁止什么 / 可机械检查的判据形状;CCR-8 另给 N-1…N-4 四条「不成为第二语义
权威」判据,N-1 以截断实验为唯一不可伪造形式)+ 五原语字段级 + Theory 组合(§27/§28)
+ Rule vs Constraint 独立成节(§四,deduction vs admissibility + 同事实两侧例子)
+ μ/ν/默认三态语法形状写死(§五)+ §31 验收标准独立成节(§二十一,三个反例各给最小
可执行测试形状 + 特殊 case 探测 + 负向钉子)。

三态纪律:几乎全 [提案](提案 30 · 已实现 8 · 已设计未实现 6,A 口径实测;
B 口径 = §二十二 A/B/C 三表 46 数据行,逐条带 file:line)。计数节采用全角自指防护 +
内容指称(不按行号),并记录本条自身的两次修订史(10→9→8)作为「A 不是主张数」的实证。

核验基线 = develop@origin @ 0eb1efd(非手边检出)。实核锚点要点:
· CCR_VERSION = 9(ccr_io.cr:135),非 8;CCR_SEG_COUNT = 8(:138)· CCR_MAGIC(:134)
· load 版本闸 = 严格等值 `ver != CCR_VERSION`(:979)· 段表三闸(:1006-1009)
· 段必备集:STR/SYM/NOD/REG/EDG + TYPE/IFACE 必备(:1030-1031),ENT 可缺(:1025)
· 段级消费者:写侧 save_ccr 8 段(:604/621/636/697/706/724/749/768/793/824/883/896/910)
  读侧 load_ccr 8 段(:1061/1085/1113/1177/1191/1227/1269/1294/1356/1413/1484/1534/1592)
  + 项索引一致性硬校验(:1758);消费者 corearch.cr:376 · 组合根 targets/…/main.cr:64
  → build_linear_schedule(regalloc.cr:867)· main.cr 两处调用点(:691/:721)
· 判据面:canary_values.tsv:180-184 四条 .ccr 锁值 · test_ccr_v7.py(2204 行) ·
  test_ccr_types.py(2362 行,run.sh:137 注记 49/49,本任务未复跑) · --dump-types 通道
· D1/D2/D3 三条设计原则原文逐条引出(existence-structure.md:13/14/15)+ 替换关系表

冲突登记 9 条(每条带核实结论,不替维护者裁决),要点:
· C-1(最重要)版本整数裁决 = 8 与现行 CCR_VERSION = 9 的碰撞:数值上是从 9 回退;
  「后缀」编码形态未定(u32 装不下串)⇒ 待裁 1;与 materialization-space.md §7.4
  「承载与 CCR_VERSION 一并立项」必须对齐
· C-2 后端改查询消费者的现状代价实核(全改 vs 分层,发射面/关系面边界未划 ⇒ 待裁 2)
· C-6 ccr_io.cr 头注释 9 处「8/36B」陈标(含 2 处直指版本闸,V8 落地必做前置)
· C-7 ccr_types.cr 调用点行号漂移 · C-9 新发现:canary_values.tsv 自身引用的行号已陈旧
  (main.cr:408-414→实核 415-421;:433-437→实收 440-448,均 +7)

待裁 10 项(后缀形态 · 后端查询范围界 · ENT/NOD/REG 层归属 · Mapping 层归属 ·
读回判据通道 · 多头规则 · Constraint 值域 · 文本/二进制 · §25 facts 节 vs §2 原语清单 ·
v9 切换方式);未核实 11 项(§二十八,含 U-1「退回」原话歧义)。

与既有文档的关系只登记与建议、未动那三份文件:v7-format spec 被取代(V8 落地前仍是
字节真源)· existence-structure.md 语义承载地位待裁 · ADR-0002 需新 ADR supersede
(按 adr/README.md 规则:不改已 accepted 记录、保留原文、新起一号 ⇒ 建议 ADR-0023)。

零实现、零编译、零测试改动:不碰任何 .cr/.py/CI/基线文件;不推。
…+ Optional Refinement Algebra)

按维护者 2026-09-22 第二版口述输入(`/tmp/briefs/ccr-v8-raw-v2.md`,14 标题 + 19 行对照表)重写本档。
**v1 全文存留于父修订**(不重写历史);文件名不动(改名会让已有引用悬空),标题变更写进正文 §〇.0。

- **§二「删除了什么、为什么」**:v2 对照表 **19 条逐条**(v1 里是什么 / 结论 / 理由 / 去处,四栏齐备)
  + v2 **未点名**但被 Term 砍/Rule 删/Constraint 砍/Query 移出/完备格删**蕴含**的 **12 条**
  (含八公理 CCR-1…8 逐条 8 子行)+ v2 **未改变**的 v1 结论 8 条对照(防误读为「全砍」)⇒ 共 **31 行**
- **§四 专节**:`Unknown 是 CCR 的信息状态,不等于 relation domain 的数学 ⊥`(v2 明称「非常重要」;
  显眼提示块 + 专节 + 四组件处共三处)· 并保留 v2 的**唯一底线**「CCR 本身绝不采用逻辑爆炸」
- **§三 四组件字段级**:EntityRef(稳定 ID + 开放 tag **仅作工具提示**)/ Relation(`R(…)` 与可选 `R(…)=v`,
  不特殊区分 fact/mapping/analysis/storage/time)/ RelationDomain(含「不要塞 proof rules/fixed points/solver/
  backend implementation」禁令 + 两条工程理由)/ Refinement(`⪯` 必需 · `⊔` 可选;core 不要求 ⊤/⊥)
- **§十 待裁重算**:v1 十项(**保留 6 / 收窄保留 1 / 作废 3**,作废项保留行 + 给消失理由)
  + **新增 11**(任务点名 7 + 本文派生 4)⇒ **21 项**
- **§八 现状锚点全部保留**(版本常量 / 闸门 / 段级消费者 / 判据面 / canary 锁值):
  基线**未动**(`develop@origin` 仍 = `0eb1efd3`,与 v1 同一修订 ⇒ 按修订同一性沿用)
  + 本会话 **16 组抽样复核**(含 9 处 C-6 陈标重读、C-9 两处行号、canary 五值逐字符)· B = 46 **机械重数 ✓**
- **§九 冲突登记 10 条**:新增 **C-10**(V8 `metadata` ↔ 现行 `g_opt_meta` 同名不同物);**C-5 本版消解**
  (v2 自己把「无格承诺」接上了);C-1 增补与 `materialization-space.md:846`「tag 9+ 两个主张者」的联动观察
- **§十四 未核实重算**:v1 十一项逐个处置(保留 7 / 转化 1 / 部分作废 1 / 降级移出本档 1 / 作废 1)+ **新增 6** ⇒ 17 项
- **§十一.3 交叉引用爆炸半径档** `docs/superpowers/specs/2026-09-22-ccr-v8-blast-radius.md`
  (另一位写手,`develop@origin` 上尚无,按名引用);分工 = 它管承载面、本档管语义面,列三处必须对齐的接缝

零实现(全文除 `[已实现]` 标注的现状锚点外均无仓库对应物)。三态计数:A = 9 / 4 / 19,B = 46。
无编译、无测试执行(本批纯文档)。
@dslsdzc
dslsdzc merged commit d81918b into develop Sep 22, 2026
4 checks passed
@dslsdzc
dslsdzc deleted the feature/ccr-v8-spec branch September 22, 2026 22:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant