inflate.c.window-public-ring.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.window-compose»
2import ZlibF.Spec.Public.Lifecycle
3import ZlibF.Proof.«adler32.c.public-block»
4
5namespace Zlib.Inflate.Proofs
6open C Zlib.Inflate Zlib.Inflate.Spec ZlibF.Spec.Public
7
8/-- The public chronological window layout agrees with the mathematical ring
9for every valid window index arrangement. -/
10theorem ringList_public (a : Array UInt8) (ws wn wh : Nat)
11    (hwn : wn ≤ wh) (hwh : wh ≤ ws) (hsize : ws ≤ a.size)
12    (hcase : wh = ws ∨ wn = wh) :
13    ringList a ws wn wh = (a.toList.drop wn).take (wh - wn) ++ a.toList.take wn := by
14  have hlen1 : ((a.toList.drop wn).take (wh - wn)).length = wh - wn := by
15    simp only [List.length_take, List.length_drop, Array.length_toList]
16    apply Nat.min_eq_left
17    omega
18  have hlen2 : (a.toList.take wn).length = wn := by
19    simp only [List.length_take, Array.length_toList]
20    exact Nat.min_eq_left (by omega)
21  apply List.ext_getElem
22  · simp [ringList, hlen1, hlen2]
23    omega
24  · intro i hi1 hi2
25    have hi : i < wh := by simpa [ringList] using hi1
26    simp only [ringList, List.getElem_map, List.getElem_range]
27    by_cases hfirst : i < wh - wn
28    · have hidx : wn + i < a.size := by omega
29      simp only [List.getElem_append_left, hlen1, hfirst, List.getElem_take, List.getElem_drop]
30      simp only [ringSlot]
31      have hnot : ¬ wh ≤ wn := by omega
32      have heq : ws - (wh - wn) = wn := by rcases hcase with h | h <;> omega
33      simp [hnot, hfirst, heq, getElem!_pos a (wn + i) hidx, Array.getElem_toList]
34    · have hsecond : i - (wh - wn) < wn := by omega
35      have hidx : i - (wh - wn) < a.size := by omega
36      simp only [List.getElem_append_right, hlen1, Nat.not_lt.mp hfirst, List.getElem_take]
37      simp only [ringSlot]
38      by_cases hle : wh ≤ wn
39      · have heq : wn = wh := by omega
40        simp [hle, heq, getElem!_pos a i (by omega), Array.getElem_toList]
41      · simp [hle, hfirst, getElem!_pos a (i - (wh - wn)) hidx, Array.getElem_toList]
42
43/-- The public dictionary predicate and ring contents describe the same bytes
44for an existing window satisfying the stream invariant. -/
45theorem inflateDictionary_eq_ring {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
46    {st : InflateState} {w : Nat} {a : Array UInt8} {xs : List UInt8}
47    (hg : Good h r zs z st) (hw : st.window = .ref (.blk w) 0)
48    (ha : h.bytes w = some a) (hasz : a.size = 2 ^ st.wbits.toNat) :
49    InflateDictionary h st xs ↔ xs = ringList a st.wsize.toNat st.wnext.toNat st.whave.toNat := by
50  have hws : st.wsize.toNat ≤ a.size := by
51    have hs := hg.inv.win.ws
52    rw [hasz]
53    omega
54  have hwh : st.whave.toNat ≤ st.wsize.toNat := hg.inv.win.hv
55  have hwn : st.wnext.toNat ≤ st.whave.toNat := by
56    by_cases ht : st.whave.toNat < st.wsize.toNat
57    · have := hg.inv.win.eq ht; omega
58    · have := hg.inv.win.wn; omega
59  have hcase : st.whave.toNat = st.wsize.toNat ∨ st.wnext.toNat = st.whave.toNat := by
60    by_cases ht : st.whave.toNat < st.wsize.toNat
61    · exact Or.inr (hg.inv.win.eq ht)
62    · left; omega
63  have hsub : (st.whave - st.wnext).toNat = st.whave.toNat - st.wnext.toNat :=
64    UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; exact hwn)
65  have hring := ringList_public a st.wsize.toNat st.wnext.toNat st.whave.toNat hwn hwh hws hcase
66  constructor
67  · intro hd
68    rcases hd with ⟨hz, rfl⟩ | ⟨ref, off, data, hp, hget, _, hxs⟩
69    · simp [ringList, hz]
70    · rw [hw] at hp
71      cases hp
72      have he : data = a := Option.some.inj (hget.symm.trans (by simpa using ha))
73      subst data
74      simpa [hsub, hring] using hxs
75  · intro hxs
76    right
77    refine ⟨.blk w, 0, a, hw, ?_, ?_, ?_⟩
78    · simpa using ha
79    · simpa using hws
80    · simpa [hsub, hring] using hxs
81
82theorem updatewindow_ring_public {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {w eo : Nat} {source : BRef}
83    {a ebytes : Array UInt8} {copy : 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 w = false)
85    (hasz : a.size = 2 ^ st.wbits.toNat)
86    (heb : Space.get H source = some ebytes) (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size)
87    (hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat st.window (2 ^ st.wbits.toNat)) :
88    ∃ H' st' A', updatewindow (some r) (.ref source eo) copy H = .ok (0, H') ∧ Good H' r zs z st' ∧
89      H'.bytes w = some A' ∧
90      ringList A' (initWinS st).wsize.toNat st'.wnext.toNat st'.whave.toNat =
91        ((ringList a (initWinS st).wsize.toNat (initWinS st).wnext.toNat (initWinS st).whave.toNat ++
92            newBytes ebytes eo copy.toNat).drop ((initWinS st).whave.toNat + copy.toNat - st'.whave.toNat)) ∧
93      st'.whave.toNat = min (initWinS st).wsize.toNat ((initWinS st).whave.toNat + copy.toNat) := by
94  have hI := hG.inv
95  obtain ⟨f1, f2, f3, hv1, hwn1, heq1, -⟩ := initWinS_facts hI.win.wbits hI.win.ws hI.win.hv hI.win.wn hI.win.eq
96  have hwb := hI.win.wbits
97  have hle : (initWinS st).wsize.toNat ≤ 2 ^ 16 := by
98    rw [f1]; have := Nat.pow_le_pow_right (by decide : 0 < 2) (by omega : st.wbits.toNat ≤ 16); omega
99  have hposn : (initWinS st).wsize.toNat ≠ 0 := by rw [f1]; exact Nat.pos_iff_ne_zero.mp (Nat.two_pow_pos _)
100  obtain ⟨H', st', hrun, hH', hst', hG', -, hb', -, -, -, -⟩ := uw_post_public hG hw ha hro hasz heb hc hoff hsep
101  refine ⟨H', st', _, hrun, hG', hb', ?_, ?_⟩
102  · rw [hst']
103    exact ring_spec hposn hv1 hwn1 heq1 hle (by rw [f1]; omega) hc hoff (by rw [f1]; omega)
104  · rw [hst']
105    exact (uwPost_counts hposn hv1 hwn1 heq1 hle).1
106
107/-- For an existing window, the actual update produces the exact public
108dictionary suffix for every readable source and permitted separation. -/
109theorem updatewindow_dictionary_existing {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
110    {st : InflateState} {w off : Nat} {source : BRef} {a bytes : Array UInt8}
111    {copy : UInt32} {old xs : List UInt8}
112    (hg : Good h r zs z st) (hw : st.window = .ref (.blk w) 0)
113    (ha : h.bytes w = some a) (hro : h.ro w = false) (hasz : a.size = 2 ^ st.wbits.toNat)
114    (hsrc : Space.get h source = some bytes) (hfit : off + copy.toNat ≤ bytes.size)
115    (hxs : xs = (bytes.toList.drop off).take copy.toNat) (hold : InflateDictionary h st old)
116    (hsep : Separate (.ref source off) copy.toNat st.window (2 ^ st.wbits.toNat)) :
117    ∃ after state, updatewindow (some r) (.ref source (off + copy.toNat)) copy h = .ok (0, after) ∧
118      Good after r zs z state ∧ state.window = st.window ∧
119      InflateDictionary after state ((old ++ xs).drop ((old ++ xs).length - 2 ^ st.wbits.toNat)) := by
120  let eo := off + copy.toNat
121  have hc : copy.toNat ≤ eo := by dsimp [eo]; omega
122  have hoff : eo ≤ bytes.size := hfit
123  have hsep' : Separate (.ref source (eo - copy.toNat)) copy.toNat st.window (2 ^ st.wbits.toNat) := by
124    simpa [eo] using hsep
125  obtain ⟨after, state, hrun, _, hstate, hg', hwindow, hbytes, hsize, _, _, _⟩ :=
126    uw_post_public hg hw ha hro hasz hsrc hc hoff hsep'
127  refine ⟨after, state, hrun, hg', hwindow, ?_⟩
128  have hwindow' : state.window = .ref (.blk w) 0 := hwindow.trans hw
129  have hI := hg.inv.win
130  obtain ⟨fsize, fbits, _, hv, hwn, heq, _⟩ :=
131    initWinS_facts hI.wbits hI.ws hI.hv hI.wn hI.eq
132  have hmax : (initWinS st).wsize.toNat ≤ 2 ^ 16 := by
133    rw [fsize]
134    have hwb := hI.wbits
135    have := Nat.pow_le_pow_right (by decide : 0 < 2) (by omega : st.wbits.toNat ≤ 16)
136    omega
137  have hpos : (initWinS st).wsize.toNat ≠ 0 := by rw [fsize]; exact Nat.ne_of_gt (Nat.two_pow_pos _)
138  have hfields := uwPost_arith (st := initWinS st) (a := a) (ebytes := bytes) (eo := eo) (copy := copy)
139    hpos hv hwn heq copy.toNat_lt hmax
140  have hbits : state.wbits = st.wbits := by
141    rw [hstate]
142    exact hfields.2.1.trans fbits
143  have hsize' : (uwPost (initWinS st) a bytes eo copy).1.size = 2 ^ state.wbits.toNat := by
144    rw [hsize, hasz, hbits]
145  apply (inflateDictionary_eq_ring hg' hwindow' hbytes hsize').2
146  have hbefore := (inflateDictionary_eq_ring hg hw ha hasz).1 hold
147  have hxs' : xs = newBytes bytes eo copy.toNat := by
148    rw [hxs]
149    have hh := Zlib.Adler32.Proofs.seg_eq_slice bytes off copy.toNat hfit
150    simpa [Zlib.Adler32.Proofs.seg, newBytes, eo] using hh.symm
151  have hinit : ringList a (initWinS st).wsize.toNat (initWinS st).wnext.toNat
152      (initWinS st).whave.toNat = ringList a st.wsize.toNat st.wnext.toNat st.whave.toNat := by
153    by_cases hz : st.wsize = 0
154    · have hwh0 : st.whave.toNat = 0 := by have := hI.hv; rw [hz] at this; simpa using Nat.eq_zero_of_le_zero this
155      simp [initWinS, hz, ringList, hwh0]
156    · simp [initWinS, hz]
157  have hwh : (initWinS st).whave.toNat = st.whave.toNat := by
158    have hh := congrArg List.length hinit
159    simpa only [ringList, List.length_map, List.length_range] using hh
160  have hcount := (uwPost_counts (st := initWinS st) (a := a) (ebytes := bytes)
161    (eo := eo) (copy := copy) hpos hv hwn heq hmax).1
162  have hring := ring_spec (st := initWinS st) (a := a) (ebytes := bytes) (eo := eo) (copy := copy)
163    hpos hv hwn heq hmax (by rw [fsize]; omega) hc hoff (by rw [fsize]; omega)
164  rw [hstate, hfields.1, hring, hinit, ← hbefore, ← hxs']
165  congr 1
166  have holdlen : old.length = st.whave.toNat := by rw [hbefore]; simp [ringList]
167  have hxslen : xs.length = copy.toNat := by rw [hxs']; simp [newBytes]
168  rw [List.length_append, holdlen, hxslen, hcount, fsize, hwh]
169  omega
170
171/-- A newly allocated window retains the exact public dictionary suffix. -/
172theorem updatewindow_dictionary_new {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
173    {st : InflateState} {eo : Nat} {source : BRef} {ebytes : Array UInt8} {copy : UInt32}
174    {old xs : List UInt8}
175    (hG : Good h r zs z st) (hza : z.zalloc = .fn "zcalloc") (hw : st.window = .null)
176    (hok : h.allocOk h.nalloc = true) (heb : Space.get h source = some ebytes)
177    (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size)
178    (hxs : xs = (ebytes.toList.drop (eo - copy.toNat)).take copy.toNat)
179    (hold : InflateDictionary h st old) :
180    ∃ H' st', updatewindow (some r) (.ref source eo) copy h = .ok (0, H') ∧
181      Good H' r zs z st' ∧
182      InflateDictionary H' st' ((old ++ xs).drop ((old ++ xs).length - 2 ^ st.wbits.toNat)) := by
183  have hL := hG.live
184  have hI := hG.inv
185  have hF := hG.fresh
186  have hne : source ≠ .blk h.nextBlk := by
187    intro he
188    subst source
189    have hfresh := Fresh.bytes hF (b := h.nextBlk) (Nat.le_refl _)
190    have hbytes : h.bytes h.nextBlk = some ebytes := by simpa using heb
191    rw [hbytes] at hfresh
192    cases hfresh
193  rw [uw_alloc_ok hL hza hI.win.wbits hw hok hF]
194  have hn : ((1 <<< st.wbits : UInt32) * 1).toNat = 2 ^ st.wbits.toNat := by
195    have := shl_toNat_aux hI.win.wbits
196    simpa using this
197  obtain ⟨A0, hA0⟩ : ∃ A0 : Array UInt8, A0 = Array.ofFn (n := ((1 <<< st.wbits : UInt32) * 1).toNat)
198      fun i => Junk.of (h.garbage h.nalloc i.val) := ⟨_, rfl⟩
199  have hA0sz : A0.size = 2 ^ st.wbits.toNat := by rw [hA0, Array.size_ofFn]; exact hn
200  have hws0 := hI.win.nullws hw
201  have hws0n : st.wsize.toNat = 0 := by rw [hws0]; rfl
202  have hA := Zlib.Zutil.Proofs.allocHeap_frame h ((1 <<< st.wbits : UInt32) * 1).toNat
203  have hAb : (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat).bytes h.nextBlk = some A0 := by
204    rw [hA0]; simp [Zlib.Zutil.Proofs.allocHeap]
205  have hAro : (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat).ro h.nextBlk = false := by
206    simp [Zlib.Zutil.Proofs.allocHeap]
207  have hS : Shape (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat)
208      (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)) :=
209    shape_setI (s0 := st) (by simpa [Zlib.Zutil.Proofs.allocHeap] using hL.hs) _
210  have hUa := uniq_allocHeap hG.uniq hF ((1 <<< st.wbits : UInt32) * 1).toNat
211  have hFa := hA.2.1 hF
212  have hG2 : Good (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk))
213      r zs z (withWin st h.nextBlk) := by
214    refine ⟨⟨?_, by simp, hL.zst, hL.back, hL.mode, hL.zalloc, hL.zfree⟩, ?_, hS.uniq hUa, hS.fresh rfl hFa⟩
215    · cases r <;> simpa [ZStreamRef.get, Zlib.Zutil.Proofs.allocHeap, setI] using hL.hz
216    · refine ⟨hI.wf, ⟨hI.win.wbits, Or.inr ⟨h.nextBlk, A0, rfl, ?_, ?_, ?_⟩, fun h0 => absurd h0 (by simp [withWin]), ?_, ?_, ?_, ?_⟩,
217        hI.reqbits, hI.bits, hI.ptr⟩
218      · simpa [setI] using hAb
219      · simpa [setI] using hAro
220      · exact hA0sz
221      · exact Or.inl hws0n
222      · have := hI.win.hv; show st.whave.toNat ≤ st.wsize.toNat; exact this
223      · right; refine ⟨hws0n, ?_⟩
224        have := hI.win.wn; show st.wnext.toNat = 0; omega
225      · intro hh; have := hI.win.hv; show st.wnext.toNat = st.whave.toNat; have := hI.win.wn; have := hI.win.hv
226        change st.whave.toNat < st.wsize.toNat at hh; omega
227  have hz2 : r.get (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)) = some z :=
228    hG2.live.hz
229  have hbe : Space.get (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs
230      (withWin st h.nextBlk)) source = some ebytes := by
231    cases source with
232    | blk b =>
233      have hbn : b ≠ h.nextBlk := fun he => hne (by cases he; rfl)
234      simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI, upd_ne _ _ _ _ hbn] using heb
235    | str b => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
236    | st_dist_code => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
237    | st_length_code => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
238    | dstate_depth b => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
239  have hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat
240      (withWin st h.nextBlk).window (2 ^ (withWin st h.nextBlk).wbits.toNat) := by
241    simp [ZlibF.Spec.Public.Separate, withWin, hne]
242  have hold0 : old = [] := by
243    rcases hold with ⟨_, he⟩ | ⟨ref, off, a, he, _⟩
244    · exact he
245    · rw [hw] at he
246      cases he
247  have hwh0 : st.whave = 0 := by
248    apply UInt32.toNat_inj.mp
249    have hwh := hI.win.hv
250    rw [hws0] at hwh
251    simpa using Nat.eq_zero_of_le_zero hwh
252  have hempty : InflateDictionary
253      (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk))
254      (withWin st h.nextBlk) [] := Or.inl ⟨by simpa [withWin] using hwh0, rfl⟩
255  obtain ⟨H', st', hrun, hgood, _, hdict⟩ := updatewindow_dictionary_existing
256    (hg := hG2) (w := h.nextBlk) (off := eo - copy.toNat) (source := source)
257    (a := A0) (bytes := ebytes) (copy := copy) (old := []) (xs := xs)
258    rfl (by simpa [setI] using hAb) (by simpa [setI] using hAro) hA0sz hbe
259    (by omega) hxs hempty hsep
260  refine ⟨H', st', ?_, hgood, ?_⟩
261  · simpa [Nat.sub_add_cancel hc, withWin] using hrun
262  · simpa [hold0, withWin] using hdict
263
264/-- The complete `updatewindow` call preserves the stream invariant and either
265retains the exact public dictionary suffix or reports a genuine allocation failure. -/
266theorem updatewindow_dictionary_public {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
267    {st : InflateState} {off : Nat} {source : BRef} {bytes : Array UInt8} {copy : UInt32}
268    {old xs : List UInt8} (hg : Good h r zs z st) (hza : z.zalloc = .fn "zcalloc")
269    (hsrc : Space.get h source = some bytes) (hfit : off + copy.toNat ≤ bytes.size)
270    (hxs : xs = (bytes.toList.drop off).take copy.toNat) (hold : InflateDictionary h st old)
271    (hsep : Separate (.ref source off) copy.toNat st.window (2 ^ st.wbits.toNat)) :
272    ∃ v after state, C.run (updatewindow (some r) (.ref source (off + copy.toNat)) copy) h =
273        .ok (v, after) ∧ Good after r zs z state ∧
274      ((v = 0 ∧ InflateDictionary after state ((old ++ xs).drop ((old ++ xs).length - 2 ^ st.wbits.toNat))) ∨
275       (v = 1 ∧ st.window = .null ∧ h.allocOk h.nalloc = false ∧
276         after = setI { h with nalloc := h.nalloc + 1 } zs st ∧ state = st)) := by
277  rcases hg.inv.win.block with hw | ⟨w, a, hw, ha, hro, hasz⟩
278  · by_cases hok : h.allocOk h.nalloc = true
279    · obtain ⟨after, state, hr, hgood, hdict⟩ :=
280        updatewindow_dictionary_new (eo := off + copy.toNat) (copy := copy)
281          hg hza hw hok hsrc (by omega) hfit (by simpa using hxs) hold
282      exact ⟨0, after, state, hr, hgood, Or.inl ⟨rfl, hdict⟩⟩
283    · have hfalse : h.allocOk h.nalloc = false := by cases he : h.allocOk h.nalloc <;> simp_all
284      have hr := uw_alloc_fail hg.live hza hg.inv.win.wbits hw hok (.ref source (off + copy.toNat)) copy
285      have hgood : Good (setI { h with nalloc := h.nalloc + 1 } zs st) r zs z st := by
286        have hz' : r.get { h with nalloc := h.nalloc + 1 } = some z := by
287          cases r <;> simpa [ZStreamRef.get] using hg.live.hz
288        have he := good_set (h0 := { h with nalloc := h.nalloc + 1 }) (z0 := z) (z' := z)
289          (s0 := st) (st' := st) hg.live.hz hg.live.hs hg.uniq hg.fresh hg.live.zst
290          hg.live.zalloc hg.live.zfree hg.live.back hg.live.mode (StInv.congr (h := h) rfl rfl hg.inv)
291        rwa [ZStreamRef.put_self hz'] at he
292      exact ⟨1, _, st, hr, hgood, Or.inr ⟨rfl, hw, hfalse, rfl, rfl⟩⟩
293  · obtain ⟨after, state, hr, hgood, _, hdict⟩ :=
294      updatewindow_dictionary_existing hg hw ha hro hasz hsrc hfit hxs hold hsep
295    exact ⟨0, after, state, hr, hgood, Or.inl ⟨rfl, hdict⟩⟩
296
297#print axioms updatewindow_dictionary_public
298#print axioms updatewindow_dictionary_new
299#print axioms updatewindow_ring_public
300#print axioms ringList_public
301#print axioms inflateDictionary_eq_ring
302#print axioms updatewindow_dictionary_existing
303end Zlib.Inflate.Proofs