get_crc_table
Return the library's byte-at-a-time CRC table.
Full chapter and shared rules ↗57ad356e10ec68ee · Source at the matching commit ↗Read the function’s preconditions and results first. Expand the shared rules below for buffer and ownership requirements used throughout this API group.
const z_crc_t FAR * ZEXPORT get_crc_table(void);
Return the library's byte-at-a-time CRC table.
Domain Full type domain; there are no arguments. Effects: pure computation returning a pointer to library memory; it does not read the entries.
Pre The library's fixed CRC tables are present, as in the selected build. No setup call is required.
Post Return a non-NULL pointer to a read-only array of 256 z_crc_t
entries. Entry i is the reflected CRC register update for byte i, starting
with register zero and without the public checksum complements.
Repeated calls return the same pointer.
Effects Preserve all memory and ownership. The library retains the table; it lives for the program's lifetime. The caller may read the 256 entries, and must neither write through the pointer nor free it.
zlib.h places this among functions outside the documented API. It exposes
only the byte table, not adjacent or braided tables. z_crc_t is unsigned
32-bit here. Dynamic table generation is outside this build's scope.
Shared conditions and scope
API manual · Contract conventions · Buffer utilities
Compute a checksum a buffer at a time, or combine the checksums of independently processed byte sequences without rereading them. The byte sequences A and B below are ordinary data; the contracts use the Adler-32 or CRC-32 of those sequences.
| Task | Entries |
|---|---|
| Update Adler-32 | Size-type length, 32-bit length |
| Combine Adler-32 | Ordinary offset, explicit 64-bit offset |
| Update CRC-32 | Size-type length, 32-bit length |
| Combine CRC-32 | Ordinary offset, explicit 64-bit offset |
| Reuse a CRC combination operator | Generate, generate with 64-bit length, apply |
| Inspect the byte table | get_crc_table |
These focused contracts follow adler32.c, crc32.c and zlib.h in the default LP64 Linux
static build, with the pinned source and listed patches. Source readings are to confirm
by proof. No checksum entry writes state, allocates, frees or performs I/O. Exceptional
numeric results are ordinary values, rather than error codes. Domain and effects remain
independent as explained in contract conventions.
The practical checksum contracts use actual byte sequences A and B. Each checksum is computed independently, starting at 1 for Adler-32 or 0 for CRC-32. These contracts deliberately omit functional promises for forged checksums. The Lean targets also describe arbitrary seeds and exact scalar results. Both the Adler entries and their Lean targets require zero length for NULL initialization queries. See scope deviations and public goals.
In this build, uLong and z_size_t are unsigned 64-bit types; uInt is
unsigned 32-bit. z_off_t and z_off64_t are signed 64-bit. Input checksum bits
above bit 31 are ignored; returned checksums fit in 32 bits. The explicit
*64 declarations depend on the header's large-file feature macros.
Formal contract
ZlibF.Spec.Public.Goal.get_crc_table
Proof status: Registered proof · Evidence and remaining work
/-- `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))