校验和的证明思路

假设应用在第一个缓冲区提供 A，在第二个缓冲区提供 B。Adler-32 递推告诉我们最终校验和是 00c60084，CRC-32 则是 30694c07。但这笔计算本身还不能说明 zlib 恰好读取了每个请求字节一次，把第一次结果接入第二次调用，或者没有越界访问就返回了。C 还为短输入、延迟约简、查表和对齐字读取安排了不同路径。证明必须把每条所选路径连接到同一字节含义。

证明既要描述字节，也要描述程序从哪里读它们。调用者的“堆”记录已有内存对象和其中的内容；指针选中首字节，长度计数本次请求的字节。“种子”是更新之前传入的校验和，正常情况下来自上次调用的结果。这些输入须满足入口明确写出的定义域。结论包含精确返回值和不变的堆。要理解它能为应用保证什么，需要分开三个问题：

即使数值计算完全正确，读错缓冲区仍然只会得到错误数据的校验和。反过来，可读缓冲区配上伪造种子也可以安全执行，但结果未必表示“整个流的校验和”。证明要让这两个区别都可见。

独立递推

第一步是先定义答案，不借用实现的优化。独立的 格式定义 用逐字节模更新定义 Adler，用逐字节 XOR 和八个反射位步骤定义 CRC。两个定义都不调用翻译后的校验和函数或它的表。因此，即使 C 算错了某张表，也不能让预期答案跟着一起变错。

对字节序列“折叠”，指从种子出发，依次对每个字节应用更新步骤。把第一段称为 X，第二段称为 Y。先在 X 上折叠，再在 Y 上折叠，等于在连接序列 X ++ Y 上折叠。这建立模型层的增量含义，尚不能说明指针循环访问了相同列表，或展开算术计算了相同步骤。

执行在实际堆上补齐这些事实。用 off 表示初始数组偏移，k 表示已经读取的字节数。循环不变量连接三件事：指针位于 off+k；还有字节时，下次读取仍然合法；寄存器表示请求字节的前 k 项。初始化在零次读取时建立它，单步保持它，退出时得到完整请求序列。

例如，短 Adler 分支维护两个和：adler 累加字节值，sum2 累加每次更新后的第一个和。buf 指向下一个字节，len 计数还剩多少字节。BASE 是 Adler 的模数 65521；MOD28 是取余宏，在所选默认构建中实现为除以 BASE 取余。这个分支实际包含下面几行，来自固定版本 adler32.c 的 85–94 行：

    if (len < 16) {
        while (len--) {
            adler += *buf++;
            sum2 += adler;
        }
        if (adler >= BASE)
            adler -= BASE;
        MOD28(sum2);            /* only added so many BASE's */
        return adler | (sum2 << 16);
    }

len < 16 只选择路径，本身不保证 buf 可读。while (len--) 检查旧计数，因此只有仍有字节时才执行循环体。*buf++ 先读当前字节，再前进指针；下一行使用更新后的第一个和。旧计数为零时，无符号后减会回绕，但不会再进入循环体；把这个回绕理解成负计数，就改变了 C 的含义。证明把实际循环关联到已读次数这个自然数，再论证余下各行：一次条件减法约简 adler，MOD28 约简 sum2，返回语句把两者装进低半和高半。对单个两字节 AB 缓冲区，两次迭代得到熟悉的 (132,198) 分量。若分成两次单字节调用，则会走前面的快速路径；执行证明必须覆盖这两条路线。

机器算术

循环不变量必须描述机器真正执行的算术。Adler 的数学模数是 65521。机器无符号溢出使用二的幂作为模数。它们不可互换：2^32 mod 65521 = 225，因此约简前一次未被发现的 32 位回绕，就可能改变期望结果。“C 允许无符号回绕”只能说明该操作被允许，不能说明结果符合 Adler 递推。

所选 LP64 构建中的指针和 unsigned long 都是 64 位，因此 Adler 加法使用 64 位 unsigned long。令 a、s 为尚未约简的第一、第二个和，j 为一批中已读的字节数。从掩码后的 16 位种子分量开始，经过至多 5552 个步骤，一个方便使用的界为：

a ≤ 65535 + 255j
s ≤ 65535 + j(65535 + 255×5552)

当 j≤5552 时，它们给出 a≤1481295、s≤8224215375，均小于 2^64。所以加法与自然数算术一致，再由同余关系支持延迟约简。Adler 章节中的批次上限 NMAX = 5552 表示两次取余之间最多处理的字节数，其推导假设 32 位的和与已经约简的分量；这个更宽的界也容纳数值执行论证中的掩码后任意种子。

CRC 使用另一种算术：每个位是取零或一的系数，相加就是不带进位的 XOR，这称为 GF(2) 算术。Lean 中的 UInt32 表示 32 位无符号值，对它做 XOR 和逻辑右移，就直接实现了 CRC 的寄存器步骤。表证明必须说明每个条目等于对应的八次多项式位步骤；只证明有 256 个条目，没有建立任何数值含义。字递推还要跟踪加宽临时值、字节顺序和最终 32 位投影。因此，Adler 算术论证的关键是未约简和的界，CRC 的关键是同一位变换的不同表示彼此相等。

内存视图

接着把字节序列连到内存。offset 是首字节位置，length 是请求数量，array.size 是包含它们的字节对象大小。可读性要求 offset+length≤array.size，解引用在终点之前发生。例如，五字节对象中，偏移为 3、长度为 2 时，可以读取位置 3、4；位置 5 只是终点，不能读取。空区间可以使用对象的 one-past 指针，即紧接最后一个字节之后的位置。两个更新都保留整个堆和所有权：只读输入，不分配，也不保留调用者指针。

