docs: 指针安全设计定论——类型双关自动验证 + crasm 硬件描述表 + TODO bug 7

TODO.md

@@ -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 记）

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 隔离，人工保证——表内标准部分仍自动验证）
 
 ## 当前状态
 

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、调度、验证。