Adler-32：有界求和与模运算细化

源代码是固定版本的 zlib/adler32.c，对应模块为 ZlibF/Zlib/adler32.c.lean。数学契约是格式指南中的 F-adler-incremental。API 指南规定空缓冲区、包装函数与组合操作。

本页按读取范围、批次算术和初值范围，展开 adler32_z 的证明路线。进度记录验收结果和当前范围。

单字节递推

校验和用两个运行和概括已经读过的字节。B = 65521 是约减用的模数；NMAX = 5552 是两次约减之间最多处理的输入字节数。先把机器中的输入累加器拆成 a = adler & 0xffff 和 s = (adler >> 16) & 0xffff。这里 a、s 是机器中保存的两个分量，α、σ 是模 B 的数学分量；b 是下一个字节的数值，范围为 0 到 255。数学步骤为：

α' = (α + b) mod B
σ' = (σ + α') mod B

未约减的机器步骤是 a' = a + b; s' = s + a'。若机器求和未回绕，a ≡ α (mod B) 与 s ≡ σ (mod B) 可推出步骤后的相同同余关系。再模 B 约减即可恢复准确的数学数对。

因此证明分成两部分：机器安全地遍历正确字节；其求和在所述初值定义域上细化模递推。

读取与终止

输入指针由对象和对象内起始偏移 off 定位，len 是当前请求的字节数，len₀ 是进入本次遍历时的初始字节数。若缓冲区非空，要求整个 [off, off + len) 范围可读。用 k 计数已经消费的字节，遍历不变量为：游标是 off + k，剩余数量是 len₀ - k，且 k ≤ len₀。每次读取时都有 k < len₀；每次指针递增最多到达末尾后一位置。

后减测试可能在最后一次失败测试时使局部无符号计数器回绕。证明必须准确建模这个测试；回绕值不代表又执行了一轮循环体。度量不仅要证明数学终止，还要满足翻译后的步数预算界限。

单字节快速路径在空缓冲区检查之前。初始化查询要求 buf == NULL 且 len == 0，不读内存而返回 1。其他调用要求可读的非空范围。该函数不写调用者内存，也不分配块。

默认构建的批次与无回绕界限

证明推迟约减安全，需要先界定机器整数在一个批次内能增长多少。用 j 表示自上次约减以来处理的字节数，范围为 0 到 5552。从 16 位分量出发，执行 j 步后可使用以下界限：

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

当 j ≤ 5552 时，得到 a ≤ 1481295 和 s ≤ 8224215375，均低于 2^64。默认 LP64 的 unsigned long 加法因此与普通自然数算术一致。这个宽松界限专用于 64 位论证；其他字长必须针对其分支建立合适界限。

16 字节展开把单字节不变量连续保持十六次。将它应用于各完整批次和尾部，然后约减，得到打包结果 a | (s << 16)。移位和打包也需要机器位宽界限。

准确的初值范围

正常的增量校验和从已约减的分量出发。但公开函数也接收整数累加器，正确性声明必须说明如何解释非规范分量。

短分支的低分量满足 a ≤ 65535 + 15 × 255 = 69360 < 2B，一次条件减法足以约减；高分量则模 B 约减。单字节分支对两个分量各只执行一次条件减法。以这种方式约减高分量，要求输入 s < B：新的低分量低于 B，两者之和才低于 2B。

因此，直接的递推论证覆盖 len ≠ 1 时的任意累加器字，以及输入高分量低于 B 时的单字节情形。空缓冲区返回还须单独处理。这只是论证范围，不授权缩小固定公开目标。

这个差异可以观察到。对于 adler32_z(0xFFFFFFF0, "\0", 1)，掩码后的低分量为 65520，高分量为 65535。字节步骤后的和是 131055，减一次得到 65534，函数返回 0xFFFEFFF0。完整模约减会使高分量等于 13。该调用内存安全；若规范对任意初值字都执行完整约减，就会给出不同结果。审查准确契约时应保留这个反例。

包装函数与组合

adler32 转换长度参数后沿用字节算法。combine 函数需要单独的算术证明：展开拼接时的两项运行和，加入初值修正，并说明翻译后的约减确实计算该公式。有符号长度的拒绝行为和位宽转换属于各自 API 契约，不能从 adler32_z 的内存安全直接推出。

早期工作为字节算法提供过 Lean 论证。复用时必须对照当前模块检查声明、机器位宽、所选补丁、执行关系和前置条件。方法解释非空泛性与变异检查要求。