Dictionary.lean

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

1import ZlibF.Math.LZ77History
2import ZlibF.Spec.Api.Basic
3
4namespace ZlibF.Spec.Proofs
5open ZlibF.Spec ZlibF.Math.LZ77History
6
7/-- A match whose distance fits a retained suffix copies the same bytes if older dictionary
8bytes are available. -/
9private theorem copy_suffix {small large history : List UInt8} {dist n : Nat}
10    (hs : small <:+ large) (hp : 0 < dist) (hd : dist ≤ (small ++ history).length) :
11    copyBack large dist n history = copyBack small dist n history := by
12  have he := retained_history_agrees large [] history small dist n (by simpa using hs) hp
13    (by simpa [List.length_append] using hd)
14  simpa using he
15
16/-- Decoding symbols is stable when extra older dictionary bytes are prepended. -/
17theorem symbols_dictionary_suffix {L D : List Nat} {small large history output : List UInt8}
18    {input rest : List Bool} (hs : small <:+ large)
19    (h : Symbols L D small history input rest output) : Symbols L D large history input rest output := by
20  induction h with
21  | eob hd => exact .eob hd
22  | lit hd hlt _ ih => exact .lit hd hlt ih
23  | @copy hist inp r1 r2 r3 r4 rest sym ds xl xd output hd h1 h2 hr1 hd2 h3 hr2 hb hcopy ih =>
24    have hbase : 0 < distBases.getD ds 0 :=
25      (by decide : ∀ i, i < 30 → 0 < distBases.getD i 0) ds (by omega)
26    have hpos : 0 < distBases.getD ds 0 + xd := by omega
27    have hfit : distBases.getD ds 0 + xd ≤ (small ++ hist).length := by omega
28    have hsame := copy_suffix hs hpos hfit (n := lengthBases.getD (sym - 257) 0 + xl)
29    have hlarge : xd + distBases.getD ds 0 ≤ (large ++ hist).length := by
30      obtain ⟨older, he⟩ := hs
31      rw [← he]
32      simp only [List.length_append] at *
33      omega
34    apply Symbols.copy hd h1 h2 hr1 hd2 h3 hr2 hlarge
35    rw [hsame]
36    exact ih
37
38/-- A block keeps its decoding when the dictionary grows by an older prefix. -/
39theorem body_dictionary_suffix {small large history output : List UInt8} {bt : Nat}
40    {input rest : List Bool} (hs : small <:+ large)
41    (h : Body small bt history input rest output) : Body large bt history input rest output := by
42  cases h with
43  | stored h1 h2 h3 h4 => exact .stored h1 h2 h3 h4
44  | fixed h => exact .fixed (symbols_dictionary_suffix hs h)
45  | dynamic h1 h2 h3 hc h4 ha hl heob hL hD h =>
46    exact .dynamic h1 h2 h3 hc h4 ha hl heob hL hD (symbols_dictionary_suffix hs h)
47
48/-- A complete sequence of blocks has the same output with a larger dictionary. -/
49theorem blocks_dictionary_suffix {small large history output : List UInt8} {input rest : List Bool}
50    (hs : small <:+ large) (h : Blocks small history input rest output) :
51    Blocks large history input rest output := by
52  induction h with
53  | last h1 h2 hb => exact .last h1 h2 (body_dictionary_suffix hs hb)
54  | more h1 h2 hb _ ih => exact .more h1 h2 (body_dictionary_suffix hs hb) ih
55
56/-- A complete raw deflate stream remains valid after prepending older dictionary bytes. -/
57theorem deflate_dictionary_suffix {small large stream output : List UInt8}
58    (hs : small <:+ large) (h : Deflate.Decodes small stream output) :
59    Deflate.Decodes large stream output := by
60  obtain ⟨rest, hb, hr⟩ := h
61  exact ⟨rest, blocks_dictionary_suffix hs hb, hr⟩
62
63/-- A stream valid for a smaller raw window is valid for the 32 KiB raw window. -/
64theorem raw_full_window {dict stream output : List UInt8} {bits : Nat} (hb : bits ≤ 15)
65    (h : Deflate.Decodes (dict.drop (dict.length - 2 ^ bits)) stream output) :
66    ZlibF.Spec.Api.Layer.Decodes .raw 15 dict stream output := by
67  have hpow : 2 ^ bits ≤ 2 ^ 15 := Nat.pow_le_pow_right (by decide) hb
68  have hi : dict.length - 2 ^ 15 ≤ dict.length - 2 ^ bits := by omega
69  have hs := List.drop_suffix ((dict.length - 2 ^ bits) - (dict.length - 2 ^ 15))
70    (dict.drop (dict.length - 2 ^ 15))
71  have hs' : dict.drop (dict.length - 2 ^ bits) <:+ dict.drop (dict.length - 2 ^ 15) := by
72    simpa only [List.drop_drop, Nat.add_sub_of_le hi] using hs
73  exact deflate_dictionary_suffix hs' h
74
75#print axioms deflate_dictionary_suffix
76#print axioms raw_full_window
77end ZlibF.Spec.Proofs