保持行为不变地翻译 C
360edabd301b7e17 · 对应提交的原文 ↗翻译逐语句保留选定的 C 程序。证明困难不能成为重排检查、缓存读取、合并语句或替换算法的理由。不匹配就是翻译缺陷：应按 C 修正，并加入差分回归测试。差分测试提供忠实性的证据，不是证明。
架构解释对象堆，可信基础记录其语义限制。准确记录字段和指针种类见生成的运行时结构参考。
翻译前固定源码
翻译默认 x86_64 Linux 静态构建，使用 LP64 位宽。预处理选择必须针对 zlib/ 加上按顺序应用的补丁解析，不能针对未应用补丁的检出版本或另一种配置。源文件映射为同名加 .lean：zlib/X.c 对应 ZlibF/Zlib/X.c.lean，头文件同理。
保留 C 函数名。文档字符串以准确 C 签名开头，包括存在的 static。每个辅助函数有独立定义。Lean 定义可以按依赖排列，但函数内部语句保持 C 顺序。为翻译块注释其对应 C 代码。状态机还应记录哪些状态对应 C 标签。
保留求值和算术
例如，若 C 先检查索引再读取数组，翻译也必须先检查。将读取提前，即使最终返回值相同，也可能把原本被检查挡住的越界访问变成可达操作。证明因此需要保留中间步骤，而不只是对比函数最后的结果。
按源码顺序展开宏。保留读写、分支条件、提前返回和短路求值。显式应用整数提升和通常算术转换。例如在本目标上，unsigned short + int 以 int 计算。
| C 类型 | LP64 上的 Lean 类型 |
|---|---|
unsigned char |
UInt8 |
unsigned short |
UInt16 |
unsigned, unsigned int |
UInt32 |
unsigned long, size_t, z_size_t |
UInt64 |
int |
Int32 |
long, z_off_t, z_off64_t |
Int64 |
无符号操作按位宽回绕。有符号操作必须检查可表示性。移位必须检查 C 操作数位宽与计数，包括负数计数。Lean 的全定义算术本身不能证明 C 操作有定义。
枚举值为无符号状态字段提供 UInt32 名称，为 C int 用法提供带 _i 后缀的 Int32 名称。宏与枚举值冲突时按需使用 GZ_<name>：GZ_COPY 命名 gzguts.h 宏，COPY 命名 inflate.h 枚举值。
每个对象只表示一次
| C 对象或操作 | 表示 |
|---|---|
| 结构体 | 对应种类的堆表中的记录，通过块标识引用 |
p->f / p->f = v |
记录字段读取/更新，不使用 ABI 偏移算术 |
| 内嵌数组 | 数组字段；复制记录也复制数组 |
| 指向内嵌数组的指针 | 命名记录、字段和索引的引用构造器 |
| 字节缓冲区 | 堆字节块与偏移 |
head / prev 字数组 |
堆字块与元素偏移 |
| 静态表 | 静态引用或经过检查的常量表；写入会故障 |
| 被取地址的局部对象 | 在声明位置表示存储，保留自动生命周期，并在每个返回前清理 |
| 字符串字面量 | 指向封闭只读源码字面量表的 strLitRef；不分配 |
ZALLOC / ZFREE |
默认分配器操作，包括失败预言机；自定义分配器不在所选模型内 |
结构定义从 C 头文件生成。翻译者通过经过审阅的运行时流程请求添加结构，不能另造一套记录布局。生成的数组字段仍需要声明长度的事实。会分配的定理还携带 Fresh，保证分配不会覆盖现有对象。
自动局部存储不能消耗分配失败索引。赋予它 ZALLOC 语义会改变哪次真实分配失败。同样，被取地址的局部对象不能在其 C 生命周期结束后仍存活。
显式处理新鲜内存
新鲜整数内容是任意值。定理必须对每个值成立，包括读取或复制 prev 已初始化部分之外或匹配前瞻区域的值。不能把这些内容替换为零。
本模型的新鲜指针字段为 NULL，比不确定的 C 指针更弱。每次读取新分配记录的指针字段，都应在翻译注释中指出此前的写入语句，并在证明中建立顺序。与 NULL 比较、复制和释放 NULL 都不能检测未写入字段。不能因为 Heap.garbage 给单元稳定值，就假设 C 对未初始化单元的重复读取一致。
X.zeroed 表示实际的整记录清零语句，X.garbage 表示新鲜内容，两者不能互换。见安全性第 3 节。
使用匹配的库操作
| C 操作 | 翻译规则 |
|---|---|
字节 memcpy / zmemcpy |
memcpyB；保留范围与不重叠检查 |
整记录 memcpy |
copyK dst src；它会检查重叠，与直接读取再写入不同 |
memmove |
对应的移动操作，允许重叠 |
字节 memset |
memsetB |
| 清零较宽元素数组 | Ptr.fill p 0 n，使用正确元素数 |
用字节 c 填充较宽元素数组 |
Ptr.memset p c n，在每个元素内重复 c |
| 整记录清零 | stK p X.zeroed |
memcpy 既复制已初始化值，也复制任意值。即使长度为零，运行时遇到 NULL 仍故障。建模的库操作按元素计数，C 字节计数必须正确转换。Libc.lean 和生成的 LibcTables.lean 定义这些操作；可信基础列出它们与 C 的差异。
让控制流保持可见
循环通过运行时循环或有界递归，在显式状态中携带局部变量。do … while 先执行主体再检查条件。循环内的 break、continue 和返回使用控制标签，保留各自不同的目的地。必要时，goto 和 switch 贯穿使用显式程序计数器。
循环额度不允许提前终止。耗尽会引发 Fault.outOfFuel，终止证明必须排除这种结果。在已记录模型差异的前提下，每个可达未定义操作都必须保持可见为 Fault.ub。包括指针边界、存活性、只读写入、无效比较、有符号算术和重叠复制。
让改动可审阅
交付镜像源码模块、函数级差分测试，以及带对应 C 行的翻译决定记录。在拉取请求中报告实际运行的检查。审计和变异证据遵循检查指南。运行时改动需要独立审阅，因为所有函数证明都依赖其语义。
若证明暴露可能的上游缺陷，应保留公开定义域。区分证明技巧问题、错误规范、翻译不匹配与真实 C 缺陷。最后一种必须先有具体输入和 sanitizer 复现，才能称为确认的发现。
选定的源码分支
输入配置配色固定在默认 x86_64 Linux LP64 构建上。改变输入参数并不会启用另一种已编译算法。
| 源码类别 | 选定分支 |
|---|---|
| 压缩 | 启用 gzip；禁用 FASTEST、LIT_MEM、UNALIGNED_OK 和调试检查；默认 MAX_WBITS 15、MAX_MEM_LEVEL 9。 |
| 解码表和 inflate | 启用 gzip 与快速解码；禁用 BUILDFIXED、MAKEFIXED、PKZIP_BUG_WORKAROUND、INFLATE_STRICT 和无效距离恢复。固定表项来自 inffixed.h。 |
| CRC | 静态表；编织参数 N=5、W=8。默认小端执行不经过大端分支。 |
| Gzip 文件 | LP64 大文件入口和 C99 格式化；未选择 Windows/宽字符和 Z_SOLO 路径。单次 I/O 请求以 2^30 为界。 |
文件专用的语句顺序与别名检查放在相应组件证明指南旁。外部 I/O 模型单独记录系统调用与格式化限制。相关表示与执行论证需要逐项连接所选分支中的实际操作。