REFERENCE / ZLIB × LEAN

inflateSync

Search for a possible full-flush boundary after damaged input.

Source snapshot · ecafc184cdf44b7f · 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.

int ZEXPORT inflateSync(z_streamp strm);

Search for a possible full-flush boundary after damaged input.

Domain Restricted domain: live streams after a data error or during a recovery search, with readable input.

Effects Consumes input, mutates state, may free a window.

Pre next_in and avail_in describe a readable range. Output is not used.

Post Searches buffered whole bytes and then input for 00 00 ff ff, retaining partial matches across calls. Input pointers/counts and total_in advance by the input searched. No output is produced and total_out is preserved. Results Z_OK means a pattern was found: history and header registration are reset, totals are preserved, decoding can resume at the following block. If no header had been read, recovery uses raw mode; otherwise it disables trailer validation. A still unknown window size becomes 15. Z_DATA_ERROR means continue searching; ordinary inflate returns Z_STREAM_ERROR during that search.

Edges No input and fewer than eight buffered bits returns Z_BUF_ERROR unchanged. A failed stream check changes nothing. A found pattern need not be a real flush point; even a sync-flush boundary can need earlier history. Recovery does not promise a valid suffix or restored checksum checking. No allocation.

Shared conditions and scope

API manual · Shared stream rules · Stream compression

Use an inflate stream to decode input in pieces while controlling output space. Select zlib, gzip or raw DEFLATE at initialization, then continue with more input or room until completion, a dictionary request or an error. End releases the decoder after any of those outcomes. For whole-buffer zlib decoding, see uncompress.

Task	Entries
Start or reuse	Init, configured init, reset, new configuration, keep history
Decode or provide metadata	Inflate, set dictionary, read history, gzip header
Recover or inspect	Sync search, sync point, mark, table use
Adjust or branch	Prime bits, validation, distance option, copy
Release storage	End

The focused contracts follow the pinned inflate.c and zlib.h in the default LP64 Linux build, with gzip enabled and without optional invalid-distance or strict-distance modes. Source readings are to confirm by proof. The broader registered public goals retain their domains. See contract conventions for terminology and progress for proof status and remaining work.

Common conditions

All contracts below have a Restricted domain. A C pointer type alone does not supply the storage, lifetime or call history required here.

A live stream was successfully initialised or copied, has not been ended, retains its library-owned state, and is used without concurrent calls. Use the default allocator and free function. Init takes a writable, non-live stream with allocator fields set to NULL or the default functions.
A readable or writable range has the stated capacity for the whole call. Caller ranges are separate from the stream and its owned storage. Input and output ranges do not overlap. Dictionary destinations, the registered header record and its destination buffers are separate from each other and from the stream. Registered header storage is also separate from input/output ranges on calls using it. These are explicit focused-domain restrictions.
The caller owns its stream object and buffers. The library owns the state and optional window. A call changes only its stream, owned storage, stated output ranges and any registered header destination. It never frees caller buffers.
A rejected stream check returns Z_STREAM_ERROR without changes, unless a query or copy contract says otherwise. This covers NULL and safely readable records rejected by the check; it does not cover dangling or arbitrary pointers. The check requires allocators, state, the state's back-pointer and a valid mode.
Counters use the C unsigned widths and wrap. No contract assumes allocation succeeds. End remains available after decoding, dictionary or allocation errors.

flowchart LR
    I["Init"] --> F["inflate"]
    F -->|"Z_NEED_DICT"| D["SetDictionary"] --> F
    F -->|"more room or input"| F
    F -->|"end or abandon"| E["End"]
    F -->|"data error"| R["Reset or Sync"] --> F

Formal contract

ZlibF.Spec.Public.Goal.inflateSync

Proof status: Not completed · Evidence and remaining work

/-- `int inflateSync(z_streamp strm)`.
Search byte-aligned held bits before new input, retaining the partial marker match.
On success retain totals and restart at TYPE with validation disabled. -/
def Goal.inflateSync : Prop :=
  ∀ h r i z s input,
    StreamReachable .inflate h r → Zlib.Inflate.Spec.Good h r i z s →
    Zlib.Inflate.Spec.DefAlloc z → Bytes h z.next_in z.avail_in.toNat input →
    ∃ rc after z' s' used,
      C.run (Zlib.Inflate.inflateSync (some r)) h = .ok (rc, after) ∧
      Zlib.Inflate.Spec.Good after r i z' s' ∧ used ≤ input.length ∧
      z'.next_in = advance z.next_in used ∧ z'.avail_in.toNat + used = z.avail_in.toNat ∧
      z'.total_in = z.total_in + UInt64.ofNat used ∧ z'.total_out = z.total_out ∧
      (if z.avail_in = 0 ∧ s.bits.toNat < 8 then rc = Z_BUF_ERROR ∧ z' = z ∧ s' = s
       else let start := if s.mode = SYNC then s.have.toNat else
              (Api.syncSearch 0 (heldSyncBytes s)).1
            let found := Api.syncSearch start input
            used = found.2 ∧
            if found.1 = 4 then rc = Z_OK ∧ s'.mode = TYPE ∧ (s'.wrap &&& 4) = 0
            else rc = Z_DATA_ERROR ∧ s'.mode = SYNC ∧ s'.have.toNat = found.1) ∧
      Frame h after (fun b => StreamRoot r b ∨ InflateOwned i s b) ∧
      LiveChange h after (fun _ => False)
        (fun b => InflateOwned i s b ∧ ¬ InflateOwned i s' b)

Related definitions and source ↗