diff --git a/DEBUG_REPORT.md b/DEBUG_REPORT.md index 9e1edbf..34f0fba 100644 --- a/DEBUG_REPORT.md +++ b/DEBUG_REPORT.md @@ -3,7 +3,7 @@ > 日期: 2026-07-06 > PR: https://github.com/dslsdzc/core/compare/main...RhineIris:core:main > -> **⚠️ 历史存档**：本报告描述的问题均已在后续修复中解决—— +> ** 历史存档**：本报告描述的问题均已在后续修复中解决—— > 文中 3 个已修复 Bug 已合并（PR #9/#16 时期）；"仍未解决的根本性 Bug" > （rip_patch 位置错位）已由 2026-07-23 P0 全量修复（`emit_instr()` disp32 > 写入补上当前指令基址）解决，corec2 → corec3 自举现已全程通过。 @@ -114,7 +114,7 @@ fn tokenize() { PATCH gvi=698 ppos=74669 off=5584 target=4736480 rel=467503 PATCH gvi=698 ppos=74751 off=5584 target=4736480 rel=467421 PATCH gvi=698 ppos=74845 off=5584 target=4736480 rel=467327 -... (16 total, all target=4736480 ✓) +... (16 total, all target=4736480 ) ``` - `off=5584` → 全部一致 @@ -188,8 +188,8 @@ syscall3(1, fd, g_elf_buf, sz); | 位置 | 期望值 | 实际值 | 状态 | |------|--------|--------|------| -| buf[500000] | 0x12345678 | 0x12345678 | 保留 ✓ | -| buf[74717] | 0xCAFEBABE 或 0xDEADBEEF | 0x458948ff | 覆盖 ✗ | +| buf[500000] | 0x12345678 | 0x12345678 | 保留 | +| buf[74717] | 0xCAFEBABE 或 0xDEADBEEF | 0x458948ff | 覆盖 | - 标记 1（位置 500000）→ **保留成功**，说明 buffer 在 elf_gen 返回后没有被整体污染 - 标记 2（位置 74717）和标记 3（位置 74717）→ **都被覆盖**，最终值是原始指令代码 diff --git a/TODO.md b/TODO.md index 9f26d61..920cf73 100644 --- a/TODO.md +++ b/TODO.md @@ -30,7 +30,7 @@ - emit_alloc_body 零初始化 + 链式扩容标记满 ### @ 内建原语（12 个全部完整） -- `@sizeOf(T)` / `@alignOf(T)` — 编译期常量，ELF 验证 8 / 1 ✅ +- `@sizeOf(T)` / `@alignOf(T)` — 编译期常量，ELF 验证 8 / 1 - `@fields(T)` — 遍历 struct fields，返回逗号分隔名字符串 - `@hasField(T, name)` / `@field(T, name)` — 结构体字段存在性 + 偏移量 - `@typeInfo(T)` — 类型名称字符串 @@ -84,10 +84,10 @@ RVSDG 式嵌套 region 已落地（规格 docs/superpowers/specs/2026-08-08-regi - 仅增加 mmap 扩容会让热缓存路径增长到约 7.6 GiB RSS 并触发 WSL OOM；需要按函数回收临时 IR/缓存数据，而不是继续扩大堆 ### 2. 并发集成：单 M 已端到端验证，多 M 未验证 -- ✅ `go f(args)` 端到端已通：`sched_go(@addr(f), arg)` → g_new 存 saved_fn/saved_arg → 静态构建由 ELF 后端内联发射 fiber_init/fiber_switch/goroutine_entry_wrapper（不再依赖 rt.s 链接）→ wrapper 调用 saved_fn(saved_arg) → 结果经 result_ch 回传 -- ✅ 主线程注册为 G 0，可经 channel 阻塞/唤醒；sched_yield 不再重排 Gwaiting -- ⏳ M 线程 worker loop（m_start_workers）未连到调度器完整测试——静态构建尚未内联发射 m_start_workers（rt.s 符号） -- ⏳ channel wait queue 链表操作未在多线程并发下验证 +- `go f(args)` 端到端已通：`sched_go(@addr(f), arg)` → g_new 存 saved_fn/saved_arg → 静态构建由 ELF 后端内联发射 fiber_init/fiber_switch/goroutine_entry_wrapper（不再依赖 rt.s 链接）→ wrapper 调用 saved_fn(saved_arg) → 结果经 result_ch 回传 +- 主线程注册为 G 0，可经 channel 阻塞/唤醒；sched_yield 不再重排 Gwaiting +- M 线程 worker loop（m_start_workers）未连到调度器完整测试——静态构建尚未内联发射 m_start_workers（rt.s 符号） +- channel wait queue 链表操作未在多线程并发下验证 - 注意：G 结构 offset 56 同时用作 saved_fn（goroutine.cr）与 temp_val（chan.cr 等待队列 handoff）——单 G 流程可用（wrapper 在 chan 操作前读取 saved_fn），但字段语义重叠，重构时需拆分 ### 3. 解释器局限 diff --git a/docs/comptime.md b/docs/comptime.md index 768af02..10ec328 100644 --- a/docs/comptime.md +++ b/docs/comptime.md @@ -54,8 +54,8 @@ comptime fn fibonacci(n: int) -> int { return fibonacci(n - 1) + fibonacci(n - 2); } -x := fibonacci(40); // ✅ 编译时算 -y := fibonacci(user_input); // ❌ 编译错误：comptime fn 需要已知参数 +x := fibonacci(40); // 编译时算 +y := fibonacci(user_input); // 编译错误：comptime fn 需要已知参数 ``` ## 可编译时执行的条件 @@ -64,8 +64,8 @@ y := fibonacci(user_input); // ❌ 编译错误：comptime fn 需要已知 | 执行条件 | 自动执行 | @comptime | |---------|---------|-----------| -| 纯函数，所有输入已知 | ✅ | ✅ | -| read_file，路径已知 | ✅ | ✅ | -| 有未知输入 | ❌ 留给运行时 | ❌ 编译错误 | -| 调用 FFI / volatile | ❌ | ❌ 编译错误 | -| 类型内省（@typeInfo 等） | — | ✅ | +| 纯函数，所有输入已知 | | | +| read_file，路径已知 | | | +| 有未知输入 | 留给运行时 | 编译错误 | +| 调用 FFI / volatile | | 编译错误 | +| 类型内省（@typeInfo 等） | — | | diff --git a/docs/distributed.md b/docs/distributed.md index 1d7dcb2..8c0e92a 100644 --- a/docs/distributed.md +++ b/docs/distributed.md @@ -86,9 +86,9 @@ go @("server2") worker(1); | 调用处 | 远端接口 | 结果 | |--------|---------|------| -| `fn(x: int) -> int` | `fn(x: int) -> int` | ✅ 匹配 | -| `fn(x: int) -> int` | `fn(x: int) -> string` | ❌ 不匹配 | -| `fn(x: int) -> int` | `fn(x: dyn) -> int` | ✅ dyn 兼容 | +| `fn(x: int) -> int` | `fn(x: int) -> int` | 匹配 | +| `fn(x: int) -> int` | `fn(x: int) -> string` | 不匹配 | +| `fn(x: int) -> int` | `fn(x: dyn) -> int` | dyn 兼容 | 不需要版本号。接口签名一致就能跑。版本号是人控制的，编译器只看接口类型。 diff --git a/docs/generics.md b/docs/generics.md index b939639..11f2b90 100644 --- a/docs/generics.md +++ b/docs/generics.md @@ -48,8 +48,8 @@ fn print_size(x: T) { 约束推导：编译器看图，发现 `x.size()` 调用，检查传入的实际类型是否有 `.size()` 方法。 ```core -print_size(42); // ❌ int 没有 .size() -print_size("hello"); // ✅ string 有 .len()，编译器推导约束匹配 +print_size(42); // int 没有 .size() +print_size("hello"); // string 有 .len()，编译器推导约束匹配 ``` ### 隐式约束推导 @@ -61,8 +61,8 @@ fn add(a: T, b: T) -> T { return a + b; // 编译器推导：T 必须支持 + 运算 } -add(1, 2); // ✅ int 支持 + -add("a", "b"); // ✅ string 支持 + +add(1, 2); // int 支持 + +add("a", "b"); // string 支持 + ``` ## 图上的实现 @@ -145,7 +145,7 @@ arr := make_array(); 编译器处理方式：`N` 被约束为 `int`，且在调用处必须是 `@comptime` 已知的编译时值。 ```core -make_array(); // ❌ 编译错误：泛型参数 N 需要编译时已知 +make_array(); // 编译错误：泛型参数 N 需要编译时已知 ``` ## 设计与替代方案 diff --git a/docs/ir-schema/coreir-schema.md b/docs/ir-schema/coreir-schema.md index 6e16306..c81e7eb 100644 --- a/docs/ir-schema/coreir-schema.md +++ b/docs/ir-schema/coreir-schema.md @@ -21,7 +21,7 @@ Core 编译器使用两种中间表示： .cir = 程序的数据流图 + 规约约束 ↓ 验证工具消费 .cir： - 1. 编译器已证明的约束（自动推导标签）标注为 ✓ + 1. 编译器已证明的约束（自动推导标签）标注为 2. 用户写的约束标注为 pending 3. 验证工具尝试证明 pending 约束 4. 输出：每个约束绿/黄/红 diff --git a/docs/spec-design.md b/docs/spec-design.md index 5a40dd0..ef5ae2f 100644 --- a/docs/spec-design.md +++ b/docs/spec-design.md @@ -1,6 +1,6 @@ -# Core 规约系统设计 +# Core 规约系统设计（v2 — CIC 内核 + SMT 证书架构） -> 规约 = 图上的约束。 +> 规约 = 图上的约束。表达力 = CIC（归纳构造演算）。自动化 = SMT 证书外包。 ## 一、哲学 @@ -16,15 +16,38 @@ corec build file.cr -s → .cir + .ccr + 自动生成 file.csp → .csr 验证 = 证明图的所有可达状态满足图上的约束。 ``` -**.csp 是编译器自动生成的：** -- 包含所有函数的声明骨架 + 自动推导标签 -- 用户在这个 `.csp` 里手写 `#check` / `#ensure` / `spec fn` -- 下次 `-s` 重新生成：新函数加入、删除的函数移除、已有手写规约保留 -- 版本管理：`.csp` 应该入版本库 +## 二、架构总览（v2） -`.csr` 是将 `.csp` 中的规约约束（check/ensure/invariant/spec fn）编译为 TagNode 元数据的二进制序列化，与 `.cir`（DFNode）配套供验证工具消费。 +规约语言（一套 Core 语法）编译为 **CIC 项**（归纳构造演算），验证走双通道： -## 二、平民化原理 +``` +Core 规约语言（.corespec / .csp / .cr 内联） + ↓ 编译（翻译桥：命令式 → 函数式） +CIC 项（归纳构造演算——一切表达力：量词/归纳/依赖类型/递归性质） + ├─ 目标一阶可表达 → SMT 通道（自动求解 + 用户可选 #smt） + │ → SMT 返回证书（证明轨迹） + │ → 翻译成 CIC 证明项 → 内核重新验证 ← 健全性永远在内核 + └─ 归纳/高阶 → CIC 内核直接处理 +``` + +**健全性唯一来源是 CIC 内核。** SMT 是证明搜索器（可以凭启发式甚至不健全地猜），其输出必须经内核验证才被接受——证书校验失败即拒绝，绝不引入不健全。这是 SMTCoq 模式（CAV'17，先例）。 + +### 表达力边界 + +CIC 提供 Coq 级别的全部表达力，逐项对应： + +| 能力 | CIC 承担 | Core 用户付出 | +|---|---|---| +| 全称/存在量词（无限域） | `forall/exists` 是语言一等构造 | 零——量词是规约语言语法 | +| 归纳类型 + 归纳原理 | 枚举/结构体 → 归纳类型，原理在内核 | 零 | +| 递归函数 + 终止性 | 递归定义 + `loop variant` 标注 | 变体标注（EBNF 已有） | +| 高阶量词（∀f: int→int） | 函数空间原生可量化 | 零（规约层函数类型，见 §10） | +| 依赖类型（`Vec n`） | 内核有，**但 Core 不需要** | 被图验证替代：边界安全由图保证，长度性质由谓词表达（`#ensure(result.len() == |a|)`） | +| 引理/定理复用 | 证明项可组合 | 见 §12 用户入口 | + +**Core 对依赖类型的替代**：Coq 用 `Vec n` 在类型层面保证索引不越界/长度匹配；Core 里这两个需求已被其他机制消化——索引越界由指针模型图验证保证（已实现），长度性质由谓词表达。安全性由图承担，性质由谓词承担——这就是 Core 不用付出依赖类型学习成本的根源。 + +## 三、平民化原理 **不需要写公式，不需要学数理逻辑。规约用 Core 语言本身书写。** @@ -38,7 +61,7 @@ corec build file.cr -s → .cir + .ccr + 自动生成 file.csp → .csr 三个层级最终都编译为 `.cir` 的规约 DFNode（条件表达式）+ `.csr` 的 TagNode（约束元数据），对验证工具无差别。 -## 三、文件格式 +## 四、文件格式 ### `.cr` — 实现源码（也可内联规约） @@ -109,7 +132,7 @@ spec fn vec_invariant[T](v: Vec[T]) -> bool { 每条 `#check`、`#ensure`、`#invariant` 以及每个 `spec fn` 的身体，都编译为 `.cir` 的规约 DFNode（条件表达式）+ `.csr` 的 TagNode（约束元数据：类型、验证状态、行列号）。TagNode 通过 `target_node` 指向 `.cir` 中对应的 DFNode，通过 `condition_node` 指向条件表达式所在的 DFNode。 -## 四、编译器自动推导（零门槛的核心） +## 五、编译器自动推导（零门槛的核心） 编译器从 `.cir` 图结构中自动推导性质，写入 `.csr`，不需要用户写任何东西。 @@ -159,7 +182,7 @@ fn transfer(from: &mut Account, to: &mut Account, amt: int) **模式匹配库可扩展**：社区可以贡献新的图模式 → 标签映射，编译器新增推导能力。 -## 五、标签语法（标注/annotation） +## 六、标签语法（标注/annotation） 使用 `#` 前缀，与 `@`（外部项目引用）区分。 @@ -180,7 +203,7 @@ fn foo() -> int - 不占用 `@`（后者保留给 `import @project`） - 语义清晰：`#` 标记的东西不影响运行时语义 -## 六、检查函数（规约的主力） +## 七、检查函数（规约的主力） 检查函数是用 Core 语言写的纯函数，返回值是 `bool`。它们被编译为 `.cir` 图，然后与实现函数的 `.cir` 并列供验证器消费。 @@ -222,19 +245,198 @@ spec fn all_nonneg(arr: [int]) -> bool = forall x in arr: x >= 0; ``` -## 七、约束的验证 +## 八、量词（v2 新增） + +`forall x: int => P(x)` 必须是规约语言的一等构造（**不是** for 循环的翻译）——int 域无限，遍历不了；for 循环只是有限域的便利糖（§7 纯公式支持的 `forall x in arr` 是有限域情形）。 + +```core +// EBNF 已定义（grammar/corespec.ebnf） +forall (x: int) => x >= 0 +exists (i: int) => a[i] == target +``` + +## 九、翻译桥：spec fn（命令式）→ CIC 项（函数式）（v2 新增） + +### 9.1 问题定义：两个语言的语义鸿沟 + +spec fn 用 Core 书写——命令式：变量重复赋值、循环、数组、`return`。CIC 是纯函数式逻辑：lambda 演算、递归定义、归纳类型、没有赋值没有循环。翻译桥把前者确定性变换为后者，**不丢语义、不加语义**。 + +可行的根本保障：spec fn 是纯的（project-book："规约表达式限于纯逻辑运算"——无副作用、无 IO、无 unsafe、无外部调用）。纯命令式程序与函数式程序的翻译是经典确定性问题。 + +### 9.2 结构翻译表（Core 构造 → CIC 构造） + +| Core 构造 | CIC 翻译 | 示例 | +|---|---|---| +| `x := expr` / 单次赋值 | `let x = expr in ...` | `total := 0` → `let total = 0 in ...` | +| 重复赋值 `x = expr` | SSA 化 → 递归参数传递 | `x = x + 1` → 递归调用参数 `f(x+1)` | +| `return expr` | 直接表达式化 | 函数体即表达式 | +| `if/else` | 条件表达式（ite/match） | `if b { A } else { B }` → `if b then A else B` | +| `for x in arr` | fold/递归遍历 | `for x in arr: acc += x` → 对 list 递归 | +| `for i in 0..n` | 有界递归（参数递减） | 变体 = `n - i` | +| `loop { ... }` + `break` | 尾递归（需要变体） | 变体标注（EBNF 已有） | +| 数组 `a[i]` 读写 | 归纳列表索引 / 数组理论 select-store | 或带长度约束的结构 | +| 结构体/枚举 | 归纳类型构造子 + match | `Point{x, y}` → `mk_point x y` | +| 递归调用 | CIC 递归定义（良基递归） | `fact(n) = n * fact(n-1)` | + +核心模式——循环即递归： + +``` +for i in 0..n: acc += a[i] + ↓ +f(acc, i) = if i >= n then acc + else f(acc + a[i], i + 1) // 变体 = n - i，递减保证终止 +``` + +### 9.3 终止性：变体是翻译的前提 + +CIC 只接受**良基递归**（递归参数严格递减）——非终止的"递归"在 CIC 里无法定义。因此： + +- 每个循环/递归翻译必须携带**变体**（loop variant，EBNF 已有）——递减度量 +- 编译器自动推导（§五 的 `#terminating` 图模式）优先；推导不出的要求用户标注 +- 无变体的循环 → 翻译失败（编译错误），或降级为未解释函数（用户确认语义） + +### 9.4 整数语义：机器整数 vs 数学整数（关键决策） + +Core 的 `int` 是 64 位机器整数（会溢出），CIC 的整数是数学整数（Z，无界）。**翻译桥必须选择规约里的整数语义**： + +| 选项 | 语义 | 代价 | +|---|---|---| +| 数学整数（默认） | 规约性质在无界整数上证明 | 简单；但 `#ensure(x + y > x)` 在数学域成立、机器域可能因溢出失败——**证明的结论可能不反映实际行为** | +| 机器整数（位向量） | 精确匹配运行语义（SMTCoq 已支持位向量理论） | 复杂；需要位向量 + 溢出模式建模，证明义务更繁 | +| 混合 | 默认数学整数；位宽相关性质用显式位向量类型标注 | 平衡；用户只对溢出敏感的性质声明位宽 | + +**待定**：默认数学整数 + 显式位宽标注（混合方案）是倾向方向，与内核选择（§十七）一并决策。 + +### 9.5 实现函数进规约的身份 + +`#ensure(f(x) == y)` 引用实现函数 f——f 不是 spec fn，是运行时代码。它的 CIC 身份是**语义模型**： + +- 函数式子集（纯、可翻译）→ 翻译为递归定义（与 spec fn 同路径） +- 其余（有副作用/未翻译）→ **未解释函数**（Uninterpreted Function）：CIC 只知道签名，不知道定义——性质只能由用户另行声明 +- 有副作用/非纯的实现函数不能进规约（project-book 规定） + +### 9.6 失败情形（翻译不了怎么办） + +| 情形 | 处理 | +|---|---| +| 循环无变体 | 编译错误（要求 `variant` 标注）或降级未解释函数 | +| 数组索引可能越界 | 翻译时插入越界条件（`i < len`），越界路径 → 未定义值（⊥） | +| 副作用/IO/unsafe | 翻译拒绝——规约只能引用纯函数 | +| 溢出敏感性质 | 显式位宽标注（见 9.4） | + +## 十、函数类型归属（v2 决策：规约专属） + +函数类型在两个层面是两个不同的东西，**必须拆分决策**： + +| | 规约层 | 实现层 | +|---|---|---| +| 函数是什么 | 数学对象（映射）——CIC 的 lambda | 运行时对象（代码/闭包） | +| 机制 | 箭头类型 `int -> int` → CIC 原生 | TYP_FN + 闭包/捕获/调用约定 | +| 需求 | 高阶量词 `forall f: int -> int => P(f)` | 函数值编程（map/filter 传函数、回调表） | + +**决策：规约专属函数类型。** `int -> int` 只存在于规约语言（`.corespec` 类型宇宙的一部分），直接映射 CIC 箭头；量化的是数学函数，不需要实现层有函数值。零污染 Core 语言（checker/ir_gen/后端/内存模型不动），符合"规约是独立源文件"的哲学。 + +**实现层函数值（TYP_FN/闭包）按 YAGNI 挂起**：现状 `@addr(f)` + int 能表达函数地址（内核函数表、中断向量表）；闭包与 arena 内存模型（捕获变量归属）交互复杂，无真实用例不做。 + +## 十一、验证器：CIC 内核 + SMT 证书（v2 新增） + +> 内核选型与融合架构的完整论证见 `docs/verifier-kernel.md`（理论谱系、2025–2026 论文扫描、融合决策、自举路线）。 + +### 内核 + +CIC 类型检查器（Coq 内核级别：约数千行的信任根）。初期绑定成熟实现，后期自举为 Core 版（见 §14 与 `docs/verifier-kernel.md`）。 + +### SMT 通道（证书架构，SMTCoq 模式） + +``` +目标（CIC 项） + → 一阶化翻译（数组/算术/UF 理论） + → SMT 求解器（Z3/veriT/CVC5 类） + → 证书（unsat 证明/求解轨迹） + → 翻译成 CIC 证明项（refl/omega/... 构造） + → CIC 内核重新验证 ← 健全性唯一来源 +``` + +- SMT 不求信任：可以跑不健全启发式，证书校验失败即拒绝 +- 用户可**主动选择** SMT：目标标注 `#smt`（hammer 的手动挡） +- 覆盖范围：线性算术、数组边界、位向量、UF——"绝大多数"；SMT 表达不了的目标（归纳/高阶）直接走内核——**表达力边界由 CIC 决定，SMT 只是加速器** + +### 反例调试 + +SMT 解不出时返回**反例模型**（哪个输入违反性质）——开发期黄金能力：`#check(b != 0)` 被违反 → SMT 给出 `b = 0` 的具体反例。验证报告区分三种状态：**绿**（证明）/ **黄**（部分）/ **红**（反例或未证明）。 + +## 十二、约束的验证与用户入口 验证器（外部贡献）的操作： 1. 加载 `.cir`（程序图）+ `.csr`（图上约束） 2. 从图结构推导自动标签（标签 = 编译器已证明） -3. 对 `#check`/`#ensure`：生成证明义务 → SMT / 溯因推理 / 归纳 +3. 对 `#check`/`#ensure`：生成证明义务 → SMT 通道 / CIC 内核 4. 对 `spec fn`：检查实现函数的图是否蕴含检查函数的图 -5. 输出：每条约束绿（证明）/ 黄（部分证明）/ 红（未证明） +5. 输出：每条约束绿（证明）/ 黄（部分证明）/ 红（反例或未证明） 约束可以同时在开发期插桩运行时 assert 检查，验证器到位前也有保障。 -## 八、完整管线 +### 用户入口分层（自动化失败时降级，v2 新增） + +| 层 | 入口 | 用户要做什么 | 学习成本 | +|---|---|---|---| +| 0 | 默认全自动 | 什么都不做 | 零 | +| 1 | `#induct x` 归纳引导 | 标注"对哪个变量做结构归纳" | 一句话 | +| 2 | `#lemma` 引理拆解 | 写中间性质（Core 规约语言） | 理解"拆解"思维 | +| 3 | CIC 证明项逃逸 | 直接给证明项 | 高（最后手段，对应 unsafe 的位置） | + +- 层 1 本质：生成 CIC 归纳原理实例化（基例 + 归纳步两个目标），各回自动化——归纳框架是 CIC 的，步骤求解是 SMT 的 +- 层 3 远期演化：Core 自举 CIC 内核成熟后，可变成"用户用 Core 写证明"（Curry-Howard 在 Core 呈现） + +### .csr 状态 + +`.csr` 的 status 字段（0=unproven, 1=auto_proven, 2=user_proven）承接验证结果： + +| 来源 | status | +|---|---| +| 编译器自动推导标签 | auto_proven | +| SMT 证书经内核验证 | user_proven | +| 用户入口产物 | user_proven | +| 未证明 | unproven（不拦编译——证明失败 ≠ 程序不安全） | + +## 十三、规约的回报：证明驱动的优化（v2 新增） + +**写的证明越多，编译器优化越狠。** 规约不只是验证负担——证明过的性质流入优化器，成为激进变换的前提。这是"语义保鲜"的闭环：用户注入的语义（规约）流经验证变成**可证明的事实**，再流进优化器，验证的回报不只是安全，还有性能。 + +### 机制：证明状态门控的优化信息流 + +``` +用户写规约 → 验证（SMT/内核）→ 状态 proven / unproven + │ + proven 的性质 ──┼──→ 优化 pass（变换前提） + unproven 的性质 ──→ 丢弃（绝不喂优化器） +``` + +**关键：只有被证明的性质才进优化器。** `.csr` 的证明状态（auto_proven / user_proven）就是优化器的许可证——unproven 的性质可能为假，喂给优化器 = 优化器引入 bug。**证明错误 = 优化错误，门控是机制核心。** + +### 收益清单（证明 → 优化映射） + +| 证明的性质 | 优化器能做什么 | +|---|---| +| `#check(b != 0)` 已证 | 除法免零检查 | +| `#safe_index` 已证 | DEREF 运行时边界检查（cmp+jae+ud2）直接消除——编译期证明免检的规约版，覆盖运行时数组 | +| `#pure` 已证 | CSE / 死代码删除 / 重排（纯调用可删可移） | +| `#no_alloc` 已证 | 栈分配替代堆分配 | +| `loop invariant` + `#terminating` 已证 | 循环变换（向量化/强度削减/展开）前提满足 | +| 指针分离/别名规约已证 | 内存访问重排（否则保守不重排） | +| `#deterministic` 已证 | 更激进的缓存/重算策略 | + +### 动机闭环 + +**规约从"验证负担"变成"性能投资"**——普通程序员为性能写 `#check`/`#ensure`，验证顺手完成。这解决了"为什么要写规约"的动机问题。先例：LLVM 的 `llvm.assume`（用户声明的事实喂优化器）。 + +### 两个注意点 + +1. **编译器内部回读通道**：`.csr` 现在只服务外部验证器——需要编译器内部读取已证性质表（管线：编译 → 规约 → 证明 → 已证性质表 → 优化 pass） +2. **证明时效**：代码改动后证明需重验——增量缓存已有函数级 `.cir` 缓存，证明缓存同理 + +## 十四、完整管线 ``` # 编译（无规约） @@ -258,8 +460,8 @@ corec build file.cr -s # 验证（外部工具） verify file.csr → 加载 .cir + .csr - → 验证 pending 约束 - → 输出验证报告 + → 验证 pending 约束（SMT 通道 / CIC 内核） + → 输出验证报告（绿/黄/红） ``` 编译器输出的 `.csr` 包含： @@ -267,7 +469,15 @@ verify file.csr - 用户写的 `#check/#ensure/#invariant`（status=pending） - `spec fn` 编译为 spec 图节点（status=pending） -## 九、内核场景的应用 +## 十五、信任根与自举路线（v2 新增） + +验证的信任根是 CIC 内核——内核有 bug = 一切证明皆空。路线（与 corec 自举同构）： + +1. **初期**：绑定成熟内核（候选：Rocq / Lean 4，决策挂起，见 §16） +2. **自举**：有人用 Core 写出 CIC 内核版本 → 替换外部依赖 +3. 先例：Coq Coq Correct!（被 Coq 证明正确的 Coq 内核）、Milawa（链式自举：A 验证 B，B 验证 C…，信任降到最小可审计内核） + +## 十六、内核场景的应用 普通开发者的代码：编译器自动推导 + 可能几行 `#ensure`。 @@ -302,12 +512,39 @@ fn map_page(pt: &mut PageTable, virt: Addr, phys: Addr, flags: u64) 内核的量词（`for all mappings`）写成了 `for` 循环，编译器把它编译成纯逻辑约束。纯公式语法糖（`forall`）也存在，但只是编译器的展开。 -## 十、总结 +## 十七、实现里程碑（建议） + +1. `.corespec` 解析（量词/函数类型/变体）+ 规约类型检查 +2. 翻译桥：spec fn → CIC 项（循环→递归、数组→归纳列表） +3. SMT 通道：目标翻译 + 证书校验 + 内核验证（绑定内核起步） +4. 用户入口：`#induct` → `#lemma` → 逃逸 +5. 自举 CIC 内核（Core 版） + +## 十八、开放决策点（挂起，待外部贡献者参与） + +| 决策点 | 状态 | +|---|---| +| **内核选择：Rocq vs Lean 4** | 挂起——两者都是 CIC 类，规约语言/SMT 证书/翻译桥/自举路线不受影响，等社区参与 | +| 实现层函数值（TYP_FN/闭包） | YAGNI 挂起，等真实用例 | +| 证明项逃逸的最终形态 | 随内核选择与自举进度演化 | + +## 十九、总结 ``` 不需要学新语言 ── 规约 = Core 函数 不需要写公式 ── 编译器从图推导能推导的一切 不需要自己来 ── 剩下的用同一门语言写检查函数 +表达力无上限 ── 编译为 CIC，量词/归纳/高阶全在内核 +健全性有保证 ── SMT 证书经内核验证，信任根最小化 ``` 完全形式化的代价被压缩到最低：只有编译器推导不了的函数正确性需要手写检查函数，而检查函数本身也是 Core 代码，不是数理逻辑公式。 + +## 参考 + +- **SMTCoq**（Ekici/Mebsout/…, CAV'17）— SMT 证书 → Coq 证明项，求解器不可信、健全性只在内核 +- **Why3**（POPL'24 论文）— 中间验证语言：一套规约语言编译到 SMT + Coq 多后端 +- **Liquid Types / LiquidHaskell**（Jhala 系）— 谓词表达性质 + SMT 自动证明义务 +- **Sledgehammer**（Blanchette 系）— 外部证明器找证明 → 在内核重建（LCF 哲学） +- **Coq Coq Correct!**（Sozeau 等, 2020）— 被 Coq 证明正确的 Coq 内核 +- **Milawa / Self-certification**（POPL'12）— 链式自举，信任降到最小可审计内核 diff --git a/docs/superpowers/plans/2026-08-08-region-cfg.md b/docs/superpowers/plans/2026-08-08-region-cfg.md index 78a08d2..f5f4595 100644 --- a/docs/superpowers/plans/2026-08-08-region-cfg.md +++ b/docs/superpowers/plans/2026-08-08-region-cfg.md @@ -758,7 +758,7 @@ jj commit -m "feat: RegionCheck via explicit node→region mapping + docs sync ( ## Self-Review（执行前自查） -- **规格覆盖**：P1（SG_IF+映射+DOT）→ Task 1/2；P2（region 迭代）→ Task 3；P3（state edges）→ Task 4；P4（序列化 v2）→ Task 5；P5（RegionCheck+回归+文档）→ Task 6。规格第 11 节文档同步 → Task 6 Step 5 ✓ -- **类型一致**：`g_df_node_region`/`g_cur_sg`/`g_loop_region_*`/`OFF_DFE_KIND`/`SG_IF` 在各 Task 定义处与使用处一致 ✓ -- **全局约束**：所有长任务命令带 `nice -n 19`；提交用 `jj` ✓ +- **规格覆盖**：P1（SG_IF+映射+DOT）→ Task 1/2；P2（region 迭代）→ Task 3；P3（state edges）→ Task 4；P4（序列化 v2）→ Task 5；P5（RegionCheck+回归+文档）→ Task 6。规格第 11 节文档同步 → Task 6 Step 5 +- **类型一致**：`g_df_node_region`/`g_cur_sg`/`g_loop_region_*`/`OFF_DFE_KIND`/`SG_IF` 在各 Task 定义处与使用处一致 +- **全局约束**：所有长任务命令带 `nice -n 19`；提交用 `jj` - **已知不确定点**：Task 3 复现测试若与预期失败模式不符，以实际输出为准修正（步骤已注明）；Task 5 的 v4 存档文件若无现成产物则跳过兼容测试并在提交注明 diff --git a/docs/superpowers/plans/2026-08-09-repo-governance.md b/docs/superpowers/plans/2026-08-09-repo-governance.md index f7d833e..715f28d 100644 --- a/docs/superpowers/plans/2026-08-09-repo-governance.md +++ b/docs/superpowers/plans/2026-08-09-repo-governance.md @@ -514,7 +514,7 @@ jj log -r main@origin --no-graph -T 'commit_id.short()' && jj log -r develop@ori - [ ] **Step 4: 收尾核对 spec §12 状态清单** -全部 ⬜ 项变为 ✅（本地配置、develop、ruleset、签名密钥、首个 PR）。剩余 ⬜（CI 完整层点亮、opt-regress）属后续项，在 spec §11 跟踪。 +全部 项变为 （本地配置、develop、ruleset、签名密钥、首个 PR）。剩余 （CI 完整层点亮、opt-regress）属后续项，在 spec §11 跟踪。 --- diff --git a/docs/superpowers/specs/2026-08-09-repo-governance-design.md b/docs/superpowers/specs/2026-08-09-repo-governance-design.md index fa066a8..59528b6 100644 --- a/docs/superpowers/specs/2026-08-09-repo-governance-design.md +++ b/docs/superpowers/specs/2026-08-09-repo-governance-design.md @@ -157,9 +157,9 @@ gh pr create --base main --fill # develop→main PR（required reviewers = ## 12. 当前状态 -- ✅ CI 骨架：已实现（2026-08-09），本地验证通过，随首个 PR 上线 -- ✅ 社区四件套：PR 模板 / CONTRIBUTING / SECURITY / CODE_OF_CONDUCT 已写（2026-08-09），随本 spec 首 PR 上线 -- ✅ 本地配置：jj protect / jj 签名（behavior=own）/ hook / settings 清理 / CLAUDE.md——全部落地（2026-08-09） -- ✅ `develop` 集成分支已创建并承载 PR #25 -- ✅ GitHub ruleset：**main-only-maintainer**（id 20601201）+ **develop-integration**（id 20601189）已创建并 active（2026-08-09）；gh TLS 间歇性故障期间以重试创建成功；squash-only（allowed_merge_methods=['squash']）已应用于双 ruleset；delete_branch_on_merge=True 已设 -- ✅ 首个 PR（#25 → develop）与发布 PR（#26 → main，B 流程）已完成；治理全流程端到端验证 +- CI 骨架：已实现（2026-08-09），本地验证通过，随首个 PR 上线 +- 社区四件套：PR 模板 / CONTRIBUTING / SECURITY / CODE_OF_CONDUCT 已写（2026-08-09），随本 spec 首 PR 上线 +- 本地配置：jj protect / jj 签名（behavior=own）/ hook / settings 清理 / CLAUDE.md——全部落地（2026-08-09） +- `develop` 集成分支已创建并承载 PR #25 +- GitHub ruleset：**main-only-maintainer**（id 20601201）+ **develop-integration**（id 20601189）已创建并 active（2026-08-09）；gh TLS 间歇性故障期间以重试创建成功；squash-only（allowed_merge_methods=['squash']）已应用于双 ruleset；delete_branch_on_merge=True 已设 +- 首个 PR（#25 → develop）与发布 PR（#26 → main，B 流程）已完成；治理全流程端到端验证 diff --git a/docs/verifier-kernel.md b/docs/verifier-kernel.md new file mode 100644 index 0000000..d5ce3b0 --- /dev/null +++ b/docs/verifier-kernel.md @@ -0,0 +1,102 @@ +# 验证内核选型与融合架构（Verifier Kernel） + +> 信任根 = CIC 内核。表达力 = CIC + 公理 + HoTT 库。自动化 = 证书形态（计算在外、健全性在内）。 +> 融合各家之长，不选边——每个维度取最优，其他体系全部变成方法贡献。 + +## 一、问题 + +规约系统（`docs/spec-design.md`）需要 Coq 级别的表达力（依赖类型/归纳/高阶量词）。表达力由**验证内核**承载——内核是信任根：**内核有 bug = 一切证明皆空**。本文档记录内核选型论证与融合架构决策（2026-08-10）。 + +## 二、理论体系全谱系（选型时的候选） + +| 体系 | 代表 | 表达力 | 内核规模 | 数学完备性 | 自动化生态 | +|---|---|---|---|---|---| +| **CIC**（归纳构造演算） | Rocq / Lean 4 | 依赖类型+归纳+高阶 | 中等（Rocq 7.8k 行 / **Lean 3k 行**） | 函数外延性/商类型要公理 | SMTCoq（Rocq）、hammer | +| **MLTT**（Martin-Löf） | Agda / McTT | 同 CIC 族（归纳族更精确） | 中等 | 同 CIC | 弱 | +| **HoTT/Cubical** | Cubical Agda、redtt | + 商类型/外延性定理可证 | 大（归一化复杂） | 理论最优 | 生态小 | +| **HOL**（简单类型论） | Isabelle/HOL、HOL Light | 无依赖类型（表达力上限） | 极小（HOL Light ~500 行） | 外延性天然 | sledgehammer 最强 | +| **LF/公理拼装** | Metamath | 靠公理 | 极小（~600 行） | 依赖公理集 | | + +**选型结论**：对 Core 的约束（依赖类型表达力 + 自举路线 + SMT 证书架构）—— +- 理论最优是 HoTT，**工程最优是 CIC 系** +- HOL 系出局（无依赖类型）；MLTT 与 CIC 同族（CIC 的归纳类型更完整）；HoTT 的完备性用公理 + 库层补 +- CIC 系中 Lean 4 内核（~3k 行）是自举最友好的实现 + +## 三、2025–2026 最新扫描（无全新竞争体系，全新的是方法） + +| 工作 | 年份 | 贡献 | 对 Core 的意义 | +|---|---|---|---| +| **McTT**（Jang/Gaulin/Hu/Pientka, ICFP'25） | 2025 | **全验证**的 MLTT 内核（含 NbE 归一化证明，OCaml 提取；除 lexer/pretty-printer 全管线验证） | 内核"全验证"从口号变工程——自举路线终点的参考方法 | +| **Andromeda 2**（Bauer/Petković） | 2022+ | **证书内核形态**：归一化/等式检查在内核外，内核只构造 judgement + 验证证书；用户可定义理论 | 与 SMT 证书架构**同构**——确认"计算在外、健全性在内"是当代前沿 | +| **Definitional Proof Irrelevance**（Felicissimo 等, LICS'26） | 2026 | CIC + 观察等式 + 严格命题（定义性证明无关），一致性与 canonicity 证明，Rocq 实现 | CIC 系在活跃演进（不是停滞旧技术） | +| **Lean4Less**（Vaishnav, 2026） | 2026 | Lean 内核缩小化翻译（去掉 K 归约等便利定义性等式，Lean− 更小理论） | 抄 Lean 内核可抄缩小版——内核最小化参考 | +| **Lean 内核 bug 事件**（Collatz/AI） | 2025 | AI 利用嵌套归纳类型的**无规范内核 bug** 产出假证明；外部检查器复制同一 bug（代码即规范） | **教训：自举内核必须有正式规范**——先规范后实现，或用 Rocq 验证（MetaRocq 路径） | + +**扫描结论**：没有推翻 CIC 的全新理论体系；全新的是**内核形态**（证书化、验证化）和**元方法**（NbE 验证）——全部可以吸收进既有架构。 + +## 四、融合架构（决策，2026-08-10） + +不选边——**每个维度取最优，其他体系降级为方法贡献**： + +``` +┌─ 内核层（信任根）───────────────────────────────────┐ +│ CIC（Lean 4 风格，~3k 行，可 Lean4Less 式缩小化） │ +│ ├─ 表达力：依赖类型/归纳/高阶量词 ← CIC 原生 │ +│ ├─ 理论扩展：公理层 + HoTT 库（用 CIC 证明 HoTT） │ +│ │ ← Voevodsky 路线（HoTT/Coq、UniMath 先例） │ +│ └─ 远期：McTT 式 NbE 全验证（自举后给内核机械证明） │ +│ ← ICFP'25 McTT │ +└────────────────────────────────────────────────────┘ +┌─ 验证层（计算在外，内核只验证证书）─────────────────┐ +│ ├─ SMT 证书 → 证明项 → 内核验证 ← SMTCoq (CAV'17) │ +│ ├─ 归一化/等式检查外置，judgement 证书化 │ +│ │ ← Andromeda 2（同构确认） │ +│ └─ 复杂检查器反射化（库层实现 + 一次证明） │ +│ ← SMTCoq 检查器模式 │ +└────────────────────────────────────────────────────┘ +``` + +### 决策要点：三个维度各自最优，互不妥协 + +| 维度 | 取谁的 | 为什么 | +|---|---|---| +| 信任根 | CIC 内核（最小）+ McTT 验证方法（远期机械证明） | 表达力 + 可验证性兼得 | +| 表达力 | CIC + 公理 + HoTT 库（不换理论，挂载） | 数学完备性用库层拿，内核零增长 | +| 自动化 | 证书形态（SMTCoq + Andromeda 同构） | 计算在外、健全性在内——与自举/验证路线天然兼容 | + +### 为什么 HoTT 不换内核：用 CIC 证明 HoTT + +- HoTT/Coq 与 UniMath 的先例：标准 CIC 内核 + Univalence 公理（Voevodsky 模型证明一致） +- 公理化 UA 不可计算（含 UA 消除的证明项归一化会 stuck）——但**日常规约验证不用 UA**，它只在数学库层需要——工程分层天然隔离 +- Lean 4 内核原生支持 quotient + proof irrelevance（Rocq 无）——Lean 内核 + UA 公理 ≈ 更完整的 HoTT 基础 +- 结论：**HoTT 是挂在 CIC 上的公理 + 库层，不是竞争体系** + +## 五、信任根与自举路线 + +1. **初期**：绑定成熟内核（候选：Rocq / Lean 4，开放决策） +2. **自举**：用 Core 写出 CIC 内核（Lean 4 风格，可缩小化）→ 替换外部依赖（与 corec 自举同构） +3. **验证**（远期）：McTT 式 NbE 全验证——给自举内核机械正确性证明 +4. **规范先行**（内核 bug 事件教训）：自举内核**先有正式规范，后实现**——避免"代码即规范"；规范可用 Rocq 验证（MetaRocq 路径） + +先例：Coq Coq Correct!（被证明正确的 Coq 内核）、Milawa（链式自举：A 验证 B，B 验证 C…）、McTT（全验证管线）、MetaRocq / lean4lean / agda-core（验证内核进行中——"验证内核时代即将到来"）。 + +## 六、开放决策点（挂起，待外部贡献者参与） + +| 决策点 | 状态 | +|---|---| +| **内核选择：Rocq vs Lean 4** | 挂起——两者都是 CIC 类，规约语言/SMT 证书/翻译桥/自举路线不受影响，等社区参与 | +| 整数语义（数学整数 vs 机器整数，见 spec-design §9.4） | 倾向"默认数学整数 + 显式位宽标注"，与内核选择一并决策 | +| 自举内核的规范语言 | 随自举进度演化（候选：Core 规约语言自身 / Rocq） | +| 证明项逃逸的最终形态 | 随内核选择与自举进度演化 | + +## 参考 + +- **SMTCoq**（Ekici/Mebsout/…, CAV'17）— SMT 证书 → Coq 证明项，求解器不可信、健全性只在内核 +- **McTT**（Jang/Gaulin/Hu/Pientka, ICFP'25）— 全验证 MLTT 内核，NbE 归一化证明，OCaml 提取 +- **Andromeda 2**（Bauer/Petković Komel, LMCS'22）— 证书内核形态：归一化在内核外，judgement 证书化，用户可定义理论 +- **Definitional Proof Irrelevance Made Accessible**（Felicissimo 等, LICS'26）— CIC + 观察等式 + 严格命题 +- **Lean4Less**（Vaishnav, 2026）— Lean 内核缩小化翻译（extensional-to-intensional） +- **Coq Coq Correct!**（Sozeau 等, 2020）— 被 Coq 证明正确的 Coq 内核 +- **Milawa / Self-certification**（Strub 等, POPL'12）— 链式自举，信任降到最小可审计内核 +- **MetaRocq / lean4lean / agda-core** — 验证内核进行中项目（INRIA 2026 综述） +- **HoTT/Coq、UniMath** — CIC + Univalence 公理形式化 HoTT 的先例 diff --git a/editor/README.md b/editor/README.md index f92c861..6ba0b6b 100644 --- a/editor/README.md +++ b/editor/README.md @@ -20,7 +20,7 @@ cp -r editor/nvim/plugin/*.lua ~/.config/nvim/lua/plugins/ |------|----------|------| | 语法高亮 | 自动 | `.cr`/`.cir`/`.ccr` 文件 | | 代码补全 | 自动 | blink.cmp 关键字 + types | -| 代码片段 | `fn⭾` `struct⭾` 等 | 共 20+ 片段 | +| 代码片段 | `fn` `struct` 等 | 共 20+ 片段 | | 诊断 | 保存时自动 | 编译器错误显示在行内 | | Quickfix | `:make` | 编译结果 + 错误列表 | | 悬浮信息 | `K` | 查看标识符定义 |