deflate.c.life.getdict.lean

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

1import ZlibF.Proof.«deflate.c.base»
2import ZlibF.Proof.«deflate.c.engine.macros»
3
4/-!
5# deflate.c: `deflateGetDictionary`
6
7`deflateGetDictionary` copies the last `len = min(strstart + lookahead, w_size)` bytes of the history that the window
8holds into the caller's buffer, and reports `len`. It never changes the stream or the state. The stream check refuses a
9stream that is not initialised with `Z_STREAM_ERROR`.
10-/
11
12namespace Zlib.Deflate.Spec
13open C
14
15/-- The number of bytes `deflateGetDictionary` returns: the history in the window, `strstart + lookahead`, at most
16`w_size` (the sum is in `unsigned`; for a state with `strstart + lookahead <= window_size <= 2^16` it does not wrap). -/
17def dictLen (d : DeflateState) : UInt32 :=
18  if d.strstart + d.lookahead > d.w_size then d.w_size else d.strstart + d.lookahead
19
20/-- The caller's buffer can take the `n` bytes: it is a writable byte block with room for them at its offset, and the
21range does not overlap the source range `[src, src + n)` of the window (the two may share a block only if the ranges are
22disjoint, as `memcpy` requires). -/
23def DictDest (h : Heap) (d : DeflateState) (src n : Nat) (dictionary : BPtr) : Prop :=
24  ∃ x off da, dictionary = .ref (.blk x) off ∧ h.bytes x = some da ∧ h.ro x = false ∧ off + n ≤ da.size ∧
25    ∀ w, d.window = .ref (.blk w) 0 → (x ≠ w ∨ off + n ≤ src ∨ src + n ≤ off)
26
27end Zlib.Deflate.Spec
28
29namespace Zlib.Deflate.Proofs
30open C Zlib.Deflate Zlib.Deflate.Spec Zlib.Deflate.Engine.Proofs
31
32theorem dictLen_toNat {d : DeflateState} (hw : d.window_size.toNat = 2 * d.w_size.toNat)
33    (hws : d.w_size.toNat ≤ 32768) (hfill : d.strstart.toNat + d.lookahead.toNat ≤ d.window_size.toNat) :
34    (dictLen d).toNat = min (d.strstart.toNat + d.lookahead.toNat) d.w_size.toNat := by
35  have hs : (d.strstart + d.lookahead).toNat = d.strstart.toNat + d.lookahead.toNat := by
36    rw [UInt32.toNat_add]; exact Nat.mod_eq_of_lt (by omega)
37  unfold dictLen
38  by_cases hc : d.strstart + d.lookahead > d.w_size
39  · simp only [hc, ite_true]
40    have := UInt32.lt_iff_toNat_lt.mp hc
41    omega
42  · simp only [hc, ite_false]
43    have : ¬ d.w_size.toNat < (d.strstart + d.lookahead).toNat := fun e => hc (UInt32.lt_iff_toNat_lt.mpr e)
44    omega
45
46theorem getdict_unfold {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
47    (hL : DLive h r ds z d) (dictionary : BPtr) (hasDictLength : Bool) :
48    deflateGetDictionary (some r) dictionary hasDictLength h =
49      ((if dictionary != .null && dictLen d != 0 then
50          (do let from_ ← padd (← padd d.window d.strstart.toNat) d.lookahead.toNat
51              memcpyB dictionary (← psub from_ (dictLen d).toNat) (dictLen d).toNat
52              pure (Z_OK, if hasDictLength then some (dictLen d) else none) : M (Int32 × Option UInt32))
53        else pure (Z_OK, if hasDictLength then some (dictLen d) else none)) h) := by
54  unfold deflateGetDictionary
55  dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, dictLen]
56  split <;> split <;> simp_all
57
58/-- No copy: the buffer is `NULL`, or the history is empty. -/
59theorem deflateGetDictionary_run_nocopy {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
60    (hL : DLive h r ds z d) (dictionary : BPtr) (hasDictLength : Bool)
61    (hn : dictionary = .null ∨ dictLen d = 0) :
62    deflateGetDictionary (some r) dictionary hasDictLength h =
63      .ok ((Z_OK, if hasDictLength then some (dictLen d) else none), h) := by
64  rw [getdict_unfold hL]
65  have : ¬ (dictionary != .null && dictLen d != 0) = true := by
66    rcases hn with e | e <;> simp [e]
67  simp only [this]
68  rfl
69
70/-- A copy of `n = dictLen d` bytes into a good buffer. -/
71theorem deflateGetDictionary_run_copy {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
72    {w p q b : Nat} (hL : DLive h r ds z d) (hB : DBlocks h d w p q b)
73    (hfill : d.strstart.toNat + d.lookahead.toNat ≤ d.window_size.toNat)
74    (dictionary : BPtr) (hasDictLength : Bool) {x off : Nat} {da wa : Array UInt8}
75    (hd : dictionary = .ref (.blk x) off) (hda : h.bytes x = some da) (hro : h.ro x = false)
76    (hroom : off + (dictLen d).toNat ≤ da.size) (hwa : h.bytes w = some wa)
77    (hlen : (dictLen d).toNat = min (d.strstart.toNat + d.lookahead.toNat) d.w_size.toNat)
78    (hne : (dictLen d) ≠ 0)
79    (hdis : x ≠ w ∨ off + (dictLen d).toNat ≤ d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat ∨
80      d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat + (dictLen d).toNat ≤ off)
81    (hwsz : wa.size = d.window_size.toNat) :
82    deflateGetDictionary (some r) dictionary hasDictLength h =
83      .ok ((Z_OK, if hasDictLength then some (dictLen d) else none),
84        { h with bytes := upd h.bytes x (some (copyRange da wa off
85          (d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat) (dictLen d).toNat)) }) := by
86  rw [getdict_unfold hL]
87  have hc : (dictionary != .null && dictLen d != 0) = true := by simp [hd, hne]
88  simp only [hc, ite_true]
89  have hwa' : Space.get h (BRef.blk w) = some wa := hwa
90  have e1 : padd d.window d.strstart.toNat h = .ok (.ref (.blk w) d.strstart.toNat, h) := by
91    have := padd_ok' (r := BRef.blk w) (T := UInt8) (off := 0) (n := d.strstart.toNat) hwa' (by omega)
92    rw [hB.win]; simpa using this
93  have e2 : padd (.ref (.blk w) d.strstart.toNat : BPtr) d.lookahead.toNat h =
94      .ok (.ref (.blk w) (d.strstart.toNat + d.lookahead.toNat), h) :=
95    padd_ok' (r := BRef.blk w) (T := UInt8) (off := d.strstart.toNat) (n := d.lookahead.toNat) hwa' (by omega)
96  have e3 : psub (.ref (.blk w) (d.strstart.toNat + d.lookahead.toNat) : BPtr) (dictLen d).toNat h =
97      .ok (.ref (.blk w) (d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat), h) :=
98    psub_ok' (r := BRef.blk w) (T := UInt8) (off := d.strstart.toNat + d.lookahead.toNat) (n := (dictLen d).toNat)
99      hwa' (by omega) (by omega)
100  have e4 : memcpyB dictionary (.ref (.blk w) (d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat))
101      (dictLen d).toNat h = .ok ((), { h with bytes := upd h.bytes x (some (copyRange da wa off
102          (d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat) (dictLen d).toNat)) }) := by
103    subst hd
104    have := Ptr.memcpy_ok (rd := BRef.blk x) (rs := BRef.blk w) (od := off)
105      (os := d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat) (n := (dictLen d).toNat) (da := da) (sa := wa)
106      (by simpa using hda) (by simpa using hwa) (by simpa using hro) hroom (by omega)
107      (by rcases hdis with e | e | e
108          · exact Or.inl (fun hh => e (BRef.blk.inj hh))
109          · exact Or.inr (Or.inl e)
110          · exact Or.inr (Or.inr e))
111    simpa using this
112  simp only [bind_app, e1, e2, e3, e4, pure_app]
113
114
115theorem getD_copyRange (da wa : Array UInt8) (off s n : Nat) (hfit : off + n ≤ da.size) (i : Nat) :
116    (copyRange da wa off s n).getD i 0 = if off ≤ i ∧ i < off + n then wa.getD (s + (i - off)) 0 else da.getD i 0 := by
117  rw [Array.getD_eq_getD_getElem?, getElem?_copyRange _ _ _ _ _ _ hfit]
118  by_cases hi : off ≤ i ∧ i < off + n
119  · simp [hi, Array.getD_eq_getD_getElem?, getElem!_def]
120    split <;> simp_all <;> rfl
121  · simp [hi, Array.getD_eq_getD_getElem?]
122
123/-- **deflateGetDictionary, safety and specification.** On an initialised stream with the invariant (any stream state
124reachable by the engine: `strstart + lookahead <= window_size`, the precondition `hfill`, which `deflateInit2_`,
125`lm_init` and `fill_window` maintain) the call never faults and returns `Z_OK`. The length it reports (when the pointer
126`dictLength` is not `NULL`, `hasDictLength`) is `min(strstart + lookahead, w_size)`; it copies that many bytes, the
127last ones of the history `window[0 .. strstart + lookahead)`, to the caller's buffer `dictionary`; a `NULL` buffer
128receives nothing. The buffer must be a writable byte block with room for them that overlaps the source range at most
129if it lies in the window block outside it (`DictDest`); `zlib.h` says the buffer holds at least `w_size` bytes. The
130stream and the state are unchanged; only the bytes of the buffer's block in `[off, off + len)` change, and no block is
131allocated or freed. -/
132theorem deflateGetDictionary_safe {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
133    (hG : DGood h r ds z d) (hfill : d.strstart.toNat + d.lookahead.toNat ≤ d.window_size.toNat)
134    (dictionary : BPtr) (hasDictLength : Bool)
135    (hdict : dictionary ≠ .null → dictLen d ≠ 0 →
136      DictDest h d (d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat) (dictLen d).toNat dictionary) :
137    ∃ h', C.run (deflateGetDictionary (some r) dictionary hasDictLength) h =
138        .ok ((Z_OK, if hasDictLength then some (dictLen d) else none), h') ∧
139      DGood h' r ds z d ∧
140      (dictLen d).toNat = min (d.strstart.toNat + d.lookahead.toNat) d.w_size.toNat ∧
141      h'.dstates = h.dstates ∧ h'.streams = h.streams ∧ h'.gzstates = h.gzstates ∧ h'.words = h.words ∧
142      h'.ro = h.ro ∧ h'.gzheaders = h.gzheaders ∧ h'.istates = h.istates ∧ h'.nextBlk = h.nextBlk ∧
143      h'.nalloc = h.nalloc ∧
144      (∀ x, (∀ off, dictionary ≠ .ref (.blk x) off) → h'.bytes x = h.bytes x) ∧
145      (∀ w wa, d.window = .ref (.blk w) 0 → h.bytes w = some wa → ∀ x off da, dictionary = .ref (.blk x) off →
146        h.bytes x = some da → ∃ da', h'.bytes x = some da' ∧ da'.size = da.size ∧
147          (∀ i, i < (dictLen d).toNat →
148            da'.getD (off + i) 0 = wa.getD (d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat + i) 0) ∧
149          (∀ i, (i < off ∨ off + (dictLen d).toNat ≤ i) → da'.getD i 0 = da.getD i 0)) := by
150  obtain ⟨w, p, q, b, hB⟩ := hG.inv.blocks
151  have hI := hG.inv
152  obtain ⟨wa, hwa, hwsz⟩ := hB.wa
153  have hws : d.w_size.toNat ≤ 32768 := by
154    have := hI.wsize; have := hI.wbits_hi
155    have : 2 ^ d.w_bits.toNat ≤ 2 ^ 15 := Nat.pow_le_pow_right (by omega) hI.wbits_hi
156    omega
157  have hlen := dictLen_toNat hI.wsz hws hfill
158  have hwsz' : wa.size = d.window_size.toNat := by have := hI.wsz; omega
159  by_cases hn : dictionary = .null ∨ dictLen d = 0
160  · refine ⟨h, ?_, hG, hlen, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, fun _ _ => rfl, ?_⟩
161    · rw [C.run]; exact deflateGetDictionary_run_nocopy hG.live dictionary hasDictLength hn
162    · intro w' wa' hw' hwa' x off da hd hda
163      refine ⟨da, hda, rfl, ?_, fun _ _ => rfl⟩
164      intro i hi
165      rcases hn with e | e
166      · rw [e] at hd; cases hd
167      · rw [e] at hi; simp at hi
168  · have hnn : dictionary ≠ .null := fun e => hn (Or.inl e)
169    have hne : dictLen d ≠ 0 := fun e => hn (Or.inr e)
170    obtain ⟨x, off, da, hd, hda, hro, hroom, hdis⟩ := hdict hnn hne
171    have hdis' := hdis w hB.win
172    have hrun := deflateGetDictionary_run_copy hG.live hB hfill dictionary hasDictLength hd hda hro hroom hwa hlen hne
173      hdis' hwsz'
174    have hsz : (copyRange da wa off (d.strstart.toNat + d.lookahead.toNat - (dictLen d).toNat)
175        (dictLen d).toNat).size = da.size := size_copyRange _ _ _ _ _
176    refine ⟨_, by rw [C.run]; exact hrun, hG.bytes_set x _ da hda hsz, hlen, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl,
177      ?_, ?_⟩
178    · intro y hy
179      have hyx : y ≠ x := fun e => hy off (by rw [hd, e])
180      simp [upd_apply, hyx]
181    · intro w' wa' hw' hwa' x' off' da' hd' hda'
182      rw [hd] at hd'
183      cases hd'
184      rw [hB.win] at hw'
185      cases hw'
186      rw [hwa] at hwa'
187      cases hwa'
188      rw [hda] at hda'
189      cases hda'
190      refine ⟨_, by simp, hsz, ?_, ?_⟩
191      · intro i hi
192        rw [getD_copyRange _ _ _ _ _ hroom]
193        simp only [show off ≤ off + i ∧ off + i < off + (dictLen d).toNat by omega, and_self, ite_true]
194        congr 2; omega
195      · intro i hi
196        rw [getD_copyRange _ _ _ _ _ hroom]
197        have : ¬ (off ≤ i ∧ i < off + (dictLen d).toNat) := by omega
198        simp only [this, ite_false]
199
200/-- **deflateGetDictionary, refusal.** On a stream the check refuses (including `NULL`): `Z_STREAM_ERROR`, no length
201stored, nothing changes. -/
202theorem deflateGetDictionary_reject {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm)
203    (dictionary : BPtr) (hasDictLength : Bool) :
204    C.run (deflateGetDictionary strm dictionary hasDictLength) h = .ok ((Z_STREAM_ERROR, none), h) := by
205  unfold deflateGetDictionary
206  exact check_refuse hD hN _ _
207
208end Zlib.Deflate.Proofs