CRC 的八字节读取需要地址为八的倍数。这不仅取决于数组索引，还取决于对象起始地址。模型让分配的字节块从对齐地址开始；静态和嵌入数组的起始地址除以八，则可以有任意但固定的余数，这就是“原点余数”。一般字节视图定理 覆盖这些已表示的视图和余数。它不证明一般的机器 ABI，也不覆盖所有有效类型别名。

CRC 章节的字读取路径给五条交织通道各分配一个八字节的字，合起来是一块 40 字节。它的入口阈值为 47 字节：最多处理七个字节就能达到对齐地址，因此仍至少留下一整块。这在执行前减块循环之前非常重要。行索引小于 8，字节索引小于 256，64 位字中的提取移位最多为 56 位。这些事实支持访问；多项式不变量支持表内容和合并的正确性。

平台前提 要求每个表示的字节对象小于 2^63 字节，不限制流总长度。不能把它悄悄加入定义域更广的校验和命题。一般 C 对齐、转换和别名对应关系仍记在 可信基础 中。

组合长度

继续更新需要字节，组合需要两个校验和及第二段长度。如果 A、B 独立计算过，Adler 组合应得到 00c60084，CRC 组合应得到 30694c07，期间不读取任何一个缓冲区。证明既要覆盖精确的标量计算，也要把输入关联到真实序列。第二段长度错误仍会算出一个数，却没有连接后的保证。

Adler 组合展开两个独立开始的分量和，去掉重复的初始一，核算第一块对新前缀的贡献。实现对非负长度取余，必须保持这项长度贡献；负长度则走独立的拒绝分支。

CRC 组合要先把第一段的贡献推进到第二段之后。把第二段的字节长度称为 n，把一个零输入位对应的寄存器步骤称为 T。于是 T^(8n) 表示执行 8n 次这个步骤，因为每字节有八位。这个前进操作既能用二进制矩阵表示，也能用模 CRC 多项式的乘法表示。

所选源码使用多项式乘法：multmodp 的两个输入用低 32 位编码多项式余数，生成的算子则编码所需的 n 字节前进操作。x2n_table 保存的幂，让实现能够按 n 中置位的位置组合出算子，不必执行 8n 个独立步骤。证明要把这些预计算幂和每次实际乘法连接到独立的位递推。

终止性具有真实的定义域条件。在固定版本 crc32.c 的 166–175 行，multmodp 从位 31 开始扫描。只有找到一个置位、且其下方再无置位时，才可能跳出。如果操作数的低 32 位全为零，扫描掩码不断右移也永远到不了这个跳出条件。因此，任意非零 64 位整数并不足够。

算子生成定理会在乘法之前建立低位所需的事实。因此，crc32_combine_op 契约 使用生成的算子，包括零拒绝结果。C 的 969–972 行在生成算子为零时，先返回零，不调用 multmodp。对有效的正算子，证明使用已经证明的乘法结果，不能假定被调函数契约成立。

查询与种子定义域

种子是调用者传给更新函数的校验和值。短例子通常使用初始种子：Adler 为 1，CRC 为 0。公开数值定理还必须解释其他种子字、空区间和查询参数。这些情况都要按实际分支顺序阅读。

Adler 的 70–82 行单字节快速路径位于 NULL 检查之前：长度为一时，先读 buf[0]，才可能到查询分支。本项目显式的初始化查询定义域是 NULL 配合零长度；该限制记在 偏离说明 中。CRC 先检查 NULL，对任何提供的长度都返回零。非 NULL 的空 CRC 更新保持传入的低 32 位。

Adler 还要区分正常校验和与伪造种子字。对于 adler32_z(0xfffffff0,"\0",1)，掩码后的分量为 65520 和 65535。低半的 65520 是第一个和，高半的 65535 是第二个和。加上零字节后，第一个和不变，再把它加进第二个和，得到 131055；一次条件减法留下 65534，产生 0xfffefff0。若先完整约简起始分量，高分量则会是 13。这个调用内存安全；朴素的任意种子功能命题却是错的。

数值规格 adlerValue 保留这个单字节行为，并在其他长度下规范化起始值。真实增量种子与普通递推一致。入口宽度、非 NULL 空区间、负组合长度和生成算子需要不同的情况划分。

精确结果

源码修订 e8232b1bfb90938be902ef226c7dc7436a2f07c0 包含下列结果命题与证明。链接用于核对它们的范围；当前登记和接受证据由进度维护，不能从这些页面的算例推断。

adler_z_public 与 adler_public覆盖所有表示中的可读区间和全部种子，显式的零长度 NULL 查询、精确数值结果与不变的堆。Adler 组合结果 给出标量参数的全执行、负长度拒绝，以及当校验和与第二段长度描述真实序列时的连接结论。

CRC 更新结果 保留固定全局表前提和完整的已表示字节视图定义域。CRC 组合结果 覆盖生成器、生成算子的应用和两种组合宽度，并给出精确多项式结果与不变的堆。get_crc_table 另外规定静态指针及全部 256 个条目。

这些范围没有建立完整压缩器或解压器的结论：调用者还必须对恰好已接收或已产生的字节计算校验和，并验证相应封装字段。完整定义域的 C 对应证明未完成：参考文档中列出的地址、对齐、转换与别名边界仍需分别建立对应关系。进度 维护当前登记和接受证据；组件论证 提供详细推导。