InflateDictionary.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Spec.Api.Inflate
2
3/-!
4# Dictionary independence for wrapped streams
5
6This format-level bridge replaces the supplied dictionary when a non-raw
7stream does not request one. It does not assert a property of the translated
8decoder or change the API model's causal conditions.
9-/
10
11namespace ZlibF.Spec.Api.Proofs
12
13open ZlibF.Spec
14
15private theorem zlib_decodes_dictionary_irrelevant
16    {w : Wrap} {b : Nat} {d1 d2 stream output : List UInt8}
17    (hw : w = .zlib ∨ w = .auto) (hn : ¬ HdrNeedsDict w b stream)
18    (hf : ZlibFits b stream) (hd : Zlib.Decodes d1 stream output) :
19    Zlib.Decodes d2 stream output := by
20  rcases hd with ⟨cmf, flg, pre, s, hs, hh, hclear, _⟩
21  refine ⟨cmf, flg, pre, s, hs, hh, hclear, ?_⟩
22  intro hset
23  exact False.elim (hn ⟨hw, cmf, flg, pre ++ s, hs, hh, hset, hf⟩)
24
25/-- A wrapped stream that does not request a preset dictionary decodes to the
26same output for every supplied dictionary. Raw streams are excluded because
27their back-references can use the dictionary without an announcing header. -/
28theorem layer_decodes_dictionary_irrelevant
29    {w : Wrap} {b : Nat} {d1 d2 stream output : List UInt8}
30    (hw : w ≠ .raw) (hn : ¬ HdrNeedsDict w b stream)
31    (hd : Layer.Decodes w b d1 stream output) :
32    Layer.Decodes w b d2 stream output := by
33  cases w with
34  | raw => exact False.elim (hw rfl)
35  | zlib =>
36    rcases hd with ⟨hz, hf⟩
37    exact ⟨zlib_decodes_dictionary_irrelevant (Or.inl rfl) hn hf hz, hf⟩
38  | gzip => exact hd
39  | auto =>
40    rcases hd with ⟨hz, hf⟩ | hg
41    · exact Or.inl ⟨zlib_decodes_dictionary_irrelevant (Or.inr rfl) hn hf hz, hf⟩
42    · exact Or.inr hg
43
44end ZlibF.Spec.Api.Proofs