Lean 中的格式模型

文档首页 · 数据格式 · API 指南

格式模型描述压缩字节如何决定未压缩字节，没有堆或指针。 它是需要被实现细化的规范，不是流式 API 的实现。 规则见格式指南，调用、缓冲区和返回值见 API 模型。 已接受结果与剩余工作记录于进度。

总入口模块是 ZlibF/Spec/Format.lean。 单个符号步骤的扩展单独导入。下列定义位于 ZlibF.Spec 命名空间， 局部符号步骤关系则位于 ZlibF.Spec.Token。

模块映射

从字节到输出

flowchart TD
    B["bytesToBits：字节转位"] --> K["Blocks：头部与主体"]
    K --> S["Body.stored：对齐的字节"]
    K --> F["Body.fixed：固定码"]
    K --> D["Body.dynamic：长度与编码"]
    D --> C["CodeLens：展开码长符号"]
    F --> Y["Symbols：字面量、复制、结束"]
    D --> Y
    S --> P["Deflate.Prefix：最终填充与字节尾随部分"]
    Y --> P
    P --> R["Deflate.Decodes：空尾随部分"]
    P --> Z["Zlib.Decodes：Adler-32 尾部"]
    P --> G["Gzip.Decodes：CRC-32 与长度尾部"]

readBits、readBytes 和 decodeSym 等读取器返回 none，或返回一个值与剩余位组成的二元组。 关系构造器要求相应的读取器等式。无效块类型或保留的长度／距离符号没有对应构造器。

先把一次块解码的输入和结果分开：inp 是尚未读取的位序列，rest 是解码停止时剩下的位，out 是新产生的字节。dict 是预置字典，h 是此前已经产生的历史字节；L、D 分别为字面量／长度和距离字母表保存各符号的码长，码长以比特计。

Symbols L D dict h inp rest out 从历史 h 开始，使用字面量／长度码长 L 和距离码长 D， 并在块结束符号处结束。它将 inp 消费到 rest，留下输出 out。 copyBack 每复制一个字节，就先追加它，再读取下一个，因此重叠匹配具有通常的逐字节含义。

Blocks dict h inp rest out 组合各主体，直到遇到 BFINAL = 1 的块。 块语法使用从完整输入字节得到的位。在该入口条件下，inp.length % 8 是到下一个字节边界前的剩余位数； 直接存储主体丢弃相应数量的位。例如刚读取完三位块头，当前字节还剩五位时，先跳过这五位，再读取按字节排列的长度字段。

公开格式关系对于最后一个块之后的要求不同：

包装关系使用 Deflate.Prefix，将所需尾部字节作为剩余序列参数 tail。 它们仍描述精确流：排除尾部之后的字节。 关于 Z_STREAM_END 后剩余输入的 API 定理，需要独立的已消费前缀陈述。

规则映射

F-* 规则定义在格式指南中。本表将每项规则定位到相应形式化定义，便于从格式要求找到 Lean 陈述。

Valid 谓词将 Decodes 的关注方向反过来：压缩参数必须解码为所给输入。 它们不选择唯一编码。Zlib.ValidWith 提供预置字典；其他列出的 Valid 谓词不使用字典。

模型选择与边界

历史与小窗口。 Symbols.copy 使用完整 dict ++ h 历史，不显式表示保存窗口的状态。 距离表将引用上限设为 32768。zlib 头的窗口字段限制初始字典后缀， 但没有给 Symbols.copy 增加距离前提。这明确保留了已有模型选择： 默认解码可以使用当前调用中超过较小保存窗口范围的输出，但下一次调用可能已无法取得那些字节。 C 也有独立的 INFLATE_STRICT 检查。全部配置窗口和输出缓冲区边界的细化未完成。 仅有声明式关系不能建立每种切分下的运行接受性。

字典。 有 FDICT 时，Zlib.Decodes dict 检查整个所提供字典的 Adler-32， 但仅将最后 Zlib.windowSize cmf 字节传给 DEFLATE 关系。 没有 FDICT 时，传入 []，忽略 dict。Adler-32 为 1 的字典可能为空。 无封装的 Deflate.Decodes 直接接收字典历史。Gzip 从空历史开始。

表的接受规则。 Acceptable 对三种编码类型都允许全零长度集合，但这种集合无法解码任何符号。 长度为 1 的单个已使用符号只在字面量／长度和距离类型下允许。 HasEndOfBlock 单独排除空的动态字面量／长度码。 表被接受或局部符号步骤成功，都不蕴含整个块有效。

填充。 直接存储块对齐和最后字节填充会丢弃位，不要求这些位为零。 额外的完整字节由显式的尾随序列 tail 处理，不视为填充。

gzip 元数据。 Gzip.Decodes 要求四个 MTIME 字节、保留标志位为零、 额外字段长度小于 2^16，以及所选名称或注释中不含嵌入零字节。 除此之外，FTEXT、MTIME、XFL 和 OS 不受约束。 标志未置位的可选字段见证不贡献字节；空见证可以满足其约束。 一个关系覆盖一个成员，而非拼接后的整个 gzip 文件。

局部解码。 Token.Step 描述一个字面量、匹配或块结束，不假设后续输入有效。 Token.Rejected 描述不可逆的无效编码或历史不可用情况。 目标 step_composes_symbols、symbols_exposes_step 和 rejected_has_no_symbols 将这些局部关系连接到原始 Symbols 语法。 这一边界防止以将来能够有效完成为假设，来论证 API 调用已经返回的输出。

格式关系之外的义务

Examples.lean 提供规范的具体正反例检查。其证明使用内核求值、关系构造器或反演。 这些例子帮助审阅定义，不能建立它们与每个 RFC 情况或翻译后实现的对应关系。 差分测试同样提供一致性证据，而非证明。 实现细化的验收状态见进度。