参考文档 / ZLIB × LEAN

adler32

用 32 位字节计数更新 Adler-32。

此页源文件快照 · 57ad356e10ec68ee · 对应提交的原文 ↗

先看本函数的前置条件和返回结果；可展开下方共同规则，查看整组接口的缓冲区与所有权要求。

uLong ZEXPORT adler32(uLong adler, const Bytef *buf, uInt len);

用 32 位字节计数更新 Adler-32。

定义域 受限定义域。当 buf 非 NULL 时，效果为只读。

前置条件 buf 为 NULL 且 len == 0，或它指向 len 个可读字节。要满足校验和后置条件，adler 的低 32 位须为 A 的 Adler-32。

返回与保证 返回值与 adler32_z(adler, buf, len) 完全相同。 NULL、零长度查询返回 1。非 NULL 的空范围保持校验和值的低 32 位。

内存与状态效果 保持全部内存与所有权。只读取给定范围。零长度范围允许使用尾后指针。

长度最多为 2^32 - 1。把更大长度转换为 uInt 会在调用前丢弃高位；更大范围应使用 adler32_z 或分多次调用。 adler32_z 关于零长度 NULL 查询和伪造种子的范围同样适用。

本组共同前提与范围

API 手册 · 契约约定 · 缓冲区工具

逐块计算缓冲区的校验和，或合并独立处理的字节序列的校验和，而不重新读取数据。下文的字节序列 A 和 B 是普通数据；契约使用这些序列的 Adler-32 或 CRC-32。例如先处理 A，再处理 B，可以把 A 的校验和作为下一次更新的起始值；若 A、B 已在不同位置独立处理，也可以用组合接口得到 A 后接 B 的校验和。

更新函数里的 buf 指向这一批输入，len 是这一批的字节数，传入的 adler 或 crc 是继续计算的起始值。组合函数里的 len2 则只表示后一段 B 的字节数，不是两段总长度。

任务	入口
更新 Adler-32	大小类型长度、32 位长度
合并 Adler-32	普通偏移类型、显式 64 位偏移类型
更新 CRC-32	大小类型长度、32 位长度
合并 CRC-32	普通偏移类型、显式 64 位偏移类型
复用 CRC 合并算子	生成、用 64 位长度生成、应用
查看字节表	get_crc_table

这些聚焦契约对应固定版本源码及登记补丁，在默认 LP64 Linux 静态构建下的 adler32.c、crc32.c 和 zlib.h。所有校验和入口都不写入状态、不分配或释放内存，也不执行 I/O。特殊数值结果是普通值，而不是错误码。定义域和效果互相独立，见契约约定。超出聚焦前提只表示本契约不作保证，不自动等于 C 未定义行为（UB），也不保证一定返回错误码。

实用校验和契约使用真实字节序列 A 和 B。各校验和独立计算：Adler-32 从 1 开始， CRC-32 从 0 开始。这些契约有意不对伪造校验和值作功能保证。 Lean 目标还描述任意种子及精确标量结果。 Adler 入口及其 Lean 目标都要求 NULL 初始化查询的长度为零。见范围偏差和公开目标。

此构建中，uLong 和 z_size_t 是无符号 64 位类型；uInt 是无符号 32 位类型。 z_off_t 和 z_off64_t 是有符号 64 位类型。输入校验和值中高于第 31 位的位被忽略；返回校验和值可用 32 位表示。显式 *64 声明取决于头文件的大文件特性宏。

形式化约定

ZlibF.Spec.Public.Goal.adler32

证明状态：已登记证明 · 证明记录与剩余工作

/-- `uLong adler32(uLong adler, const Bytef *buf, uInt len)`.
The public 32-bit length entry has the same buffer domain and exact result as `_z`.
NULL queries require zero length, as recorded in `docs/deviations.md`. -/
def Goal.adler32 : Prop :=
  ∀ (h : Heap) (seed : UInt64) (pointer : BPtr) (length : UInt32) (bytes : List UInt8),
    AdlerBufferBytes h pointer length.toNat bytes →
    C.run (Zlib.Adler32.adler32 seed pointer length) h =
      .ok ((if pointer = .null then 1 else adlerValue seed bytes), h)