inftrees.c.content.result.lean

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

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