堆表审阅记录

这份历史审阅覆盖从函数表到数组支撑的 Tbl 值和 Space.modify 的迁移。在检查过的代码中未发现错误的原语结果，但识别出表相等性与求值成本的重要差异。它不是独立基线批准或当前缺陷清单。当前工作见进度。

范围与方法

审阅检查 Runtime/Space.lean（Tbl、upd、Space.modify）、Ptr.lean、Alloc.lean、Tables.lean、生成的 Space 实例、模式生成器、可信基础说明和审计锁。构建运行时模块后，用 Lean 4.35.0 编译了小例子。临时例子导入 ZlibF.Runtime.Alloc。没有修改源码。完整审计、见证构建和差分套件没有重跑。审阅引用了此前记录的审计通过结果，但当时及本次文档重写都没有复现它。

这里的表把分配编号映射到对象：get 读取表项，put 或 upd 更新表项，“存活”表示对象尚未释放。表内槽位是否存在，与 zlib 对象是否仍存活，是两个不同的问题。

审阅发现 get、put、upd、存活性、槽使用、新鲜性、分配和释放具有与函数表相同的逐项行为。结构相等性和资源使用不同。下列例子保留审阅证据，不声称已在后续修订上重跑。

已检查的操作

F1. 结构相等强于逐项一致

历史严重程度：低风险，涉及完备性和命题设计。Tbl 保存数组。在末尾之外写入默认值会扩大数组，即使全部可观察条目不变。因此，不存在一个外延性定理能把所有逐项相同的表认定为相等。

审阅编译了这些反例：

theorem neq : upd (Tbl.empty : Tbl (Option Nat)) 3 none ≠ Tbl.empty := by
  intro h
  have := congrArg (fun t => t.arr.size) h
  simp [upd, Tbl.set, Tbl.empty] at this

example : ¬ ∀ (t : Tbl (Option Nat)) k, t k = none → upd t k none = t := by
  intro H
  exact neq (H Tbl.empty 3 (by simp))

example : ¬ (∀ (a b : Tbl (Option Nat)), (∀ k, a k = b k) → a = b) := by
  intro H
  have := H (upd Tbl.empty 3 none) Tbl.empty
    (by intro k; by_cases k = 3 <;> simp_all [upd_apply])
  exact neq this

upd Tbl.empty 3 none 的数组大小为四。分配一个字节再释放后，字节表保留一个 none 槽。因此，分配／释放后精确恢复堆，与恢复存活对象和表项，并不是同一个命题。

表相等性前提也可能比逐项条件更窄。审阅在 Schema.lean 之外的搜索未发现这种假设；检查过的命题锁中的表相等性都出现在结论中。这个搜索是有范围的证据，不是定义域不会空洞的一般保证。错误的恢复目标属于需单独审阅的规范问题，不能悄悄弱化以完成证明。可信基础解释相等性的区别。

F2. 大块编号导致成比例的数组分配

历史严重程度：低风险，涉及求值成本。Tbl.set 的扩展分支填充到所选下标。编译例子中，将空表的下标 3,000,000 设值，会产生 3,000,001 个槽。从空堆开始，分配编号逐一增加，表大小受分配次数限制。手工构造巨大 nextBlk 则可能在求值或内核约简期间需要巨大数组。这是测试／见证的资源风险，不是错误数学结果。审阅过的不变量没有限制 nextBlk。

F3. 注释仍描述函数表闭包

历史严重程度：低风险，涉及文档。旧 Space.lean 头部将 upd 描述为更新函数。deflate、inflate 和回调 inflate 的驱动注释描述闭包压紧和展开。其重建步骤保留每个条目，却可能改变结构相等性。驱动不比较表，因此没有发现错误观察。这些是审阅时的注释发现；后续文字必须另行评估。

F4. 类法则只约束存活引用的修改

历史分类：提示性；审阅尚未找到需要额外法则的调用者。在下面的类法则中，h 是内存状态，r 是对象引用，a 是读出的对象值，f 是更新该值的函数。Space.modify_eq 假设 get h r = some a，不说明死亡引用的修改。生成实例安全处理死亡引用，审阅过的原语先检查存活性。后续未经检查的调用者不能仅凭这个类法则推导死亡引用行为。建议增加的法则是 get h r = none → modify h r f = h；检查过的调用者并不需要它。

F5. 锁覆盖定义，但缺少定向负向自测

历史严重程度：低风险，涉及检查覆盖。检查过的可信锁覆盖 C.Tbl、其数组字段、get/set/modify/empty、强制转换和默认实例、C.upd、C.Space、Space.modify，以及生成实例和辅助声明。类型与值的指纹包含 Space.mk 中的 modify_eq 字段。辅助定理经过内核检查和公理审计，而非语义锁定。

已有的运行时触碰和运行时弱化取巧样例测试一般机制。审阅没有发现定向样例，例如使 Tbl.get 忽略数组，或使修改复活死亡块。未执行对这些变异的检测，因此尚缺对这些具体变异的检测结果。这不是弱化审计的许可。

F6. 释放的槽仍占用模型表的存储

历史分类：提示性。块编号从不复用。释放用 none 替换条目，不缩小数组。每个使用过的表因此保留到其最大已分配块编号为止的槽。旧闭包表示有相同的增长阶，常数更差。这是从不复用模型的性质，与已证明的存活 zlib 对象所有权不同。

对后续审阅的启示

将对象级帧性质和所有权结论，与表示层的存储相等性分开。像审阅空堆运行一样仔细审阅任意堆前提。要求在原位修改前检查存活性，并保留类法则与特定生成实例之间的区别。编译例子和源码搜索帮助测试这些边界，不能建立整个运行时对 C 的忠实性，也不能替代独立批准。