docs: 规约系统设计 v2——CIC 内核 + SMT 证书架构 + 验证内核选型

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）→ **都被覆盖**，最终值是原始指令代码

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. 解释器局限

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 等） | — |  |

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 兼容 |
 
 不需要版本号。接口签名一致就能跑。版本号是人控制的，编译器只看接口类型。
 

docs/generics.md

@@ -48,8 +48,8 @@ fn print_size<T>(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<T>(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<int, 10>();
 编译器处理方式：`N` 被约束为 `int`，且在调用处必须是 `@comptime` 已知的编译时值。
 
 ```core
-make_array<int, user_input>();  // ❌ 编译错误：泛型参数 N 需要编译时已知
+make_array<int, user_input>();  //  编译错误：泛型参数 N 需要编译时已知
 ```
 
 ## 设计与替代方案

docs/ir-schema/coreir-schema.md

@@ -21,7 +21,7 @@ Core 编译器使用两种中间表示：
 .cir = 程序的数据流图 + 规约约束
          ↓
 验证工具消费 .cir：
-  1. 编译器已证明的约束（自动推导标签）标注为 ✓
+  1. 编译器已证明的约束（自动推导标签）标注为 
   2. 用户写的约束标注为 pending
   3. 验证工具尝试证明 pending 约束
   4. 输出：每个约束绿/黄/红