crc32_combine_op
Compute the CRC-32 of A followed by B using a previously generated operator.
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.
uLong ZEXPORT crc32_combine_op(uLong crc1, uLong crc2, uLong op);
Compute the CRC-32 of A followed by B using a previously generated operator.
Domain Restricted domain. Effects: pure computation.
Pre For the concatenation result, the low 32 bits of crc1 and crc2
are the CRC-32 checksums of A and B, each started at 0. op is the unchanged
result of crc32_combine_gen or crc32_combine_gen64 for the length of B.
The separate rejection case permits op == 0 with any checksum arguments.
Post Return the CRC-32 of A followed by B. If op == 0, return 0.
An operator for an empty B leaves A's checksum unchanged.
Effects Preserve all memory and ownership. Read no buffers or stream state. The operator can be reused for any pairs with the same B length.
There is no guarantee for a forged operator or one for the wrong B length.
In particular, a nonzero LP64 op with zero low 32 bits can fail to terminate;
this is outside the generated-operator contract. Zero is a rejection value,
not an unambiguous error code, since a valid CRC can also be zero.
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.crc32_combine_op
Proof status: Registered proof · Evidence and remaining work
/-- `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)