get_crc_table
返回库逐字节计算 CRC 使用的表。
完整章节与共同规则 ↗57ad356e10ec68ee · 对应提交的原文 ↗先看本函数的前置条件和返回结果；可展开下方共同规则，查看整组接口的缓冲区与所有权要求。
const z_crc_t FAR * ZEXPORT get_crc_table(void);
返回库逐字节计算 CRC 使用的表。
定义域 完整类型定义域；没有参数。效果为纯计算，返回指向库内存的指针， 不读取表项。
前置条件 库的固定 CRC 表存在，如所选构建中所示。 不要求准备调用。
返回与保证 返回非 NULL 指针，指向由 256 个 z_crc_t 表项组成的只读数组。
表项 i 表示从零寄存器出发处理字节 i 的反射 CRC 寄存器更新，
不包含公开校验和接口的取反步骤。重复调用返回相同指针。
内存与状态效果 保持全部内存与所有权。表仍由库持有，生存期覆盖整个程序。 调用者可读取这 256 项，但不得通过指针写入，也不得释放它。
zlib.h 将此入口列于文档化 API 之外的函数中。它只公开字节表，不公开相邻表或
交织表。此处 z_crc_t 为无符号 32 位类型。动态建表不属于本构建范围。
本组共同前提与范围
逐块计算缓冲区的校验和，或合并独立处理的字节序列的校验和，而不重新读取数据。 下文的字节序列 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.get_crc_table
证明状态：已登记证明 · 证明记录与剩余工作
/-- `const z_crc_t *get_crc_table(void)`.
The returned table is static and read-only, has 256 entries given by the reflected CRC
recurrence, and leaves every heap observation unchanged. -/
def Goal.get_crc_table : Prop :=
∀ h : Heap, CrcGlobals h → ∃ pointer table,
C.run Zlib.Crc32.get_crc_table h = .ok (pointer, h) ∧
pointer = .ref .st_crc_table 0 ∧ Space.get h URef.st_crc_table = some table ∧
Space.ro h URef.st_crc_table = true ∧ table.size = 256 ∧
∀ i : Fin 256, table[i.val]? = some (ZlibF.Spec.crcByte 0 (UInt8.ofNat i.val))