diff --git a/.lia.cache b/.lia.cache new file mode 100644 index 0000000..f3a76d1 Binary files /dev/null and b/.lia.cache differ 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 43f0e05..34ac700 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. 解释器局限 @@ -132,6 +132,19 @@ RVSDG 式嵌套 region 已落地（规格 docs/superpowers/specs/2026-08-08-regi - `lexer.cr` 浮点/`..` 范围修复（main 已有）→ 核对 lexer.md 是否已反映 - 完成后需重跑 `python3 tools/pseudocode_check.py` 并更新相应文档的源行数标注 +### 7. 类型双关验证缺口（2026-08-10 记） +- 背景：设计讨论定论——指针模型扩展收敛：**"程序内部地址直接指"（0x 字面量指内部对象）不做**（YAGNI：内部对象用 `&` 取址更优——无漂移/类型全/验证无条件；外部契约地址 unsafe 已够用；0x 字面量仅保留 unsafe 外部入口角色）；**类型双关保留**——图只认字节（pts/offset/alloc_size 全字节级，无类型检查），双关在图层天然合法，验证 = 边界 + 宽度 +- 现状核实（源码）： + - checker EXPR_AS **无类型兼容检查**（checker.cr:2188 仅推断内层 + 返回目标类型）→ `*(float*)&i` 已放行 + - cast 透传（ir_gen.cr:1595 EXPR_AS 返回内层表达式）→ provenance 边不断 + - DEREF 边界检查只查 `off >= alloc_size`（provenance_verify.cr:58-64）→ 越界双关照拦 + - DEREF 节点不携带类型（ir_gen.cr:735 `emit(IR_DEREF, dv, inner_var, 0, 0, 0)`，type_kind=0）→ 访问宽度无从查 + - **asp 无主机制**：checker.cr:404/1451 写入 TYP_PTR 的 asp 标志（unsafe 块内 = 外部地址空间），全仓库无任何消费点——`0x... as *int` 在 safe 代码同样放行，安全语义未落地 +- 待修： + 1. DEREF 宽度检查：`off + width <= alloc_size`（width 从 s1 指针变量的 TYP_PTR 指向类型经 type_size（ir_gen.cr:295）取；DEREF 的 type_kind 是占位 0，需从变量类型推导或改 emit 传真实类型） + 2. asp 机制收尾：完成（asp=1 指针的 DEREF 要求 unsafe 包裹）或删除（当前写入无人消费，是隐患） +- 参考：docs/pointer-model.md（unsafe 边界表已删"类型双关"行 + 新增类型双关节 + 2026-08-10 设计定论） + ## 待实现特性 ### 控制流自动惰性（2026-08-09 记） @@ -165,3 +178,19 @@ RVSDG 式嵌套 region 已落地（规格 docs/superpowers/specs/2026-08-08-regi 6. （后补）ARM64/RISC-V 映射表 - 明确不做（YAGNI）：模拟器/调试器、C 生态兼容、指令级时序验证、特权副作用验证（隔离，人工保证） - 参考：`docs/crasm.md`（正式文档）、`docs/superpowers/specs/2026-08-08-crasm-design.md`（批准记录） + +### 对照 CompCert 审查发现的未修复 bug（2026-08-11 记，详见 docs/compcert-reference.md） + +- **int_str 空字符串 bug**：`int_str(7)` 恒返回空、`int_str(567)` 随编译产物不稳定——打印链问题（预先存在，修复 .ccr s1 64 位后被大数路径暴露）。影响：float 打印精度（`float_str_bits(3.14)` 显示 "3.4"）、大 int 常量打印 +- **字符串拼接 + println 崩溃**：`println("AB" + "CD")` 程序核心转储（预先存在，concat 相关）。影响：check_error 的拼接错误信息不可读 +- **region_check 误报（B11）**：deref 读出的 int 值被当作指针做区域逃逸检查——`v := *p; return v;` 被拦（预先存在，pts 语义需按类型过滤） +- **float 打印精度**：float_str_bits 的舍入为简单实现（第 7 位 ≥5 时第 6 位 +1，无进位传播）——±1ulp 显示误差可接受，但依赖 int_str 修复后重新验证 + +### float 支持实现记录（2026-08-11，对照 IEEE 754 / SysV 标准实现） + +- 字面量：decimal → binary64 位模式（纯整数算法，≤18 位有效数字，±1ulp） +- 算术：addsd/subsd/mulsd/divsd（F2 0F 5x C1）；比较：comisd + setcc 无符号标志 +- 转换：IR_I2F/IR_F2I（cvtsi2sd/cvttsd2si）+ float 运算 int 操作数隐式转换 +- 参数/返回：SysV XMM0-7（int/float 独立编号）+ XMM0 返回 + 栈参数（float 超 8） +- 打印：float_str_bits（位模式 → 十进制，长除 + 去尾零） +- 验证：O0/O1/O2 运行全部通过；待办：float 打印精度（int_str 修复后）、f32 单精度、printf 风格最短表示 diff --git a/coq/.fmt_int.aux b/coq/.fmt_int.aux new file mode 100644 index 0000000..99f6125 --- /dev/null +++ b/coq/.fmt_int.aux @@ -0,0 +1,29 @@ +COQAUX1 8816420a23d81c5ff7d074740c359321 /home/DslsDZC/core/coq/fmt_int.v +0 0 VernacProof "tac:no using:no" +1481 1485 proof_build_time "0.007" +0 0 digits_rev "0.007" +1458 1480 context_used "" +1458 1480 context_used "" +1458 1480 context_used "" +1481 1485 proof_check_time "0.096" +0 0 VernacProof "tac:no using:no" +3281 3285 proof_build_time "0.027" +0 0 parse_rev_digits_rev "0.027" +2765 2799 context_used "" +3281 3285 proof_check_time "0.008" +0 0 VernacProof "tac:no using:no" +3783 3787 proof_build_time "0.005" +0 0 parse_fwd_snoc "0.005" +3770 3782 context_used "" +3783 3787 proof_check_time "0.002" +0 0 VernacProof "tac:no using:no" +3973 3977 proof_build_time "0.008" +0 0 parse_fwd_rev "0.008" +3968 3972 context_used "" +3973 3977 proof_check_time "0.005" +0 0 VernacProof "tac:no using:no" +4534 4538 proof_build_time "0.004" +0 0 roundtrip "0.004" +4479 4506 context_used "" +4534 4538 proof_check_time "0.001" +0 0 vo_compile_time "0.719" diff --git a/coq/fmt_int.glob b/coq/fmt_int.glob new file mode 100644 index 0000000..af9235c --- /dev/null +++ b/coq/fmt_int.glob @@ -0,0 +1,172 @@ +DIGEST 8816420a23d81c5ff7d074740c359321 +Ffmt_int +R1025:1028 Stdlib.Lists.List <> <> lib +R1030:1037 Stdlib.Arith.PeanoNat <> <> lib +R1039:1044 Stdlib.funind.Recdef <> <> lib +R1046:1048 Stdlib.micromega.Lia <> <> lib +R1078:1083 Stdlib.Arith.Wf_nat <> <> lib +R1093:1105 Stdlib.Lists.List ListNotations <> mod +R1273:1275 Corelib.Init.Datatypes <> nat ind +binder 1269:1269 <> n:1 +R1305:1308 Corelib.Init.Datatypes <> list ind +R1310:1312 Corelib.Init.Datatypes <> nat ind +R1325:1325 fmt_int <> n:1 var +R1341:1343 Corelib.Init.Datatypes <> nil constr +R1349:1349 Corelib.Init.Datatypes <> S constr +R1356:1356 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1365:1369 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1358:1362 Stdlib.Arith.PeanoNat <> ::nat_scope:x_'mod'_x not +R1357:1357 fmt_int <> n:1 var +R1370:1379 fmt_int <> digits_rev:2 def +R1383:1385 Stdlib.Arith.PeanoNat <> ::nat_scope:x_'/'_x not +R1382:1382 fmt_int <> n:1 var +binder 1269:1269 <> n:4 +binder 1269:1269 <> n:5 +binder 1269:1269 <> n:7 +R1325:1325 fmt_int <> n:7 var +R1341:1343 Corelib.Init.Datatypes <> nil constr +R1349:1349 Corelib.Init.Datatypes <> S constr +R1356:1356 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1365:1369 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1358:1362 Stdlib.Arith.PeanoNat <> ::nat_scope:x_'mod'_x not +R1357:1357 fmt_int <> n:7 var +R1370:1379 fmt_int <> digits_rev:6 def +R1383:1385 Stdlib.Arith.PeanoNat <> ::nat_scope:x_'/'_x not +R1382:1382 fmt_int <> n:7 var +binder 1269:1269 <> n:9 +binder 1269:1269 <> n:10 +R1325:1325 fmt_int <> n:10 var +R1341:1343 Corelib.Init.Datatypes <> nil constr +R1349:1349 Corelib.Init.Datatypes <> S constr +R1356:1356 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1365:1369 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1358:1362 Stdlib.Arith.PeanoNat <> ::nat_scope:x_'mod'_x not +R1357:1357 fmt_int <> n:10 var +R1370:1379 fmt_int <> digits_rev:6 def +R1383:1385 Stdlib.Arith.PeanoNat <> ::nat_scope:x_'/'_x not +R1382:1382 fmt_int <> n:10 var +binder 1292:1292 <> x:13 +R1297:1297 fmt_int <> x:13 var +R1464:1473 Stdlib.Arith.PeanoNat Nat div_lt def +R1464:1473 Stdlib.Arith.PeanoNat Nat div_lt def +def 1596:1604 <> parse_fwd +R1613:1615 Corelib.Init.Datatypes <> nat ind +binder 1607:1609 <> acc:22 +R1624:1627 Corelib.Init.Datatypes <> list ind +R1629:1631 Corelib.Init.Datatypes <> nat ind +binder 1619:1620 <> ds:23 +R1636:1638 Corelib.Init.Datatypes <> nat ind +R1651:1652 fmt_int <> ds:23 var +R1663:1665 Corelib.Init.Datatypes <> nil constr +R1670:1672 fmt_int <> acc:22 var +R1679:1682 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1691:1699 fmt_int <> parse_fwd:24 def +R1710:1712 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not +R1705:1707 Corelib.Init.Peano <> ::nat_scope:x_'*'_x not +R1702:1704 fmt_int <> acc:22 var +def 1820:1828 <> parse_rev +R1836:1839 Corelib.Init.Datatypes <> list ind +R1841:1843 Corelib.Init.Datatypes <> nat ind +binder 1831:1832 <> ds:26 +R1848:1850 Corelib.Init.Datatypes <> nat ind +R1863:1864 fmt_int <> ds:26 var +R1875:1877 Corelib.Init.Datatypes <> nil constr +R1889:1892 Corelib.Init.Datatypes <> ::list_scope:x_'::'_x not +R1902:1904 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not +R1907:1909 Corelib.Init.Peano <> ::nat_scope:x_'*'_x not +R1910:1918 fmt_int <> parse_rev:27 def +def 2010:2015 <> digits +R2022:2024 Corelib.Init.Datatypes <> nat ind +binder 2018:2018 <> n:29 +R2029:2032 Corelib.Init.Datatypes <> list ind +R2034:2036 Corelib.Init.Datatypes <> nat ind +R2049:2049 fmt_int <> n:29 var +R2065:2065 Stdlib.Lists.List ListNotations ::list_scope:'['_x_']' not +R2067:2067 Stdlib.Lists.List ListNotations ::list_scope:'['_x_']' not +R2078:2080 Stdlib.Lists.List <> rev def +R2083:2092 fmt_int <> digits_rev thm +R2094:2094 fmt_int <> n:29 var +prf 2431:2450 <> parse_rev_digits_rev +R2465:2467 Corelib.Init.Datatypes <> nat ind +binder 2461:2461 <> n:31 +R2494:2496 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R2470:2478 fmt_int <> parse_rev def +R2481:2490 fmt_int <> digits_rev thm +R2492:2492 fmt_int <> n:31 var +R2497:2497 fmt_int <> n:31 var +R2538:2546 Stdlib.Arith.Wf_nat <> lt_wf_ind thm +R2538:2546 Stdlib.Arith.Wf_nat <> lt_wf_ind thm +R2585:2603 fmt_int <> digits_rev_equation def +R2585:2603 fmt_int <> digits_rev_equation def +R2585:2603 fmt_int <> digits_rev_equation def +R2733:2751 fmt_int <> digits_rev_equation def +R2754:2754 Corelib.Init.Datatypes <> S constr +R2733:2751 fmt_int <> digits_rev_equation def +R2754:2754 Corelib.Init.Datatypes <> S constr +R2733:2751 fmt_int <> digits_rev_equation def +R2754:2754 Corelib.Init.Datatypes <> S constr +R2772:2778 Stdlib.Arith.PeanoNat Nat div def +R2780:2789 Stdlib.Arith.PeanoNat Nat modulo def +R2791:2797 Stdlib.Arith.PeanoNat Nat mul def +R3007:3016 Stdlib.Arith.PeanoNat Nat div_lt def +R3007:3016 Stdlib.Arith.PeanoNat Nat div_lt def +R3238:3248 Stdlib.Arith.PeanoNat Nat div_mod thm +R3251:3251 Corelib.Init.Datatypes <> S constr +R3238:3248 Stdlib.Arith.PeanoNat Nat div_mod thm +R3251:3251 Corelib.Init.Datatypes <> S constr +R3238:3248 Stdlib.Arith.PeanoNat Nat div_mod thm +R3251:3251 Corelib.Init.Datatypes <> S constr +R3238:3248 Stdlib.Arith.PeanoNat Nat div_mod thm +R3251:3251 Corelib.Init.Datatypes <> S constr +R2772:2778 Stdlib.Arith.PeanoNat Nat div def +R2780:2789 Stdlib.Arith.PeanoNat Nat modulo def +R2791:2797 Stdlib.Arith.PeanoNat Nat mul def +prf 3546:3559 <> parse_fwd_snoc +R3577:3579 Corelib.Init.Datatypes <> nat ind +binder 3571:3573 <> acc:32 +R3587:3590 Corelib.Init.Datatypes <> list ind +R3592:3594 Corelib.Init.Datatypes <> nat ind +binder 3583:3583 <> l:33 +R3602:3604 Corelib.Init.Datatypes <> nat ind +binder 3598:3598 <> x:34 +R3634:3636 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R3610:3618 fmt_int <> parse_fwd def +R3620:3622 fmt_int <> acc:32 var +R3626:3629 Corelib.Init.Datatypes <> ::list_scope:x_'++'_x not +R3625:3625 fmt_int <> l:33 var +R3630:3630 Stdlib.Lists.List ListNotations ::list_scope:'['_x_']' not +R3632:3632 Stdlib.Lists.List ListNotations ::list_scope:'['_x_']' not +R3631:3631 fmt_int <> x:34 var +R3657:3659 Corelib.Init.Peano <> ::nat_scope:x_'+'_x not +R3652:3654 Corelib.Init.Peano <> ::nat_scope:x_'*'_x not +R3637:3645 fmt_int <> parse_fwd def +R3647:3649 fmt_int <> acc:32 var +R3651:3651 fmt_int <> l:33 var +R3660:3660 fmt_int <> x:34 var +prf 3795:3807 <> parse_fwd_rev +R3822:3825 Corelib.Init.Datatypes <> list ind +R3827:3829 Corelib.Init.Datatypes <> nat ind +binder 3818:3818 <> l:35 +R3851:3853 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R3832:3840 fmt_int <> parse_fwd def +R3845:3847 Stdlib.Lists.List <> rev def +R3849:3849 fmt_int <> l:35 var +R3854:3862 fmt_int <> parse_rev def +R3864:3864 fmt_int <> l:35 var +R3940:3953 fmt_int <> parse_fwd_snoc thm +R3940:3953 fmt_int <> parse_fwd_snoc thm +R3940:3953 fmt_int <> parse_fwd_snoc thm +prf 4212:4220 <> roundtrip +R4235:4237 Corelib.Init.Datatypes <> nat ind +binder 4231:4231 <> n:36 +R4262:4264 Corelib.Init.Logic <> ::type_scope:x_'='_x not +R4240:4248 fmt_int <> parse_fwd def +R4253:4258 fmt_int <> digits def +R4260:4260 fmt_int <> n:36 var +R4265:4265 fmt_int <> n:36 var +R4296:4301 fmt_int <> digits def +R4413:4425 fmt_int <> parse_fwd_rev thm +R4413:4425 fmt_int <> parse_fwd_rev thm +R4413:4425 fmt_int <> parse_fwd_rev thm +R4485:4504 fmt_int <> parse_rev_digits_rev thm +R4485:4504 fmt_int <> parse_rev_digits_rev thm diff --git a/coq/fmt_int.v b/coq/fmt_int.v new file mode 100644 index 0000000..adf2584 --- /dev/null +++ b/coq/fmt_int.v @@ -0,0 +1,115 @@ +(* ===================================================================== + fmt_int.v — 用 Coq (Rocq) 验证 Core stdlib 的 int_str ↔ str_int 互逆 + + 源码: src/stdlib/fmt.cr:96 (int_str), src/stdlib/fmt.cr:134 (str_int) + 文档: docs/coq/README.md + + 建模约定 (见 docs/coq/README.md 第①步): + - string 建模为 list nat (digits 0..9), 消去 alloc/load8/store8/header + - ASCII +48/-48 消去 (验证算法语义, 不是字符编码) + - int 建模为 nat (非负情形; 负数/溢出留待后续) + + 翻译对照: + - int_str 循环1 (数位数, 决定 buffer 大小) → 消去 (list 自动增长) + - int_str 循环2 (从高位往低位填位) → digits_rev (低位在前递归) + - str_int 主循环 (res = res*10 + d) → parse_fwd (累加器递归) + + 验证目标: + Theorem roundtrip : forall n, parse_fwd 0 (digits n) = n. + (对任意非负整数 n: str_int(int_str(n)) == n) + ===================================================================== *) + +From Stdlib Require Import List PeanoNat Recdef Lia. +From Stdlib Require Import Wf_nat. +Import ListNotations. + +(* ---- int_str 循环2 的翻译: 逆序 digits (低位在前) ---- + 除法递归, 结构上不递减, 需 measure + 终止性证明 *) +Function digits_rev (n : nat) {measure (fun x => x) n} : list nat := + match n with + | 0 => nil + | S _ => (n mod 10) :: digits_rev (n / 10) + end. +(* 终止性义务: n/10 < n (n ≠ 0) *) +Proof. + intros. + apply Nat.div_lt; lia. +Qed. + +(* ---- str_int 的翻译: 从左往右解析 (累加器递归, 结构递减, 直接通过) ---- *) +Fixpoint parse_fwd (acc : nat) (ds : list nat) : nat := + match ds with + | nil => acc + | d :: rest => parse_fwd (acc * 10 + d) rest + end. + +(* ---- 逆序解析: 对应 digits_rev 的逆序列表 (低位系数小) ---- *) +Fixpoint parse_rev (ds : list nat) : nat := + match ds with + | nil => 0 + | d :: rest => d + 10 * parse_rev rest + end. + +(* ---- int_str 的输出: 正序 digits (n=0 特例 "0") ---- *) +Definition digits (n : nat) : list nat := + match n with + | 0 => [0] + | _ => rev (digits_rev n) + end. + +(* ===================================================================== + 引理① (核心): 逆序 digits 解析回来等于原数 + parse_rev (digits_rev n) = n + 证明: 良基归纳 (m < n 的假设), 关键步用 Nat.div_mod 展开 n + ===================================================================== *) +Lemma parse_rev_digits_rev : forall n : nat, parse_rev (digits_rev n) = n. +Proof. + induction n as [n IHn] using lt_wf_ind. + destruct n as [| m]. + - rewrite (digits_rev_equation 0). simpl. reflexivity. + - (* 用 equation 引理精确展开 digits_rev (S m)，避免 simpl 展开 wf 包装 *) + rewrite (digits_rev_equation (S m)). + Opaque Nat.div Nat.modulo Nat.mul. (* 锁住 div/mod/mul，保持文字形态 *) + simpl. + (* parse_rev ((S m) mod 10 :: digits_rev ((S m)/10)) + = (S m) mod 10 + 10 * parse_rev (digits_rev ((S m)/10)) *) + rewrite IHn; [| apply Nat.div_lt; lia]. + (* 目标: (S m) mod 10 + 10 * ((S m)/10) = S m + 由 Nat.div_mod: S m = 10 * (S m / 10) + S m mod 10 *) + symmetry. + (* at 1: 只替换最外层的 S m，不动 mod/div 参数里的 *) + rewrite (Nat.div_mod (S m) 10) at 1; [ lia | lia ]. +Qed. + +(* ===================================================================== + 引理② (桥): 正序解析 = 逆序解析 + 先证 append 一步的展开, 再用它推全列表 + ===================================================================== *) +Lemma parse_fwd_snoc : forall (acc : nat) (l : list nat) (x : nat), + parse_fwd acc (l ++ [x]) = parse_fwd acc l * 10 + x. +Proof. + intros acc l x. + induction l as [| y l' IH] in acc |- *; simpl. + - reflexivity. + - rewrite IH. reflexivity. +Qed. + +Lemma parse_fwd_rev : forall l : list nat, parse_fwd 0 (rev l) = parse_rev l. +Proof. + induction l as [| x l' IH]; simpl. + - reflexivity. + - rewrite parse_fwd_snoc. rewrite IH. lia. +Qed. + +(* ===================================================================== + 主定理: 对任意自然数 n, 先转 digits 再解析回来, 等于 n + ===================================================================== *) +Theorem roundtrip : forall n : nat, parse_fwd 0 (digits n) = n. +Proof. + intros n. + unfold digits. + destruct n as [| n']. + - simpl. reflexivity. (* n = 0: parse_fwd 0 [0] = 0 *) + - rewrite parse_fwd_rev. (* 正序解析 = 逆序解析 *) + apply parse_rev_digits_rev. (* 核心引理 *) +Qed. diff --git a/coq/fmt_int.vo b/coq/fmt_int.vo new file mode 100644 index 0000000..a78a8db Binary files /dev/null and b/coq/fmt_int.vo differ diff --git a/coq/fmt_int.vok b/coq/fmt_int.vok new file mode 100644 index 0000000..e69de29 diff --git a/coq/fmt_int.vos b/coq/fmt_int.vos new file mode 100644 index 0000000..e69de29 diff --git a/docs/compcert-reference.md b/docs/compcert-reference.md new file mode 100644 index 0000000..69adb05 --- /dev/null +++ b/docs/compcert-reference.md @@ -0,0 +1,139 @@ +# CompCert 后端对照参考（形式化验证过的 C 编译器） + +> CompCert：世界上唯一被形式化验证过的 C 编译器（INRIA，Leroy 团队）。 +> 整个后端用 Coq 编写并被 Coq 证明正确——学习"验证过的后端"如何写、如何证的唯一教材。 +> 本文件是对照 Core 后端的阅读地图。 + +## 获取源码 + +网络恢复后执行 `bash ~/get-compcert.sh`（自动尝试 GitHub / INRIA GitLab / 代理）。 +或者手动下载 `https://github.com/AbsInt/CompCert/archive/refs/tags/v3.17.tar.gz`。 + +许可证：GPL v2（研究使用无问题）。 + +## 目录地图（v3.17 解压后，2026-08-11 已下载到 ~/compcert/） + +``` +compcert/ +├── backend/ ← 后端核心（Coq 源码 + 证明并排） +│ ├── RTL.v ← 3 地址中间表示（CFG，接近 Core 的 .cir 数据流图） +│ ├── Allocation.v ← 寄存器分配（图着色） +│ ├── Allocproof.v ← 分配正确性证明（最著名的证明之一） +│ ├── Linearize.v ← CFG → 线性指令序列 +│ ├── Linearizeproof.v ← 线性化正确性证明 +│ └── Mach.v ← 机器抽象层 +└── x86/ ← x86 目标（3.17 已合并 x86_32/64） + ├── Asm.v ← 每条指令的精确语义模型 + ├── Asmgen.v ← 指令生成（Mach → Asm） + ├── Asmgenproof.v + Asmgenproof1.v ← 生成正确性证明 + ├── Op.v ← 操作语义（运算的数学定义） + ├── Machregs.v ← 寄存器定义 + └── TargetPrinter.ml ← 汇编文本打印（对应 Core 的 ELF 编码） +``` + +> 注：3.17 版本中 `backend/Asm.v`、`backend/Asmgen.v` 不存在——Asm/Asmgen 在目标目录 `x86/` 下；`Architecture.v` 也不存在（由 Machregs.v/Conventions1.v/Stacklayout.v 承担）。 + +## 与 Core 后端的对照表（v3.17 实际路径） + +| CompCert 文件 | 内容 | 对照 Core 的 | +|---|---|---| +| `backend/RTL.v` | 3 地址 IR | `src/compiler/dataflow.cr`（数据流图） | +| `backend/Allocation.v` + `Allocproof.v` | 寄存器分配 + 正确性证明 | `src/compiler/opt.cr`（寄存器分配器） | +| `backend/Linearize.v` | 图 → 线性序列 | `src/compiler/ccr_io.cr` 的线性 CFG | +| `x86/Asm.v` | 每条机器指令的语义模型 | `src/arch/linux/ld/instr.cr`（指令编码） | +| `x86/Asmgen.v` + `Asmgenproof.v` | 指令生成 + 生成正确性 | `corearch.cr` 的发射逻辑 | +| `x86/TargetPrinter.ml` | 汇编文本打印 | `src/arch/linux/ld/elf.cr`（ELF 输出） | +| `arm/Asm.v` / `aarch64/Asm.v` / `riscV/Asm.v` | 各目标指令定义 | `bootstrap/corec/backend/arm64_asm.py` | + +## 两个最值得先看的点 + +1. **`backend/Allocproof.v` 的证明结构**——回答"寄存器分配正确性到底意味着什么"： + 分配前程序与分配后程序在**什么等价关系**下行为一致（模拟关系 + 良基归纳）。 + 这正是 `opt.cr` 缺的那层论证。 + +2. **`backend/Asm.v` 的指令语义**——CompCert 正确性的地基：每条指令先有精确语义 + （作为数学对象定义，而不是字符串/字节），才有正确性可言。 + Core 的 `instr.cr` 目前只有编码没有语义——差距就在这里。 + +## 与 Core 的关键差异 + +- CompCert 生成汇编文本交外部 `as`/`ld`；Core 自己发射 ELF（`src/arch/linux/ld/`） + ——ELF 输出是 Core 独有、CompCert 没有对照的部分 +- CompCert 不验证前端（Clight 语法解析）；它的验证从语义化的中间语言开始 +- CompCert 用 pass 分阶段 + 每阶段一个证明；Core 是单趟管线（架构哲学不同，对照时注意） + +## 审查发现与修复记录（2026-08-11） + +对照 CompCert 审查 Core 后端 + 指针分析链，发现并修复 6 个连锁 bug（安全关键）： + +### 已修复（越界检查绕过链——5 个 bug 连锁，单独每个都不生效） + +| # | 位置 | Bug | 修复 | +|---|---|---|---| +| 1 | `ptr_analysis.cr` IR_ADDR_INDEX | `&arr[i]` 运行时索引的 offset 无条件传播为数组 offset（0），provenance 误判"编译期安全"→ 越界裸读 | 索引常量可精确算（idx×8），运行时索引 → offset=-1（迫使运行时检查） | +| 2 | `instr.cr` IR_DEREF s3≠0 | ud2 写 `buf[cp]`（应为 `buf[pos+cp]`，污染函数头）；jae 越界跳 .safe（不崩溃）；jne 多 +2 跳指令中间 | 三处编码修正 | +| 3 | `ptr_analysis.cr` alloc 分支 + `get_alloc_size` | 所有 alloc 的 pts 恒设 bit 0（无 alloc 序号）；`get_alloc_size(bi)` 把位号当 DF 节点序号查节点 0 → 恒 -1 → 运行时检查**从设计上不可达** | 新增 `g_pa_alloc_count`/`g_pa_alloc_nodes` 映射表（alloc_seq → 节点序号），get_alloc_size 查表 + 修正 IR_ALLOC_ARRAY size（s1×8 非 s1×s2） | +| 4 | `ptr_analysis.cr` LOAD/STORE 传播 | STORE 传播混进 LOAD 分支（用 dest d，而 IR_STORE 的 d 恒 -1）→ 永不执行 → `p = &arr[i]` 的 offset 传播链断 | STORE 分支独立（s1 ← s2），移到 `if d >= 0` 块外 | +| 5 | `main.cr` build 流程 | provenance 的诊断只记录不拦截，编译期确定的越界照常生成二进制 | build 流程检查新增诊断数 → 打印 + return 1 | +| 6 | `region_check.cr`（3 处） | `alloc_seq := bi + nstart`（位号+函数起点）——修复 3 后位号是全局 alloc 序号，语义错位 → B11 误报 | 查 `g_pa_alloc_nodes` 映射表 | + +验证：常量越界（`&arr[100]`）编译期拦截 ✓；运行时索引越界生成 `and $0xfff` + `cmp` + `jae→ud2` + `test` + `jne→.safe` 检查序列（objdump 确认跳转精确）✓。 + +### 第二轮审查（栈布局/调用约定，任务 2）新增修复 + +| # | 位置 | Bug | 修复 | +|---|---|---|---| +| 8 | `elf.cr` emit_alloc_body 全局 bump 路径 jbe | jbe 偏移 +14 漏了 `mov rdi,r9`（3 字节）→ 跳到指令中间 → 死循环（**所有无 arena 的堆分配程序挂起**） | jbe 改为 +17 | +| 11 | `elf.cr` 栈帧大小（dry run + 实际两处） | `size = vc*8` 未按 SysV 16 字节对齐：opt≥1 时需 ≡8 (mod 16)（6 个 push 后 rsp%16=8），vc 偶数时未对齐 → 调用点 rsp 未 16 对齐（FFI/外部调用会崩） | 对齐规则：opt≥1 → %16==8；opt<1 → %16==0 | +| 12 | `ptr_analysis.cr` alloc 分支 + `get_alloc_size` | `IR_ALLOC`（标量变量槽标记，不发射代码）被当作堆分配参与 pts 追踪 → `p = &arr[i]` 的 pts 含多个位（污染）→ s3 取错 alloc（标量 8 而非数组 40）→ 正常程序被误杀 | 只追踪 IR_ALLOC_STRUCT/IR_ALLOC_ARRAY | + +验证（干净构建）：正常索引 `v=30` exit 0 ✓；越界索引 exit 132（SIGILL）✓；常量越界编译期拦截 ✓。 + +### 未修复（预先存在，另行处理） + +| # | 现象 | 影响 | +|---|---|---| +| 7 | 字符串拼接 + println 崩溃/挂起（`"AB"+"CD"`） | 自举产物坏代码；check_error 的错误 msg 因此为空 | +| 9 | 数组读取值错位（ptr_arith 的 `*p != 30`——旧工具链产物） | 数组布局/header 问题（新工具链下正常程序已通过，待复核） | +| 10 | region_check B11 对 deref 读出的 int 误报指针逃逸 | 部分合法程序被拦（region_check 的 pts 语义需按类型过滤） | +| 13 | ~~float 类型是壳~~ **已实现（2026-08-11）**：字面量（IEEE 754 位模式，±1ulp）+ 算术（addsd/subsd/mulsd/divsd）+ 比较（comisd+setcc），运行时验证通过 | 待续：int↔float 转换、XMM 参数传递、float 打印 | +| 14 | `.ccr` 序列化 s1 用 32 位（buf_write_i32）——大 int 常量 / float 位模式 > 2^31 被截断（静默损坏） | 修复：s1 改 64 位（写/读/尺寸同步） | +| 15 | `buf_read_i64` 缺 `h3 < 128` 的 else 分支——高位字节（bit 56-62）贡献丢失（0x4009... → 0x0009...） | 修复：补 else 分支 | +| 16 | `int_str` 对部分值返回空字符串（int_str(7) 恒空、int_str(567) 编译相关不稳定）——打印链 bug（预先存在，大数路径暴露） | 未修——影响 float 打印的精度显示（3.14 → "3.4"）；单独处理 | + +## float 支持实现记录（阶段 4-6，2026-08-11） + +| 阶段 | 内容 | 验证 | +|---|---|---| +| 4 | int↔float 转换：IR_I2F/IR_F2I + cvtsi2sd（F2 0F 2A）/cvttsd2si（F2 48 0F 2C）；ir_gen float 运算中 int 操作数隐式转换 | `3.14 + 2`（int 2 隐式转）> 5.0 → exit 0 ✓ | +| 5 | XMM 参数传递（SysV：int 用 ir 0-5 → rdi..r9，float 用 fr 0-7 → xmm0-7，独立编号）+ float 返回（xmm0）+ 栈参数（float 超 8 用 sub+movsd） | `add_f(1.5, 2.5)` = 4.0 > 3.9 → exit 0 ✓ | +| 6 | float 打印：`float_str_bits`（位模式 → 十进制，长除小数提取 + 去尾零 + 简单舍入） | 2.0→"2"、0.5→"0.5"、6.5→"6.5"、-1.0→"-1" ✓；3.14→"3.4"（int_str bug 干扰，见发现 16） | + +## 寄存器分配对照结论（任务 3，2026-08-11） + +对照 CompCert `backend/Allocation.v` + `Allocproof.v`（图着色 + 溢出 + 模拟关系证明）审查 `opt.cr` 的 `alloc_registers`（线性扫描）： + +| 对照点 | CompCert | Core | 结论 | +|---|---|---|---| +| 分配算法 | 冲突图着色（干涉图）+ 溢出 | 线性扫描：活跃区间 [first,last]，每变量独占寄存器、**从不重用** | ⚠️ 保守正确但浪费（5 寄存器后全栈） | +| 正确性条件 | 着色无冲突 + 模拟关系证明 | 变量独占寄存器 → 无冲突（隐式满足） | ✅ 正确 | +| 活跃性 | 精确 liveness（控制流敏感） | 线性区间近似（保守） | ✅ 正确（保守） | +| 跨调用存活 | caller/callee-saved 混合 | 只用 callee-saved（rbx,r12-15，prologue push/epilogue pop） | ✅ 正确（简化但有效） | +| 溢出 | 图着色溢出到栈 | 无溢出——超 5 变量全栈 | ⚠️ 性能差距 | + +**O2 运行验证**（首次验证，全部通过）：简单运算（42 ✓）、跨函数调用（callee-saved 保护，30 ✓）、循环（45 ✓）、指针 deref（✓）、越界 SIGILL（132 ✓）。 + +**未发现正确性 bug**——差距在优化能力（寄存器重用/溢出/精确活跃性），非正确性。 + +## 调用约定对照结论（任务 2 完整版） + +| 约定点 | CompCert（SysV） | Core | 结论 | +|---|---|---|---| +| 整数参数寄存器 | DI,SI,DX,CX,R8,R9 | rdi,rsi,rdx,rcx,r8,r9 | ✅ 一致 | +| callee-saved | rbx,rbp,r12-r15 | 同 | ✅ 一致 | +| 栈参数（第 7+ 个） | S Outgoing，调用点 [rsp+0..] | push r10（右到左）+ add rsp 清理 | ✅ 一致 | +| 栈帧 16 字节对齐 | frame_env_aligned 证明 | 修复 11 前未对齐 | ✅ 已修 | +| 返回值 | rax（128 位用 rdx:rax） | rax（无 128 位类型） | ✅ 一致 | +| varargs | 调用点 AL = XMM 参数数 | 不设 AL（无 float → AL 无意义） | ✅ 无 float 时正确 | +| outgoing 区域 | 固定帧内区域 | push/add 临时区 | ✅ 功能等价 | +| float 参数 | XMM0-7 | 无 SSE 实现（发现 13） | ❌ 类型壳 | 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/coq/README.md b/docs/coq/README.md new file mode 100644 index 0000000..ecc79a3 --- /dev/null +++ b/docs/coq/README.md @@ -0,0 +1,101 @@ +# 用 Coq 验证 Core stdlib 纯函数 + +> 目标：用 Coq（Rocq）做**程序验证**——验证 Core 系统里**几乎永远不会改**的部分（stdlib 纯函数）。 +> 注意：这不是规约系统（`.corespec` / 翻译桥那套基础设施），是直接用 Coq 验证程序本身的性质。 + +## 为什么选 stdlib 纯函数 + +- **几乎永不变**：`int_str`（数字→字符串）、`str_eq` 等是语言无关的经典算法，语言怎么演进都不变。验证是长期投入，选会变动的代码证明就过时了。 +- **纯函数**：无副作用，语义干净，Coq 里建模没有状态/内存干扰。 +- **规模适中**：每个函数几十行，翻译 + 证明一晚上一个闭环。 + +## 第一刀目标：`int_str` ↔ `str_int` 互逆 + +源码：`src/stdlib/fmt.cr:96`（int_str）、`src/stdlib/fmt.cr:134`（str_int）。 + +**要证明的性质（非负情形）**： + +``` +对任意非负整数 n：str_int(int_str(n)) == n +``` + +即：数字转成字符串，再解析回来，等于原数。这是 fmt.cr 的灵魂性质（数字转换正确性）。 + +## 验证工作流（5 步） + +``` +① 建模约定 Core 程序怎么"翻译"进 Coq 世界（抽象哪些、保留哪些） +② 翻译 int_str 循环 → 递归（核心技能） +③ 声明性质 互逆定理长什么样 +④ 证明 归纳 + div/mod 引理 +⑤ 验证 coqc 编译通过 = 证明成立 +``` + +--- + +## 第 ① 步：建模约定（已完成） + +**关键概念：验证不是逐行翻译代码，而是用 Coq 的语言重新表达同一个算法语义。** 要回答的问题："int_str 的语义是什么？"——不是"它怎么操作内存"，而是"它把一个数字变成了什么"。 + +对照 `fmt.cr:96` 的 int_str，逐项消去： + +| Core 里的东西 | 为什么能消去 | Coq 里的表达 | +|---|---|---| +| `alloc(n)` / `load8` / `store8` | 内存布局是实现细节，语义 = "产生一个字符串" | `list`（字符串就是字符列表） | +| 字符串 header（`str_len` 读 -8 偏移） | 长度已内建在 list 里 | `length` | +| `+ 48` / `- 48`（ASCII 转换） | 字符编码是实现细节，语义 = "数字的十进制位" | 数字 `0..9` | +| `int`（64 位机器整数） | **先只验证非负情形**，负数/溢出留到后面 | `nat` | + +**消去后 int_str 的算法语义**： + +``` +int_str(n) = n 的十进制 digits 序列 + 比如 int_str(123) = [1, 2, 3] +``` + +**str_int 的语义**（`fmt.cr:134`）： + +``` +str_int(s) = 从左往右读 digits，每读一位 res = res*10 + d + [1,2,3] → ((0*10+1)*10+2)*10+3 = 123 +``` + +**待确认点**：int_str 里有两个循环（数位数的循环 + 填位的循环）——翻译成 Coq 时两个循环会合体成一个递归函数。 + +## 进度 + +- [x] 第①步 建模约定 +- [x] 第②步 翻译 int_str（循环 → 递归） +- [x] 第③步 声明性质 +- [x] 第④步 证明 +- [x] 第⑤步 coqc 验证 —— **2026-08-11 编译通过** + +## 成果 + +- **证明文件**：`coq/fmt_int.v`（编译命令：`coqc coq/fmt_int.v`） +- **主定理**：`roundtrip : forall n : nat, parse_fwd 0 (digits n) = n` —— 即 `str_int(int_str(n)) == n`（非负情形） +- **引理**： + - `parse_rev_digits_rev` — 核心引理：逆序 digits 解析回来等于原数（良基归纳 + div_mod） + - `parse_fwd_snoc` / `parse_fwd_rev` — 桥引理：正序解析 = 逆序解析 + - 终止性义务：`n/10 < n`（Function measure 证明） + +## 过程中踩的坑（Rocq 9.1 实测） + +1. **除法递归不被 Fixpoint 接受**（guard condition）——`n / 10` 不是结构子项，需 `Function` + measure +2. **`Function f (n : nat) {measure n}` 语法在 Rocq 9.1 坏了**——报 "Illegal application: n cannot be applied to n"；须写 `{measure (fun x => x) n}` +3. **`simpl` 会展开 wf 包装 / divmod / 乘法**——`Function` 定义展开带证明项，`mod`/`div` 内部是 `divmod` fix，`10 * x` 展开成加法链。解法：`Opaque Nat.div Nat.modulo Nat.mul` + 用 `digits_rev_equation` 精确展开 +4. **`rewrite` 替换所有匹配**——`rewrite (Nat.div_mod (S m) 10) at 1` 限定只替换最外层 +5. **归纳需要泛化累加器**——`induction l in acc |- *`，否则 IH 里的 acc 与目标不匹配 + +## 下一步候选 + +- `int_str` 负数分支（neg 处理，用 Z） +- 溢出语义（64 位机器整数，用 bitvector 或 mod 2^64） +- `concat` 正确性（`str_len(concat a b) = str_len a + str_len b`） +- `str_eq` 等价关系 +- `collections.sum` / `reverse`（`rev (rev l) = l`） + +## 环境 + +- Rocq Prover 9.1.1（opam，`~/.opam/default/bin/coqc`） +- 无 coqide，用命令行 coqc 编译 + 编辑器 diff --git a/docs/crasm.md b/docs/crasm.md index c099efe..f44f5ea 100644 --- a/docs/crasm.md +++ b/docs/crasm.md @@ -77,13 +77,15 @@ extern fn port_read(addr: u64) fn port_read(addr: u64) -> u8 { ### 特权指令固定集 特权指令是**标准手册定义的有限固定集**（几十条）——固定 = 约束有限 = 可形式化 = 可验证。 +标准硬件布局同理：标准手册定义的寄存器/MMIO 区域也是固定集 → 可建表验证（见下文硬件描述表）。 ## 示例 ```crasm unsafe fn port_write(addr: u64, val: u8) { // 用法验证：addr 必须 64 位、val 必须 8 位（与 MMIO 寄存器宽度匹配） - // 副作用隔离：写入后的硬件行为由人工保证 + // 硬件表验证：addr 落在标准/厂商表声明区域 → 自动（归属/宽度/对齐） + // 表外隔离：仅表外硬件行为与动态时序由人工保证 mmio_write(addr, val); } ``` @@ -95,7 +97,7 @@ unsafe fn port_write(addr: u64, val: u8) { | 级 | 指令 | 验证策略 | |---|---|---| | 普通级 | 数据传输/算术/分支/内存操作/地址计算 | **自动验证**：寄存器生命周期 + 地址 provenance/边界（复用现有指针模型 pass）——"绝大多数可验证" | -| 特权级 | mmio/barrier/irq/swap_context/halt | **用法验证**（自动）：参数类型/宽度、放置规则、指令间约束（固定集 → 可形式化）；**副作用隔离**（unsafe 边界）：硬件行为/时序超出编译期验证范围，人工保证 | +| 特权级 | mmio/barrier/irq/swap_context/halt | **用法验证**（自动）：参数类型/宽度、放置规则、指令间约束（固定集 → 可形式化）；**硬件表验证**（自动）：地址落在标准/厂商表声明区域、寄存器宽度匹配；**表外隔离**（unsafe 边界）：表外硬件行为与动态时序人工保证 | ### 寄存器生命周期规则（新 pass，.crasm 专用） @@ -107,12 +109,29 @@ unsafe fn port_write(addr: u64, val: u8) { | 宽度一致 | 运算操作数宽度匹配（8/16/32/64） | `%0(8bit) := %1(64bit) + 1` | | 分支一致性 | goto 目标存在；if 条件是条件寄存器 | `if %0 == 0 goto missing` | +### 硬件描述表：标准部分自动验证 + +"硬件有的地方是标准的，也是可以验证的"——特权访问的验证对象分三层： + +| 层 | 覆盖 | 验证依据 | +|---|---|---| +| 标准表 | 公开标准硬件：UART 16550、x86 APIC/IOAPIC、PCIe ECAM、CMOS RTC | 标准手册 → 形式化表（地址范围、寄存器宽度、读写语义） | +| 厂商表 | SoC 外设：GPIO、SPI 控制器等 | 厂商手册 → 与标准表同构的形式化描述 | +| 表外 | 自定义 FPGA 逻辑、非标准设备 | unsafe 入口标注一次，人工保证 | + +mmio_read/write 的地址落在表内 → 编译器自动验证区域归属、寄存器宽度匹配、对齐合法。 +这与指针模型同构：unsafe 标注的是"图边界入口"（外部地址、FFI 返回），进入图内编译器 +重新获得追踪权——硬件表让标准部分拿回自动验证，unsafe 只承担表外入口。 + +无论硬件多标准，**动态行为**（时序、中断延迟、握手时序）都超出编译期验证范围， +始终位于表外，人工保证。 + ### 与现有验证的关系 - 寄存器规则：新 pass（`.crasm` 专用——虚拟寄存器是抽象层概念） - 地址/内存验证：复用 PointerAnalysis / RegionCheck / ProvenanceVerify （`.crasm` 的 `load [addr]` 转成与 IR 相同的 provenance 检查） -- 特权用法验证：固定指令集约束表（参数宽度/放置规则），pass 检查 +- 特权用法验证：固定指令集约束表（参数宽度/放置规则）+ 硬件描述表（区域/宽度/对齐），pass 检查 - 错误报告：走新错误码体系（验证类，挂错误码规格类别表，实现时定归属） ## 交互接口 @@ -172,8 +191,8 @@ x86 mov / arm ldr）——映射正确性由固定表保证。 - 模拟器/调试器支持 - .crasm 的 C 生态兼容（新生态无义务） -- 指令级时序验证（超出编译期验证范围） -- 特权指令副作用验证（隔离，人工保证） +- 指令级时序验证（动态行为无论硬件多标准都超出编译期验证范围） +- 表外硬件行为验证（unsafe 隔离，人工保证——表内标准部分仍自动验证） ## 当前状态 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/pointer-model.md b/docs/pointer-model.md index c5c8f7d..e15818a 100644 --- a/docs/pointer-model.md +++ b/docs/pointer-model.md @@ -185,7 +185,18 @@ fail → panic | 外部硬件地址 | `0x7fff0000 as *int` 没有 ALLOC 节点 | | FFI 返回值 | 外部函数返回的指针没有 Core 的 provenance | | inline assembly | 汇编的输出指针没有来源 | -| `unsafe` 类型双关 | 违反类型系统假设，编译器无法推导 | + +### 类型双关 + +`*(float*)&i` **不需要 unsafe**。图的内存模型是"字节序列 + 宽度 + 边界"——provenance +（alloc 归属）、offset（字节偏移）、alloc_size（字节大小）全部与类型无关，类型只是 +DEREF 处的"视图"。cast 在图里无节点（ir_gen 透传），provenance 边不断： + +- 双关合法判据 = 边界 + 宽度：`offset ∈ [0, alloc_size)` 且访问宽度不超出分配 +- 越界双关由现有 DEREF 边界检查拦截 +- 宽度检查（`off + width <= alloc_size`）待补，见 TODO 预存 bug 7 +- 编译器内部 `asp`（外部地址空间）标志在 checker 写入 TYP_PTR 但全仓库无消费点—— + `0x... as *int` 在 safe 代码同样放行，归属待定，见 TODO 预存 bug 7 `unsafe` 块内部的指针操作仍然被三点 pass 追踪。`unsafe` 不是"关掉验证"——是"标注图边界入口"。一旦进入 safe 代码，编译器重新获得追踪权。 @@ -218,6 +229,12 @@ Core 编译器已有数据流图（`src/compiler/dataflow.cr`）和线性扫描 边界检查序列（s3 编码 alloc_size），运行时 prov_table 维护堆边界并 patch DEREF 检查点， 配合 2026-07-28 的 Arena 内存模型（`src/stdlib/arena.cr`）。细节见 `TODO.md`。 +**更新（2026-08-10）**：设计定论—— +1. 类型双关由图自动验证（见上"类型双关"节），不需要 unsafe；宽度检查待补（TODO 预存 bug 7） +2. **不扩展"程序内部地址直接指"（0x 字面量指内部对象）**——YAGNI：内部对象用 `&` 取址 + 更优（无漂移、类型全、验证无条件）；外部契约地址 unsafe 已够用。0x 字面量仅保留 + unsafe 外部入口角色（上表前三行），详见 TODO 预存 bug 7 + ## 参考 - **SVF** (SVF-tools): LLVM 上的值流图框架，自动检测 use-after-free、double-free、buffer overflow。Core 的数据流图是更统一的形式——同一张图同时做 regalloc、调度、验证。 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/specs/2026-08-09-repo-governance-design.md b/docs/superpowers/specs/2026-08-09-repo-governance-design.md index 591bfee..3036614 100644 --- a/docs/superpowers/specs/2026-08-09-repo-governance-design.md +++ b/docs/superpowers/specs/2026-08-09-repo-governance-design.md @@ -17,8 +17,8 @@ Core 的愿景是成为严肃系统语言（语义保鲜、内核路线、形式 ## 2. 治理模型 - **GitFlow 标准**：`main` = 正式版线（仅正式版内容，对应 semver 发布）；`develop` = 集成分支（日常 PR 目标）；feature → develop 走 PR（审查 + CI + merge queue）；**develop → main 的合入只有维护者（DslsDZC）能做**（GitFlow 的发布负责人语义） -- **非对称**：唯一实际审查 = 你对 RhineIris PR 的单向把关；你的改动走 PR 但自批兜底 -- **愿景结构 + 现状执行**：规则按最终形态全立（将来贡献者增多规则自动生效）；执行上互审约定优先、自批兜底（GitHub 无原生"非作者审批"开关，工具层面拦不住作者自批——此为已知限制，流程约定补充） +- **非对称**：唯一实际审查 = 你对 RhineIris PR 的单向把关；你的改动走 PR，合入经 **B 流程**（临时豁免，见 §3.3） +- **愿景结构 + 现状执行**：规则按最终形态全立（将来贡献者增多规则自动生效）；执行上互审约定优先（**实测修正 2026-08-09**：GitHub 原生禁止作者批准自己的 PR——"自批兜底"不成立，维护者自有 PR 合入经 B 流程临时豁免，见 §3.3） - **机制限制（如实记录）**：GitHub 无原生"禁止以 main 为 base 创建 PR"开关——"PR 不能指向 main"由 **main 规则组合强制**（restrict pushes 仅 DslsDZC + required reviewers 仅 DslsDZC：指向 main 的 PR 无维护者批准无法合入）+ CONTRIBUTING 约定（PR 一律指向 develop）实现 - **铁律机械执行**：CLAUDE.md 第 2 条（禁止 git、全面 jj）用 hook 硬拦截 @@ -61,6 +61,11 @@ Core 的愿景是成为严肃系统语言（语义保鲜、内核路线、形式 - `merge_queue` 规则被 API 拒绝（"Invalid rule 'merge_queue'" 空原因）——**降级为手动合入**：审批 + CI 状态检查门槛保留（D1/D3/D8 的自动化串行部分由人工点击合入替代） - pull_request 参数 schema 实测：5 个必填布尔（含 `require_code_owner_review`）、`allowed_merge_methods: ["squash"]` 强制 squash-only - `required_status_checks` 参数数组字段名是 `required_status_checks`（非 `checks`） + - **2026-08-09 实测（流程验证）**： + - GitHub **原生禁止作者批准自己的 PR**（"Can not approve your own pull request"）——"自批兜底"前提不成立；管理员强制合并亦被 bypass_actors 空集拦截 + - **B 流程**（既定路径）：维护者自有 PR 合入 = 临时禁用对应 ruleset → squash 合并 → 恢复 active（PR #26 首次执行，2026-08-09） + - RhineIris 的审批要计入 required approvals 需 write 权限（fork 贡献者审批不满足要求）——待决策是否授予 collaborator + - CI 工作流注册冻结持续（GitHub 侧，注册表含已删文件/缺新文件）——develop 的 required_status_checks 暂移除，注册自愈后回填 - M7（release/* 标签保护）与 D7（文件路径限制）未落地：脚本与已建 ruleset 均未含（免费计划可用但暂缓），列入后续项 ## 4. GitHub 侧：落地方式 @@ -104,7 +109,7 @@ jj bookmark create feature/xxx # feature 分支（base = develop） ...开发提交（自动签名）... jj git push -b feature/xxx gh pr create --base develop --fill # PR 指向 develop（"不能指向 main"） -→ 审查（互审优先/自批兜底）→ 手动合入（审批过 + PR CI 绿） +→ 审查（RhineIris 的 PR 你审；你自己的 PR 走 B 流程临时豁免）→ 手动合入（PR CI 绿） → squash 合入 develop + 自动删源分支 jj git fetch && jj bookmark move develop -r develop@origin # 本地 develop 对齐 @@ -119,7 +124,7 @@ gh pr create --base main --fill # develop→main PR（required reviewers = - [ ] 直推 main 被拒（403）；推 feature 分支成功 - [ ] 指向 main 的 PR（非你创建）无法被批准合入——required reviewers 仅 DslsDZC - [ ] develop→main 合并只有你执行成功 -- [ ] 你的 feature PR：自批 → queue → squash 合入 develop → 源分支自动删除 +- [ ] 你的 feature PR：B 流程（临时豁免）→ squash 合入 develop → 源分支自动删除 - [ ] RhineIris fork PR：base=develop，完整流程，你审批后合入 develop - [ ] 未签名提交的 PR 被拒（签名规则生效）；`jj log --no-graph -T 'signature'` 可见签名 - [ ] 管理员账号直推 main 同样被拒（绕过已关闭） @@ -152,9 +157,171 @@ 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 签名 / hook / settings 清理 / CLAUDE.md——零网络依赖，待落地 -- ⬜ 创建 `develop` 集成分支（从 main 派生，作为日常 PR 目标） -- ✅ 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 已设 -- ⬜ spec 提交与 PR 流程本身（本条 spec 将作为首个 PR 提交） +- 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 from: zvolvptw 86ca5252 "docs: 惰性控制流定案编译期下沉路线（TODO）+ .crasm 正式文档 + 文档状态同步" +\\\\\\\ to: pvnmqnrn 1f3af03d "fix: stabilize backend self-hosting (#23)" ++# 仓库治理与分支保护设计 ++ ++日期：2026-08-09 ++状态：设计已批准（brainstorming 会话，分节确认）；CI 部分已实现，其余待落地 ++ ++## 1. 概述 ++ ++Core 的愿景是成为严肃系统语言（语义保鲜、内核路线、形式验证）——开发流程按**最终形态**立规，执行按**现状规模**宽松。治理模型参考 Rust/Linux：main 即 mainline，**任何人（含维护者）不得直推**，全部改动经 PR + 审查 + 合入门槛进入 main。 ++ ++| 事实 | 值 | ++|---|---| ++| 维护者（唯一写权限） | DslsDZC（你） | ++| 贡献者 | RhineIris——fork + PR 模式，无写权限，feature 分支在其 fork 上 | ++| 仓库形态 | jj colocated（.git 存在，git 命令物理可用） | ++| 合并历史 | 直推 main 为主，偶发 PR 合并 | ++ ++## 2. 治理模型 ++ ++- **GitFlow 标准**：`main` = 正式版线（仅正式版内容，对应 semver 发布）；`develop` = 集成分支（日常 PR 目标）；feature → develop 走 PR（审查 + CI + merge queue）；**develop → main 的合入只有维护者（DslsDZC）能做**（GitFlow 的发布负责人语义） ++- **非对称**：唯一实际审查 = 你对 RhineIris PR 的单向把关；你的改动走 PR 但自批兜底 ++- **愿景结构 + 现状执行**：规则按最终形态全立（将来贡献者增多规则自动生效）；执行上互审约定优先、自批兜底（GitHub 无原生"非作者审批"开关，工具层面拦不住作者自批——此为已知限制，流程约定补充） ++- **机制限制（如实记录）**：GitHub 无原生"禁止以 main 为 base 创建 PR"开关——"PR 不能指向 main"由 **main 规则组合强制**（restrict pushes 仅 DslsDZC + required reviewers 仅 DslsDZC：指向 main 的 PR 无维护者批准无法合入）+ CONTRIBUTING 约定（PR 一律指向 develop）实现 ++- **铁律机械执行**：CLAUDE.md 第 2 条（禁止 git、全面 jj）用 hook 硬拦截 ++ ++## 3. GitHub 侧：ruleset 最终清单（main / develop 两个 ruleset） ++ ++### 3.1 main ruleset（目标：main）——只有维护者能触碰 ++ ++| # | 规则 | 配置 | ++|---|---|---| ++| M1 | 推送限定 | Restrict pushes：**仅 DslsDZC**——物理上只有维护者能向 main 推送/合入（develop→main 合并只能由你执行） | ++| M2 | 禁强推 | Block force pushes | ++| M3 | 禁删分支 | Block deletions | ++| M4 | 合入门槛 | Require a pull request before merging + **required reviewers 仅 DslsDZC** + ≥1 approval——任何指向 main 的 PR（含 RhineIris、未来协作者）**无维护者批准无法合入** | ++| M5 | 强制签名提交 | Require signed commits（SSH 签名；GitHub 合并产生的 squash 提交自带 GitHub 签名，自动通过） | ++| M6 | 管理员无绕过 | 规则对仓库管理员同样生效（关闭 admin bypass——否则 M1 形同虚设） | ++| M7 | Protected tags | `release/*` 标签禁强推、禁删除 | ++ ++### 3.2 develop ruleset（目标：develop 集成分支）——日常开发入口 ++ ++| # | 规则 | 配置 | ++|---|---|---| ++| D1 | 禁直推 | Require a pull request before merging（PR 是唯一合入通道） | ++| D2 | 禁强推 | Block force pushes | ++| D3 | 强制审批 | Require 1 approval + required reviewers 仅 DslsDZC（合入 develop 亦须维护者批准，队列自动执行合并） | ++| D4 | 过时审批作废 | Dismiss stale pull request approvals when new commits are pushed | ++| D5 | 对话必须解决 | Require conversation resolution before merging | ++| D6 | 合并前必须更新分支 | Require branches to be up to date（merge queue 下由队列保证，双保险） | ++| D7 | 文件路径限制 | 核心路径 `src/compiler/**`、`src/arch/**` 变更需审批（防御性双保险） | ++| D8 | merge queue | Require merge queue（bors 对应物）；入口 = 审批过 + PR 层 CI 绿 | ++| D9 | 合并策略 | Allow squash merges only + 自动删除已合并源分支 | ++| D10 | 状态检查 | PR 层 CI job 名（check / bootstrap-tests / selfhost-tests）——CI 已实现（见第 5 节），配置时直接填入 | ++| D11 | 管理员无绕过 | 规则对仓库管理员同样生效 | ++ ++### 3.3 机制限制与过渡 ++ ++- **GitHub 无原生"禁止以 main 为 base 创建 PR"开关**：M4（required reviewers 仅 DslsDZC）使指向 main 的 PR 无法被非你合入——"PR 不能指向 main"以规则兜底 + CONTRIBUTING 约定（PR 一律指向 develop）实现 ++- **落地过渡**：两个 ruleset 先以 **evaluate（试运行）模式**启用，观察确认无干扰后转 active ++- **2026-08-09 落地偏差（免费计划限制，已实测）**： ++ - `enforcement: evaluate` 仅 Enterprise 可用——免费计划已直接以 **active** 创建（无试运行期，规则即刻生效） ++ - `merge_queue` 规则被 API 拒绝（"Invalid rule 'merge_queue'" 空原因）——**降级为手动合入**：审批 + CI 状态检查门槛保留（D1/D3/D8 的自动化串行部分由人工点击合入替代） ++ - pull_request 参数 schema 实测：5 个必填布尔（含 `require_code_owner_review`）、`allowed_merge_methods: ["squash"]` 强制 squash-only ++ - `required_status_checks` 参数数组字段名是 `required_status_checks`（非 `checks`） ++ - M7（release/* 标签保护）与 D7（文件路径限制）未落地：脚本与已建 ruleset 均未含（免费计划可用但暂缓），列入后续项 ++ ++## 4. GitHub 侧：落地方式 ++ ++- **路径 A（gh 恢复后）**：`tools/gh_setup_ruleset.sh`——`gh api` 按上述清单创建 ruleset（脚本内嵌规则 JSON） ++- **路径 B（现在可用）**：网页版 Settings → Rules → Rulesets，按第 3 节清单逐项配置 ++- **前置**：SSH 签名密钥（`~/.ssh/id_ed25519.pub`）在 GitHub Settings → SSH keys 注册为 **Signing key**（仅注册为认证 key 则签名校验失败） ++ ++## 5. CI（已实现，2026-08-09） ++ ++照 rust-lang/rust 模板（`~/rust`）重写，已本地验证： ++ ++``` ++.github/workflows/ci.yml ← 矩阵 job + 双层触发 ++src/ci/run.sh ← job 分发器（本地复现入口） ++src/ci/shared.sh ← helper ++src/ci/scripts/run-build-from-ci.sh ← GHA 入口 ++src/ci/scripts/setup-environment.sh ← 环境转储 ++``` ++ ++- 双层触发：`pull_request`（PR 快速层：check / bootstrap-tests / selfhost-tests）+ `merge_group`（完整层：suite / full-bootstrap）——PR 层 job 在 merge 下也运行（Rust 的 PR-jobs-auto-register 语义） ++- 砍掉：citool（静态矩阵内联）、全部 install-*.sh（Core 零工具链依赖）、docker/、artifacts ++- 已知风险（如实标记）：`full-bootstrap` 撞 corec2 tokenizer 死循环（TODO 自举阻塞项）+ 预存 bug 1（1GiB bump heap 峰值）——完整层按 TODO 逐个点亮；`opt-regress`（O0/O1 回归）留位 ++- 本地验证：`CI_JOB_NAME=bootstrap-tests src/ci/run.sh` 端到端通过 ++ ++## 6. 本地配置 ++ ++| 项 | 命令/文件 | 效果 | ++|---|---|---| ++| jj bookmark 保护 | `jj config set --repository bookmarks.main.protect true` | main 不被 rebase/rewrite 意外挪动 | ++| jj 提交签名 | `jj config set --user signing.backend ssh`、`signing.key ~/.ssh/id_ed25519.pub`、`signing.sign-all true` | 全部新提交 SSH 签名（满足规则 M5（强制签名提交）） | ++| git 硬拦截 hook | `.claude/settings.json`（提交入库）：PreToolUse 检测 Bash 命令以 `git` 开头 → 输出报错 + 非零退出 → 命令被拒绝 | 铁律 #2 机械执行 | ++| settings.local.json 清理 | 移除 `Bash(git *)` 允许项 | 权限模型与 hook 一致 | ++| CLAUDE.md | 新增"版本控制流程"段（下述命令序列） | 文档与机制一致 | ++ ++## 7. 新工作流（你） ++ ++``` ++日常开发（feature → develop）： ++jj bookmark create feature/xxx # feature 分支（base = develop） ++...开发提交（自动签名）... ++jj git push -b feature/xxx ++gh pr create --base develop --fill # PR 指向 develop（"不能指向 main"） ++→ 审查（互审优先/自批兜底）→ 手动合入（审批过 + PR CI 绿） ++→ squash 合入 develop + 自动删源分支 ++jj git fetch && jj bookmark move develop -r develop@origin # 本地 develop 对齐 ++ ++develop → main（只有你能）： ++jj git push -b develop # 你有写权限 ++gh pr create --base main --fill # develop→main PR（required reviewers = 你） ++→ 你批准 → 手动 squash 合入 main ++``` ++ ++## 8. 验证清单（合入后端到端） ++ ++- [ ] 直推 main 被拒（403）；推 feature 分支成功 ++- [ ] 指向 main 的 PR（非你创建）无法被批准合入——required reviewers 仅 DslsDZC ++- [ ] develop→main 合并只有你执行成功 ++- [ ] 你的 feature PR：自批 → queue → squash 合入 develop → 源分支自动删除 ++- [ ] RhineIris fork PR：base=develop，完整流程，你审批后合入 develop ++- [ ] 未签名提交的 PR 被拒（签名规则生效）；`jj log --no-graph -T 'signature'` 可见签名 ++- [ ] 管理员账号直推 main 同样被拒（绕过已关闭） ++- [ ] `git` 命令被 hook 硬拦截；`jj` 一切正常 ++- [ ] jj main protect 生效（rebase 移不动 main） ++- [ ] PR 层 CI 绿；完整层 job 状态如实标记 ++ ++## 9. 社区协作基础设施（2026-08-09 补充） ++ ++| 文件 | 内容 | ++|---|---| ++| `.github/pull_request_template.md` | PR 模板：变更描述 / 测试 / 语义保鲜影响 / 已知限制 | ++| `.github/CONTRIBUTING.md` | 贡献指南：fork→PR→审查→queue 流程、铁律（禁 git）、构建测试命令、编码约定、审查标准 | ++| `.github/SECURITY.md` | 漏洞报告路径（GitHub 私有漏洞报告）与响应承诺 | ++| `.github/CODE_OF_CONDUCT.md` | 贡献者行为规范（Contributor Covenant 2.1 中文版，执行联系人 dsls.dzc@gmail.com） | ++ ++## 10. 发布规范 ++ ++- 版本号：**semver**（`MAJOR.MINOR.PATCH`） ++- 标签：`release/vMAJOR.MINOR.PATCH`（对应 protected tags 规则 `release/*`） ++- 发布流程：维护者从 main 打 tag → 标签保护防止强推/删除 ++- changelog：按需维护（后续项） ++ ++## 11. 后续项（明确延期） ++ ++- Issue 模板（bug/特性请求）、标签体系——贡献者规模上来后补 ++- Dependabot——**不做**（仓库零外部依赖） ++- CI 优化：actions/cache 缓存 `build/corec`（多 job 共享构建产物）；`full-bootstrap` 点亮（依赖自举阻塞项修复）；`opt-regress`（O0/O1 回归）启用 ++- 部署环境门禁（required deployment）——无发布流水线前不做 ++ ++## 12. 当前状态 ++ ++- ✅ CI 骨架：已实现（2026-08-09），本地验证通过，随首个 PR 上线 ++- ✅ 社区四件套：PR 模板 / CONTRIBUTING / SECURITY / CODE_OF_CONDUCT 已写（2026-08-09），随本 spec 首 PR 上线 ++- ⬜ 本地配置：jj protect / jj 签名 / hook / settings 清理 / CLAUDE.md——零网络依赖，待落地 ++- ⬜ 创建 `develop` 集成分支（从 main 派生，作为日常 PR 目标） ++- ✅ 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 已设 ++- ⬜ spec 提交与 PR 流程本身（本条 spec 将作为首个 PR 提交） 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` | 查看标识符定义 | diff --git a/src/arch/linux/ld/elf.cr b/src/arch/linux/ld/elf.cr index 8291d35..9cfcc28 100644 --- a/src/arch/linux/ld/elf.cr +++ b/src/arch/linux/ld/elf.cr @@ -267,8 +267,9 @@ fn emit_alloc_body(buf: string, pos: int, bss_va: int, globals_size: int) -> int } // cmp rdx, [rcx] -- 48 3B 11 w8(buf, pos+cp, 72); w8(buf, pos+cp+1, 59); w8(buf, pos+cp+2, 17); cp = cp + 3; - // jbe +14 (skip call+reload+jmp if within bounds) -- 76 0E - w8(buf, pos+cp, 118); w8(buf, pos+cp+1, 14); cp = cp + 2; + // jbe +17 (skip call+reload+rdi+jmp if within bounds) + // 修复：原 +14 漏了 mov rdi,r9（3 字节）→ 跳到指令中间（0xf9）→ 死循环 + w8(buf, pos+cp, 118); w8(buf, pos+cp+1, 17); cp = cp + 2; // call heap_expand -- E8 xx xx xx xx (patched in elf_gen after heap_expand emitted) g_heap_expand_call_pos = pos + cp; e2_w8(buf, pos+cp, 232); e2_w32(buf, pos+cp+1, 0); cp = cp + 5; @@ -1078,7 +1079,14 @@ fn elf_gen(buf: string) -> int { pc2 := r64(g_ir_func_param_count, fi * 8); fsz := r64(g_x86_func_code_sz, fi * 8); + // SysV 16 字节对齐（发现 11）：call 后 rsp%16=8； + // opt≥1 有 6 个 push（rbx,r12-15,rbp）→ rsp%16=8 → size 需 ≡8 (mod 16)； + // opt<1 有 1 个 push（rbp）→ rsp%16=0 → size 需 ≡0 (mod 16)。 g_x86_emit_stack_size = vc2 * 8; + if (g_x86_emit_stack_size % 16 == 0 && g_opt_level >= 1) || + (g_x86_emit_stack_size % 16 == 8 && g_opt_level < 1) { + g_x86_emit_stack_size = g_x86_emit_stack_size + 8; + } total_code = total_code + sz_push_rbp() + sz_mov_rbp_rsp(); if g_opt_level >= 1 { total_code = total_code + 18; } // push rbx,r12-r15(9) + pop r15-r12,rbx(9) ss_dry := g_x86_emit_stack_size; @@ -1195,7 +1203,12 @@ fi = 0; loop { if fi >= g_ir_func_count { break; } g2_init(); g_current_func_var_start = vs; vi := 0; loop { if vi >= vc { break; } g2_slot(vs + vi); vi = vi + 1; } + // SysV 16 字节对齐（发现 11）：与 dry run 相同的对齐规则 g_x86_emit_stack_size = vc * 8; + if (g_x86_emit_stack_size % 16 == 0 && g_opt_level >= 1) || + (g_x86_emit_stack_size % 16 == 8 && g_opt_level < 1) { + g_x86_emit_stack_size = g_x86_emit_stack_size + 8; + } // Init label state for single-pass backpatching (-1 = not yet seen) li2 : ., mut = 0; @@ -1225,17 +1238,43 @@ fi = 0; loop { if fi >= g_ir_func_count { break; } // Save register and caller-stack params into this function's slots. pi := 0; loop { if pi >= pc { break; } po2 := -(vs + pi + 1 - g_current_func_var_start) * 8; // force stack slot, ignore reg alloc - if pi == 0 { cp = cp + e2_st(buf, cp, 7, po2); } - if pi == 1 { w8(buf, cp, 72); w8(buf, cp+1, 137); w8(buf, cp+2, 117); w8(buf, cp+3, po2); cp = cp + 4; } - if pi == 2 { w8(buf, cp, 72); w8(buf, cp+1, 137); w8(buf, cp+2, 85); w8(buf, cp+3, po2); cp = cp + 4; } - if pi == 3 { w8(buf, cp, 72); w8(buf, cp+1, 137); w8(buf, cp+2, 77); w8(buf, cp+3, po2); cp = cp + 4; } - if pi == 4 { w8(buf, cp, 76); w8(buf, cp+1, 137); w8(buf, cp+2, 69); w8(buf, cp+3, po2); cp = cp + 4; } - if pi == 5 { w8(buf, cp, 76); w8(buf, cp+1, 137); w8(buf, cp+2, 77); w8(buf, cp+3, po2); cp = cp + 4; } - if pi >= 6 { + pty := irv_type(vs + pi); + if pty == TI_FLOAT && pi < 6 { + // float 参数在 XMM：movsd [rbp+po2], xmm{frn}（SysV） + // frn = 第 pi 个参数前的 float 参数数 + frn : ., mut = 0; + fj : ., mut = 0; + loop { if fj >= pi { break; } + if irv_type(vs + fj) == TI_FLOAT { frn = frn + 1; } + fj = fj + 1; } + if frn < 8 { + // movsd [rbp+po2], xmm{frn} — F2 0F 11 /rn（mod=01, rm=5） + w8(buf, cp, 242); w8(buf, cp+1, 15); w8(buf, cp+2, 17); + w8(buf, cp+3, 64 + frn * 8 + 5); w8(buf, cp+4, po2); cp = cp + 5; + } else { + // 9+ float 参数在栈上（边缘场景，位置布局简化处理） + caller_off := 16 + (pi - 6) * 8; + if g_opt_level >= 1 { caller_off = caller_off + 40; } + cp = cp + e2_sd_load(buf, cp, caller_off); + cp = cp + e2_sd_store(buf, cp, po2); + } + } else if pi >= 6 { caller_off := 16 + (pi - 6) * 8; if g_opt_level >= 1 { caller_off = caller_off + 40; } - cp = cp + e2_ld(buf, cp, 10, caller_off); - cp = cp + e2_st(buf, cp, 10, po2); + if pty == TI_FLOAT { + cp = cp + e2_sd_load(buf, cp, caller_off); + cp = cp + e2_sd_store(buf, cp, po2); + } else { + cp = cp + e2_ld(buf, cp, 10, caller_off); + cp = cp + e2_st(buf, cp, 10, po2); + } + } else { + if pi == 0 { cp = cp + e2_st(buf, cp, 7, po2); } + if pi == 1 { w8(buf, cp, 72); w8(buf, cp+1, 137); w8(buf, cp+2, 117); w8(buf, cp+3, po2); cp = cp + 4; } + if pi == 2 { w8(buf, cp, 72); w8(buf, cp+1, 137); w8(buf, cp+2, 85); w8(buf, cp+3, po2); cp = cp + 4; } + if pi == 3 { w8(buf, cp, 72); w8(buf, cp+1, 137); w8(buf, cp+2, 77); w8(buf, cp+3, po2); cp = cp + 4; } + if pi == 4 { w8(buf, cp, 76); w8(buf, cp+1, 137); w8(buf, cp+2, 69); w8(buf, cp+3, po2); cp = cp + 4; } + if pi == 5 { w8(buf, cp, 76); w8(buf, cp+1, 137); w8(buf, cp+2, 77); w8(buf, cp+3, po2); cp = cp + 4; } } pi = pi + 1; } diff --git a/src/arch/linux/ld/instr.cr b/src/arch/linux/ld/instr.cr index 7bcf941..70cb989 100644 --- a/src/arch/linux/ld/instr.cr +++ b/src/arch/linux/ld/instr.cr @@ -262,6 +262,86 @@ fn e2_alu(b: string, p: int, op: int) -> int { return cp - p; } +// ── SSE2 double 运算（IEEE 754 标准，float 支持）── +// movsd xmm0, [rbp+disp] — F2 0F 10 /0 +fn e2_sd_load(b: string, p: int, o: int) -> int { + cp := p; + w8(b, cp, 242); w8(b, cp+1, 15); w8(b, cp+2, 16); cp = cp + 3; + if o >= -128 && o <= 127 { + w8(b, cp, 69); w8(b, cp+1, o); cp = cp + 2; // ModRM 01 000 101 + } else { + w8(b, cp, 133); cp = cp + 1; // ModRM 10 000 101 + cp = cp + e2_w32(b, cp, o); + } + return cp - p; +} +// movsd xmm1, [rbp+disp] — F2 0F 10 /1 +fn e2_sd_load1(b: string, p: int, o: int) -> int { + cp := p; + w8(b, cp, 242); w8(b, cp+1, 15); w8(b, cp+2, 16); cp = cp + 3; + if o >= -128 && o <= 127 { + w8(b, cp, 77); w8(b, cp+1, o); cp = cp + 2; // ModRM 01 001 101 + } else { + w8(b, cp, 141); cp = cp + 1; // ModRM 10 001 101 + cp = cp + e2_w32(b, cp, o); + } + return cp - p; +} +// movsd xmm{rn}, [rbp+disp] — F2 0F 10 /rn（rn=0..7，SysV float 参数） +fn e2_sd_load_x(b: string, p: int, o: int, rn: int) -> int { + cp := p; + w8(b, cp, 242); w8(b, cp+1, 15); w8(b, cp+2, 16); cp = cp + 3; + if o >= -128 && o <= 127 { + w8(b, cp, 64 + rn * 8 + 5); w8(b, cp+1, o); cp = cp + 2; + } else { + w8(b, cp, 128 + rn * 8 + 5); cp = cp + 1; + cp = cp + e2_w32(b, cp, o); + } + return cp - p; +} + +// 存返回值到 dest：float → movsd [slot], xmm0（SysV XMM0 返回）；int → rax +fn e2_store_ret(b: string, p: int, d: int) -> int { + if d >= 0 && irv_type(d) == TI_FLOAT { + return e2_sd_store(b, p, g2_slot(d)); + } + return e2_st(b, p, 0, g2_slot(d)); +} + +// 压栈 float（8 字节）：sub rsp,8 + movsd [rsp],xmm0 +fn e2_push_xmm0(b: string, p: int) -> int { + cp := p; + w8(b, cp, 72); w8(b, cp+1, 131); w8(b, cp+2, 236); w8(b, cp+3, 8); cp = cp + 4; + w8(b, cp, 242); w8(b, cp+1, 15); w8(b, cp+2, 17); w8(b, cp+3, 4); w8(b, cp+4, 36); cp = cp + 5; + return cp - p; +} + +// cvtsi2sd xmm0, [rbp+disp] — F2 0F 2A /0（int→float 转换） +fn e2_sd_cvt(b: string, p: int, o: int) -> int { + cp := p; + w8(b, cp, 242); w8(b, cp+1, 15); w8(b, cp+2, 42); cp = cp + 3; + if o >= -128 && o <= 127 { + w8(b, cp, 69); w8(b, cp+1, o); cp = cp + 2; // ModRM 01 000 101 + } else { + w8(b, cp, 133); cp = cp + 1; // ModRM 10 000 101 + cp = cp + e2_w32(b, cp, o); + } + return cp - p; +} + +// movsd [rbp+disp], xmm0 — F2 0F 11 /0 +fn e2_sd_store(b: string, p: int, o: int) -> int { + cp := p; + w8(b, cp, 242); w8(b, cp+1, 15); w8(b, cp+2, 17); cp = cp + 3; + if o >= -128 && o <= 127 { + w8(b, cp, 69); w8(b, cp+1, o); cp = cp + 2; + } else { + w8(b, cp, 133); cp = cp + 1; + cp = cp + e2_w32(b, cp, o); + } + return cp - p; +} + // ── emit_instr: write one instruction to buffer, return bytes written ── fn e2_load_var(buf: string, pos: int, reg: int, var_idx: int) -> int { @@ -302,6 +382,24 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { if op == IR_NOP { return 0; } + if op == IR_I2F && d >= 0 { + // int → float：cvtsi2sd xmm0, [rbp+disp] — F2 0F 2A /0，然后 movsd 存回 + do2 := g2_slot(d); + cp = cp + e2_sd_cvt(buf, pos+cp, g2_slot(s1)); // cvtsi2sd xmm0, [s1] + cp = cp + e2_sd_store(buf, pos+cp, do2); + return cp; + } + + if op == IR_F2I && d >= 0 { + // float → int：movsd xmm0, [s1]；cvttsd2si rax, xmm0（F2 48 0F 2C C0）；存回 + do2 := g2_slot(d); + cp = cp + e2_sd_load(buf, pos+cp, g2_slot(s1)); + w8(buf, pos+cp, 242); w8(buf, pos+cp+1, 72); w8(buf, pos+cp+2, 15); + w8(buf, pos+cp+3, 44); w8(buf, pos+cp+4, 192); cp = cp + 5; + cp = cp + e2_st(buf, pos+cp, 0, do2); + return cp; + } + if op == IR_CONST && d >= 0 { do2 := g2_slot(d); if ti == TI_STR { @@ -321,6 +419,35 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { if op == IR_BINARY { do2 := g2_slot(d); + if ti == TI_FLOAT { + // float 运算（SSE2 double，IEEE 754）——标准答案实现 + cp = cp + e2_sd_load(buf, pos+cp, g2_slot(s1)); // xmm0 = s1 + cp = cp + e2_sd_load1(buf, pos+cp, g2_slot(s2)); // xmm1 = s2 + // F2 0F 5x C1：addsd/subsd/mulsd/divsd xmm0, xmm1 + if s3 == OP_ADD { w8(buf, pos+cp, 242); w8(buf, pos+cp+1, 15); w8(buf, pos+cp+2, 88); w8(buf, pos+cp+3, 193); cp = cp + 4; } + else if s3 == OP_SUB { w8(buf, pos+cp, 242); w8(buf, pos+cp+1, 15); w8(buf, pos+cp+2, 92); w8(buf, pos+cp+3, 193); cp = cp + 4; } + else if s3 == OP_MUL { w8(buf, pos+cp, 242); w8(buf, pos+cp+1, 15); w8(buf, pos+cp+2, 89); w8(buf, pos+cp+3, 193); cp = cp + 4; } + else if s3 == OP_DIV { w8(buf, pos+cp, 242); w8(buf, pos+cp+1, 15); w8(buf, pos+cp+2, 94); w8(buf, pos+cp+3, 193); cp = cp + 4; } + if s3 >= OP_ADD && s3 <= OP_DIV { + cp = cp + e2_sd_store(buf, pos+cp, do2); + } else if s3 >= OP_EQ && s3 <= OP_GE { + // float 比较：comisd xmm0, xmm1 — 66 0F 2F C1，用无符号标志 + // （IEEE 754：< → CF=1；== → ZF=1；> → CF=0&&ZF=0） + // 比较结果是 int（0/1），用整数路径存储 + w8(buf, pos+cp, 102); w8(buf, pos+cp+1, 15); w8(buf, pos+cp+2, 47); w8(buf, pos+cp+3, 193); cp = cp + 4; + sop : ., mut = 148; // sete + if s3 == OP_NE { sop = 149; } + else if s3 == OP_LT { sop = 146; } // setb（CF） + else if s3 == OP_GT { sop = 151; } // seta（CF=0 && ZF=0） + else if s3 == OP_LE { sop = 150; } // setbe + else if s3 == OP_GE { sop = 147; } // setae + w8(buf, pos+cp, 15); w8(buf, pos+cp+1, sop); w8(buf, pos+cp+2, 192); cp = cp + 3; + // movzx r10d, al — 44 0F B6 D0 + w8(buf, pos+cp, 68); w8(buf, pos+cp+1, 15); w8(buf, pos+cp+2, 182); w8(buf, pos+cp+3, 208); cp = cp + 4; + cp = cp + e2_st(buf, pos+cp, 10, do2); + } + return cp; + } cp = cp + e2_load_var(buf, pos+cp, 10, s1); cp = cp + e2_load_var(buf, pos+cp, 11, s2); if s3 == OP_ADD { cp = cp + e2_alu(buf, pos+cp, 1); } @@ -420,19 +547,51 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { if op == IR_CALL { fa := s1; ac := s2; + // SysV AMD64 参数分派：int 用 ir（0-5 → rdi,rsi,rdx,rcx,r8,r9）， + // float 用 fr（0-7 → xmm0-7），各自独立编号（标准答案） + // 第一遍：寄存器参数（位置顺序，左到右） + ir_cnt : ., mut = 0; fr_cnt : ., mut = 0; ai := 0; - loop { if ai >= ac { break; } if ai >= 6 { break; } - r := -1; - if ai == 0 { r = 7; } if ai == 1 { r = 6; } if ai == 2 { r = 2; } if ai == 3 { r = 1; } if ai == 4 { r = 8; } if ai == 5 { r = 9; } - if r >= 0 { cp = cp + e2_load_var(buf, pos+cp, r, fa + ai); } + loop { if ai >= ac { break; } + pt := irv_type(fa + ai); + if pt == TI_FLOAT { + if fr_cnt < 8 { + cp = cp + e2_sd_load_x(buf, pos+cp, g2_slot(fa + ai), fr_cnt); + fr_cnt = fr_cnt + 1; + } + } else { + if ir_cnt < 6 { + r := -1; + if ir_cnt == 0 { r = 7; } if ir_cnt == 1 { r = 6; } if ir_cnt == 2 { r = 2; } + if ir_cnt == 3 { r = 1; } if ir_cnt == 4 { r = 8; } if ir_cnt == 5 { r = 9; } + cp = cp + e2_load_var(buf, pos+cp, r, fa + ai); + ir_cnt = ir_cnt + 1; + } + } ai = ai + 1; } - // System V AMD64 passes the 7th and later arguments on the stack, - // rightmost first, so argument 7 is closest to the return address. + // 第二遍：栈参数（右到左压，第 7 个 int / 第 9 个 float 超限才压） + stack_total : ., mut = 0; stack_ai : ., mut = ac - 1; loop { - if stack_ai < 6 { break; } - cp = cp + e2_load_var(buf, pos+cp, 10, fa + stack_ai); - e2_w8(buf, pos+cp, 65); e2_w8(buf, pos+cp+1, 82); cp = cp + 2; // push r10 + if stack_ai < 0 { break; } + ic2 : ., mut = 0; fc2 : ., mut = 0; + j2 : ., mut = 0; + loop { if j2 >= stack_ai { break; } + if irv_type(fa + j2) == TI_FLOAT { fc2 = fc2 + 1; } else { ic2 = ic2 + 1; } + j2 = j2 + 1; } + if irv_type(fa + stack_ai) == TI_FLOAT { + if fc2 >= 8 { + cp = cp + e2_sd_load_x(buf, pos+cp, g2_slot(fa + stack_ai), 0); + cp = cp + e2_push_xmm0(buf, pos+cp); + stack_total = stack_total + 1; + } + } else { + if ic2 >= 6 { + cp = cp + e2_load_var(buf, pos+cp, 10, fa + stack_ai); + e2_w8(buf, pos+cp, 65); e2_w8(buf, pos+cp+1, 82); cp = cp + 2; // push r10 + stack_total = stack_total + 1; + } + } stack_ai = stack_ai - 1; } // Match builtins by interned string index (integer compare, no str_eq) @@ -443,12 +602,12 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { cp = cp + e2_mov(buf, pos+cp, 2, 1); // syscall: 2-byte 0x0F 0x05 e2_w8(buf, pos+cp, 15); e2_w8(buf, pos+cp+1, 5); cp = cp + 2; - if d >= 0 { cp = cp + e2_st(buf, pos+cp, 0, g2_slot(d)); } + if d >= 0 { cp = cp + e2_store_ret(buf, pos+cp, d); } } else if s3 == g_ni_load8 { // movzx rax, byte [rdi+rsi] — REX.W + 0x0FB6 + SIB cp = cp + emit_rex(buf, pos+cp, 1, 0, 0, 0); e2_w8(buf, pos+cp, 15); cp = cp + 1; e2_w8(buf, pos+cp, 182); cp = cp + 1; cp = cp + emit_modrm(buf, pos+cp, 0, 0, 4); cp = cp + emit_sib(buf, pos+cp, 0, 6, 7); - if d >= 0 { cp = cp + e2_st(buf, pos+cp, 0, g2_slot(d)); } + if d >= 0 { cp = cp + e2_store_ret(buf, pos+cp, d); } } else if s3 == g_ni_store8 { // mov [rdi+rsi], dl — 0x88 + SIB (3rd arg in rdx = register 2) e2_w8(buf, pos+cp, 136); cp = cp + 1; cp = cp + emit_modrm(buf, pos+cp, 0, 2, 4); cp = cp + emit_sib(buf, pos+cp, 0, 6, 7); @@ -457,7 +616,7 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { // mov rax, [rdi+rsi] — REX.W + 0x8B + SIB cp = cp + emit_rex(buf, pos+cp, 1, 0, 0, 0); e2_w8(buf, pos+cp, 139); cp = cp + 1; cp = cp + emit_modrm(buf, pos+cp, 0, 0, 4); cp = cp + emit_sib(buf, pos+cp, 0, 6, 7); - if d >= 0 { cp = cp + e2_st(buf, pos+cp, 0, g2_slot(d)); } + if d >= 0 { cp = cp + e2_store_ret(buf, pos+cp, d); } } else if s3 == g_ni_store_str_ptr { // mov [rdi + rsi], rdx // mov [rdi+rsi], rdx — REX.W + 0x89 + SIB @@ -521,7 +680,7 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { // test dl, dl e2_w8(buf, pos+cp, 132); cp = cp + 1; cp = cp + emit_modrm(buf, pos+cp, 3, 2, 2); e2_w8(buf, pos+cp, 117); e2_w8(buf, pos+cp+1, 241); cp = cp + 2; // jne copy_loop - if d >= 0 { cp = cp + e2_st(buf, pos+cp, 0, g2_slot(d)); } + if d >= 0 { cp = cp + e2_store_ret(buf, pos+cp, d); } } else if s3 == g_ni_w64 { // w64(buf, pos, val) → mov [rsi+rdi??], rdx // Actually args: rdi=buf, rsi=pos, rdx=val @@ -583,13 +742,13 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { g_x86_ext_rel_count = g_x86_ext_rel_count + 1; cp = cp + e2_call(buf, pos+cp, 0); } - if d >= 0 { cp = cp + e2_st(buf, pos+cp, 0, g2_slot(d)); } + if d >= 0 { cp = cp + e2_store_ret(buf, pos+cp, d); } } else { // xor eax, eax e2_w8(buf, pos+cp, 49); e2_w8(buf, pos+cp+1, 192); cp = cp + 2; - if d >= 0 { cp = cp + e2_st(buf, pos+cp, 0, g2_slot(d)); } + if d >= 0 { cp = cp + e2_store_ret(buf, pos+cp, d); } } - stack_count := ac - 6; + stack_count := stack_total; // 实际压栈数（int 超 6 + float 超 8） if stack_count > 0 { stack_bytes := stack_count * 8; if stack_bytes <= 127 { @@ -665,7 +824,10 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { if op == IR_RETURN { if s1 >= 0 { - if r64(g_x86_is_global, s1 * 8) != 0 { + if irv_type(s1) == TI_FLOAT { + // float 返回：movsd xmm0, [slot]（SysV 返回值在 XMM0） + cp = cp + e2_sd_load(buf, pos+cp, g2_slot(s1)); + } else if r64(g_x86_is_global, s1 * 8) != 0 { // Global: load via RIP-relative into rax grow_rip_patch(g_x86_rip_patch_count + 1); w64(g_x86_rip_patch_pos, g_x86_rip_patch_count * 8, pos + cp + 3); @@ -858,12 +1020,13 @@ fn emit_instr(instr_idx: int, buf: string, pos: int) -> int { // jne .safe (skip ud2 if non-null) safe_jmp_pos := pos+cp; e2_w8(buf, pos+cp, 117); e2_w8(buf, pos+cp+1, 0); cp = cp + 2; // placeholder - // .crash: ud2 - w8(buf, cp, 15); w8(buf, cp+1, 11); cp = cp + 2; - // Patch jae to jump here - e2_w32(buf, crash_jmp_pos + 2, (pos+cp) - (crash_jmp_pos + 6)); - // Patch jne to jump past ud2 to .safe - w8(buf, safe_jmp_pos + 1, (pos+cp) - (safe_jmp_pos + 2) + 2); + // .crash: ud2（必须写 pos+cp 绝对位置——修复前写 buf[cp] 污染函数头） + e2_w8(buf, pos+cp, 15); e2_w8(buf, pos+cp+1, 11); cp = cp + 2; + // Patch jae to jump to ud2 (crash): target = crash_jmp_pos+6+3+2 + // (jae 6 + test 3 + jne 2 = ud2 起点)。修复前跳到 .safe，越界不崩溃。 + e2_w32(buf, crash_jmp_pos + 2, (pos+cp) - (crash_jmp_pos + 6) - 2); + // Patch jne to jump past ud2 to .safe（修复前多 +2，跳到指令中间） + w8(buf, safe_jmp_pos + 1, (pos+cp) - (safe_jmp_pos + 2)); // .safe: deref } // mov r10, [r10] diff --git a/src/compiler/ast.cr b/src/compiler/ast.cr index 3be0fdf..ed701c0 100644 --- a/src/compiler/ast.cr +++ b/src/compiler/ast.cr @@ -571,6 +571,8 @@ IR_CALL_EXTERN : int = 45; // dest=result_var, s1=func_name_ni, s2=first_arg, s IR_LAZY_THUNK : int = 46; // dest=thunk_var, s1=expr_var — wrap as lazy thunk IR_LAZY_FORCE : int = 47; // dest=val_var, s1=thunk_var — force evaluation IR_FNADDR : int = 48; // dest=addr_var, s1=fn_name_ni — load function address (movabs + link-time patch) +IR_I2F : int = 49; // dest=float_var, s1=int_var — int → float（cvtsi2sd） +IR_F2I : int = 50; // dest=int_var, s1=float_var — float → int（cvttsd2si） // Resolution flag for BRANCH/JUMP (stored in type_kind field after label resolution) IR_RESOLVED : int = 1; diff --git a/src/compiler/ccr_io.cr b/src/compiler/ccr_io.cr index 74052ad..2c78c47 100644 --- a/src/compiler/ccr_io.cr +++ b/src/compiler/ccr_io.cr @@ -43,6 +43,10 @@ fn buf_write_i32(buf: string, pos: int, val: int) { w32(buf, pos, val); } +fn buf_write_i64(buf: string, pos: int, val: int) { + w64(buf, pos, val); +} + fn buf_read_u32(buf: string, pos: int) -> int { b0 := load8(buf, pos); b1 := load8(buf, pos + 1); @@ -76,6 +80,7 @@ fn buf_read_i64(buf: string, pos: int) -> int { h3 := load8(buf, pos + 7); hi : ., mut = h0 + h1 * 256 + h2 * 65536; if h3 >= 128 { hi = hi + (h3 - 256) * 16777216; } + else { hi = hi + h3 * 16777216; } // 修复 15：h3 < 128 时漏加 h3×2^24 → bit 56-62 丢失 // Keep the factor within the parser's supported integer-literal range. hi_part := hi * 65536; hi_part = hi_part * 65536; @@ -97,7 +102,7 @@ fn calc_ccr_size() -> int { } sz = sz + g_ir_func_count * 28; // func meta - sz = sz + g_ir_instr_count * 24; // instrs + sz = sz + g_ir_instr_count * 28; // instrs（s1 为 64 位） sz = sz + g_ir_var_count * 12; // vars sz = sz + g_ir_str_const_count * 4; // str_consts @@ -202,7 +207,9 @@ fn save_ccr(path: string) -> int { if ii >= g_ir_instr_count { break; } buf_write_u32(buf, pos, iri_op(ii)); pos = pos + 4; buf_write_i32(buf, pos, iri_dest(ii)); pos = pos + 4; - buf_write_i32(buf, pos, iri_s1(ii)); pos = pos + 4; + // 修复 14：s1 改 64 位——IR_CONST 的大 int 常量 / float 位模式 + // 之前被截断成 32 位（float 常量静默损坏） + buf_write_i64(buf, pos, iri_s1(ii)); pos = pos + 8; buf_write_i32(buf, pos, iri_s2(ii)); pos = pos + 4; buf_write_i32(buf, pos, iri_s3(ii)); pos = pos + 4; buf_write_u32(buf, pos, iri_tk(ii)); pos = pos + 4; @@ -406,7 +413,7 @@ fn load_ccr(data: string, fsize: int) -> int { if ii >= instr_cnt { break; } opcode := buf_read_u32(data, pos); pos = pos + 4; dest := buf_read_i32(data, pos); pos = pos + 4; - s1 := buf_read_i32(data, pos); pos = pos + 4; + s1 := buf_read_i64(data, pos); pos = pos + 8; // 修复 14：s1 64 位 s2 := buf_read_i32(data, pos); pos = pos + 4; s3 := buf_read_i32(data, pos); pos = pos + 4; tk := buf_read_u32(data, pos); pos = pos + 4; diff --git a/src/compiler/globals.cr b/src/compiler/globals.cr index 432b0d7..4bcbb96 100644 --- a/src/compiler/globals.cr +++ b/src/compiler/globals.cr @@ -138,6 +138,9 @@ g_plugin_rtypes : string, mut; g_plugin_rtype_count : int, mut; g_plugin_rtype_c // Pointer analysis storage g_pts : string, mut; g_pts_count : int, mut; g_pts_cap : int, mut; g_offsets : string, mut; g_offsets_count : int, mut; g_offsets_cap : int, mut; +// Alloc 序号 → DF 节点序号映射（修复 3：alloc pts 需要递增位号，provenance 按位号查 alloc 大小） +g_pa_alloc_count : int, mut; +g_pa_alloc_nodes : string, mut; g_pa_alloc_nodes_cap : int, mut; fn grow_plugin_tags(needed: int) { if needed < g_plugin_tag_cap { return; } diff --git a/src/compiler/ir_gen.cr b/src/compiler/ir_gen.cr index 8a3b30f..8e36a10 100644 --- a/src/compiler/ir_gen.cr +++ b/src/compiler/ir_gen.cr @@ -643,8 +643,24 @@ fn gen_expr(node: int) -> int { } } } - v := new_ir_var("bin", TI_INT); - emit(IR_BINARY, v, left_var, right_var, op, 0); + // float 运算：类型标记 TI_FLOAT（后端按 ti 分派 SSE2，IEEE 754 标准） + // int 操作数隐式转换（cvtsi2sd）——阶段 4 + fti : int = 0; + if lt == TI_FLOAT || rt == TI_FLOAT { + fti = TI_FLOAT; + if lt != TI_FLOAT { + t1 := new_ir_var("_f0", TI_FLOAT); + emit(IR_I2F, t1, left_var, 0, 0, TI_FLOAT); + left_var = t1; + } + if rt != TI_FLOAT { + t2 := new_ir_var("_f1", TI_FLOAT); + emit(IR_I2F, t2, right_var, 0, 0, TI_FLOAT); + right_var = t2; + } + } + v := new_ir_var("bin", fti); + emit(IR_BINARY, v, left_var, right_var, op, fti); return v; } diff --git a/src/compiler/lexer.cr b/src/compiler/lexer.cr index 6d8ea29..9f4afd4 100644 --- a/src/compiler/lexer.cr +++ b/src/compiler/lexer.cr @@ -107,6 +107,77 @@ fn lookup_keyword(s: string) -> int { return T_IDENT; } +// 2^k（纯整数，k >= 0） +fn pow2i(k: int) -> int { + v : int = 1; i : ., mut = 0; + loop { if i >= k { break; } v = v * 2; i = i + 1; } + return v; +} + +// decimal string → IEEE 754 binary64 位模式（纯整数近似，≤18 位有效数字） +// 实现：value = ip + fp/den → 整数部分位 + 64 位长除小数 → 53 位尾数窗口 +// 精度：截断（无舍入），≤18 位有效数字内 ~2ulp +fn str_to_f64_bits(s: string) -> int { + sl := str_len(s); + i : ., mut = 0; + neg : int = 0; + if i < sl && load8(s, i) == 45 { neg = 1; i = i + 1; } + ip : int = 0; fp : int = 0; den : int = 1; sd : int = 0; dg : ., mut = 0; + loop { if i >= sl { break; } + c := load8(s, i); + if c == 46 { sd = 1; i = i + 1; continue; } + if c < 48 || c > 57 { break; } + dg = dg + 1; + if dg <= 18 { + if sd != 0 { fp = fp * 10 + (c - 48); den = den * 10; } + else { ip = ip * 10 + (c - 48); } + } + i = i + 1; } + if ip == 0 && fp == 0 { + if neg != 0 { return -9223372036854775808; } + return 0; + } + // 小数 64 位（长除：r=fp，每轮 r×2 vs den） + frac64 : int = 0; + r : ., mut = fp; + bits : ., mut = 0; + loop { if bits >= 64 { break; } + if r >= 4611686018427387904 { r = r / 2; den = den / 2; } + r = r * 2; + frac64 = frac64 * 2; + if r >= den { r = r - den; frac64 = frac64 + 1; } + bits = bits + 1; } + // 整数部分位宽 + bi : ., mut = 0; t2 : ., mut = ip; + loop { if t2 == 0 { break; } t2 = t2 / 2; bi = bi + 1; } + mant : int = 0; + exp : int = 0; + if bi > 0 { + sh := 53 - bi; + mant = (ip * pow2i(sh)) + (frac64 / pow2i(64 - sh)); + exp = 1023 + (bi - 1); + } else { + // 纯小数：frac64 的最高位 + bf : ., mut = 0; t2 = frac64; + loop { if t2 == 0 { break; } t2 = t2 / 2; bf = bf + 1; } + if bf == 0 { + if neg != 0 { return -9223372036854775808; } + return 0; + } + sh := 53 - bf; + if sh >= 0 { mant = frac64 * pow2i(sh); } + else { mant = frac64 / pow2i(-sh); } + exp = 1023 + (bf - 65); + } + // 组装（mant 截断到 52 位——无舍入） + bits64 : int = 0; + if exp > 0 && exp < 2047 { + bits64 = (mant % 4503599627370496) + exp * 4503599627370496; + } + if neg != 0 { bits64 = bits64 + -9223372036854775808; } + return bits64; +} + fn add_tok(kind: int, lex: int, start_line: int, start_col: int) { grow_tokens(g_token_count + 1); tp := g_token_count * ESZ_TOKEN; @@ -236,8 +307,10 @@ fn tokenize(_src: string) { // Float: only consume the '.' when it does not start a '..' // range operator (otherwise `0..4` lexes as `0.` `.4` and the // range is silently lost — the for-loop body never executes). + has_dot : ., mut = 0; if cur_char_at(_src, _pos, _slen) == 46 && peek_at(_src, _pos, _slen) != 46 { _pos = _pos + 1; + has_dot = 1; loop { if is_digit(cur_char_at(_src, _pos, _slen)) != 0 { _pos = _pos + 1; } else { break; } } } // Suffix @@ -251,13 +324,18 @@ fn tokenize(_src: string) { suffix = str_sub(_src, ss, _pos - ss); } num_str := str_sub(_src, start, _pos - start - str_len(suffix)); - ival : ., mut = str_int(num_str); - if suffix == "u8" || suffix == "u16" || suffix == "u32" || suffix == "u64" { } - else if suffix == "i8" || suffix == "i16" || suffix == "i32" || suffix == "i64" { } - else if suffix == "f32" || suffix == "f64" { } - else if str_len(suffix) > 0 { } - if str_len(suffix) > 0 { add_tok(T_INT, -1, start_line, start_col); } - else { add_tok_int(T_INT, ival, start_line, start_col); } + // float 字面量（含小数点或 f32/f64 后缀）→ IEEE 754 binary64 位模式 + // 修复前 float 走 str_int（3.14 解析成 3，小数静默丢弃） + if has_dot != 0 || suffix == "f32" || suffix == "f64" { + add_tok_int(T_FLOAT, str_to_f64_bits(num_str), start_line, start_col); + } else { + ival : ., mut = str_int(num_str); + if suffix == "u8" || suffix == "u16" || suffix == "u32" || suffix == "u64" { } + else if suffix == "i8" || suffix == "i16" || suffix == "i32" || suffix == "i64" { } + else if str_len(suffix) > 0 { } + if str_len(suffix) > 0 { add_tok(T_INT, -1, start_line, start_col); } + else { add_tok_int(T_INT, ival, start_line, start_col); } + } _pos = skip_ws(_src, _pos, _slen); continue; } diff --git a/src/compiler/main.cr b/src/compiler/main.cr index 8bc524f..ac0f8ad 100644 --- a/src/compiler/main.cr +++ b/src/compiler/main.cr @@ -479,9 +479,16 @@ fn corec_main() -> int { } // === Pointer analysis + safety passes (always run, even at opt_level 0) === + base_diags := g_diag_count; ptr_analysis_all(); region_check_all(); provenance_verify_all(); + // 修复 5：编译期确定的越界（provenance 诊断）是硬错误——拦截编译。 + // 修复前诊断只记录不拦截，越界程序照常生成。 + if g_diag_count > base_diags { + print_diagnostics(); + return 1; + } // === build | ccr need lower_to_ccr === if g_opt_level >= 1 { diff --git a/src/compiler/provenance_verify.cr b/src/compiler/provenance_verify.cr index 85361c7..7e5195e 100644 --- a/src/compiler/provenance_verify.cr +++ b/src/compiler/provenance_verify.cr @@ -3,15 +3,27 @@ // Runs after PointerAnalysis (ptr_analysis.cr) and RegionCheck (region_check.cr). // Detects out-of-bounds pointer accesses at compile time. -fn get_alloc_size(alloc_node_seq: int) -> int { - op := r64(g_df_nodes, alloc_node_seq * ESZ_DFNODE + OFF_DF_OPCODE); - s1 := r64(g_df_nodes, alloc_node_seq * ESZ_DFNODE + OFF_DF_S1); - s2 := r64(g_df_nodes, alloc_node_seq * ESZ_DFNODE + OFF_DF_S2); - s3 := r64(g_df_nodes, alloc_node_seq * ESZ_DFNODE + OFF_DF_S3); +fn get_alloc_size(alloc_seq: int) -> int { + // 修复 3：alloc_seq 是 pts 位号（第几个 alloc），经映射表查 DF 节点序号再算大小。 + // 修复前直接当节点序号用 → 查到节点 0 → 恒返回 -1 → 运行时检查永不生成。 + if alloc_seq < 0 || alloc_seq >= g_pa_alloc_count { return -1; } + an := r64(g_pa_alloc_nodes, alloc_seq * 8); + op := r64(g_df_nodes, an * ESZ_DFNODE + OFF_DF_OPCODE); + s1 := r64(g_df_nodes, an * ESZ_DFNODE + OFF_DF_S1); + s3 := r64(g_df_nodes, an * ESZ_DFNODE + OFF_DF_S3); - if op == IR_ALLOC { return 8; } // scalar = 8 bytes - if op == IR_ALLOC_STRUCT { return 8 + s2 * 8; } // struct size - if op == IR_ALLOC_ARRAY { return s1 * s2; } // count * element_size + // 修复 12：IR_ALLOC（标量变量槽标记）不是堆分配——不返回 8（修复前把 + // 变量槽当 8 字节堆块，误报/误取 size） + if op == IR_ALLOC_ARRAY { return s1 * 8; } // count * 8（元素恒 8 字节，见 instr.cr IR_ALLOC_ARRAY） + if op == IR_ALLOC_STRUCT { + // 与 instr.cr IR_ALLOC_STRUCT 一致：fc * 8（field count × 8） + fi : int = -1; si2 : ., mut = 0; + loop { if si2 >= g_struct_count { break; } + if si_name(si2) == s3 { fi = si2; break; } + si2 = si2 + 1; } + if fi >= 0 { return si_field_count(fi) * 8; } + return 8; + } return -1; // unknown (defer to runtime check) } diff --git a/src/compiler/ptr_analysis.cr b/src/compiler/ptr_analysis.cr index bb3604d..ef70a7d 100644 --- a/src/compiler/ptr_analysis.cr +++ b/src/compiler/ptr_analysis.cr @@ -40,6 +40,16 @@ fn grow_alloc_pts(n: int) { g_alloc_pts = nb; g_alloc_pts_cap = nc; } +fn grow_pa_alloc_nodes(n: int) { + if n < g_pa_alloc_nodes_cap { return; } + nc := g_pa_alloc_nodes_cap; + if nc == 0 { nc = 16; } + loop { if nc > n { break; } nc = nc * 2; } + nb := alloc(nc * 8); + if g_pa_alloc_nodes_cap > 0 { _dyncpy(g_pa_alloc_nodes, g_pa_alloc_nodes_cap * 8, nb); } + g_pa_alloc_nodes = nb; g_pa_alloc_nodes_cap = nc; +} + // Set a bit in a pts bitmap at given index fn pa_set_bit(bitmap: int, bitpos: int) -> int { // bitpos: which bit to set (0-63) @@ -192,10 +202,21 @@ fn ptr_analysis_func(nstart: int, ncount: int, vstart: int, vcount: int) { if d >= 0 { // Addr: ALLOC/REF/ADDR_INDEX → self-pointer - if op == IR_ALLOC || op == IR_ALLOC_STRUCT || op == IR_ALLOC_ARRAY { + if op == IR_ALLOC_STRUCT || op == IR_ALLOC_ARRAY { + // 修复 12：IR_ALLOC（标量变量槽标记，不发射代码）不是堆分配， + // 不参与 pts 追踪——修复前它被分配 pts 位，导致 p = &arr[i] + // 的 pts 含变量槽的位（多个 alloc 位污染）→ s3 取错 alloc。 if r64(g_pts, d * 8) == 0 { - w64(g_pts, d * 8, 1); - changed = 1; + // 修复 3：每个 alloc 分配递增位号（bit = alloc_seq），并登记 + // alloc_seq → DF 节点序号。修复前恒设 bit 0——所有 alloc 别名 + // 串扰，provenance 的 get_alloc_size(0) 查到节点 0 → 检查永远不生成。 + if g_pa_alloc_count < 64 { + grow_pa_alloc_nodes(g_pa_alloc_count + 1); + w64(g_pa_alloc_nodes, g_pa_alloc_count * 8, ni); + w64(g_pts, d * 8, pa_set_bit(0, g_pa_alloc_count)); + g_pa_alloc_count = g_pa_alloc_count + 1; + changed = 1; + } } w64(g_offsets, d * 8, 0); } @@ -208,7 +229,26 @@ fn ptr_analysis_func(nstart: int, ncount: int, vstart: int, vcount: int) { if op == IR_ADDR_INDEX && s1 >= 0 { if pa_merge_pts(d, s1) != 0 { changed = 1; } - w64(g_offsets, d * 8, r64(g_offsets, s1 * 8)); + // offset 由索引 s2 决定：常量索引可精确计算（idx*8）， + // 运行时索引 → 未知（-1），迫使 provenance_verify 生成运行时检查。 + // 修复前：无条件传播 s1 的 offset（数组=0），运行时越界被误判为 + // 编译期安全 → 越界裸读（见 docs/compcert-reference.md 审查记录）。 + base_off := r64(g_offsets, s1 * 8); + idx_val : int = -1; + if s2 >= 0 { + prod := r64(g_df_var_producer, s2 * 8); + if prod >= 0 { + prod_op := r64(g_df_nodes, prod * ESZ_DFNODE + OFF_DF_OPCODE); + if prod_op == IR_CONST { + idx_val = r64(g_df_nodes, prod * ESZ_DFNODE + OFF_DF_S1); + } + } + } + if idx_val >= 0 && base_off >= 0 { + w64(g_offsets, d * 8, base_off + idx_val * 8); + } else { + w64(g_offsets, d * 8, -1); + } } // BINARY with PTR ops: propagate with offset @@ -234,11 +274,15 @@ fn ptr_analysis_func(nstart: int, ncount: int, vstart: int, vcount: int) { } } - // Copy: LOAD/STORE propagate pts along def-use - if (op == IR_LOAD || op == IR_STORE) && s1 >= 0 { + // LOAD: d ← s1 拷贝传播 + if op == IR_LOAD && s1 >= 0 { if pa_merge_pts(d, s1) != 0 { changed = 1; } w64(g_offsets, d * 8, r64(g_offsets, s1 * 8)); } + // STORE: s1 ← s2 拷贝传播。修复 4：IR_STORE 的 dest 恒为 -1， + // 原代码把 STORE 混进 LOAD 分支（用 d 传播）→ 永不执行 → + // p = &arr[i] 的 offset 丢失 → 越界检查被跳过。 + // 注意：此分支必须在 if d >= 0 块外（d 恒为 -1）。 // PHI: merge pts from both predecessors (implicit flow) if op == IR_PHI { @@ -253,6 +297,12 @@ fn ptr_analysis_func(nstart: int, ncount: int, vstart: int, vcount: int) { } } + // Store: s1 ← s2 拷贝传播（IR_STORE 的 d 恒为 -1，必须在 if d >= 0 块外） + if op == IR_STORE && s1 >= 0 && s2 >= 0 { + if pa_merge_pts(s1, s2) != 0 { changed = 1; } + w64(g_offsets, s1 * 8, r64(g_offsets, s2 * 8)); + } + // Store: *p = v (Andersen store rule) — s1=ptr, s2=val if op == IR_STORE_PTR && s1 >= 0 && s2 >= 0 { if pa_store(s1, s2) != 0 { changed = 1; } diff --git a/src/compiler/region_check.cr b/src/compiler/region_check.cr index d3c2b9d..3a49f4c 100644 --- a/src/compiler/region_check.cr +++ b/src/compiler/region_check.cr @@ -37,8 +37,11 @@ fn rc_pts_has_escaped(pts: int, ni: int, nstart: int) -> int { bi : ., mut = 0; loop { if bi >= 64 { break; } if (pts / mask) % 2 == 1 { - alloc_seq := bi + nstart; - alloc_sg := alloc_seq_to_sg(alloc_seq); + // 修复 3 配套：pts 位号 = 全局 alloc 序号（g_pa_alloc_count）， + // 经映射表查 DF 节点序号（旧代码 bi+nstart 是错误语义——alloc 序号 + // 不是"函数内第 nstart+bi 个节点"）。 + alloc_node := r64(g_pa_alloc_nodes, bi * 8); + alloc_sg := alloc_seq_to_sg(alloc_node); deref_sg := subgraph_containing(ni); if alloc_sg >= 0 && deref_sg >= 0 { alloc_exit := r64(g_sgs, alloc_sg * ESZ_SG + OFF_SG_EXIT); @@ -66,8 +69,8 @@ fn rc_return_escape(ni: int, s1: int, nstart: int) { bi : ., mut = 0; loop { if bi >= 64 { break; } if (pts / mask) % 2 == 1 { - alloc_seq := bi + nstart; - alloc_sg := alloc_seq_to_sg(alloc_seq); + alloc_node := r64(g_pa_alloc_nodes, bi * 8); + alloc_sg := alloc_seq_to_sg(alloc_node); if alloc_sg >= 0 { alloc_sg_kind := r64(g_sgs, alloc_sg * ESZ_SG + OFF_SG_KIND); if alloc_sg_kind == SG_FUNC { // function-level alloc = ok to return @@ -112,8 +115,8 @@ fn region_check_func(nstart: int, ncount: int) { bi : ., mut = 0; loop { if bi >= 64 { break; } if (pts / mask) % 2 == 1 { - alloc_seq := bi + nstart; - alloc_sg := alloc_seq_to_sg(alloc_seq); + alloc_node := r64(g_pa_alloc_nodes, bi * 8); + alloc_sg := alloc_seq_to_sg(alloc_node); deref_sg := subgraph_containing(ni); if alloc_sg >= 0 && deref_sg >= 0 { alloc_exit := r64(g_sgs, alloc_sg * ESZ_SG + OFF_SG_EXIT); diff --git a/src/stdlib/fmt.cr b/src/stdlib/fmt.cr index 0d51822..cfe418a 100644 --- a/src/stdlib/fmt.cr +++ b/src/stdlib/fmt.cr @@ -190,3 +190,82 @@ fn format2(fmt_str: string, a0: string, a1: string) -> string { fn format_int(fmt_str: string, val: int) -> string { return format(fmt_str, int_str(val)); } + +// ── float 打印（IEEE 754 double → 十进制字符串，定点最多 6 位小数）── +// 纯整数实现：提取符号/指数/尾数 → 规范化 → 整数部分 + 小数长除 + +fn fpow2i(k: int) -> int { + v : int = 1; i : ., mut = 0; + loop { if i >= k { break; } v = v * 2; i = i + 1; } + return v; +} + +fn float_str_bits(bits: int) -> string { + // 符号（bit63） + neg : int = 0; u : int = bits; + if u < 0 { neg = 1; u = u - (-9223372036854775808); } // 减 -2^63 = 清 bit63（无 & 运算符） + // 提取字段（除以 2^52 代替移位） + exp := (u / 4503599627370496) % 2048; + mant := u % 4503599627370496; + // 特殊值（IEEE 754 标准） + if exp == 0 && mant == 0 { + if neg != 0 { return "-0"; } + return "0"; + } + if exp == 2047 { + if mant == 0 { if neg != 0 { return "-inf"; } return "inf"; } + return "nan"; + } + // 归一化：m = 1.mant（正规）或 0.mant（次正规），e = exp - 1023 + m : int = mant; e : int = exp - 1023; + if exp != 0 { m = mant + 4503599627370496; } + else { e = e + 1; } + // value = m × 2^(e-52)（m 是 2^52 缩放的尾数） + ip : int = 0; + den : int = 1; // 小数分母（小数部分 = r/den） + r : int = 0; + if e >= 52 { + if e - 52 <= 10 { ip = m * fpow2i(e - 52); } + else { ip = m * 1024; } // 大数近似（超出 int 范围） + } else { + if 52 - e <= 53 { + den = fpow2i(52 - e); + ip = m / den; + r = m % den; + } else { + ip = 0; den = fpow2i(53); r = m; // 极小值 + } + } + // 长除：r × 10 / den，提取 7 位（第 7 位用于舍入） + frac_str : ., mut = ""; + r2 : ., mut = r; + di : ., mut = 0; + loop { if di >= 7 { break; } + r2 = r2 * 10; + dg2 := r2 / den; + if dg2 > 9 { dg2 = 9; } + r2 = r2 - dg2 * den; + if di < 6 { frac_str = frac_str + int_str(dg2); } + else if dg2 >= 5 { + // 第 7 位 ≥ 5：第 6 位 +1（简单舍入） + fl2 := str_len(frac_str); + if fl2 > 0 { + last := load8(frac_str, fl2 - 1) - 48; + if last < 9 { + pre := str_sub(frac_str, 0, fl2 - 1); + frac_str = pre + chr(last + 49); + } + } + } + di = di + 1; } + // 去尾零 + fl := str_len(frac_str); + loop { if fl <= 0 { break; } if load8(frac_str, fl - 1) != 48 { break; } fl = fl - 1; } + if fl > 0 { frac_str = str_sub(frac_str, 0, fl); } + // 组装 + out : ., mut = ""; + if neg != 0 { out = out + "-"; } + out = out + int_str(ip); + if fl > 0 { out = out + "." + frac_str; } + return out; +}