crc32_combine_op
使用预先生成的算子，计算 A 后接 B 的 CRC-32。
完整章节与共同规则 ↗57ad356e10ec68ee · 对应提交的原文 ↗先看本函数的前置条件和返回结果；可展开下方共同规则，查看整组接口的缓冲区与所有权要求。
uLong ZEXPORT crc32_combine_op(uLong crc1, uLong crc2, uLong op);
使用预先生成的算子，计算 A 后接 B 的 CRC-32。
定义域 受限定义域。效果为纯计算。
前置条件 要得到拼接结果，crc1 和 crc2 的低 32 位须分别为 A 和 B 从 0
独立开始计算的 CRC-32。op 是按 B 的长度调用 crc32_combine_gen 或
crc32_combine_gen64 得到、且未经修改的结果。
独立的拒绝情形允许 op == 0 配合任意校验和参数。
返回与保证 返回 A 后接 B 的 CRC-32。若 op == 0，返回 0。
用于空 B 的算子保持 A 的校验和不变。
内存与状态效果 保持全部内存与所有权。不读取缓冲区或流状态。 该算子可复用于 B 长度相同的任意序列对。
伪造算子或用于错误 B 长度的算子不受保证。
特别地，若 LP64 op 非零、但低 32 位全为零，调用可能不终止；这不在生成算子契约内。
零是拒绝值，不是无歧义的错误码，因为有效 CRC 也可能为零。
本组共同前提与范围
逐块计算缓冲区的校验和，或合并独立处理的字节序列的校验和，而不重新读取数据。 下文的字节序列 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.crc32_combine_op
证明状态：已登记证明 · 证明记录与剩余工作
/-- `uLong crc32_combine_op(uLong crc1, uLong crc2, uLong op)`.
`zlib.h` requires an operator generated from a length by `crc32_combine_gen`. The domain here
is exactly those mathematical operators, including its zero rejection result. Arbitrary forged
operators are not promised termination. Every permitted call has the polynomial result and
preserves the whole heap. -/
def Goal.crc32_combine_op : Prop :=
∀ (h : Heap) (first second : UInt64) (length : Int64), CrcGlobals h →
C.run (Zlib.Crc32.crc32_combine_op first second (crcOperator length)) h =
.ok (crcCombined first second length, h)