REFERENCE / ZLIB × LEAN

adler32

Update an Adler-32 checksum using a 32-bit byte count.

Source snapshot · 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 adler32(uLong adler, const Bytef *buf, uInt len);

Update an Adler-32 checksum using a 32-bit byte count.

Domain Restricted domain. Effects: read-only when buf is non-NULL.

Pre Either buf is NULL and len == 0, or it points to len readable bytes. For the checksum postcondition, the low 32 bits of adler are the Adler-32 of A.

Post Return exactly the result of adler32_z(adler, buf, len). A NULL, zero-length query returns 1. A non-NULL empty range preserves the checksum's low 32 bits.

Effects Preserve all memory and ownership. Read only the given range. A one-past pointer is allowed for a zero-length range.

The length is at most 2^32 - 1. Converting a larger length to uInt discards high bits before the call; use adler32_z or several calls for larger ranges. The zero-length NULL query and forged-seed scope of adler32_z apply here too.

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.adler32

Proof status: Registered proof · Evidence and remaining work

/-- `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)

Related definitions and source ↗