feat: float 完整支持（IEEE 754/SysV）+ 对照 CompCert 审查修复 16 bug

DEBUG_REPORT.md

@@ -3,7 +3,7 @@
 > 日期: 2026-07-06
 > PR: https://github.com/dslsdzc/core/compare/main...RhineIris:core:main
 >
-> **⚠️ 历史存档**：本报告描述的问题均已在后续修复中解决——
+> ** 历史存档**：本报告描述的问题均已在后续修复中解决——
 > 文中 3 个已修复 Bug 已合并（PR #9/#16 时期）；"仍未解决的根本性 Bug"
 > （rip_patch 位置错位）已由 2026-07-23 P0 全量修复（`emit_instr()` disp32
 > 写入补上当前指令基址）解决，corec2 → corec3 自举现已全程通过。
@@ -114,7 +114,7 @@ fn tokenize() {
 PATCH gvi=698 ppos=74669 off=5584 target=4736480 rel=467503
 PATCH gvi=698 ppos=74751 off=5584 target=4736480 rel=467421
 PATCH gvi=698 ppos=74845 off=5584 target=4736480 rel=467327
-... (16 total, all target=4736480 ✓)
+... (16 total, all target=4736480 )
 ```
 
 - `off=5584` → 全部一致
@@ -188,8 +188,8 @@ syscall3(1, fd, g_elf_buf, sz);
 
 | 位置 | 期望值 | 实际值 | 状态 |
 |------|--------|--------|------|
-| buf[500000] | 0x12345678 | 0x12345678 | 保留 ✓ |
-| buf[74717] | 0xCAFEBABE 或 0xDEADBEEF | 0x458948ff | 覆盖 ✗ |
+| buf[500000] | 0x12345678 | 0x12345678 | 保留  |
+| buf[74717] | 0xCAFEBABE 或 0xDEADBEEF | 0x458948ff | 覆盖  |
 
 - 标记 1（位置 500000）→ **保留成功**，说明 buffer 在 elf_gen 返回后没有被整体污染
 - 标记 2（位置 74717）和标记 3（位置 74717）→ **都被覆盖**，最终值是原始指令代码

TODO.md

@@ -30,7 +30,7 @@
 - emit_alloc_body 零初始化 + 链式扩容标记满
 
 ### @ 内建原语（12 个全部完整）
-- `@sizeOf(T)` / `@alignOf(T)` — 编译期常量，ELF 验证 8 / 1 ✅
+- `@sizeOf(T)` / `@alignOf(T)` — 编译期常量，ELF 验证 8 / 1 
 - `@fields(T)` — 遍历 struct fields，返回逗号分隔名字符串
 - `@hasField(T, name)` / `@field(T, name)` — 结构体字段存在性 + 偏移量
 - `@typeInfo(T)` — 类型名称字符串
@@ -84,10 +84,10 @@ RVSDG 式嵌套 region 已落地（规格 docs/superpowers/specs/2026-08-08-regi
 - 仅增加 mmap 扩容会让热缓存路径增长到约 7.6 GiB RSS 并触发 WSL OOM；需要按函数回收临时 IR/缓存数据，而不是继续扩大堆
 
 ### 2. 并发集成：单 M 已端到端验证，多 M 未验证
-- ✅ `go f(args)` 端到端已通：`sched_go(@addr(f), arg)` → g_new 存 saved_fn/saved_arg → 静态构建由 ELF 后端内联发射 fiber_init/fiber_switch/goroutine_entry_wrapper（不再依赖 rt.s 链接）→ wrapper 调用 saved_fn(saved_arg) → 结果经 result_ch 回传
-- ✅ 主线程注册为 G 0，可经 channel 阻塞/唤醒；sched_yield 不再重排 Gwaiting
-- ⏳ M 线程 worker loop（m_start_workers）未连到调度器完整测试——静态构建尚未内联发射 m_start_workers（rt.s 符号）
-- ⏳ channel wait queue 链表操作未在多线程并发下验证
+-  `go f(args)` 端到端已通：`sched_go(@addr(f), arg)` → g_new 存 saved_fn/saved_arg → 静态构建由 ELF 后端内联发射 fiber_init/fiber_switch/goroutine_entry_wrapper（不再依赖 rt.s 链接）→ wrapper 调用 saved_fn(saved_arg) → 结果经 result_ch 回传
+-  主线程注册为 G 0，可经 channel 阻塞/唤醒；sched_yield 不再重排 Gwaiting
+-  M 线程 worker loop（m_start_workers）未连到调度器完整测试——静态构建尚未内联发射 m_start_workers（rt.s 符号）
+-  channel wait queue 链表操作未在多线程并发下验证
 - 注意：G 结构 offset 56 同时用作 saved_fn（goroutine.cr）与 temp_val（chan.cr 等待队列 handoff）——单 G 流程可用（wrapper 在 chan 操作前读取 saved_fn），但字段语义重叠，重构时需拆分
 
 ### 3. 解释器局限
@@ -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 风格最短表示

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"

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