inflate.c.dict.lean

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

1import ZlibF.Proof.«inflate.c.ring»
2import ZlibF.Proof.«adler32.c»
3
4/-!
5# inflate.c: `inflateGetDictionary` and `inflateSetDictionary`
6-/
7
8namespace Zlib.Inflate.Spec
9open C
10
11/-- The caller's dictionary buffer after `inflateGetDictionary` copied the window: `whave` bytes at offset `off`,
12oldest first, in two pieces (`window[wnext .. whave)`, then `window[0 .. wnext)`). -/
13def getDictBytes (D win : Array UInt8) (off wn wh : Nat) : Array UInt8 :=
14  copyRange (copyRange D win off wn (wh - wn)) win (off + wh - wn) 0 wn
15
16end Zlib.Inflate.Spec
17
18namespace Zlib.Inflate.Proofs
19open C Zlib.Inflate Zlib.Inflate.Spec
20
21theorem inflateGetDictionary_copy {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
22    {w db off : Nat} {a D : Array UInt8} {dl : Option UInt32}
23    (hL : Live H r zs z st) (hw : st.window = .ref (.blk w) 0) (ha : H.bytes w = some a) (hro : H.ro db = false)
24    (hD : H.bytes db = some D) (hne : db ≠ w) (hpos : st.whave ≠ 0) (hv : st.wnext.toNat ≤ st.whave.toNat)
25    (hwh : st.whave.toNat ≤ a.size) (hfit : off + st.whave.toNat ≤ D.size) :
26    inflateGetDictionary (some r) (.ref (.blk db) off) dl H =
27      .ok ((Z_OK, dl.map (fun _ => st.whave)),
28        { H with bytes := upd H.bytes db (some (getDictBytes D a off st.wnext.toNat st.whave.toNat)) }) := by
29  have hz := hL.hz
30  have hs := hL.hs
31  have hsub : (st.whave - st.wnext).toNat = st.whave.toNat - st.wnext.toNat :=
32    UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; exact hv)
33  have hwn : (st.window == Ptr.null) = false := by rw [hw]; simp
34  have hwh0 : (st.whave != 0) = true := by simpa using hpos
35  have hn0' : Ptr.add (Ptr.ref (BRef.blk w) 0) (st.wnext.toNat : Int) H = .ok (Ptr.ref (BRef.blk w) (0 + st.wnext.toNat), H) :=
36    Ptr.add_nat_ok (a := a) (by simpa using ha) (by omega)
37  have hcp1 := memcpyB_blk_ok (nb := db) (no := off) (pb := w) (po := 0 + st.wnext.toNat) (n := (st.whave - st.wnext).toNat)
38    (h := H) hD ha hro hne (by omega) (by omega)
39  simp only [Nat.zero_add] at hcp1 hn0'
40  unfold inflateGetDictionary
41  simp only [bind_app, pure_app, ldI_eq, ldZ_eq, hz, hL.zst, castI, hs, stateCheck_live hL, bne_iff_ne, ne_eq, hpos,
42    not_false_eq_true, hw, hn0', hcp1, not_true_eq_false, ite_false, ite_true]
43  simp only [bind_app, ldI_eq, ldZ_eq, hz, hL.zst, castI, hs, hw, hn0', hcp1, bne_iff_ne, ne_eq, hpos, not_false_eq_true,
44    ite_true, Bool.and_eq_true, hwh0, Ptr.noConfusion]
45  have hnn : ¬ (Ptr.ref (BRef.blk db) off : BPtr) = Ptr.null := by simp
46  simp only [true_and, hnn, not_false_eq_true, ite_true, bind_app, hn0', hcp1]
47  have hA1sz : (copyRange D a off st.wnext.toNat (st.whave - st.wnext).toNat).size = D.size := size_copyRange ..
48  have hb1 : ({ H with bytes := upd H.bytes db (some (copyRange D a off st.wnext.toNat (st.whave - st.wnext).toNat)) } : Heap).bytes db
49      = some (copyRange D a off st.wnext.toNat (st.whave - st.wnext).toNat) := by simp
50  have hbw1 : ({ H with bytes := upd H.bytes db (some (copyRange D a off st.wnext.toNat (st.whave - st.wnext).toNat)) } : Heap).bytes w
51      = some a := by simp [upd_ne _ _ _ _ hne.symm, ha]
52  have hd1 := Ptr.add_nat_ok (h := ({ H with bytes := upd H.bytes db (some (copyRange D a off st.wnext.toNat (st.whave - st.wnext).toNat)) } : Heap))
53    (r := BRef.blk db) (off := off) (n := st.whave.toNat) (a := copyRange D a off st.wnext.toNat (st.whave - st.wnext).toNat)
54    (by simpa using hb1) (by omega)
55  have hd2 := Ptr.sub_nat_ok (h := ({ H with bytes := upd H.bytes db (some (copyRange D a off st.wnext.toNat (st.whave - st.wnext).toNat)) } : Heap))
56    (r := BRef.blk db) (off := off + st.whave.toNat) (n := st.wnext.toNat) (a := copyRange D a off st.wnext.toNat (st.whave - st.wnext).toNat)
57    (by simpa using hb1) (by omega) (by omega)
58  have hcp2 := memcpyB_blk_ok (nb := db) (no := off + st.whave.toNat - st.wnext.toNat) (pb := w) (po := 0) (n := st.wnext.toNat)
59    (h := ({ H with bytes := upd H.bytes db (some (copyRange D a off st.wnext.toNat (st.whave - st.wnext).toNat)) } : Heap))
60    hb1 hbw1 (by simpa using hro) hne (by omega) (by omega)
61  have hd1' : Ptr.add (Ptr.ref (BRef.blk db) off) (st.whave.toNat : Int) _ = _ := hd1
62  have hd2' : Ptr.add (Ptr.ref (BRef.blk db) (off + st.whave.toNat)) (-(st.wnext.toNat : Int)) _ = _ := hd2
63  simp only [hd1', hd2', hcp2]
64  cases dl <;> simp [getDictBytes, upd_upd, hsub]
65  done
66
67theorem getDictBytes_ring (D a : Array UInt8) (off ws wn wh : Nat) (hv : wn ≤ wh) (hwh : wh ≤ ws) (hws : ws ≤ a.size)
68    (hfit : off + wh ≤ D.size) (hcase : wh = ws ∨ wn = wh) (j : Nat) (hj : j < wh) :
69    (getDictBytes D a off wn wh)[off + j]! = a[ringSlot ws wn wh j]! := by
70  have hin : (copyRange D a off wn (wh - wn)).size = D.size := size_copyRange ..
71  unfold getDictBytes ringSlot
72  rw [copyRange_bang _ _ _ _ _ (by omega) (by omega) _ (by omega)]
73  repeat' split
74  all_goals (try (rw [copyRange_bang _ _ _ _ _ (by omega) (by omega) _ (by omega)]; repeat' split))
75  all_goals first | rfl | (exfalso; omega) | (congr 1 <;> omega)
76
77/-- **inflateGetDictionary, specification and safety.** On an initialised stream whose window (if any) is not the
78caller's buffer, with a `dictionary` that is `NULL` or has room for `whave` bytes: the call returns `Z_OK`, never
79faults, and stores `*dictLength = whave` when `dictLength` is given. When `dictionary` is not `NULL` and `whave` is not 0,
80the `whave` bytes at `dictionary` are afterwards the window's history, oldest first (`ringList`), and the rest of the
81buffer is unchanged. -/
82theorem inflateGetDictionary_spec {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
83    {db off w : Nat} {a D : Array UInt8} {dl : Option UInt32}
84    (hG : Good H r zs z st) (hw : st.window = .ref (.blk w) 0) (ha : H.bytes w = some a) (hro : H.ro db = false)
85    (hD : H.bytes db = some D) (hne : db ≠ w) (hfit : off + st.whave.toNat ≤ D.size) :
86    ∃ H', C.run (inflateGetDictionary (some r) (.ref (.blk db) off) dl) H = .ok ((Z_OK, dl.map (fun _ => st.whave)), H') ∧
87      (st.whave = 0 ∧ H' = H ∨
88       (st.whave ≠ 0 ∧ H' = { H with bytes := upd H.bytes db (some (getDictBytes D a off st.wnext.toNat st.whave.toNat)) } ∧
89        (List.range st.whave.toNat).map (fun j => (getDictBytes D a off st.wnext.toNat st.whave.toNat)[off + j]!) =
90          ringList a st.wsize.toNat st.wnext.toNat st.whave.toNat)) := by
91  have hL := hG.live
92  have hI := hG.inv
93  by_cases h0 : st.whave = 0
94  · refine ⟨H, ?_, Or.inl ⟨h0, rfl⟩⟩
95    show inflateGetDictionary (some r) (.ref (.blk db) off) dl H = _
96    unfold inflateGetDictionary
97    have hnn : ¬ (Ptr.ref (BRef.blk db) off : BPtr) = Ptr.null := by simp
98    cases dl <;> simp [stateCheck_live hL, ldZ_eq, ldI_eq, hL.hz, hL.zst, castI, hL.hs, h0, hnn]
99  · have hwn_le : st.wnext.toNat ≤ st.whave.toNat := by
100      rcases Nat.lt_or_ge st.whave.toNat st.wsize.toNat with h1 | h1
101      · have := hI.win.eq h1; omega
102      · have := hI.win.wn; have := hI.win.hv; omega
103    have hasz : a.size = 2 ^ st.wbits.toNat := by
104      rcases hI.win.block with hb | ⟨w', a', hw', ha', -, hsz'⟩
105      · rw [hb] at hw; cases hw
106      · rw [hw] at hw'; have := (BRef.blk.inj (Ptr.ref.inj hw').1); subst this; rw [ha] at ha'; cases ha'; exact hsz'
107    have hwsz : st.wsize.toNat ≤ a.size := by
108      rcases hI.win.ws with h1 | h1
109      · omega
110      · omega
111    have hwh0 : st.whave.toNat ≤ a.size := by have := hI.win.hv; omega
112    refine ⟨_, ?_, Or.inr ⟨h0, rfl, ?_⟩⟩
113    · exact inflateGetDictionary_copy hL hw ha hro hD hne h0 hwn_le hwh0 hfit
114    · apply List.ext_getElem
115      · simp [ringList]
116      · intro j h1 h2
117        simp only [ringList, List.getElem_map, List.getElem_range] at h1 h2 ⊢
118        have hcase : st.whave.toNat = st.wsize.toNat ∨ st.wnext.toNat = st.whave.toNat := by
119          rcases Nat.lt_or_ge st.whave.toNat st.wsize.toNat with h1 | h1
120          · right; exact hI.win.eq h1
121          · left; have := hI.win.hv; omega
122        simp only [List.length_map, List.length_range] at h1
123        exact getDictBytes_ring D a off _ _ _ hwn_le hI.win.hv hwsz hfit hcase j h1
124
125theorem mode_mem : HEAD ≤ MEM ∧ MEM ≤ SYNC := by decide
126
127theorem adler32_dict {H : Heap} {db off : Nat} {D : Array UInt8} (hD : H.bytes db = some D) (L : UInt32)
128    (hfit : off + L.toNat ≤ D.size) :
129    ∃ r, Zlib.Adler32.adler32 1 (.ref (.blk db) off) L H = .ok (r, H) ∧ r.toNat = Zlib.Adler32.Spec.adler32 1 (Zlib.Adler32.Proofs.seg D off L.toNat) := by
130  have hL : L.toUInt64 = L.toNat.toUInt64 := by
131    apply UInt64.toNat_inj.mp; simp
132  have := Zlib.Adler32.Proofs.adler32_z_correct H db D hD 1 off L.toNat hfit (by have := L.toNat_lt; omega) (by decide)
133  obtain ⟨r, hr, hv⟩ := this
134  refine ⟨r, ?_, by simpa using hv⟩
135  unfold Zlib.Adler32.adler32
136  rw [hL]; exact hr
137
138theorem adler32_init (H : Heap) : Zlib.Adler32.adler32 0 .null 0 H = .ok (1, H) := by
139  simp [Zlib.Adler32.adler32, Zlib.Adler32.adler32_z]
140
141/-- **inflateSetDictionary, safety.** For a good stream with the default allocator and a `dictionary` that is a
142readable byte block holding `dictLength` bytes at `off` (not the stream's window), a stream that is raw (`wrap = 0`) or
143waiting for its dictionary (`mode = DICT`, with the dictionary's Adler-32 equal to the one in the stream), the call
144never faults. It returns `Z_OK` with the dictionary appended to the window history and `havedict = 1`, or
145`Z_MEM_ERROR` (the window could not be allocated) with `mode = MEM`. The stream stays good. -/
146theorem inflateSetDictionary_safe {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
147    {db off : Nat} {D : Array UInt8} {L : UInt32}
148    (hG : Good H r zs z st) (hza : z.zalloc = .fn "zcalloc") (hD : H.bytes db = some D) (hfit : off + L.toNat ≤ D.size)
149    (hdisj : ∀ w, st.window = .ref (.blk w) 0 → db ≠ w) (hwrap : st.wrap = 0 ∨ st.mode = DICT)
150    (hadler : st.mode = DICT → Zlib.Adler32.Spec.adler32 1 (Zlib.Adler32.Proofs.seg D off L.toNat) = st.check.toNat) :
151    ∃ v H' st', C.run (inflateSetDictionary (some r) (.ref (.blk db) off) L) H = .ok (v, H') ∧ Good H' r zs z st' ∧
152      ((v = Z_OK ∧ st'.havedict = 1 ∧ st'.window ≠ .null ∧
153          ∀ S, H.Owns S → H'.Owns (fun b => S b ∨ (st.window = .null ∧ b = H.nextBlk))) ∨
154       (v = Z_MEM_ERROR ∧ st'.mode = MEM ∧ st.window = .null ∧ ¬ H.allocOk H.nalloc = true)) := by
155  have hL := hG.live
156  obtain ⟨v0, H1, st1, hr1, hG1, hcase⟩ := updatewindow_safe (copy := L) (eb := db) (eo := off + L.toNat) (ebytes := D)
157    hG hza hD (by omega) hfit hdisj
158  have hadd : OkOn H (Ptr.add (Ptr.ref (BRef.blk db) off) (L.toNat : Int)) (Ptr.ref (BRef.blk db) (off + L.toNat)) :=
159    Ptr.add_nat_ok (a := D) (by simpa using hD) hfit
160  have hadd' : Ptr.add (Ptr.ref (BRef.blk db) off) (L.toNat : Int) H = .ok (Ptr.ref (BRef.blk db) (off + L.toNat), H) := hadd
161  have hnn : (Ptr.ref (BRef.blk db) off == (Ptr.null : BPtr)) = false := by simp
162  have hr1' : updatewindow (some r) (Ptr.ref (BRef.blk db) (off + L.toNat)) L H = .ok (v0, H1) := hr1
163  have hstate : H.istates zs = some st := hL.hs
164  have hrun : inflateSetDictionary (some r) (.ref (.blk db) off) L H =
165      (if v0 = 0 then .ok (Z_OK, setI H1 zs { st1 with havedict := 1 })
166       else .ok (Z_MEM_ERROR, setI H1 zs { st1 with mode := MEM })) := by
167    have hs1 : H1.istates zs = some st1 := hG1.live.hs
168    unfold inflateSetDictionary
169    simp only [bind_app, stateCheck_live hL, ldZ_eq, ldI_eq, hL.hz, hL.zst, castI, hL.hs, hnn, bne_self_eq_false,
170      Bool.or_self, Bool.false_eq_true, ite_false]
171    by_cases hm : st.mode = DICT
172    · obtain ⟨ra, hra, hrv⟩ := adler32_dict hD L hfit
173      have hck : ra = st.check := by
174        apply UInt64.toNat_inj.mp; rw [hrv]; exact hadler hm
175      have hmb : (st.mode == DICT) = true := by simpa using hm
176      simp only [hmb, adler32_init, hra, hck, bne_self_eq_false, hadd', hr1', ite_true, Bool.false_eq_true, ite_false, Bool.and_false, hmb, hm, beq_self_eq_true]
177      simp only [bind_app, adler32_init, hra, hck, bne_self_eq_false, hadd', hr1', Bool.false_eq_true, ite_false, setMode, wrI_eq, hs1]
178      by_cases hv0 : v0 = 0
179      · simp only [hv0, bne_self_eq_false, Bool.false_eq_true, ite_false, ite_true, bind_app, wrI_eq, hs1, pure_app, setI]
180      · have hb : (v0 != 0) = true := by simpa using hv0
181        simp only [hb, ite_true, hv0, ite_false, setMode, bind_app, wrI_eq, hs1, pure_app, setI]
182    · have hw0 : st.wrap = 0 := by rcases hwrap with h | h; exact h; exact absurd h hm
183      have hmb : (st.mode == DICT) = false := by simpa using hm
184      simp only [hmb, hw0, hadd', hr1', bne_self_eq_false, Bool.false_and, Bool.false_eq_true, ite_false, Bool.and_false]
185      simp only [bind_app, hadd', hr1', Bool.false_eq_true, ite_false, setMode, wrI_eq, hs1]
186      by_cases hv0 : v0 = 0
187      · simp only [hv0, bne_self_eq_false, Bool.false_eq_true, ite_false, ite_true, bind_app, wrI_eq, hs1, pure_app, setI]
188      · have hb : (v0 != 0) = true := by simpa using hv0
189        simp only [hb, ite_true, hv0, ite_false, setMode, bind_app, wrI_eq, hs1, pure_app, setI]
190  have hs1 : H1.istates zs = some st1 := hG1.live.hs
191  by_cases hv0 : v0 = 0
192  · rcases hcase with ⟨-, hw1, hO⟩ | ⟨h1, -⟩
193    · refine ⟨Z_OK, setI H1 zs { st1 with havedict := 1 }, { st1 with havedict := 1 }, ?_, ?_, Or.inl ⟨rfl, rfl, hw1, ?_⟩⟩
194      · rw [C.run, hrun, ite_eq_left hv0]
195      · exact good_state hG1 rfl hG1.live.mode (hG1.inv.of_fields rfl rfl rfl rfl rfl rfl rfl rfl rfl hG1.inv.bits rfl rfl rfl)
196      · intro S hOw
197        have := (shape_setI hs1 { st1 with havedict := 1 }).owns (hO S hOw)
198        exact this
199    · rw [hv0] at h1; exact absurd h1 (by decide)
200  · rcases hcase with ⟨h1, -⟩ | ⟨-, hw0, hnok, -, hst⟩
201    · exact absurd h1 hv0
202    · refine ⟨Z_MEM_ERROR, setI H1 zs { st1 with mode := MEM }, { st1 with mode := MEM }, ?_, ?_, Or.inr ⟨rfl, rfl, hw0, hnok⟩⟩
203      · rw [C.run, hrun, ite_eq_right hv0]
204      · exact good_state hG1 rfl mode_mem (hG1.inv.of_fields rfl rfl rfl rfl rfl rfl rfl rfl rfl hG1.inv.bits rfl rfl rfl)
205
206
207/-- **inflateSetDictionary, wrong state.** A stream that has a wrapper (`wrap ≠ 0`) and is not waiting for a dictionary
208(`mode ≠ DICT`) is refused: `Z_STREAM_ERROR`, nothing changes. -/
209theorem inflateSetDictionary_streamerr {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
210    {db off : Nat} {L : UInt32} (hL : Live H r zs z st) (hw : st.wrap ≠ 0) (hm : st.mode ≠ DICT) :
211    C.run (inflateSetDictionary (some r) (.ref (.blk db) off) L) H = .ok (Z_STREAM_ERROR, H) := by
212  have hnn : (Ptr.ref (BRef.blk db) off == (Ptr.null : BPtr)) = false := by simp
213  have hb : (st.wrap != 0 && st.mode != DICT) = true := by simp [hw, hm]
214  show inflateSetDictionary (some r) (.ref (.blk db) off) L H = _
215  unfold inflateSetDictionary
216  simp only [bind_app, stateCheck_live hL, ldZ_eq, ldI_eq, hL.hz, hL.zst, castI, hL.hs, hnn, bne_self_eq_false,
217    Bool.or_self, Bool.false_eq_true, ite_false, hb, ite_true]
218  rfl
219
220/-- **inflateSetDictionary, wrong dictionary.** A stream waiting for its dictionary (`mode = DICT`) refuses one whose
221Adler-32 is not the stream's `check`: `Z_DATA_ERROR`, nothing changes. -/
222theorem inflateSetDictionary_dataerr {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
223    {db off : Nat} {D : Array UInt8} {L : UInt32} (hL : Live H r zs z st) (hD : H.bytes db = some D)
224    (hfit : off + L.toNat ≤ D.size) (hm : st.mode = DICT)
225    (hbad : Zlib.Adler32.Spec.adler32 1 (Zlib.Adler32.Proofs.seg D off L.toNat) ≠ st.check.toNat) :
226    C.run (inflateSetDictionary (some r) (.ref (.blk db) off) L) H = .ok (Z_DATA_ERROR, H) := by
227  have hnn : (Ptr.ref (BRef.blk db) off == (Ptr.null : BPtr)) = false := by simp
228  obtain ⟨ra, hra, hrv⟩ := adler32_dict hD L hfit
229  have hne : (ra != st.check) = true := by
230    simp only [bne_iff_ne, ne_eq]
231    intro e; apply hbad; rw [← hrv, e]
232  have hmb : (st.mode == DICT) = true := by simpa using hm
233  show inflateSetDictionary (some r) (.ref (.blk db) off) L H = _
234  unfold inflateSetDictionary
235  simp only [bind_app, stateCheck_live hL, ldZ_eq, ldI_eq, hL.hz, hL.zst, castI, hL.hs, hnn, bne_self_eq_false,
236    Bool.or_self, Bool.false_eq_true, ite_false, hm, beq_self_eq_true, Bool.and_false, ite_true]
237  simp only [bind_app, adler32_init, hra, hne, ite_true]
238  rfl
239
240end Zlib.Inflate.Proofs