deflateCopy
创建压缩进度相同、彼此独立的压缩器。
完整章节与共同规则 ↗39ab1ace4bbe0b0e · 对应提交的原文 ↗先看本函数的前置条件和返回结果；可展开下方共同规则，查看整组接口的缓冲区与所有权要求。
int ZEXPORT deflateCopy(z_streamp dest, z_streamp source);
创建压缩进度相同、彼此独立的压缩器。
定义域 受限定义域。影响： 分配并复制拥有的状态。
前置条件 source 有效。dest 是另一个可写 z_stream，不拥有状态，且与源的内存分离。源缓冲区和任何保留的头部满足生命周期要求。
返回与保证 Z_OK 使 dest 获得五项新拥有的分配，包含等价的压缩状态；源不变。复制的流字段包括总计数、分配器字段、输入／输出指针和保留的头部指针。内部拥有的指针被重定位到新分配。两个流各自需要 deflateEnd，可独立继续。复制的调用者 输入／输出指针起初指向相同缓冲区；继续两个流前应分配独立输出空间。头部仍是共享的调用者自有存储。
Z_MEM_ERROR 释放每项新分配、清空 dest->state，并保持其他目标字段和源不变。没有新的有效状态需要释放。
聚焦范围之外： NULL 目标返回 Z_STREAM_ERROR；源检查失败还会清空非 NULL 目标的状态。公开目标显式假设两个流不同。这里排除自复制和覆盖已有效目标，不为它们提供无泄漏契约。
本组共同前提与范围
输入分批到达、输出空间有限，或需要选择封装、字典、刷新边界时，使用 z_stream 压缩器。封装是在 DEFLATE 压缩数据之外增加的头部、尾部和完整性信息；raw DEFLATE 则不带这些封装。初始化一次，使用连续的缓冲区调用 deflate，即使放弃压缩也要结束流。单个缓冲区的操作见 compress 和 compress2。
| 任务 | 条目 |
|---|---|
| 开始或复用 | 初始化、配置初始化、重置、保留历史的重置 |
| 提供元数据或历史 | 字典、读取历史、gzip 头 |
| 压缩与输出大小 | 压缩、上界、待输出数据、最近刷新位数 |
| 调整或分支 | 参数、调优、位预置、复制 |
| 释放存储 | 结束 |
这些聚焦契约遵循固定版本的 deflate.c、已应用补丁和 zlib.h，采用默认 LP64 Linux 构建。它们不改变范围更广的已登记公开目标。定义域/影响标签见契约约定，证明状态和剩余工作见进度。
共享约定
在每条所述前置条件下，都要求执行无运行时故障地终止，并满足所述后置条件。调用若保留有效流，就保持其表示不变量。
先看一次调用的数据交接。next_in 指向本轮尚未读取的输入起点，avail_in 是从这里开始可读的字节数；next_out 指向本轮下一个可写位置，avail_out 是剩余输出容量，也以字节计。一次调用可以只消耗部分输入、只交付部分输出。调用者应读取更新后的指针和计数，接走已交付字节，再为同一个流补充输入或输出空间。
- 有效流： 可写的
z_stream，其压缩器状态由成功初始化或复制建立，经过合法调用保持，且尚未结束。调用者不改变其内部状态或分配器字段。同一个流的调用按顺序执行。 - 缓冲区： 输入覆盖
avail_in个可读字节；输出覆盖avail_out个可写字节。它们彼此不重叠，也不与流或流拥有的状态重叠。非 NULL 标量结果指向可写单元，与其他结果及流内存分离。这些分离条件是聚焦契约的显式假设；见 safety.md。 - 分配器： 使用默认分配/释放函数对，或在初始化前将两个字段都置为 NULL。任意一次分配尝试都可能失败。自定义分配器回调不在本页范围内。
- 帧性质与所有权： 调用只改变自己的流、其拥有的状态和所述输出区域。调用者输入只读。调用者缓冲区和头部记录仍归调用者所有。只有初始化和复制会分配；只有它们失败时的清理与
deflateEnd会释放内存。其他调用保持流的分配集合。 - 头部生命周期： 保留的 gzip 头及其可选字段在使用期间保持可读且不变。非 NULL 的
name和comment以零终止；extra覆盖所述长度。聚焦格式契约使用extra_len <= 65535。 - 检查后的拒绝： 除初始化和上界查询外，流检查失败会在正常操作之前返回
Z_STREAM_ERROR，不发生写入。deflateCopy还会清空非 NULL 目标的状态。这种拒绝不修改查询输出单元。 - 受限定义域指这些显式内存、生命周期和调用顺序条件，加上条目自身的前置条件。它不意味着接受每个可表示的指针或整数。错误概述覆盖可读、可检查的状态，不覆盖任意无效地址。
形式化约定
ZlibF.Spec.Public.Goal.deflateCopy
证明状态：未完成 · 证明记录与剩余工作
/-- `int deflateCopy(z_streamp dest, z_streamp source)`.
Copy the initialized window, hash entries, pending bytes and symbols. Relocate the owned
buffers and tree descriptors. A failure clears destination state and releases every new block. -/
def Goal.deflateCopy : Prop :=
(∀ h source, C.run (Zlib.Deflate.deflateCopy none source) h = .ok (Z_STREAM_ERROR, h)) ∧
(∀ h dest z, dest.get h = some z →
C.run (Zlib.Deflate.deflateCopy (some dest) none) h =
.ok (Z_STREAM_ERROR, dest.put h { z with state := none })) ∧
(∀ h source i z s dest oldDest,
StreamReachable .deflate h source → Zlib.Deflate.Spec.DGood h source i z s →
Zlib.Deflate.Spec.DefAlloc z → source ≠ dest → dest.get h = some oldDest →
∃ rc after,
C.run (Zlib.Deflate.deflateCopy (some dest) (some source)) h = .ok (rc, after) ∧
source.get after = some z ∧ after.dstates i = some s ∧ Frame h after (StreamRoot dest) ∧
((rc = Z_MEM_ERROR ∧ AllocationFailed h after ∧
dest.get after = some { oldDest with state := none } ∧
LiveChange h after (fun _ => False) (fun _ => False)) ∨
(rc = Z_OK ∧ ∃ copied,
Zlib.Deflate.Spec.DGood after dest h.nextBlk
{ z with state := some (.deflate h.nextBlk) } copied ∧
copied = copiedDeflate dest h.nextBlk s copied ∧
SameBytePrefix h after s.window copied.window s.high_water.toNat ∧
SameWordPrefix h after s.head copied.head s.hash_size.toNat ∧
SameWordPrefix h after s.prev copied.prev
(if s.slid ≠ 0 ∨ s.strstart - s.insert > s.w_size then s.w_size.toNat
else (s.strstart - s.insert).toNat) ∧
SameBytePrefix h after s.pending_out copied.pending_out s.pending.toNat ∧
SameBytePrefix h after s.sym_buf copied.sym_buf s.sym_next.toNat ∧
(∀ b, DeflateOwned h.nextBlk copied b ↔ h.nextBlk ≤ b ∧ b < h.nextBlk + 5) ∧
LiveChange h after (DeflateOwned h.nextBlk copied) (fun _ => False))))