证明进度与剩余工作
b6f2139fa30f8b18 · 对应提交的原文 ↗本页集中记录证明证据和剩余工作。要了解目标陈述和证明的整体结构，请先读总览。
目录
证明进度图
用连线查看依赖，再进入具体目标的输入范围、证明状态和证据。
- 固定目标
- 181
- 已登记精确证明
- 81
- 本地证明，尚未登记
- 33
- 未完成目标
- 67
未完成目标中有 2 项记录了阻塞。展开目标后，输入覆盖与证明登记状态分别列出。
从左向右看依赖。连线数字是跨组件关系条数；节点内列出组件内部关系。点击节点查看具体目标。
悬停或聚焦节点可突出相连的路径。目标图中，点击任意相邻目标可继续沿依赖查看。
逐项查看目标与依赖
先选组件，或按名称和证据状态筛选。每项都保留通往完整证据表和记录源码的链接。
库信息与容量查询6 项目标
compressBound已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
实现调用的入口 1
compressBound_z已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
调用此入口的实现 1
zlibVersion已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
调用此入口的实现 1
zlibCompileFlags已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
zError已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
调用此入口的实现 2
get_crc_table已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
校验和11 项目标
adler32已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
证明依赖项 1
实现调用的入口 1
调用此入口的实现 5
adler32_combine已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
adler32_combine64已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
crc32已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
证明依赖项 1
实现调用的入口 1
调用此入口的实现 4
crc32_z已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
证明依赖项 1
调用此入口的实现 2
crc32_combine_gen已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
实现调用的入口 1
crc32_combine_gen64已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
调用此入口的实现 2
crc32_combine_op已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
调用此入口的实现 1
crc32_combine已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
实现调用的入口 1
crc32_combine64已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
实现调用的入口 2
调用此入口的实现 1
字节地址模型9 项目标
address_read_is_pure已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
raw_block_unchanged已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
every_layout_is_representable已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
every_existing_heap_accepts_layout已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
mask_refines_base_plus_offset已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
pointer_advance_preserves_low_bits已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
依赖此目标的证明 1
first_aligned_offset已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
byte_stores_preserve_bases已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
byte_modifies_preserve_bases已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
解压流18 项目标
inflateCopy未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
inflateInit2_存在阻塞- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 存在阻塞
实现调用的入口 1
调用此入口的实现 7
inflateInit_已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
实现调用的入口 1
调用此入口的实现 1
inflateResetKeep已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
调用此入口的实现 1
inflateReset已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
inflateReset2已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
实现调用的入口 1
调用此入口的实现 1
inflateEnd已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
调用此入口的实现 2
inflateGetDictionary已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
inflateGetHeader已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
inflateSetDictionary已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
实现调用的入口 1
inflateSyncPoint已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
inflateMark已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
inflateCodesUsed已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
inflateUndermine已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
inflateValidate已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
inflatePrime已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
inflateSync未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
快速解码义务19 项目标
actual_body_preserves_origin本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
actual_body_refines_token本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
actual_fast_preserves_origin本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
actual_distance_block_preserves_origin本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
actual_distance_refines_lz77本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
distance_lookup_matches_format本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
证明依赖项 1
依赖此目标的证明 1
fast_safe本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
证明依赖项 1
依赖此目标的证明 1
step_safe本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
length_lookup_matches_format本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
证明依赖项 1
依赖此目标的证明 1
actual_body_retains_selected_length本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
证明依赖项 1
actual_copy_match_refines_lz77本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
证明依赖项 1
依赖此目标的证明 1
match_array_refines_lz77本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
actual_drop_preserves_origin本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
证明依赖项 1
依赖此目标的证明 1
actual_pull_preserves_origin本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
证明依赖项 1
actual_rollback_preserves_origin本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
证明依赖项 1
依赖此目标的证明 1
drop_preserves_origin本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
initial_origin本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
依赖此目标的证明 1
pull_preserves_origin本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
rollback_preserves_origin本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
依赖此目标的证明 1
解码表义务19 项目标
decode_table_classifies_input未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
decode_table_matches_format未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
short_decode_table_leaf_sound未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
decode_table_leaf_sound未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
decode_table_read_preserved本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
依赖此目标的证明 1
constructor_establishes_decode_table_invariant未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
decode_table_invariant_of_prefix未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
constructor_establishes_query_stability未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
query_stability_of_prefix本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
证明依赖项 1
short_rejected_leaf_stays_invalid本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
constructor_establishes_fast_leaf_flags未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
fast_leaf_flags_of_prefix未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
fixed_tables_have_fast_leaf_flags未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
leaf_classification_agrees未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
inflate_table_content已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
依赖此目标的证明 1
inflate_table_decoder_safe已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
证明依赖项 1
依赖此目标的证明 1
inflate_table_read_extent已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
证明依赖项 1
constructor_root_bits未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
constructor_subtable_bits未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
回引用复制6 项目标
output_copy_refines_lz77本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
依赖此目标的证明 1
window_copy_refines_lz77本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
依赖此目标的证明 1
copy_back_compose本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
依赖此目标的证明 1
copy_back_extends_history本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
本记录没有与其他固定目标的直接连接。
retained_history_agrees本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
依赖此目标的证明 2
window_distance_check_agrees本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
本记录没有与其他固定目标的直接连接。
压缩流17 项目标
deflateCopy未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
deflateInit2_未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
deflateInit_已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
实现调用的入口 1
调用此入口的实现 1
deflateGetDictionary已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
deflateEnd已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
调用此入口的实现 3
deflateResetKeep已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
实现调用的入口 2
调用此入口的实现 1
deflateReset已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
deflatePending已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
deflateUsed已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
deflateTune已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
deflateSetHeader已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
deflate未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
deflateBound_z未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
调用此入口的实现 1
deflateBound未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
deflatePrime未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
deflateParams未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
调用此入口的实现 1
回调解码3 项目标
inflateBackInit_已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
依赖此目标的证明 1
inflateBack未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
inflateBackEnd已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
gzip 文件32 项目标
gzclose_r未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
调用此入口的实现 1
gzclose_w未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 4
调用此入口的实现 1
gzbuffer已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
gzeof已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
gztell64未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
调用此入口的实现 1
gztell未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
gzoffset64已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
调用此入口的实现 1
gzoffset已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
实现调用的入口 1
gzerror已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
gzclearerr已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
gzrewind已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
调用此入口的实现 1
gzseek未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
gzopen未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
gzopen64未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
gzdopen未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
gzread未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 3
gzfread未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 3
gzgetc未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 3
调用此入口的实现 1
gzgetc_未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
gzungetc未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 3
gzgets未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 3
gzdirect未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 2
gzwrite未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 3
gzfwrite未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 3
gzputc未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 3
gzputs未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 3
gzvprintf未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 3
调用此入口的实现 1
gzprintf未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
gzflush未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 3
gzsetparams未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
完整缓冲区8 项目标
compress2_z未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 4
调用此入口的实现 2
compress2未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
调用此入口的实现 1
compress_z未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
compress未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
uncompress2_z未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 3
调用此入口的实现 2
uncompress2未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
调用此入口的实现 1
uncompress_z未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
uncompress未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
实现调用的入口 1
格式与 API 抽象模型20 项目标
format_deterministic已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
format_prefix_free已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
inflate_decodes已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
依赖此目标的证明 1
inflate_completes已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
依赖此目标的证明 1
inflate_rejects_invalid未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
deflate_valid已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
deflate_completes已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
deflate_full_flush_resync已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
roundtrip已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
roundtrip_completes已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
dict_roundtrip本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
证明依赖项 1
header_roundtrip本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
证明依赖项 1
deflate_bound_adequate已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
compress_bound_adequate已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
compress_roundtrip已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
gz_roundtrip已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
gz_seek_read存在阻塞- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 存在阻塞
本记录没有与其他固定目标的直接连接。
compress_bound_value已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
compress2_z_first_alloc_failure已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
inflate_deferred_distance已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
调用序列与初始化8 项目标
inflate_sequence未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
deflate_sequence未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
inflate_back_sequence未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
gz_sequence未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
inflate_initialisation_domain已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
本记录没有与其他固定目标的直接连接。
deflate_initialisation_domain未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
inflate_back_initialisation_domain已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
证明依赖项 1
gz_initialisation_domain未完成- 输入覆盖
- 尚无完整输入覆盖
- 证据状态
- 未完成
本记录没有与其他固定目标的直接连接。
其他内部义务5 项目标
crc32_z_all_byte_views已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
依赖此目标的证明 1
crc32_all_byte_views已登记证明- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 已登记证明
依赖此目标的证明 1
rejected_has_no_symbols本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
本记录没有与其他固定目标的直接连接。
step_composes_symbols本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
本记录没有与其他固定目标的直接连接。
symbols_exposes_step本地证明（未登记）- 输入覆盖
- 覆盖命题全部输入
- 证据状态
- 本地证明（未登记）
本记录没有与其他固定目标的直接连接。
没有匹配目标。请清除筛选或使用较短的名称。
41 条已观察证明复用关系 · 95 条 C 调用关系。规范引用和其他支持关系见下方证据索引。
展开组件后，再展开一个目标，即可查看它的输入范围、状态和双向依赖。证据索引保留提交 7f4311a 的目标与证明链接。
| 存在阻碍的目标 | 原因与下一步 |
|---|---|
| gz_seek_read | gzip 定位模式 |
| inflateInit2_ | 解压初始化的清理 |
目标证据
本索引包含 181 个固定目标，分为公开接口执行、调用序列、初始化、实现层义务和抽象模型。每个目标分别列出输入范围、登记情况、证明正文和剩余工作。
抽象模型研究输入输出的数学关系；实现目标还要证明真实执行符合这些关系。一个本地证明完成后，仍需登记，并在具体提交上通过 CI 验收。所有证明都保留命题中写明的前置条件。
依赖区展示记录中已经建立的联系。未完成目标还需要哪些证明，见本页后面的具体工作清单。出现不允许的公理时，生成过程会停止。
状态说明
已登记证明：存在精确覆盖该目标、经过检查且列入登记表的定理。 本地已检查：存在精确覆盖该目标的定理，但尚未列入登记表。 未证明：还没有精确覆盖该目标的定理。 存在阻碍：已有文档记录影响该目标的具体障碍。 输入覆盖范围单独列出；CI 验收对应具体提交。
库信息查询
| 目标陈述 | 覆盖范围／证据状态 | 契约／输入范围 | 证明证据 | 已审查的后续工作 |
|---|---|---|---|---|
| compressBound | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.Proofs.compressBound | — |
| compressBound_z | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.Proofs.compressBound_z | — |
| zlibVersion | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.Proofs.zlibVersion | — |
| zlibCompileFlags | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.Proofs.zlibCompileFlags | — |
| zError | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.Proofs.zError | — |
| get_crc_table | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.Proofs.get_crc_table | — |
校验和
| 目标陈述 | 覆盖范围／证据状态 | 契约／输入范围 | 证明证据 | 已审查的后续工作 |
|---|---|---|---|---|
| adler32 | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.AdlerUpdateProof.adler_public | — |
| adler32_z | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.AdlerUpdateProof.adler_z_public | — |
| adler32_combine | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.AdlerCombineProof.combine_public | — |
| adler32_combine64 | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.AdlerCombineProof.combine64_public | — |
| crc32 | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.Proofs.crc32 | — |
| crc32_z | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.Proofs.crc32_z | — |
| crc32_combine_gen | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.CrcCombineProof.gen | — |
| crc32_combine_gen64 | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.CrcCombineProof.gen64 | — |
| crc32_combine_op | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.CrcCombineProof.op | — |
| crc32_combine | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.CrcCombineProof.combine | — |
| crc32_combine64 | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.CrcCombineProof.combine64 | — |
字节地址模型
解压流
快速解码器的证明义务
解码表的证明义务
回引用复制
| 目标陈述 | 覆盖范围／证据状态 | 契约／输入范围 | 证明证据 | 已审查的后续工作 |
|---|---|---|---|---|
| output_copy_refines_lz77 | 陈述所允许的全部输入 / 本地已检查 | 确切目标陈述; 输入范围 | ZlibF.Math.LZ77Copy.output_copy_refines_lz77 | — |
| window_copy_refines_lz77 | 陈述所允许的全部输入 / 本地已检查 | 确切目标陈述; 输入范围 | ZlibF.Math.LZ77Copy.window_copy_refines_lz77 | — |
| copy_back_compose | 陈述所允许的全部输入 / 本地已检查 | 确切目标陈述; 输入范围 | ZlibF.Math.LZ77History.copy_back_compose | — |
| copy_back_extends_history | 陈述所允许的全部输入 / 本地已检查 | 确切目标陈述; 输入范围 | ZlibF.Math.LZ77History.copy_back_extends_history | — |
| retained_history_agrees | 陈述所允许的全部输入 / 本地已检查 | 确切目标陈述; 输入范围 | ZlibF.Math.LZ77History.retained_history_agrees | — |
| window_distance_check_agrees | 陈述所允许的全部输入 / 本地已检查 | 确切目标陈述; 输入范围 | ZlibF.Math.LZ77History.window_distance_check_agrees | — |
压缩流
回调解码
| 目标陈述 | 覆盖范围／证据状态 | 契约／输入范围 | 证明证据 | 已审查的后续工作 |
|---|---|---|---|---|
| inflateBackInit_ | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.InflateBackInitProof.back_init_public | — |
| inflateBack | 未证明 / 未证明 | 契约; 输入范围 | — | 所需：解码表、窗口与回调证明 |
| inflateBackEnd | 陈述所允许的全部输入 / 已登记证明 | 契约; 输入范围 | ZlibF.Spec.Public.InflateBackEndProof.back_end_public | — |
gzip 文件
完整缓冲区操作
| 目标陈述 | 覆盖范围／证据状态 | 契约／输入范围 | 证明证据 | 已审查的后续工作 |
|---|---|---|---|---|
| compress2_z | 未证明 / 未证明 | 契约; 输入范围 | — | 所需：压缩器执行证明 |
| compress2 | 未证明 / 未证明 | 契约; 输入范围 | — | 所需：压缩器执行证明 |
| compress_z | 未证明 / 未证明 | 契约; 输入范围 | — | 所需：压缩器执行证明 |
| compress | 未证明 / 未证明 | 契约; 输入范围 | — | 所需：压缩器执行证明 |
| uncompress2_z | 未证明 / 未证明 | 契约; 输入范围 | — | 所需：解码器执行证明 |
| uncompress2 | 未证明 / 未证明 | 契约; 输入范围 | — | 所需：解码器执行证明 |
| uncompress_z | 未证明 / 未证明 | 契约; 输入范围 | — | 所需：解码器执行证明 |
| uncompress | 未证明 / 未证明 | 契约; 输入范围 | — | 所需：解码器执行证明 |
格式与 API 模型
生命周期与调用序列
| 目标陈述 | 覆盖范围／证据状态 | 契约／输入范围 | 证明证据 | 已审查的后续工作 |
|---|---|---|---|---|
| inflate_sequence | 未证明 / 未证明 | 确切目标陈述; 输入范围 | — | 所需：执行与格式证明 |
| deflate_sequence | 未证明 / 未证明 | 确切目标陈述; 输入范围 | — | 所需：执行与格式证明 |
| inflate_back_sequence | 未证明 / 未证明 | 确切目标陈述; 输入范围 | — | 所需：执行与格式证明 |
| gz_sequence | 未证明 / 未证明 | 确切目标陈述; 输入范围 | — | 所需：执行与格式证明 |
| inflate_initialisation_domain | 陈述所允许的全部输入 / 已登记证明 | 确切目标陈述; 输入范围 | ZlibF.Spec.Public.Proofs.InflateInit.inflate_initialisation_domain_public | — |
| deflate_initialisation_domain | 未证明 / 未证明 | 确切目标陈述; 输入范围 | — | 起点：初始化与分配 |
| inflate_back_initialisation_domain | 陈述所允许的全部输入 / 已登记证明 | 确切目标陈述; 输入范围 | ZlibF.Spec.Public.InflateBackInitProof.back_init_domain_public | — |
| gz_initialisation_domain | 未证明 / 未证明 | 确切目标陈述; 输入范围 | — | 起点：打开与清理 |
内部证明义务
| 目标陈述 | 覆盖范围／证据状态 | 契约／输入范围 | 证明证据 | 已审查的后续工作 |
|---|---|---|---|---|
| crc32_z_all_byte_views | 陈述所允许的全部输入 / 已登记证明 | 确切目标陈述; 输入范围 | Zlib.Crc32.Proofs.crc32_z_all_byte_views | — |
| crc32_all_byte_views | 陈述所允许的全部输入 / 已登记证明 | 确切目标陈述; 输入范围 | Zlib.Crc32.Proofs.crc32_all_byte_views | — |
| rejected_has_no_symbols | 陈述所允许的全部输入 / 本地已检查 | 确切目标陈述; 输入范围 | ZlibF.Spec.Token.rejected_has_no_symbols | — |
| step_composes_symbols | 陈述所允许的全部输入 / 本地已检查 | 确切目标陈述; 输入范围 | ZlibF.Spec.Token.step_composes_symbols | — |
| symbols_exposes_step | 陈述所允许的全部输入 / 本地已检查 | 确切目标陈述; 输入范围 | ZlibF.Spec.Token.symbols_exposes_step | — |
已观察到的证明依赖
左列是被复用的来源目标，右列是使用它的目标。右列目标的定理实际使用了左列目标的证明。
C 函数调用
右列目标对应的实现调用左列入口。这种调用关系不意味着，证明时必须把左列入口的完整契约作为前提。
规格中的引用
右列目标的定义引用左列目标或实现。这里记录的是定义中的引用，不是证明依赖。
辅助证明的引用关系
这里把已观察到的定理引用按来源类别分组。一个分组不表示对应文件已经整体证明。 本表保留分组之间的全部直接连接，包括总览图为简化显示而省去的箭头。
| 辅助证明来源 | 直接引用它的目标 |
|---|---|
| API 模型引理 | compress_bound_adequate, compress_roundtrip, deflate_bound_adequate, deflate_completes, deflate_full_flush_resync, deflate_valid, dict_roundtrip, gz_roundtrip, header_roundtrip, inflate_completes, inflate_decodes, inflate_deferred_distance, roundtrip, roundtrip_completes, deflateInit_, API 模型证明, deflate 状态构造证明 |
| ByteAddress 字节地址模型证明 | first_aligned_offset, mask_refines_base_plus_offset, pointer_advance_preserves_low_bits |
| actual_body_preserves_origin | inffast.c 的证明 |
| actual_distance_block_preserves_origin | inffast.c 的证明 |
| step_safe | inffast.c 的证明 |
| actual_copy_match_refines_lz77 | inffast.c 的证明 |
| actual_drop_preserves_origin | inffast.c 的证明 |
| actual_rollback_preserves_origin | inffast.c 的证明 |
| drop_preserves_origin | inffast.c 的证明 |
| pull_preserves_origin | inffast.c 的证明 |
| inflate_table_content | inftrees.c 的证明 |
| retained_history_agrees | 格式证明 |
| deflate_valid | API 模型证明 |
| inflate_completes | API 模型证明 |
| inflate_decodes | API 模型证明 |
| inflateBackInit_ | 公开入口组合证明 |
| adler32.c 的证明 | inflateSetDictionary, inflate 入口组合证明, inflate 存储与读位证明, 公开入口组合证明 |
| API 模型证明 | output_copy_refines_lz77, retained_history_agrees, compress2_z_first_alloc_failure, compress_bound_adequate, compress_bound_value, compress_roundtrip, deflate_bound_adequate, deflate_completes, deflate_full_flush_resync, deflate_valid, dict_roundtrip, gz_roundtrip, header_roundtrip, inflate_completes, inflate_decodes, inflate_deferred_distance, roundtrip, roundtrip_completes, inflateCodesUsed, 不涉及堆的数学证明 |
| crc32.c 的证明 | crc32_all_byte_views, crc32_z_all_byte_views, crc32, crc32_z, 公开入口组合证明 |
| deflate 状态构造证明 | deflateInit_ |
| deflate 入口组合证明 | deflateEnd, deflateGetDictionary, deflatePending, deflateReset, deflateResetKeep, deflateSetHeader, deflateTune, deflateUsed |
| deflate 生命周期证明 | deflateEnd, deflateGetDictionary, deflateInit_, deflatePending, deflateReset, deflateResetKeep, deflateSetHeader, deflateTune, deflateUsed, deflate 状态构造证明, deflate 入口组合证明 |
| deflate 窗口与匹配证明 | deflate 生命周期证明, inflate 存储与读位证明 |
| 格式证明 | short_rejected_leaf_stays_invalid, compress_roundtrip, format_deterministic, format_prefix_free, header_roundtrip, inflate_completes, rejected_has_no_symbols, API 模型证明, 不涉及堆的数学证明, inffast.c 的证明 |
| gzlib.c 的证明 | gzclearerr, 公开入口组合证明 |
| 不涉及堆的数学证明 | match_array_refines_lz77, output_copy_refines_lz77, window_copy_refines_lz77, copy_back_compose, retained_history_agrees, window_distance_check_agrees, API 模型证明, inftrees.c 的证明 |
| infback.c 的证明 | inflateBackEnd, inflateBackInit_, 公开入口组合证明 |
| inffast.c 的证明 | actual_body_preserves_origin, actual_body_refines_token, actual_fast_preserves_origin, actual_distance_block_preserves_origin, actual_distance_refines_lz77, distance_lookup_matches_format, fast_safe, step_safe, length_lookup_matches_format, actual_body_retains_selected_length, actual_copy_match_refines_lz77, match_array_refines_lz77, actual_drop_preserves_origin, actual_pull_preserves_origin, actual_rollback_preserves_origin, drop_preserves_origin, initial_origin, pull_preserves_origin, rollback_preserves_origin, output_copy_refines_lz77, 不涉及堆的数学证明 |
| inflate 入口组合证明 | inflateEnd, inflateGetDictionary, inflateGetHeader, inflateInit_, inflateMark, inflatePrime, inflateReset, inflateReset2, inflateSetDictionary, inflateSyncPoint, inflateUndermine, inflateValidate, inflate_initialisation_domain |
| inflate 存储与读位证明 | deflateReset, deflateResetKeep, inflateBackEnd, inflateBackInit_, inflateEnd, inflateGetDictionary, inflateInit_, inflateMark, inflateReset, inflateReset2, inflateResetKeep, inflateSetDictionary, inflateSyncPoint, inflateUndermine, inflateValidate, API 模型证明, infback.c 的证明, inflate 入口组合证明, 公开入口组合证明 |
| inftrees.c 的证明 | decode_table_read_preserved, short_rejected_leaf_stays_invalid, inflate_table_content, inflate_table_decoder_safe, inflate_table_read_extent, 不涉及堆的数学证明 |
| 公开入口组合证明 | adler32_combine, adler32_combine64, adler32_z, compressBound, compressBound_z, crc32_combine, crc32_combine64, crc32_combine_gen, crc32_combine_gen64, crc32_combine_op, get_crc_table, gzbuffer, gzeof, gzerror, gzoffset, gzoffset64, gzrewind, inflateBackEnd, inflateBackInit_, inflate_back_initialisation_domain, zError, zlibVersion, adler32.c 的证明 |
| 运行时对象与算术引理 | byte_modifies_preserve_bases, byte_stores_preserve_bases, every_layout_is_representable, crc32_all_byte_views, crc32_z_all_byte_views, actual_body_preserves_origin, actual_body_refines_token, actual_fast_preserves_origin, actual_distance_block_preserves_origin, actual_distance_refines_lz77, fast_safe, step_safe, actual_body_retains_selected_length, actual_copy_match_refines_lz77, actual_pull_preserves_origin, actual_rollback_preserves_origin, inflate_table_content, inflate_table_decoder_safe, inflate_table_read_extent, compress2_z_first_alloc_failure, adler32, adler32_z, crc32, crc32_z, deflateEnd, deflateGetDictionary, deflateInit_, deflatePending, deflateReset, deflateResetKeep, deflateSetHeader, deflateTune, deflateUsed, get_crc_table, gzclearerr, gzerror, gzoffset, gzoffset64, gzrewind, inflateBackEnd, inflateBackInit_, inflateCodesUsed, inflateEnd, inflateGetDictionary, inflateGetHeader, inflateInit_, inflateMark, inflatePrime, inflateReset, inflateReset2, inflateResetKeep, inflateSetDictionary, inflateSyncPoint, inflateUndermine, inflateValidate, inflate_back_initialisation_domain, inflate_initialisation_domain, zError, zlibVersion, adler32.c 的证明, API 模型证明, crc32.c 的证明, deflate 状态构造证明, deflate 入口组合证明, deflate 生命周期证明, deflate 窗口与匹配证明, gzlib.c 的证明, infback.c 的证明, inffast.c 的证明, inflate 入口组合证明, inflate 存储与读位证明, inftrees.c 的证明, 公开入口组合证明, 编码树构造与输出证明, zutil.c 的证明 |
| 规格引理 | every_existing_heap_accepts_layout, actual_body_refines_token, distance_lookup_matches_format, length_lookup_matches_format, actual_body_retains_selected_length, drop_preserves_origin, pull_preserves_origin, rollback_preserves_origin, short_rejected_leaf_stays_invalid, inffast.c 的证明 |
| 编码树构造与输出证明 | deflate 状态构造证明, deflate 生命周期证明 |
| zutil.c 的证明 | inflate_table_content, deflate 状态构造证明, deflate 生命周期证明, inflate 入口组合证明, inflate 存储与读位证明, inftrees.c 的证明 |
其他已登记定理
这些声明是已经登记的辅助执行结果、引理或见证。 它们不是额外的固定目标，也不能单凭这些声明就为调用者标记某种输入覆盖状态。
更新记录
证明或登记表发生变化后，需要重新生成本页。生成过程会编译并检查 定理的精确类型，不会修改证明、目标或登记表。 结果是否通过项目验收，仍须依据检查规则。
输入指纹：49a33d32fca62884e1eba9ca62dd3bd9d8c5fb803e7b11fa90ab23abeabd9977。
当前证明范围
当前证明范围包括默认初始化、限定平台范围的快速解码接口，以及解码表的内容、安全性和读取范围。上方索引列出每个目标的证明状态和定义域。完整公开 inflate 与 deflate 目标仍未完成。
CI 验收必须对应一个明确的提交。请查看主分支运行记录和检查规则；合并或本地构建本身都不足以说明最终验收通过。平台的对象大小前提是已经接受的环境假设，不是尚待决定的范围问题。
剩余工作
红色边框表示已经记录了阻碍证明的问题，下文给出证据和下一步。证明尝试耗时很长，本身不构成这种阻碍。灰色目标可以开始推进；它们缺少的内部引理和调用序列不变量并没有全部画在图中。
公开 API 的证明准备情况
灰色表示尚未证明，不表示无法推进。可以立即开展独立工作。 被调用函数呈绿色，并不意味着调用者自身的前置条件、循环、返回结果和内存效果已经建立。一个能直接调用的 API，仍可能存在错误的契约或已确认的源码缺陷；只有这类证据才足以给目标加上阻碍边框。不能只凭图中缺少箭头判断证明准备情况。
证据索引区分证明引用、C 调用和规格引用。下面列出需要组合的证明义务，这些义务与精确目标的连接尚未完成。它们不会引入新的公开调用假设，也不会赋予目标任何已检查的输入覆盖范围。
打开、查询与关闭操作的前提
证明打开文件不需要先完成整个引擎。主要工作在公共辅助函数 gz_open：模式解析循环、真实分配、字符串复制、文件描述符效果，以及初始化不变量。位置查询尚缺的基础，是覆盖所有允许调用序列的位置不变量。关闭操作尚缺的基础，是覆盖这些调用序列的所有权事实，其中也包括分配失败。
目前本地执行证明已覆盖：
- 打开入口：NULL 参数、负文件描述符和第一次分配失败。结论给出未改变的文件系统和精确堆状态，也包括分配尝试计数器。
- 读模式关闭：NULL、模式不匹配，以及在
GzGood条件下完整的未缓冲执行。范围包含文件描述符错误，释放消息、路径和句柄，以及无关分配保持不变的框架性质。 - 位预置入口：在压紧待输出字节之前，拒绝流状态和非法位数的分支。
这些是具有明确内部范围的结果，并不是完整公开目标的证明。特别是，仍须从允许的公开调用序列推出 GzGood。不能凭一个分支的结果，就把灰色公开节点改成绿色。
回调解码器的前提
inflateBack 不必等待普通 inflate 的完整目标。建立和释放状态的操作已经登记。现有的入口、位输入、窗口交付和 stored 块论证可以复用；压缩块和完整的公开回调协议仍需组合证明。
要求输出缓冲区与状态序列缓冲区分离的快速路径定理，并不覆盖输出位于窗口内部的情形。关于解码表返回码的定理，也不能建立已安装表项的内容。回调证明指南标出可复用论证，并说明其回调定义域的限制。缺少这些前提，不妨碍独立推进其他块类型或错误路径。
每个未完成公开目标的下一步
“开始”表示无需等待完整引擎定理就能开展的工作。“组合”列出完整收束目标所需的前提；其他独立分支仍可推进。表中任何一行都不授予已检查状态，也不把被调用函数的规格当作假设。
| 公开目标 | 图中所示证明工作 | 下一步与缺少的前提 |
|---|---|---|
gzopen, gzopen64, gzdopen, gz_initialisation_domain |
开始：打开与清理 | 开始：公共模式循环、各分配结果、路径格式化与复制、文件描述符效果、OpenState 和具体见证。上文的入口与失败分支已经过本地检查。 |
gztell64, gztell |
需要：位置约束 | 组合：从读取、写入、定位和回退字节的调用序列推出位置不变量 PosInv，再复用现有算术执行证明。 |
gzclose_r |
需要：资源归属 | 开始：已初始化缓冲区的清理，以及从调用序列建立其所有权的证明。未缓冲执行及框架性质已有本地检查；仅有 inflateEnd 还不够。 |
gzclose_w, gzclose |
需要：交付与清理 | 组合：实际补零、最终压缩和文件写入，全部清理与错误路径，再利用两个完整的关闭结果证明分派操作。 |
gzseek64, gzseek |
需要：定位与状态序列 | 开始：位置与指针的状态序列不变量、缓冲和透明模式路径，以及精确的错误框架性质。负位置的可达性与溢出复核复核尚未完成。 |
gzdirect, gzread, gzfread, gzgetc, gzgetc_, gzgets, gzungetc |
需要：读取路径证明 | 开始：公共延迟准备、透明模式读取，以及缓冲区与状态序列不变量。组合：压缩路径中的实际解码执行，再建立 EOF、计数、字节回退和错误条款。gzdirect 需要格式探测与初始化，不需要完整的数据解码循环。 |
gzwrite, gzfwrite, gzputc, gzputs, gzvprintf, gzprintf, gzflush, gzsetparams |
需要：写入路径证明 | 开始：缓冲、格式化、透明模式写入及失败情况。组合：压缩输出与参数变更中的实际压缩器执行。 |
deflateInit2_, deflate_initialisation_domain |
开始：初始化与分配 | 开始：参数归一化、五次分配、全部失败清理、实际建立 DGood 和树状态，以及具体见证。重置证明要求不变量已经成立，并不会为新分配的存储建立它。 |
deflatePrime |
开始：压紧与位操作 | 开始：待输出字节的压紧、带检查的移位、位插入与交付，以及不变量和框架性质的保持。拒绝分支已有本地检查；接受的位数范围仍未完成。 |
deflateBound_z, deflateBound |
开始：上界与头部审查 | 开始：把现有执行公式连接到具有饱和语义的数学上界，包括头部字符串与额外字段长度。额外长度复核复核尚未完成，并不是新确认的阻碍。 |
deflateSetDictionary |
开始：窗口与哈希 | 开始：填充窗口、插入哈希链、恢复保存的输入，再处理校验和以及精确的状态和框架效果。绿色校验和调用只覆盖其中的校验和部分。 |
inflateCopy, deflateCopy |
开始：复制与重定位 | 开始：分配失败、缓冲区复制、指针重定位及独立所有权。在声称覆盖完整定义域之前，解决已记录的复制与状态序列调查；不能悄悄增加前提。 |
deflateParams |
需要：块交付与参数状态 | 组合：实际交付旧块、处理返回码，并更新规范的调参表行。在完整收束之前，检查拒绝路径精确保持了哪些状态。 |
inflateSync |
需要：扫描与状态序列 | 开始：组合现有的首次扫描与恢复扫描、暂存位、标记搜索、重置，以及记账和框架结果。从调用序列推出窗口与重置前提。 |
compress2_z, compress2, compress_z, compress |
需要：压缩器执行 | 开始：参数、标量长度和清理。组合：实际初始化、压缩和结束操作及精确输出，再处理外层封装。抽象的往返性质还不够。 |
uncompress2_z, uncompress2, uncompress_z, uncompress |
需要：解码器执行 | 开始：标量结果、空间不足和清理。组合：实际初始化、解压和结束操作、精确消费量与输出，再处理外层封装。 |
inflate, deflate |
需要：分派不变量 | 组合：解码表或哈希链的含义、分派不变量、循环终止，以及输出和记账。绿色校验和目标不能建立这些前提。 |
inflate_sequence, deflate_sequence, inflate_back_sequence, gz_sequence |
需要：执行与格式 | 组合：每次实际调用的安全性、状态序列保持、向独立格式模型的精化，以及跨输入输出分块的完成性质。 |
inflateBack |
需要：表、窗口与回调 | 组合：压缩块的 TABLE/LEN 执行、窗口内部的输出、公开回调所有权、循环终止和精确的输入输出记账。现有 stored 块和入口路径仍可独立推进。 |
inflateInit2_ |
阻碍：清理契约 | 已确认的清理契约反例记录在下文。成功初始化和其他独立目标仍可推进。 |
近期顺序是：先推进独立的入口、清理和算术路径，再建立公共的打开、位置和所有权不变量，最后完成整函数组合。回调压缩块可以并行推进。如果某个前提尚不清楚，应在这里记录精确问题；不能凭空制造依赖，也不能把经过的时间当作存在阻碍的证据。
集成
审查各函数手册的具体范围，并在经过评审的审计更新中重新生成文档来源策略锁。独立审查新增的源码锁、内核语法锁和首个验证基线。维护四项检查和受保护路径评审所需的仓库保护。新检查结果只有完成各自必需的检查后，才能登记。
公开契约
接受验证基线之前，须独立批准 103 个目标的陈述、调用者定义域和表示限制。把普通数据阶段的精化扩展到高级 raw 字典替换，以及所有头部、位预置和恢复组合；保留各入口精确的效果和无条件调用序列安全性。任何最终正确性声明都不能悄悄删去这些义务。
规格审查
Gzip 定位模式
抽象目标 gz_seek_read 不成立：关系 GzSeek 允许返回的句柄从读取模式变为写入模式，因此模型中的后续读取可能不返回数据。经过检查的反例使用一个已经打开、包含两个字节的读取句柄。证明该目标之前，需要审查定位关系。这是模型问题，不是已确认的 zlib 问题。
Inflate 初始化清理
当前的 inflateInit2_ 目标在窗口参数非法时不成立。后置条件 SameObjects 要求状态表的结构完全不变，但分配后再释放仍会扩展这个表。经过检查的反例使用合法的调用者堆，并证明两个表的大小分别为四和零。证明该目标之前，需要审查契约和模型。这不是已确认的 zlib 问题。
独立审查已经修正的共享关系 Uncompress2。延迟距离处理和精确释放的修正，都有独立反例和经过检查的回归证明；实现精化仍未完成。原先在内存失败时要求输出为空的条款，以及在缓冲区错误时要求扩展输出的条款，已依据现有成对反例移除。在把较早的抽象 gz 和字典模型当作完整操作精化之前，还须完成它们；具体公开目标不会假设被调用函数的契约成立。
翻译审查
审查所选构建采用的 C 语言版本和实现扩展。尤其需要确认可达的“空指针加零”和“空指针减空指针”操作是否具有定义。当前模型允许其中一些操作，而 Ptr.diff 的源码注释错误地把空指针相减归于 C23。对照表记录了实际定义和语言依据。这次文档修改不会改变运行时，也不能证明存在可达的上游缺陷。
在已修正压缩器自动存储的基础上，继续逐语句审查。压缩器的窗口滑动现在按源码顺序检查有符号减法。内部状态回归比较三个有定义的边界情形，并在 C 和 Lean 中都拒绝一个人为构造的溢出。恢复不受检查的减法，只会改变溢出情形的观察结果。这里没有声称该人为状态实际可达；仍须从合法调用序列推出有符号运算的边界。
树合并中针对所选深度的源码级重新读取已经恢复，并有六例回归和必需的结构检查；该检查会拒绝先前缓存表达式的写法。仍须证明内部深度读取之前的初始化时序。审查标量与指针的别名，以及压缩器指针相减时空指针减空指针的特殊情况；该项审查未完成。
CRC 地址模型
CRC 翻译现在为模型表示的每个静态或内嵌字节数组保留稳定的起始地址余数。两个公开 CRC 更新入口的本地证明，都覆盖所有余数、种子和可读长度，并给出同样的堆不变结论。原先的 47 字节静态输入，现在作为正向回归。公开契约和调用者定义域没有改变。本地证据仍须在集成提交上完成最终验收检查。
把表示关系扩展到一般 ABI 布局、有效类型、标量存储单元别名，以及其他记录的字节视图。当前地址抽象只表示 CRC 对齐测试观察到的低三位，不是完整的地址空间模型。
Inflate 因果模型
对照 C，完成通用输出精化和未知字典精化。先前要求整个预读区一致的条件不成立；改用支持当前结论的比特前缀，这项修正已经过评审。数据错误检测固定滞后八字节的说法也有反例；需要推导有依据的替代条件，不能直接提高常数。登记已经检查的 inflate_decodes 模型证明，再为实际解码器执行建立这些条件。除了已检查的模型见证和有限执行矩阵，还须证明通用的负值位预置衔接。
差分测试框架
在自动验证中保留新增的分配失败和负值位预置回归。测试拥有的 gz 句柄、输入行和 deflate 缓冲区现在都会释放。普通运行与未抑制报告的运行时检查器运行，都比较全部 47,890 个输入。一个清理变异确认：如果缺少结束调用，框架仍会报告库状态泄漏。
证明变异
补齐其余旧列表。每个新证明的公开入口，都必须在锁定映射中提供直接针对翻译的变异，并展示它们在对应函数证明中失败。尚未证明的入口应在取得证明时一并建立这些记录。
解码表
把已证明的规范码覆盖和表项形状引理，连接到 inflate_table 实际写出的堆；建立解码器使用的表谓词。
Inflate
对于实际构造的表，内部码长根表查找已有执行范围受限的结果。它最多读取一个输入字节，保持精确的输入游标和比特流，并在输入耗尽时退出。这个辅助结果没有完成 CODELENS、分派不变量或公开 inflate 目标。见查表证明和游标证明。
实际窗口更新函数在已有窗口、新分配和真正分配失败三种情况下，都保持逐字节对象的平台大小界和静态存储。它使用已证明的默认分配器和环形复制。平台大小界是环境前提；该定理证明操作保持了它。它还没有完成公开 inflate 目标、所有权、记账或完整的调用者框架性质。见窗口证明。
经过本地检查的内部快速路径主体，现在会产生一个独立的字面量或复制记号，结束块，或者在不产生输出的情况下拒绝非法长度码、非法距离码或距离过远的匹配。实际距离结果保持精确的剩余比特，并把复制结果等同于独立的逐字节状态序列复制。记号关系针对原始格式文法，已有经过检查的组合、分解和拒绝结果。整个快速调用的比特来源，也已贯穿循环、字节回退和最终写回进行检查。所有这些结果都保留了相同的安全性结论。
从实际构造、安装和初始化过程，建立表的含义、后缀稳定性、相容的叶标志和窗口中保留的字节。完成整个快速调用的输出组合，并覆盖所有合法缓冲区视图。完成其他解码模式、跨调用组合、复制和恢复。这些仍是内部定义域上的结果，并不是已登记的公开证明。公开 inflate 及其调用序列目标仍未完成。
回调解码
完成表构造、压缩块、回调组合和完整函数。
Deflate
完成通用初始化 deflateInit2_、字典设置、位预置、复制、fill_window、策略循环和完整函数。恢复的字典查询证明可以构建，并在自身证明中拒绝三个翻译变异；登记仍待完成。
精确目标 Goal.deflateInit_ 现在在 public-deflate-init 中有经过本地检查的证明。它展开实际的固定参数调用：窗口指数 15、内存级别 8、策略 0；压缩级别仍可任意选择。证明覆盖版本与参数拒绝、五次分配的全部结果、失败清理、调用前的对象的框架性质和精确的存活对象账目。成功执行会建立 DGood，而不是把它作为调用者前提。一个具体的默认调用者能够成功返回该不变量。通用 deflateInit2_ 定理仍未完成，也不是这项结果的依赖。
完整根构建、全新的完整内核重放、允许公理检查和零占位符扫描均在本地通过。三个直接包装层变异，在全新内核中使原始精确公开证明遭到拒绝。错误符号上限和遗漏清理这两个变异，仍保有同步后的完整源码相等性，但其执行证明因类型错误失败。资源不足造成的失败不计入结果。严格入口变异列表也已通过。
精确的默认入口证明及其具体见证已经登记。生成的锁增加了 72 条语义记录和两条定理类型记录，原有语义记录和定理类型记录没有改变。仍须在一个明确的 CI 提交上验收。这些是本地结果，不是 CI 批准。
树构造
实际的 gen_codes、叶准备、堆排序，以及完整的合并与根存储前缀，都已有经过检查的内部执行证明。节点边界和队列事实，来自实际的描述符、重置、扫描、修复和排序执行。输入堆中的数组内容、码长和深度仍不受限制。每次合并都按源码顺序选择子节点、写入尾部、更新频率与深度、写入父节点并执行向下调整。循环会终止，最终根存储具有精确的状态效果。这里使用实际被调用函数的执行定理。
实际森林和最终根存储现在会建立码长表示所需的前提。在明确的存储和静态表条件下，完整的实际 build_tree 执行两次编码生成调用。已安装的字面量、距离和位长描述符满足表条件。每个初始频率非零的符号，都得到正的受限码长，以及能够放入该长度的精确反转规范码字。这里没有假设被调用函数的契约。实际码长和存储的码字，现在与独立格式中的规范码及完整编码规则一致。其解码器会返回每个最初使用过的符号，并保留其后的任意比特后缀。
构造器的精确框架性质保持调用者的输出不变量和已有比特。实际构造再发送一个使用过的符号，可以在同一个堆上组合，并产生可独立解码的输出。它要求有十五比特可用空间，这是明确的内部义务；仍须从块与共享存储界推出这个条件。初始化与任意合法调用序列仍未完成。这些是内部状态结果，不是公开 deflate 定理。
实际 scan_tree 会终止、写入哨兵，并为每段连续游程记录精确的频率递增，运算遵循无符号回绕。实际 build_bl_tree 组合两次扫描、位长树构造、降序搜索和无符号成本更新，并保持源树码字及描述符。通用搜索返回 2..18；实际块初始化和源树构造建立了更强的 3..18 范围、字面量与距离计数范围 257..286 和 1..30，以及全部十九个位长值都不超过七的性质。
调用组合证明表明：对当前块能够容纳的任意合法实际符号记账列表，END_BLOCK 频率与位长树都保持不变。实际 init_block、这些记账操作和全部三个构造器，随后在同一个返回堆上建立相同的头部字段范围。这并没有证明策略从输入产生符号记账的状态序列，也没有证明跨块交付的保持性。
完整的实际 send_tree 现在会终止，并且精确输出共享游程编码模型描述的内容。直接重复循环包含最后一次有符号递减。所有重复分支、提前继续、下一个码长的读取和 for 循环的最后一次迭代，都按源码顺序执行。精确堆框架性质保持两棵树数组和已有输出前缀。实际位长构造现在为两个发送过程提供源容量、码长界，以及每个扫描频率为正的符号能够放入对应码长的码字。每个这样的码字，对任意后缀也都有独立的符号解码结果。
这些数据来自同一个返回堆：先实际执行 init_block，再执行任意合法的块内符号记账列表，最后执行全部三个构造器。精确的总比特空间仍是内部义务。还须完成 send_all_trees、独立的游程与头部解码，以及输出和符号共用存储的边界证明。单个码字可解码，并不代表完整游程序列已经可解码。
三个编码赋值变异、十一个扫描／重置／修复变异、五个堆调整／描述符变异，以及十七个合并／守卫／根存储变异，都会使相应执行证明失败。同步变体的完整源码相等性仍可独立检查。三个编码赋值变异，也会在构建目标包含完整构造器时被拒绝。
针对 send_code 的三个直接变异，分别改变码长表项、码字表项和发送长度；当构建目标包含完整构造与发送组合时，它们会使发送证明失败。五个扫描变异和八个位长构造变异会使各自的执行证明失败，而同步后的整函数相等性仍然通过。三个符号记账变异，分别改变字面量下标、匹配下标和缓冲区满标志；它们使执行证明失败，完整源码相等性仍然通过。
八个 send_tree 变异涉及重复递减、首个码字后的计数递减、零游程阈值、额外位的宽度与基数、continue 守卫、下次读取和最后迭代；它们会使执行证明失败。各变异完整且同步的源码相等性仍然通过。这些结果没有登记，也未获得 CI 批准。还须完成树描述发送、完整位成本精化、块压缩和共享存储边界，包括较小内存级别的情形。
其他 API
完成压缩辅助接口，以及 gz 的读取、写入和打开路径。
端到端声明
实例化堆 API，把状态序列不变量连接到格式模型，并在支持的配置上证明调用序列安全性、所有权、终止性和功能正确性。
边界情况复核
对照当前固定版本，复查 gzip 额外长度算术、部分读取后的恢复、负位置定位、参数变更丢失、结束失败后的恢复，以及 EOF 之后的向前定位。带条件的定位故障引理，不能证明状态可达；须从实际调用序列建立有符号位置与借用指针条件。
inflateBack 边界情况针对回调 API 的复核尚未完成；还需要该接口自身的复现，普通 inflate 的内存检查示例不足以完成这一步。在声称完整 gzip 所有权，或任意有限回调都会终止之前，还须审查外部字符串分配器和固定循环执行额度。怀疑存在缺陷，不等于可以把某种公开调用情形排除在外。
发现记录保存证据和置信度；当前补丁见 patches/README.md。没有应用一揽子未定义行为补丁。