inflate.c.window-compose.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-general»
2
3namespace Zlib.Inflate.Proofs
4open C Zlib.Inflate Zlib.Inflate.Spec
5
6theorem uw_main_public {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {w eo : Nat} {source : BRef}
7    {a ebytes : Array UInt8} {copy : UInt32}
8    (hL : Live H r zs z st) (hw : st.window = .ref (.blk w) 0) (ha : H.bytes w = some a) (hro : H.ro w = false)
9    (hwb : st.wbits.toNat ≤ 15) (hasz : a.size = 2 ^ st.wbits.toNat)
10    (hws : st.wsize.toNat = 0 ∨ st.wsize.toNat = 2 ^ st.wbits.toNat)
11    (hwn : st.wnext.toNat < st.wsize.toNat ∨ (st.wsize.toNat = 0 ∧ st.wnext.toNat = 0))
12    (heb : Space.get H source = some ebytes) (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size)
13    (hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat st.window (2 ^ st.wbits.toNat)) :
14    updatewindow (some r) (.ref source eo) copy H = .ok (0, setI
15      { setI H zs (initWinS st) with bytes := upd H.bytes w (some (uwPost (initWinS st) a ebytes eo copy).1) } zs
16      (uwPost (initWinS st) a ebytes eo copy).2) := by
17  have hpow := shl_toNat_aux hwb
18  have h2pos := Nat.two_pow_pos st.wbits.toNat
19  have hcase : (st.wsize = 0 ∧ initWinS st = { st with wsize := (1 : UInt32) <<< st.wbits, wnext := 0, whave := 0 }) ∨
20      (st.wsize ≠ 0 ∧ initWinS st = st) := by
21    by_cases h0 : st.wsize = 0
22    · left; exact ⟨h0, by simp [initWinS, h0]⟩
23    · right; exact ⟨h0, by simp [initWinS, h0]⟩
24  have hpos : (initWinS st).wsize ≠ 0 ∧ (initWinS st).wsize.toNat = 2 ^ st.wbits.toNat ∧ (initWinS st).wnext.toNat < (initWinS st).wsize.toNat := by
25    rcases hcase with ⟨h0, e⟩ | ⟨h0, e⟩
26    · rw [e]
27      have hz0 : ((1 : UInt32) <<< st.wbits).toNat = 2 ^ st.wbits.toNat := hpow
28      refine ⟨fun hh => ?_, hz0, ?_⟩
29      · have h0' : ((1 : UInt32) <<< st.wbits).toNat = 0 := by
30          have hh' : ((1 : UInt32) <<< st.wbits) = 0 := hh
31          rw [hh']; rfl
32        omega
33      · show (0 : UInt32).toNat < ((1 : UInt32) <<< st.wbits).toNat
34        rw [hz0]; simp; omega
35    · rw [e]
36      have : st.wsize.toNat ≠ 0 := fun hh => h0 (UInt32.toNat_inj.mp (by simpa using hh))
37      refine ⟨h0, by omega, by omega⟩
38  have hfull := hpos.2.1
39  have hsz1 : (initWinS st).wsize.toNat ≤ a.size := by omega
40  have hwn1 := hpos.2.2
41  have hpos := hpos.1
42  have hL1 : Live (setI H zs (initWinS st)) r zs z (initWinS st) :=
43    ⟨by simpa using hL.hz, by simp, hL.zst, by unfold initWinS; split <;> exact hL.back, by unfold initWinS; split <;> exact hL.mode,
44      hL.zalloc, hL.zfree⟩
45  have hw1 : (initWinS st).window = .ref (.blk w) 0 := by unfold initWinS; split <;> exact hw
46  rw [uw_init hL hw hwb]
47  have ha1 : (setI H zs (initWinS st)).bytes w = some a := ha
48  have hro1 : (setI H zs (initWinS st)).ro w = false := hro
49  have heb1 : Space.get (setI H zs (initWinS st)) source = some ebytes := by
50    cases source <;> simpa [Space.get, setI] using heb
51  have hsep1 : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat
52      (initWinS st).window (initWinS st).wsize.toNat := by
53    simpa only [hw1, hw, hfull] using hsep
54  by_cases hbig : (initWinS st).wsize ≤ copy
55  · have := uw_core_big_public hL1 hw1 ha1 hro1 hpos hsz1 heb1 hc hoff hsep1 hbig
56    simpa [uwPost, hbig] using this
57  · by_cases hP : (initWinS st).wsize - (initWinS st).wnext > copy
58    · have hlt : copy.toNat < (initWinS st).wsize.toNat := by
59        have : ¬ (initWinS st).wsize ≤ copy := hbig
60        rw [UInt32.le_iff_toNat_le] at this; omega
61      have := uw_core_small1_public hL1 hw1 ha1 hro1 hpos hsz1 hwn1 heb1 hc hoff hsep1 hbig hP
62      simpa [uwPost, hbig, hP] using this
63    · by_cases hR : copy - ((initWinS st).wsize - (initWinS st).wnext) = 0
64      · have hlt : copy.toNat < (initWinS st).wsize.toNat := by
65          have : ¬ (initWinS st).wsize ≤ copy := hbig
66          rw [UInt32.le_iff_toNat_le] at this; omega
67        have := uw_core_small3_public hL1 hw1 ha1 hro1 hpos hsz1 hwn1 heb1 hc hoff hsep1 hbig hP hR
68        simpa [uwPost, hbig, hP, hR] using this
69      · have hlt : copy.toNat < (initWinS st).wsize.toNat := by
70          have : ¬ (initWinS st).wsize ≤ copy := hbig
71          rw [UInt32.le_iff_toNat_le] at this; omega
72        have := uw_core_small2_public hL1 hw1 ha1 hro1 hpos hsz1 hwn1 heb1 hc hoff hsep1 hbig hP hR
73        simpa [uwPost, hbig, hP, hR] using this
74
75theorem uw_post_public {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {w eo : Nat} {source : BRef}
76    {a ebytes : Array UInt8} {copy : UInt32}
77    (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)
78    (hasz : a.size = 2 ^ st.wbits.toNat)
79    (heb : Space.get H source = some ebytes) (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size)
80    (hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat st.window (2 ^ st.wbits.toNat)) :
81    ∃ H' st', updatewindow (some r) (.ref source eo) copy H = .ok (0, H') ∧
82      H' = setI { setI H zs (initWinS st) with bytes := upd H.bytes w (some (uwPost (initWinS st) a ebytes eo copy).1) } zs st' ∧
83      st' = (uwPost (initWinS st) a ebytes eo copy).2 ∧ Good H' r zs z st' ∧ st'.window = st.window ∧
84      H'.bytes w = some (uwPost (initWinS st) a ebytes eo copy).1 ∧ (uwPost (initWinS st) a ebytes eo copy).1.size = a.size ∧
85      (∀ b, b ≠ w → H'.bytes b = H.bytes b) ∧ (∀ b, H'.live b ↔ H.live b) ∧ H'.nextBlk = H.nextBlk := by
86  have hL := hG.live
87  have hI := hG.inv
88  have hmain := uw_main_public hL hw ha hro hI.win.wbits hasz hI.win.ws hI.win.wn heb hc hoff hsep
89  obtain ⟨f1, f2, f3, hv1, hwn1, heq1, f4, f5, f6, f7, f8, f16, f17, f18, f12, f13⟩ :=
90    initWinS_facts hI.win.wbits hI.win.ws hI.win.hv hI.win.wn hI.win.eq
91  have hwb := hI.win.wbits
92  have hle : (initWinS st).wsize.toNat ≤ 2 ^ 16 := by
93    rw [f1]; have := Nat.pow_le_pow_right (by decide : 0 < 2) (by omega : st.wbits.toNat ≤ 16); omega
94  have hposn : (initWinS st).wsize.toNat ≠ 0 := by rw [f1]; exact Nat.pos_iff_ne_zero.mp (Nat.two_pow_pos _)
95  obtain ⟨g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, gv, gwn, geq⟩ :=
96    uwPost_arith (st := initWinS st) (a := a) (ebytes := ebytes) (eo := eo) (copy := copy) hposn hv1 hwn1 heq1 copy.toNat_lt hle
97  have hAsz := uwPost_size (initWinS st) a ebytes eo copy
98  generalize hP : uwPost (initWinS st) a ebytes eo copy = P at *
99  have hs1 : (setI H zs (initWinS st)).istates zs = some (initWinS st) := by simp
100  have hbw : (setI H zs (initWinS st)).bytes w = some a := ha
101  have hS : Shape H { setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } :=
102    (shape_setI hL.hs _).trans (shape_setB (h := setI H zs (initWinS st)) hbw P.1)
103  have hS2 : Shape H (setI { setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } zs P.2) :=
104    hS.trans (shape_setI (s0 := initWinS st) (by simp) _)
105  have hz0 : r.get { setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } = some z := by
106    cases r <;> simpa [ZStreamRef.get] using hL.hz
107  have hs0 : ({ setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } : Heap).istates zs = some (initWinS st) := by
108    simp
109  have hUh : Uniq { setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } := hS.uniq hG.uniq
110  have hFh : Fresh { setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } := hS.fresh (by simp) hG.fresh
111  have hstI : StInv { setI H zs (initWinS st) with bytes := upd H.bytes w (some P.1) } zs P.2 := by
112    refine ⟨?_, ?_, ?_, ?_, ?_⟩
113    · obtain ⟨w1, w2, w3⟩ := hI.wf
114      exact ⟨by rw [g9, f16]; exact w1, by rw [g10, f17]; exact w2, by rw [g11, f18]; exact w3⟩
115    · refine ⟨by rw [g2, f2]; exact hI.win.wbits, Or.inr ⟨w, P.1, by rw [g3, f3]; exact hw, by simp, by simpa using hro, ?_⟩,
116        fun h0 => ?_, ?_, gv, Or.inl gwn, geq⟩
117      · rw [g2, f2, hAsz, hasz]
118      · rw [g3, f3, hw] at h0; cases h0
119      · rw [g1, f1, g2, f2]; right; rfl
120    · rw [g4, f4]; exact hI.reqbits
121    · rw [g5, f5]; exact hI.bits
122    · unfold PtrInv; rw [g6, f6, g7, f7, g8, f8]; exact hI.ptr
123  refine ⟨_, P.2, hmain, rfl, rfl, ?_, by rw [g3, f3], by simp, hAsz, ?_, fun b => hS2.live b, by simp⟩
124  · have := good_set hz0 hs0 hUh hFh hL.zst hL.zalloc hL.zfree (by rw [g12, f12]; exact hL.back)
125      (by rw [g13, f13]; exact hL.mode) hstI
126    rwa [ZStreamRef.put_self hz0] at this
127  · intro b hb; simp [upd_ne _ _ _ _ hb]
128
129theorem uw_null_ok_public {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {eo : Nat} {source : BRef}
130    {ebytes : Array UInt8} {copy : UInt32}
131    (hG : Good h r zs z st) (hza : z.zalloc = .fn "zcalloc") (hw : st.window = .null)
132    (hok : h.allocOk h.nalloc = true) (heb : Space.get h source = some ebytes) (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size) :
133    ∃ H' st', updatewindow (some r) (.ref source eo) copy h = .ok (0, H') ∧ Good H' r zs z st' ∧
134      st'.window = .ref (.blk h.nextBlk) 0 ∧ (∃ A, H'.bytes h.nextBlk = some A) ∧
135      (∀ S, h.Owns S → H'.Owns (fun b => S b ∨ b = h.nextBlk)) ∧ H'.nextBlk = h.nextBlk + 1 ∧
136      (∀ b, b ≠ h.nextBlk → H'.bytes b = h.bytes b) := by
137  have hL := hG.live
138  have hI := hG.inv
139  have hF := hG.fresh
140  have hne : source ≠ .blk h.nextBlk := by
141    intro he
142    subst source
143    have hfresh := Fresh.bytes hF (b := h.nextBlk) (Nat.le_refl _)
144    have hbytes : h.bytes h.nextBlk = some ebytes := by simpa using heb
145    rw [hbytes] at hfresh
146    cases hfresh
147  rw [uw_alloc_ok hL hza hI.win.wbits hw hok hF]
148  have hn : ((1 <<< st.wbits : UInt32) * 1).toNat = 2 ^ st.wbits.toNat := by
149    have := shl_toNat_aux hI.win.wbits
150    simpa using this
151  obtain ⟨A0, hA0⟩ : ∃ A0 : Array UInt8, A0 = Array.ofFn (n := ((1 <<< st.wbits : UInt32) * 1).toNat)
152      fun i => Junk.of (h.garbage h.nalloc i.val) := ⟨_, rfl⟩
153  have hA0sz : A0.size = 2 ^ st.wbits.toNat := by rw [hA0, Array.size_ofFn]; exact hn
154  have hws0 := hI.win.nullws hw
155  have hws0n : st.wsize.toNat = 0 := by rw [hws0]; rfl
156  have hA := Zlib.Zutil.Proofs.allocHeap_frame h ((1 <<< st.wbits : UInt32) * 1).toNat
157  have hAb : (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat).bytes h.nextBlk = some A0 := by
158    rw [hA0]; simp [Zlib.Zutil.Proofs.allocHeap]
159  have hAro : (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat).ro h.nextBlk = false := by
160    simp [Zlib.Zutil.Proofs.allocHeap]
161  have hS : Shape (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat)
162      (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)) :=
163    shape_setI (s0 := st) (by simpa [Zlib.Zutil.Proofs.allocHeap] using hL.hs) _
164  have hUa := uniq_allocHeap hG.uniq hF ((1 <<< st.wbits : UInt32) * 1).toNat
165  have hFa := hA.2.1 hF
166  have hG2 : Good (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk))
167      r zs z (withWin st h.nextBlk) := by
168    refine ⟨⟨?_, by simp, hL.zst, hL.back, hL.mode, hL.zalloc, hL.zfree⟩, ?_, hS.uniq hUa, hS.fresh rfl hFa⟩
169    · cases r <;> simpa [ZStreamRef.get, Zlib.Zutil.Proofs.allocHeap, setI] using hL.hz
170    · refine ⟨hI.wf, ⟨hI.win.wbits, Or.inr ⟨h.nextBlk, A0, rfl, ?_, ?_, ?_⟩, fun h0 => absurd h0 (by simp [withWin]), ?_, ?_, ?_, ?_⟩,
171        hI.reqbits, hI.bits, hI.ptr⟩
172      · simpa [setI] using hAb
173      · simpa [setI] using hAro
174      · exact hA0sz
175      · exact Or.inl hws0n
176      · have := hI.win.hv; show st.whave.toNat ≤ st.wsize.toNat; exact this
177      · right; refine ⟨hws0n, ?_⟩
178        have := hI.win.wn; show st.wnext.toNat = 0; omega
179      · intro hh; have := hI.win.hv; show st.wnext.toNat = st.whave.toNat; have := hI.win.wn; have := hI.win.hv
180        change st.whave.toNat < st.wsize.toNat at hh; omega
181  have hz2 : r.get (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)) = some z :=
182    hG2.live.hz
183  have hbe : Space.get (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs
184      (withWin st h.nextBlk)) source = some ebytes := by
185    cases source with
186    | blk b =>
187      have hbn : b ≠ h.nextBlk := fun he => hne (by cases he; rfl)
188      simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI, upd_ne _ _ _ _ hbn] using heb
189    | str b => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
190    | st_dist_code => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
191    | st_length_code => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
192    | dstate_depth b => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
193  have hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat
194      (withWin st h.nextBlk).window (2 ^ (withWin st h.nextBlk).wbits.toNat) := by
195    simp [ZlibF.Spec.Public.Separate, withWin, hne]
196  obtain ⟨H', st', hrun, -, hst', hG', hw', hb', hsz', hbo, hlive, hnb⟩ :=
197    uw_post_public (hG := hG2) (w := h.nextBlk) (source := source) (eo := eo)
198      (a := A0) (ebytes := ebytes) (copy := copy) rfl (by simpa [setI] using hAb)
199      (by simpa [setI] using hAro) (by exact hA0sz) hbe hc hoff hsep
200  refine ⟨H', st', hrun, hG', by rw [hw']; rfl, ⟨_, hb'⟩, ?_, ?_, ?_⟩
201  · intro S hO
202    have h2 := hS.owns (hA.1 S hO)
203    exact fun b => (hlive b).trans (h2 b)
204  · rw [hnb]; simp [Zlib.Zutil.Proofs.allocHeap, setI]
205  · intro b hb; rw [hbo b (by exact hb)]; simp [Zlib.Zutil.Proofs.allocHeap, setI, upd_ne _ _ _ _ hb]
206
207theorem updatewindow_safe_public {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {eo : Nat} {source : BRef}
208    {ebytes : Array UInt8} {copy : UInt32}
209    (hG : Good h r zs z st) (hza : z.zalloc = .fn "zcalloc") (heb : Space.get h source = some ebytes)
210    (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size) (hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat st.window (2 ^ st.wbits.toNat)) :
211    ∃ v h' st', C.run (updatewindow (some r) (.ref source eo) copy) h = .ok (v, h') ∧ Good h' r zs z st' ∧
212      ((v = 0 ∧ st'.window ≠ .null ∧
213          (∀ S, h.Owns S → h'.Owns (fun b => S b ∨ (st.window = .null ∧ b = h.nextBlk)))) ∨
214       (v = 1 ∧ st.window = .null ∧ ¬ h.allocOk h.nalloc = true ∧ h' = setI { h with nalloc := h.nalloc + 1 } zs st ∧ st' = st)) := by
215  have hL := hG.live
216  have hI := hG.inv
217  rcases hI.win.block with hw | ⟨w, a, hw, ha, hro, hasz⟩
218  · by_cases hok : h.allocOk h.nalloc = true
219    · obtain ⟨H', st', hrun, hG', hw', -, hO, -, -⟩ := uw_null_ok_public hG hza hw hok heb hc hoff
220      refine ⟨0, H', st', hrun, hG', Or.inl ⟨0 |> fun _ => rfl, by rw [hw']; simp, ?_⟩⟩
221      intro S hOw
222      have := hO S hOw
223      simpa [hw] using this
224    · have hrun := uw_alloc_fail hL hza hI.win.wbits hw hok (.ref source eo) copy
225      refine ⟨1, _, st, hrun, ?_, Or.inr ⟨rfl, hw, hok, rfl, rfl⟩⟩
226      have hS : Shape h { h with nalloc := h.nalloc + 1 } := Shape.refl h
227      have := good_set (h0 := { h with nalloc := h.nalloc + 1 }) (z0 := z) (z' := z) (s0 := st) (st' := st) hL.hz hL.hs
228        hG.uniq hG.fresh hL.zst hL.zalloc hL.zfree hL.back hL.mode (StInv.congr (h := h) rfl rfl hI)
229      have hz' : r.get { h with nalloc := h.nalloc + 1 } = some z := by cases r <;> simpa [ZStreamRef.get] using hL.hz
230      rwa [ZStreamRef.put_self hz'] at this
231  · obtain ⟨H', st', hrun, -, -, hG', hw', -, -, -, hlive, -⟩ := uw_post_public hG hw ha hro hasz heb hc hoff hsep
232    refine ⟨0, H', st', hrun, hG', Or.inl ⟨rfl, by rw [hw', hw]; simp, ?_⟩⟩
233    intro S hO b
234    rw [hlive b, hO b]
235    simp [hw]
236
237#print axioms updatewindow_safe_public
238#print axioms uw_null_ok_public
239#print axioms uw_post_public
240#print axioms uw_main_public
241end Zlib.Inflate.Proofs