inftrees.c.content.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Spec.InflateTableContent
2import ZlibF.Proof.«inftrees.c.content.geometry»
3
4/-!
5# inftrees.c: retain constructed contents through the actual wrappers
6
7Companion proofs strengthen the existing execution interfaces. The translated
8function and original theorem statements remain unchanged. The main loop's
9existing write invariant supplies contents after its geometry is discharged.
10-/
11
12namespace Zlib.Inftrees.Proofs
13open C Zlib.Inftrees Zlib.Inftrees.Spec
14set_option autoImplicit false
15
16private theorem rejected_content_wp
17    {type : UInt32} {f : Nat → Nat} {n oc : Nat} {rc : CodeRef}
18    {value : Int32 × CodePtr × UInt32} {h : Heap}
19    {Q : (Int32 × CodePtr × UInt32) → Heap → Prop}
20    (reject : value.1 ≠ 0) (previous : Wp (pure value) h Q) :
21    Wp (pure value) h (fun r after => Q r after ∧ TableContent type f n rc oc r after) := by
22  obtain ⟨result, after, run, post⟩ := previous
23  change Except.ok (value, h) = Except.ok (result, after) at run
24  obtain ⟨rfl, rfl⟩ := Prod.mk.inj (Except.ok.inj run)
25  exact ⟨value, h, rfl, post, fun success => False.elim (reject success)⟩
26
27theorem itB_content_wp {h : Heap} {type : UInt32} {rl : WRef} {ol : Nat} {codes : UInt32} {rc : CodeRef} {oc : Nat}
28    {bits : UInt32} {rw : WRef} {ow : Nat} (P : CallPre h type rl ol codes rc oc bits rw ow)
29    (count : Array UInt16) (max min root : UInt32)
30    (hcs : count.size = 16) (hcc : ∀ l, 1 ≤ l → l ≤ 15 → (count.getD l 0).toNat = cnt P.f codes.toNat l)
31    (hmax : max.toNat = mxl P.f codes.toNat) (hpos : 0 < Tc P.f codes.toNat 15)
32    (hmin : min.toNat = lenAt P.f codes.toNat 0)
33    (hr1 : 1 ≤ root.toNat) (hr0 : lenAt P.f codes.toNat 0 ≤ root.toNat) (hrm : root.toNat ≤ mxl P.f codes.toNat)
34    (hrC : type = CODES → root.toNat = mxl P.f codes.toNat) :
35    Wp (itB type (Ptr.ref rl ol) codes (Ptr.ref rc oc) bits (Ptr.ref rw ow) count max min root) h
36      (fun r h' => (Result h rw rc ow oc (capOf type) codes.toNat P.wa P.ca (Ptr.ref rc oc) bits r h' ∧
37        RetInfo type P.f codes.toNat r) ∧
38        TableContent type P.f codes.toNat rc oc r h') := by
39  unfold itB
40  apply Wp.bind' (kraft_loop P.f codes.toNat count hcs hcc h)
41  rintro ⟨left, bad, len⟩ h' ⟨rfl, hk⟩
42  dsimp only at hk ⊢
43  by_cases hbad : bad = true
44  · rw [ite_eq_left hbad]
45    have hnf : ¬ Fits P.f codes.toNat := by
46      rcases hk with ⟨_, h2⟩ | ⟨h1, _⟩
47      · exact h2
48      · exact absurd (hbad.symm.trans h1) (by decide)
49    apply rejected_content_wp (by change (-1 : Int32) ≠ 0; decide)
50    exact Wp.pure' ⟨Result.unchanged P.hgw P.hgc ⟨Or.inr rfl, rfl, rfl⟩,
51      fun h => absurd (show (-1 : Int32) = 0 from h) (by decide),
52      fun h => absurd (show (-1 : Int32) = 1 from h) (by decide), fun _ hacc => hnf hacc.1⟩
53  · rw [ite_eq_right hbad]
54    have hbad' : bad = false := by simpa using hbad
55    obtain ⟨hfit, hleft⟩ : Fits P.f codes.toNat ∧ left.toInt = 2 ^ 15 - (Kc P.f codes.toNat 15 : Int) := by
56      rcases hk with ⟨h1, _⟩ | ⟨_, h2, h3⟩
57      · exact absurd h1 hbad
58      · exact ⟨h2, h3⟩
59    have hK15 := hfit 15 (by omega) (by omega)
60    by_cases hg : (decide (left > 0) && (type == CODES || max != 1)) = true
61    · rw [ite_eq_left hg]
62      have hgl' : left > 0 ∧ (type == CODES || max != 1) = true := by
63        simpa [Bool.and_eq_true, decide_eq_true_eq] using hg
64      have hl' : 0 < left.toInt := by
65        have := Int32.lt_iff_toInt_lt.mp hgl'.1; simpa using this
66      have hnacc : ¬ Acc type P.f codes.toNat := by
67        rintro ⟨_, h2 | h2 | ⟨hnc, hm1, _⟩⟩
68        · omega
69        · omega
70        · have hmax1 : max = 1 := UInt32.toNat_inj.mp (by rw [hmax, hm1]; rfl)
71          have := hgl'.2
72          simp [hnc, hmax1] at this
73      apply rejected_content_wp (by change (-1 : Int32) ≠ 0; decide)
74      exact Wp.pure' ⟨Result.unchanged P.hgw P.hgc ⟨Or.inr rfl, rfl, rfl⟩,
75        fun h => absurd (show (-1 : Int32) = 0 from h) (by decide),
76        fun h => absurd (show (-1 : Int32) = 1 from h) (by decide), fun _ => hnacc⟩
77    · rw [ite_eq_right hg]
78      have hend : Kc P.f codes.toNat 15 = 2 ^ 15 ∨ (mxl P.f codes.toNat = 1 ∧ Tc P.f codes.toNat 15 = 1 ∧ type ≠ CODES) := by
79        by_cases hl : left > 0
80        · right
81          have hl' : 0 < left.toInt := by
82            have := Int32.lt_iff_toInt_lt.mp hl; simpa using this
83          have hnc1 : type ≠ CODES := fun ht => hg (by simp [hl, ht])
84          have hnc2 : max = 1 := Classical.byContradiction (fun hne => hg (by simp [hl, hne]))
85          have hm1 : mxl P.f codes.toNat = 1 := by
86            have := congrArg UInt32.toNat hnc2; rw [hmax] at this; simpa using this
87          have hlt : Kc P.f codes.toNat 15 < 2 ^ 15 := by
88            have : (Kc P.f codes.toNat 15 : Int) < 2 ^ 15 := by omega
89            exact_mod_cast this
90          exact ⟨hm1, incomplete_one hpos hfit hlt hm1, hnc1⟩
91        · left
92          have hl' : left.toInt ≤ 0 := by
93            have : ¬ (0 < left.toInt) := fun hh => hl (Int32.lt_iff_toInt_lt.mpr (by simpa using hh))
94            omega
95          have : (2 ^ 15 : Int) ≤ Kc P.f codes.toNat 15 := by omega
96          have : 2 ^ 15 ≤ Kc P.f codes.toNat 15 := by exact_mod_cast this
97          omega
98      have hn288 : codes.toNat ≤ 288 := by
99        rcases P.hty with ht | ht | ht
100        · have := (P.hcodes ht).1; omega
101        · exact P.hlens ht
102        · have := P.hdists ht; omega
103      rw [seta_eq (by simp)]
104      rw [M_pure_bind]
105      apply Wp.bind' (offs_loop P.f codes.toNat hn288 count hcs hcc _)
106      rintro ⟨len2, offs⟩ h' ⟨rfl, hos, hoj⟩
107      dsimp only at hos hoj ⊢
108      apply Wp.bind' (sort_loop P.f codes.toNat hn288 rl rw P.hne ol ow P.la P.wa codes rfl _ P.hgl P.hgw P.hla
109        (fun k => rfl) P.hf15 P.hwa offs hos hoj)
110      rintro ⟨sym, offs'⟩ h2 ⟨hsym, wa1, rfl, hinv⟩
111      dsimp only at hinv ⊢
112      obtain ⟨_, _, hsz1, hfr1, hcont1⟩ := hinv
113      have key : ∀ (base extra : Array UInt16) (match_ : UInt32),
114          (type = CODES → match_ = 20) →
115          (type = LENS → base = lbase ∧ extra = lext ∧ match_ = 257) →
116          (type = DISTS → base = dbase ∧ extra = dext ∧ match_ = 0) →
117          Wp (itTail type (Ptr.ref rl ol) (Ptr.ref rc oc) bits (Ptr.ref rw ow) count max min root left base extra match_)
118            (Space.put h' rw wa1)
119            (fun r h2 => (Result h' rw rc ow oc (capOf type) codes.toNat P.wa P.ca (Ptr.ref rc oc) bits r h2 ∧
120              RetInfo type P.f codes.toNat r) ∧
121        TableContent type P.f codes.toNat rc oc r h2) := by
122        intro base extra match_ hC hL hD
123        let c0 : Ctx := { type, lens := Ptr.ref rl ol, work := Ptr.ref rw ow, table := Ptr.ref rc oc, root, max, base, extra, match_ }
124        let e : Env :=
125          { c := c0,
126            f := P.f, n := codes.toNat, R := root.toNat, cap := capOf type, rc := rc, oc := oc, «rw» := «rw», ow := ow,
127            rl := rl, ol := ol, hb := Space.put h' rw wa1, la := P.la, wa := wa1,
128            h_table := rfl, h_lens := rfl, h_work := rfl, h_ro := P.hro,
129            h_live := ⟨P.ca, by rw [cget_put_word]; exact P.hgc⟩,
130            h_get_la := by rw [wget_put_ne P.hne]; exact P.hgl,
131            h_get_wa := wget_put_self P.hgw wa1, h_f := fun k => rfl, h_la := P.hla, h_f15 := P.hf15,
132            h_wa := by rw [hsz1]; exact P.hwa,
133            h_wcont := fun i hi => by
134              have hb := lenAt_bounds (f := P.f) (n := codes.toNat) hi
135              have blk := (lenAt_eq_iff (f := P.f) (n := codes.toNat) (l := lenAt P.f codes.toNat i) hb.1 hb.2 hi).mp rfl
136              have hlt : i - Tc P.f codes.toNat (lenAt P.f codes.toNat i - 1) < cnt P.f codes.toNat (lenAt P.f codes.toNat i) := by
137                have := Tc_succ' (f := P.f) (n := codes.toNat) hb.1
138                omega
139              have := hcont1 (lenAt P.f codes.toNat i) (i - Tc P.f codes.toNat (lenAt P.f codes.toNat i - 1)) hb.1 hb.2 hlt
140              rw [show ow + Tc P.f codes.toNat (lenAt P.f codes.toNat i - 1) + (i - Tc P.f codes.toNat (lenAt P.f codes.toNat i - 1)) = ow + i by omega] at this
141              rw [this, ws_getD hi],
142            h_n := hn288, h_root := rfl, h_max := hmax, h_R1 := hr1, h_Rmx := hrm, h_R0 := hr0, h_pos := hpos,
143            h_fits := hfit, h_end := hend, h_type := P.hty, h_cap := rfl,
144            h_codes := fun ht => ⟨by
145                have hall := (P.hcodes ht).2.1
146                show lenAt P.f codes.toNat (Tc P.f codes.toNat 15 - 1) ≤ 7
147                unfold lenAt
148                exact hall _ (ws_getD_lt (by omega)), hrC ht, (P.hcodes ht).1, hC ht⟩,
149            h_lens' := fun ht => ⟨hn288, hL ht⟩, h_dists := fun ht => ⟨(P.hdists ht), hD ht⟩ }
150        have hcnt0 : CountOK e count 0 := ⟨hcs, fun l h1 h2 => by
151          rw [hcc l h1 h2]; exact (rem_zero (f := P.f) (n := codes.toNat) h1).symm⟩
152        have hhc : e.hc P.ca = Space.put h' rw wa1 :=
153          cput_self (by rw [cget_put_word]; exact P.hgc)
154        have := itTail_wp e P.ca count bits min left hcnt0 hmin P.hca
155        rw [hhc] at this
156        refine Wp.mono this ?_
157        rintro r h3 ⟨ca', rfl, hf, hr, hrne⟩
158        constructor
159        · have hacc : Acc type P.f codes.toNat := by
160            refine ⟨hfit, ?_⟩
161            rcases hend with h | ⟨a, b, c⟩
162            · exact Or.inl h
163            · exact Or.inr (Or.inr ⟨c, a, b⟩)
164          have hr01 : r.1 = 0 ∨ r.1 = 1 := by
165            rcases hr with ⟨h0, _⟩ | ⟨h1, _⟩
166            · exact Or.inl h0
167            · exact Or.inr h1
168          refine ⟨⟨wa1, ca', rfl, hsz1, hf.1.trans rfl, hfr1, hf.2, ?_⟩,
169            fun _ => hacc, fun h1 => ⟨hacc, hrne.1 h1⟩, fun hm => ?_⟩
170          · rcases hr with ⟨h0, u, hu, hr2, _⟩ | ⟨h1, h2, h3⟩
171            · exact Or.inl ⟨h0, u, hu, hr2⟩
172            · exact Or.inr ⟨Or.inl h1, h2, h3⟩
173          · exfalso
174            rcases hr01 with h0 | h0 <;> rw [h0] at hm <;> exact absurd hm (by decide)
175        · intro success
176          obtain ⟨written, links⟩ := (hrne.2 success).established
177          rcases hr with ⟨_, used, bounded, endPointer, rootBits⟩ | ⟨bad, _, _⟩
178          · right
179            refine ⟨hpos, e, ca', rfl, rfl, ?_, rfl, rfl, rfl, ?_, written, links⟩
180            · exact congrArg UInt32.toNat rootBits.symm
181            · exact cget_put_self (Classical.choose_spec e.h_live) e.h_ro ca'
182          · have : (1 : Int32) = 0 := bad.symm.trans success
183            contradiction
184      rcases P.hty with ht | ht | ht
185      · subst ht
186        rw [ite_eq_left (by decide)]
187        exact key #[] #[] 20 (fun _ => rfl) (fun h => absurd h (by decide)) (fun h => absurd h (by decide))
188      · subst ht
189        rw [ite_eq_right (by decide), ite_eq_left (by decide)]
190        exact key lbase lext 257 (fun h => absurd h (by decide)) (fun _ => ⟨rfl, rfl, rfl⟩) (fun h => absurd h (by decide))
191      · subst ht
192        rw [ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_left (by decide)]
193        exact key dbase dext 0 (fun h => absurd h (by decide)) (fun h => absurd h (by decide)) (fun _ => ⟨rfl, rfl, rfl⟩)
194
195theorem itA_content_wp {h : Heap} {type : UInt32} {rl : WRef} {ol : Nat} {codes : UInt32} {rc : CodeRef} {oc : Nat}
196    {bits : UInt32} {rw : WRef} {ow : Nat} (P : CallPre h type rl ol codes rc oc bits rw ow)
197    (count : Array UInt16) (max root : UInt32)
198    (hcs : count.size = 16) (hcc : ∀ l, 1 ≤ l → l ≤ 15 → (count.getD l 0).toNat = cnt P.f codes.toNat l)
199    (hmaxq : (Tc P.f codes.toNat 15 = 0 ∧ max.toNat = 0) ∨ (0 < Tc P.f codes.toNat 15 ∧ max.toNat = mxl P.f codes.toNat))
200    (hroot : root.toNat ≤ max.toNat) (hrC : type = CODES → root.toNat = max.toNat) :
201    Wp (itA type (Ptr.ref rl ol) codes (Ptr.ref rc oc) bits (Ptr.ref rw ow) count max root) h
202      (fun r h' => (Result h rw rc ow oc (capOf type) codes.toNat P.wa P.ca (Ptr.ref rc oc) bits r h' ∧
203        RetInfo type P.f codes.toNat r) ∧
204        TableContent type P.f codes.toNat rc oc r h') := by
205  unfold itA
206  by_cases hm0 : (max == 0) = true
207  · rw [ite_eq_left hm0]
208    have hcap2 := capOf_ge type
209    have hca := P.hca
210    show Wp (do Ptr.store (Ptr.ref rc oc) (⟨64, 1, 0⟩ : Code)
211                let table ← Ptr.add (Ptr.ref rc oc) 1
212                Ptr.store table (⟨64, 1, 0⟩ : Code)
213                let table ← Ptr.add table 1
214                return ((0 : Int32), table, (1 : UInt32))) _ _
215    apply Wp.bind' (Q := fun _ h2 => h2 = Space.put h rc (P.ca.set! oc ⟨64, 1, 0⟩))
216      (wpC_store h rc P.ca oc _ P.hgc P.hro (by omega))
217    rintro _ h1 rfl
218    have hg1 := cget_put_self P.hgc P.hro (P.ca.set! oc (⟨64, 1, 0⟩ : Code))
219    apply Wp.bind' (Q := fun q h2 => q = Ptr.ref rc (oc + 1) ∧ h2 = Space.put h rc (P.ca.set! oc ⟨64, 1, 0⟩))
220      (wpC_add _ rc _ oc 1 hg1 (by rw [Array.size_set!]; omega))
221    rintro q h2 ⟨rfl, rfl⟩
222    apply Wp.bind' (Q := fun _ h3 => h3 = Space.put h rc ((P.ca.set! oc ⟨64, 1, 0⟩).set! (oc + 1) ⟨64, 1, 0⟩))
223      (by
224        have := wpC_store _ rc _ (oc + 1) (⟨64, 1, 0⟩ : Code) hg1 P.hro (by rw [Array.size_set!]; omega)
225        refine Wp.mono this ?_
226        intro _ h3 hh; rw [hh, cput_put])
227    rintro _ h3 rfl
228    have hg2 := cget_put_self P.hgc P.hro ((P.ca.set! oc (⟨64, 1, 0⟩ : Code)).set! (oc + 1) (⟨64, 1, 0⟩ : Code))
229    apply Wp.bind' (Q := fun q h4 => q = Ptr.ref rc (oc + 1 + 1) ∧ h4 = Space.put h rc ((P.ca.set! oc ⟨64, 1, 0⟩).set! (oc + 1) ⟨64, 1, 0⟩))
230      (wpC_add _ rc _ (oc + 1) 1 hg2 (by rw [Array.size_set!, Array.size_set!]; omega))
231    rintro q h4 ⟨rfl, rfl⟩
232    have hT0 : Tc P.f codes.toNat 15 = 0 := by
233      have hm0' : max.toNat = 0 := by
234        have : max = 0 := by simpa using hm0
235        rw [this]; rfl
236      rcases hmaxq with ⟨a, _⟩ | ⟨a, b⟩
237      · exact a
238      · have := lenAt_bounds (f := P.f) (n := codes.toNat) a
239        have h3 : mxl P.f codes.toNat = lenAt P.f codes.toNat (Tc P.f codes.toNat 15 - 1) := rfl
240        have := lenAt_bounds (f := P.f) (n := codes.toNat) (show Tc P.f codes.toNat 15 - 1 < Tc P.f codes.toNat 15 by omega)
241        omega
242    have hacc : Acc type P.f codes.toNat := ⟨fits_of_zero hT0, Or.inr (Or.inl hT0)⟩
243    apply Wp.pure'
244    constructor
245    · refine ⟨⟨P.wa, (P.ca.set! oc ⟨64, 1, 0⟩).set! (oc + 1) ⟨64, 1, 0⟩, ?_, rfl, ?_, fun _ _ => rfl, ?_, Or.inl ⟨rfl, 2, hcap2, rfl⟩⟩,
246        fun _ => hacc, fun h => absurd (show (0 : Int32) = 1 from h) (by decide),
247        fun h => absurd (show (0 : Int32) = -1 from h) (by decide)⟩
248      · rw [wput_self P.hgw]
249      · simp [Array.size_set!]
250      · intro x hx
251        have h1 : oc + 1 ≠ x := by omega
252        have h2 : oc ≠ x := by omega
253        rw [getElem?_set!_ne h1, getElem?_set!_ne h2]
254    · intro _
255      left
256      refine ⟨hT0, rfl, rfl, _, hg2, ?_, ?_⟩
257      · rw [getElem?_set!_ne (by omega : oc + 1 ≠ oc)]
258        exact getElem?_set!_self (by omega)
259      · exact getElem?_set!_self (by rw [Array.size_set!]; omega)
260  · rw [ite_eq_right hm0]
261    have hm0' : max.toNat ≠ 0 := fun h0 => hm0 (by
262      have : max = 0 := UInt32.toNat_inj.mp (by rw [h0]; rfl)
263      simp [this])
264    obtain ⟨hpos, hmx⟩ : 0 < Tc P.f codes.toNat 15 ∧ max.toNat = mxl P.f codes.toNat := by
265      rcases hmaxq with ⟨_, h2⟩ | h2
266      · exact absurd h2 hm0'
267      · exact h2
268    obtain ⟨hl1, hl2⟩ := lenAt_bounds (f := P.f) (n := codes.toNat) hpos
269    have hl0mx : lenAt P.f codes.toNat 0 ≤ mxl P.f codes.toNat :=
270      lenAt_mono (f := P.f) (n := codes.toNat) (show 0 ≤ Tc P.f codes.toNat 15 - 1 by omega) (by omega)
271    apply Wp.bind' (min_loop P.f codes.toNat count hcs hcc max hmx hpos _)
272    rintro ⟨min, brk⟩ h' ⟨rfl, hmin⟩
273    dsimp only at hmin ⊢
274    by_cases hr : root < min
275    · rw [ite_eq_left hr]
276      have hr' : root.toNat < min.toNat := UInt32.lt_iff_toNat_lt.mp hr
277      exact itB_content_wp P count max min min hcs hcc hmx hpos hmin (by omega) (by omega) (by omega)
278        (fun hC => by have := hrC hC; omega)
279    · rw [ite_eq_right hr]
280      have hr' : min.toNat ≤ root.toNat := by
281        have := (not_congr UInt32.lt_iff_toNat_lt).mp hr; omega
282      exact itB_content_wp P count max min root hcs hcc hmx hpos hmin (by omega) (by omega) (by omega)
283        (fun hC => by have := hrC hC; omega)
284
285theorem itTop_content_wp {h : Heap} {type : UInt32} {rl : WRef} {ol : Nat} {codes : UInt32} {rc : CodeRef} {oc : Nat}
286    {bits : UInt32} {rw : WRef} {ow : Nat} (P : CallPre h type rl ol codes rc oc bits rw ow) :
287    Wp (itTop type (Ptr.ref rl ol) codes (Ptr.ref rc oc) bits (Ptr.ref rw ow)) h
288      (fun r h' => (Result h rw rc ow oc (capOf type) codes.toNat P.wa P.ca (Ptr.ref rc oc) bits r h' ∧
289        RetInfo type P.f codes.toNat r) ∧
290        TableContent type P.f codes.toNat rc oc r h') := by
291  have hn288 : codes.toNat ≤ 288 := by
292    rcases P.hty with ht | ht | ht
293    · have := (P.hcodes ht).1; omega
294    · exact P.hlens ht
295    · have := P.hdists ht; omega
296  unfold itTop
297  apply Wp.bind' (zero_loop h)
298  rintro ⟨len, count⟩ h' ⟨rfl, hs, hz⟩
299  dsimp only at hs hz ⊢
300  apply Wp.bind' (count_loop P.f codes.toNat hn288 rl ol P.la codes rfl _ P.hgl P.hla (fun k => rfl) P.hf15 count hs hz)
301  rintro ⟨sym, count2⟩ h2 ⟨rfl, hsym, hs2, hc2⟩
302  dsimp only at hs2 hc2 ⊢
303  have hcc : ∀ l, 1 ≤ l → l ≤ 15 → (count2.getD l 0).toNat = cnt P.f codes.toNat l := fun l h1 h2 => hc2 l (by omega)
304  apply Wp.bind' (max_loop P.f codes.toNat count2 hs2 hcc _)
305  rintro ⟨max, brk⟩ h3 ⟨rfl, hmaxq⟩
306  dsimp only at hmaxq ⊢
307  by_cases hgt : bits > max
308  · rw [ite_eq_left hgt]
309    exact itA_content_wp P count2 max max hs2 hcc hmaxq (Nat.le_refl _) (fun _ => rfl)
310  · rw [ite_eq_right hgt]
311    have hle : bits.toNat ≤ max.toNat := by
312      have := (not_congr UInt32.lt_iff_toNat_lt).mp hgt; omega
313    exact itA_content_wp P count2 max bits hs2 hcc hmaxq hle
314      (fun hC => by
315        obtain ⟨_, h7, hb7⟩ := P.hcodes hC
316        rcases hmaxq with ⟨a, b⟩ | ⟨a, b⟩
317        · omega
318        · have := mxl_le7 (f := P.f) (n := codes.toNat) a h7
319          omega)
320
321/-- `int inflate_table(codetype type, unsigned short *lens, unsigned codes,
322code **table, unsigned *bits, unsigned short *work)`.
323The actual constructor retains safety, return classification and every
324canonical leaf/link written by the main loop. Geometry is proved from the
325constructor environment; it is not a caller premise. Empty and single-symbol
326codes and all constructor error returns are included. -/
327theorem inflate_table_content : Goal.inflate_table_content := by
328  intro h type rl ol codes rc oc bits rw ow pre
329  obtain ⟨result, after, run, old, content⟩ := itTop_content_wp pre
330  refine ⟨result, after, ?_, old.1, old.2, content⟩
331  rw [C.run, inflate_table_eq]
332  exact run
333
334end Zlib.Inftrees.Proofs