inflate.c.window-public-mode.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-public-ring»
2import ZlibF.Spec.Public.Lifecycle
3
4namespace Zlib.Inflate.Proofs
5open C Zlib.Inflate Zlib.Inflate.Spec ZlibF.Spec.Public
6
7private theorem uwPost_mode (s : InflateState) (a b : Array UInt8) (eo : Nat) (n : UInt32) :
8    (uwPost (initWinS s) a b eo n).2.mode = s.mode := by
9  have hh : (uwPost (initWinS s) a b eo n).2 =
10      { s with
11        window := (uwPost (initWinS s) a b eo n).2.window
12        wsize := (uwPost (initWinS s) a b eo n).2.wsize
13        whave := (uwPost (initWinS s) a b eo n).2.whave
14        wnext := (uwPost (initWinS s) a b eo n).2.wnext } := by
15    unfold uwPost initWinS
16    repeat' split
17    all_goals rfl
18  have hm := congrArg InflateState.mode hh
19  exact hm
20
21/-- An existing-window update changes only the owned state and window blocks. -/
22theorem uw_existing_frame {h : Heap} {r : ZStreamRef} {zs w : Nat} {st st0 st1 : InflateState}
23    {a : Array UInt8} (hw : st.window = .ref (.blk w) 0) :
24    Frame h (setI { setI h zs st0 with bytes := upd h.bytes w (some a) } zs st1)
25      (fun b => StreamRoot r b ∨ InflateOwned zs st b) := by
26  simp only [Frame, setI, true_and]
27  refine ⟨Nat.le_refl _, Nat.le_refl _, ?_⟩
28  intro b _ hb
29  have hi : b ≠ zs := fun he => hb (Or.inr (Or.inl he))
30  have hw' : b ≠ w := fun he => hb (Or.inr (Or.inr (by simpa [hw] using he.symm)))
31  simp [upd_ne, hi, hw']
32
33/-- A new-window update changes only the owned state among pre-existing
34objects; the allocated block was not live before the call. -/
35theorem uw_new_frame {h : Heap} {r : ZStreamRef} {zs n : Nat} {st st0 st1 st2 : InflateState}
36    {a : Array UInt8} (hf : Fresh h) :
37    let alloc := Zlib.Zutil.Proofs.allocHeap h n
38    let prior := setI alloc zs st0
39    Frame h (setI { setI prior zs st1 with bytes := upd prior.bytes h.nextBlk (some a) } zs st2)
40      (fun b => StreamRoot r b ∨ InflateOwned zs st b) := by
41  dsimp only
42  simp only [Frame, setI, Zlib.Zutil.Proofs.allocHeap, true_and]
43  refine ⟨Nat.le_succ _, Nat.le_succ _, ?_⟩
44  intro b hl hb
45  have hi : b ≠ zs := fun he => hb (Or.inr (Or.inl he))
46  have hn : b ≠ h.nextBlk := fun he => hf b (by omega) hl
47  simp [upd_ne, hi, hn]
48
49/-- Allocation followed by a successful window update preserves the stream mode. -/
50theorem uw_null_mode_public {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
51    {st : InflateState} {eo : Nat} {source : BRef} {ebytes : Array UInt8} {copy : UInt32}
52    (hG : Good h r zs z st) (hza : z.zalloc = .fn "zcalloc") (hw : st.window = .null)
53    (hok : h.allocOk h.nalloc = true) (heb : Space.get h source = some ebytes)
54    (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size) :
55    ∃ after state, updatewindow (some r) (.ref source eo) copy h = .ok (0, after) ∧
56      Good after r zs z state ∧ state.mode = st.mode := by
57  have hL := hG.live
58  have hI := hG.inv
59  have hF := hG.fresh
60  have hne : source ≠ .blk h.nextBlk := by
61    intro he
62    subst source
63    have hfresh := Fresh.bytes hF (b := h.nextBlk) (Nat.le_refl _)
64    have hbytes : h.bytes h.nextBlk = some ebytes := by simpa using heb
65    rw [hbytes] at hfresh
66    cases hfresh
67  rw [uw_alloc_ok hL hza hI.win.wbits hw hok hF]
68  have hn : ((1 <<< st.wbits : UInt32) * 1).toNat = 2 ^ st.wbits.toNat := by
69    have := shl_toNat_aux hI.win.wbits
70    simpa using this
71  obtain ⟨A0, hA0⟩ : ∃ A0 : Array UInt8, A0 = Array.ofFn (n := ((1 <<< st.wbits : UInt32) * 1).toNat)
72      fun i => Junk.of (h.garbage h.nalloc i.val) := ⟨_, rfl⟩
73  have hA0sz : A0.size = 2 ^ st.wbits.toNat := by rw [hA0, Array.size_ofFn]; exact hn
74  have hws0 := hI.win.nullws hw
75  have hws0n : st.wsize.toNat = 0 := by rw [hws0]; rfl
76  have hA := Zlib.Zutil.Proofs.allocHeap_frame h ((1 <<< st.wbits : UInt32) * 1).toNat
77  have hAb : (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat).bytes h.nextBlk = some A0 := by
78    rw [hA0]; simp [Zlib.Zutil.Proofs.allocHeap]
79  have hAro : (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat).ro h.nextBlk = false := by
80    simp [Zlib.Zutil.Proofs.allocHeap]
81  have hS : Shape (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat)
82      (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)) :=
83    shape_setI (s0 := st) (by simpa [Zlib.Zutil.Proofs.allocHeap] using hL.hs) _
84  have hUa := uniq_allocHeap hG.uniq hF ((1 <<< st.wbits : UInt32) * 1).toNat
85  have hFa := hA.2.1 hF
86  have hG2 : Good (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk))
87      r zs z (withWin st h.nextBlk) := by
88    refine ⟨⟨?_, by simp, hL.zst, hL.back, hL.mode, hL.zalloc, hL.zfree⟩, ?_, hS.uniq hUa, hS.fresh rfl hFa⟩
89    · cases r <;> simpa [ZStreamRef.get, Zlib.Zutil.Proofs.allocHeap, setI] using hL.hz
90    · refine ⟨hI.wf, ⟨hI.win.wbits, Or.inr ⟨h.nextBlk, A0, rfl, ?_, ?_, ?_⟩, fun h0 => absurd h0 (by simp [withWin]), ?_, ?_, ?_, ?_⟩,
91        hI.reqbits, hI.bits, hI.ptr⟩
92      · simpa [setI] using hAb
93      · simpa [setI] using hAro
94      · exact hA0sz
95      · exact Or.inl hws0n
96      · have := hI.win.hv; show st.whave.toNat ≤ st.wsize.toNat; exact this
97      · right; refine ⟨hws0n, ?_⟩
98        have := hI.win.wn; show st.wnext.toNat = 0; omega
99      · intro hh; have := hI.win.hv; show st.wnext.toNat = st.whave.toNat; have := hI.win.wn; have := hI.win.hv
100        change st.whave.toNat < st.wsize.toNat at hh; omega
101  have hz2 : r.get (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)) = some z :=
102    hG2.live.hz
103  have hbe : Space.get (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs
104      (withWin st h.nextBlk)) source = some ebytes := by
105    cases source with
106    | blk b =>
107      have hbn : b ≠ h.nextBlk := fun he => hne (by cases he; rfl)
108      simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI, upd_ne _ _ _ _ hbn] using heb
109    | str b => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
110    | st_dist_code => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
111    | st_length_code => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
112    | dstate_depth b => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
113  have hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat
114      (withWin st h.nextBlk).window (2 ^ (withWin st h.nextBlk).wbits.toNat) := by
115    simp [ZlibF.Spec.Public.Separate, withWin, hne]
116  obtain ⟨after, state, hr, _, hstate, hgood, _, _, _, _, _, _⟩ :=
117    uw_post_public (hG := hG2) (w := h.nextBlk) (source := source) (eo := eo)
118      (a := A0) (ebytes := ebytes) (copy := copy) rfl (by simpa [setI] using hAb)
119      (by simpa [setI] using hAro) hA0sz hbe hc hoff hsep
120  refine ⟨after, state, hr, hgood, ?_⟩
121  rw [hstate, uwPost_mode]
122  rfl
123
124/-- Allocation followed by an update preserves the public frame of every
125pre-existing unowned object. -/
126theorem uw_null_frame_public {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
127    {st : InflateState} {eo : Nat} {source : BRef} {ebytes : Array UInt8} {copy : UInt32}
128    (hG : Good h r zs z st) (hza : z.zalloc = .fn "zcalloc") (hw : st.window = .null)
129    (hok : h.allocOk h.nalloc = true) (heb : Space.get h source = some ebytes)
130    (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size) :
131    ∃ after state, updatewindow (some r) (.ref source eo) copy h = .ok (0, after) ∧
132      Good after r zs z state ∧ Frame h after (fun b => StreamRoot r b ∨ InflateOwned zs st b) := by
133  have hL := hG.live
134  have hI := hG.inv
135  have hF := hG.fresh
136  have hne : source ≠ .blk h.nextBlk := by
137    intro he
138    subst source
139    have hfresh := Fresh.bytes hF (b := h.nextBlk) (Nat.le_refl _)
140    have hbytes : h.bytes h.nextBlk = some ebytes := by simpa using heb
141    rw [hbytes] at hfresh
142    cases hfresh
143  rw [uw_alloc_ok hL hza hI.win.wbits hw hok hF]
144  have hn : ((1 <<< st.wbits : UInt32) * 1).toNat = 2 ^ st.wbits.toNat := by
145    have := shl_toNat_aux hI.win.wbits
146    simpa using this
147  obtain ⟨A0, hA0⟩ : ∃ A0 : Array UInt8, A0 = Array.ofFn (n := ((1 <<< st.wbits : UInt32) * 1).toNat)
148      fun i => Junk.of (h.garbage h.nalloc i.val) := ⟨_, rfl⟩
149  have hA0sz : A0.size = 2 ^ st.wbits.toNat := by rw [hA0, Array.size_ofFn]; exact hn
150  have hws0 := hI.win.nullws hw
151  have hws0n : st.wsize.toNat = 0 := by rw [hws0]; rfl
152  have hA := Zlib.Zutil.Proofs.allocHeap_frame h ((1 <<< st.wbits : UInt32) * 1).toNat
153  have hAb : (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat).bytes h.nextBlk = some A0 := by
154    rw [hA0]; simp [Zlib.Zutil.Proofs.allocHeap]
155  have hAro : (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat).ro h.nextBlk = false := by
156    simp [Zlib.Zutil.Proofs.allocHeap]
157  have hS : Shape (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat)
158      (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)) :=
159    shape_setI (s0 := st) (by simpa [Zlib.Zutil.Proofs.allocHeap] using hL.hs) _
160  have hUa := uniq_allocHeap hG.uniq hF ((1 <<< st.wbits : UInt32) * 1).toNat
161  have hFa := hA.2.1 hF
162  have hG2 : Good (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk))
163      r zs z (withWin st h.nextBlk) := by
164    refine ⟨⟨?_, by simp, hL.zst, hL.back, hL.mode, hL.zalloc, hL.zfree⟩, ?_, hS.uniq hUa, hS.fresh rfl hFa⟩
165    · cases r <;> simpa [ZStreamRef.get, Zlib.Zutil.Proofs.allocHeap, setI] using hL.hz
166    · refine ⟨hI.wf, ⟨hI.win.wbits, Or.inr ⟨h.nextBlk, A0, rfl, ?_, ?_, ?_⟩, fun h0 => absurd h0 (by simp [withWin]), ?_, ?_, ?_, ?_⟩,
167        hI.reqbits, hI.bits, hI.ptr⟩
168      · simpa [setI] using hAb
169      · simpa [setI] using hAro
170      · exact hA0sz
171      · exact Or.inl hws0n
172      · have := hI.win.hv; show st.whave.toNat ≤ st.wsize.toNat; exact this
173      · right; refine ⟨hws0n, ?_⟩
174        have := hI.win.wn; show st.wnext.toNat = 0; omega
175      · intro hh; have := hI.win.hv; show st.wnext.toNat = st.whave.toNat; have := hI.win.wn; have := hI.win.hv
176        change st.whave.toNat < st.wsize.toNat at hh; omega
177  have hz2 : r.get (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs (withWin st h.nextBlk)) = some z :=
178    hG2.live.hz
179  have hbe : Space.get (setI (Zlib.Zutil.Proofs.allocHeap h ((1 <<< st.wbits : UInt32) * 1).toNat) zs
180      (withWin st h.nextBlk)) source = some ebytes := by
181    cases source with
182    | blk b =>
183      have hbn : b ≠ h.nextBlk := fun he => hne (by cases he; rfl)
184      simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI, upd_ne _ _ _ _ hbn] using heb
185    | str b => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
186    | st_dist_code => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
187    | st_length_code => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
188    | dstate_depth b => simpa [Space.get, Zlib.Zutil.Proofs.allocHeap, setI] using heb
189  have hsep : ZlibF.Spec.Public.Separate (.ref source (eo - copy.toNat)) copy.toNat
190      (withWin st h.nextBlk).window (2 ^ (withWin st h.nextBlk).wbits.toNat) := by
191    simp [ZlibF.Spec.Public.Separate, withWin, hne]
192  obtain ⟨after, state, hr, he, _, hgood, _, _, _, _, _, _⟩ :=
193    uw_post_public (hG := hG2) (w := h.nextBlk) (source := source) (eo := eo)
194      (a := A0) (ebytes := ebytes) (copy := copy) rfl (by simpa [setI] using hAb)
195      (by simpa [setI] using hAro) hA0sz hbe hc hoff hsep
196  refine ⟨after, state, hr, hgood, ?_⟩
197  rw [he]
198  exact uw_new_frame hF
199
200/-- A successful `updatewindow` preserves the stream mode for all readable
201sources permitted by the public range-separation condition. -/
202theorem updatewindow_mode_public {h after : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
203    {st state : InflateState} {off : Nat} {source : BRef} {bytes : Array UInt8} {copy : UInt32}
204    (hg : Good h r zs z st) (hza : z.zalloc = .fn "zcalloc")
205    (hsrc : Space.get h source = some bytes) (hfit : off + copy.toNat ≤ bytes.size)
206    (hsep : Separate (.ref source off) copy.toNat st.window (2 ^ st.wbits.toNat))
207    (hr : C.run (updatewindow (some r) (.ref source (off + copy.toNat)) copy) h = .ok (0, after))
208    (hstate : after.istates zs = some state) : state.mode = st.mode := by
209  change updatewindow (some r) (.ref source (off + copy.toNat)) copy h = .ok (0, after) at hr
210  have hsep' : Separate (.ref source ((off + copy.toNat) - copy.toNat)) copy.toNat
211      st.window (2 ^ st.wbits.toNat) := by simpa using hsep
212  rcases hg.inv.win.block with hw | ⟨w, a, hw, ha, hro, hasz⟩
213  · by_cases hok : h.allocOk h.nalloc = true
214    · obtain ⟨result, s', hrun, hgood, hmode⟩ :=
215        uw_null_mode_public (copy := copy) (eo := off + copy.toNat) hg hza hw hok hsrc (by omega) hfit
216      have he : after = result := by rw [hr] at hrun; cases hrun; rfl
217      subst result
218      have hs : state = s' := Option.some.inj (hstate.symm.trans hgood.live.hs)
219      simpa [hs] using hmode
220    · have hfail := uw_alloc_fail hg.live hza hg.inv.win.wbits hw hok
221        (.ref source (off + copy.toNat)) copy
222      rw [hr] at hfail
223      cases hfail
224  · obtain ⟨result, s', hrun, _, hs', hgood, _, _, _, _, _, _⟩ :=
225      uw_post_public (copy := copy) (eo := off + copy.toNat) hg hw ha hro hasz hsrc (by omega) hfit hsep'
226    have he : after = result := by rw [hr] at hrun; cases hrun; rfl
227    have hgood' : Good after r zs z s' := by rw [he]; exact hgood
228    have hs : state = s' := Option.some.inj (hstate.symm.trans hgood'.live.hs)
229    rw [hs, hs', uwPost_mode]
230
231/-- A successful `updatewindow` preserves the public frame. -/
232theorem updatewindow_frame_public {h after : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
233    {st : InflateState} {off : Nat} {source : BRef} {bytes : Array UInt8} {copy : UInt32}
234    (hg : Good h r zs z st) (hza : z.zalloc = .fn "zcalloc")
235    (hsrc : Space.get h source = some bytes) (hfit : off + copy.toNat ≤ bytes.size)
236    (hsep : Separate (.ref source off) copy.toNat st.window (2 ^ st.wbits.toNat))
237    (hr : C.run (updatewindow (some r) (.ref source (off + copy.toNat)) copy) h = .ok (0, after)) :
238    Frame h after (fun b => StreamRoot r b ∨ InflateOwned zs st b) := by
239  change updatewindow (some r) (.ref source (off + copy.toNat)) copy h = .ok (0, after) at hr
240  have hsep' : Separate (.ref source ((off + copy.toNat) - copy.toNat)) copy.toNat
241      st.window (2 ^ st.wbits.toNat) := by simpa using hsep
242  rcases hg.inv.win.block with hw | ⟨w, a, hw, ha, hro, hasz⟩
243  · by_cases hok : h.allocOk h.nalloc = true
244    · obtain ⟨result, _, hrun, _, hframe⟩ :=
245        uw_null_frame_public (copy := copy) (eo := off + copy.toNat) hg hza hw hok hsrc (by omega) hfit
246      have he : after = result := by rw [hr] at hrun; cases hrun; rfl
247      simpa [he] using hframe
248    · have hfail := uw_alloc_fail hg.live hza hg.inv.win.wbits hw hok
249        (.ref source (off + copy.toNat)) copy
250      rw [hr] at hfail
251      cases hfail
252  · obtain ⟨result, s', hrun, he, _, _, _, _, _, _, _, _⟩ :=
253      uw_post_public (copy := copy) (eo := off + copy.toNat) hg hw ha hro hasz hsrc (by omega) hfit hsep'
254    have heq : after = result := by rw [hr] at hrun; cases hrun; rfl
255    rw [heq, he]
256    exact uw_existing_frame hw
257
258/-- A successful `updatewindow` retains all existing objects and allocates
259only its new owned window, if one was needed. -/
260theorem updatewindow_live_public {h after : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream}
261    {st state : InflateState} {off : Nat} {source : BRef} {bytes : Array UInt8} {copy : UInt32}
262    (hg : Good h r zs z st) (hza : z.zalloc = .fn "zcalloc")
263    (hsrc : Space.get h source = some bytes) (hfit : off + copy.toNat ≤ bytes.size)
264    (hsep : Separate (.ref source off) copy.toNat st.window (2 ^ st.wbits.toNat))
265    (hr : C.run (updatewindow (some r) (.ref source (off + copy.toNat)) copy) h = .ok (0, after))
266    (hstate : after.istates zs = some state) :
267    LiveChange h after (fun b => InflateOwned zs state b ∧ ¬ h.live b) (fun _ => False) := by
268  change updatewindow (some r) (.ref source (off + copy.toNat)) copy h = .ok (0, after) at hr
269  have hzs : h.live zs := by simp [Heap.live, hg.live.hs]
270  have hsep' : Separate (.ref source ((off + copy.toNat) - copy.toNat)) copy.toNat
271      st.window (2 ^ st.wbits.toNat) := by simpa using hsep
272  rcases hg.inv.win.block with hw | ⟨w, a, hw, ha, hro, hasz⟩
273  · by_cases hok : h.allocOk h.nalloc = true
274    · obtain ⟨result, s', hrun, hgood, hwin, _, hown, _, _⟩ :=
275        uw_null_ok_public (copy := copy) (eo := off + copy.toNat) hg hza hw hok hsrc (by omega) hfit
276      have he : after = result := by rw [hr] at hrun; cases hrun; rfl
277      subst result
278      have hs : state = s' := Option.some.inj (hstate.symm.trans hgood.live.hs)
279      subst state
280      have ho := hown (fun b => h.live b) (fun _ => Iff.rfl)
281      intro b
282      have hl : after.live b ↔ h.live b ∨ b = h.nextBlk := ho b
283      by_cases hb : h.live b
284      · simp [LiveChange, hb, hl.mpr (Or.inl hb)]
285      · have hbi : b ≠ zs := fun he => hb (he ▸ hzs)
286        have hwnd : InflateOwned zs s' b ↔ b = h.nextBlk := by
287          simp [InflateOwned, hwin, hbi, eq_comm]
288        simpa [LiveChange, hb, hwnd] using hl
289    · have hfail := uw_alloc_fail hg.live hza hg.inv.win.wbits hw hok
290        (.ref source (off + copy.toNat)) copy
291      rw [hr] at hfail
292      cases hfail
293  · obtain ⟨result, s', hrun, _, _, hgood, hwin, _, _, _, hlive, _⟩ :=
294      uw_post_public (copy := copy) (eo := off + copy.toNat) hg hw ha hro hasz hsrc (by omega) hfit hsep'
295    have he : after = result := by rw [hr] at hrun; cases hrun; rfl
296    have hgood' : Good after r zs z s' := by rw [he]; exact hgood
297    have hs : state = s' := Option.some.inj (hstate.symm.trans hgood'.live.hs)
298    have hwindow : state.window = .ref (.blk w) 0 := by rw [hs, hwin, hw]
299    have howned : ∀ b, InflateOwned zs state b → h.live b := by
300      intro b ho
301      rcases ho with he | he
302      · subst b; exact hzs
303      · rw [hwindow] at he
304        cases he
305        simp [Heap.live, ha]
306    intro b
307    have hl : after.live b ↔ h.live b := by rw [he]; exact hlive b
308    simp only [LiveChange, not_false_eq_true, and_true]
309    constructor
310    · intro he; exact Or.inl (hl.mp he)
311    · intro he
312      rcases he with he | ⟨ho, hn⟩
313      · exact hl.mpr he
314      · exact (hn (howned b ho)).elim
315
316#print axioms uw_null_frame_public
317#print axioms uw_null_mode_public
318#print axioms updatewindow_mode_public
319#print axioms updatewindow_frame_public
320#print axioms updatewindow_live_public
321end Zlib.Inflate.Proofs