trees.c.heap.gbtop.lean

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

1import ZlibF.Proof.«trees.c.heap.gbre»
2import ZlibF.Proof.«trees.c.heap.gbsym»
3
4/-!
5# trees.c: `gen_bitlen` (safe and correct)
6
7The proof chains the loops: `bl_count` zeroing, the root `Len := 0`, the first pass (`ws_gbPass1`), and, when the
8clamped depths overflowed, the repair (`ws_gbFixLoop`) and the reassignment (`ws_gbOuter`).
9-/
10
11namespace Zlib.Trees.Proofs
12open C Zlib.Trees Zlib.Trees.Proofs.GB
13
14theorem mk_eq (tk : TK) (d : DeflateState) (B0 : Array UInt16) (A : Array CtData) :
15    tk.setArr { d with bl_count := B0 } A = mkP1 tk d A B0 d.opt_len d.static_len := by cases tk <;> rfl
16
17/-- The state after the zeroing of `bl_count` and the root `Len := 0` is the start of the first pass. -/
18theorem p1_init {h0 : Heap} {id : Nat} {tk : TK} {d : DeflateState} {stree : CtDataPtr} {extra : IPtr}
19    {mc base ml : Int32} {hm J elems maxc L baseN : Nat} {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
20    (ctx : P1Ctx h0 id tk d stree extra mc base ml hm J elems maxc L baseN xb slOpt) (B0 : Array UInt16)
21    (hB0s : B0.size = 16) (hB0z : ∀ i, i < 16 → B0[i]! = 0) :
22    P1State tk d hm J elems maxc L xb slOpt 0
23      (mkP1 tk d (setLen (tk.arr d) (Hn d hm) 0) B0 d.opt_len d.static_len) := by
24  have PS := ctx.shape
25  have hm_eq := PS.hm_eq
26  have hC : Clamped (Hn d) hm J elems L (clK (Hn d) hm elems L (2 * J)) := clK_clamped PS
27  have hnT : Hn d hm < (tk.arr d).size := by
28    rcases PS.kind hm (Nat.le_refl _) (by omega) with h1 | h1
29    · have := PS.maxc_lt; have := ctx.nc; omega
30    · have := ctx.nc; omega
31  have hget : ∀ v, (setLen (tk.arr d) (Hn d hm) 0)[v]! =
32      if v = Hn d hm then { (tk.arr d)[Hn d hm]! with dl := UInt16.ofNat 0 } else (tk.arr d)[v]! := fun v => by
33    unfold setLen; exact getD_set _ _ v _ hnT
34  refine ⟨setLen (tk.arr d) (Hn d hm) 0, B0, d.opt_len, d.static_len, rfl, ?_, ?_, ?_, hB0s, ?_, ?_, ?_, ?_, ?_⟩
35  · show d.opt_len = d.opt_len + UInt64.ofNat 0
36    rw [show UInt64.ofNat 0 = 0 from rfl, UInt64.add_zero]
37  · cases slOpt with
38    | none => rfl
39    | some sl => show d.static_len = d.static_len + UInt64.ofNat 0; rw [show UInt64.ofNat 0 = 0 from rfl, UInt64.add_zero]
40  · unfold setLen; rw [size_set!]
41  · intro q h1 h2
42    have : q = hm := by omega
43    subst this
44    rw [hget, ite_eq_left rfl, hC.root]
45  · intro i _ hi
46    rw [hget, ite_eq_right]
47    · exact ctx.dad i hi
48    · intro e; have := PS.inj (hm + 1 + i) hm (by omega) (by omega) (Nat.le_refl _) (by omega) e; omega
49  · intro v; rw [hget]; split
50    · rename_i e; subst e; rfl
51    · rfl
52  · intro v hv; rw [hget, ite_eq_right]
53    intro e; exact hv hm (Nat.le_refl _) (by omega) e.symm
54  · intro b hb; rw [hB0z b hb]; show (0 : UInt16) = UInt16.ofNat 0; rfl
55
56
57/-- What `gen_bitlen` establishes: the tree array `Tf` holds the lengths, `Bf` the counts. -/
58def GBDone (tk : TK) (d : DeflateState) (hm J maxc L : Nat) (xb : Nat → Nat) (slOpt : Option (Nat → Nat))
59    (e : DeflateState) : Prop :=
60  ∃ (Tf : Array CtData) (Bf : Array UInt16) (O S : UInt64), e = mkP1 tk d Tf Bf O S ∧ Tf.size = (tk.arr d).size ∧
61    Bf.size = 16 ∧ (∀ v : Nat, (Tf[v]!).fc = ((tk.arr d)[v]!).fc) ∧
62    (∀ v : Nat, (∀ q, hm ≤ q → q < 573 → Hn d q ≠ v) → (Tf[v]!).dl = ((tk.arr d)[v]!).dl) ∧
63    (∀ i, i < 2 * J → Hn d (hm + 1 + i) ≤ maxc →
64      1 ≤ curL Tf (Hn d (hm + 1 + i)) ∧ curL Tf (Hn d (hm + 1 + i)) ≤ L) ∧
65    rs (fun i => if Hn d (hm + 1 + i) ≤ maxc then 2 ^ (L - curL Tf (Hn d (hm + 1 + i))) else 0) (2 * J) = 2 ^ L ∧
66    (∀ b, b < 16 → Bf[b]! = UInt16.ofNat (if b = 0 then 0 else blP (Hn d) hm maxc (curL Tf) (2 * J) b)) ∧
67    O = d.opt_len + UInt64.ofNat (costP (Hn d) hm maxc (frn (tk.arr d)) (curL Tf) xb (2 * J)) ∧
68    S = addOpt d.static_len (slOpt.map fun sl => costP (Hn d) hm maxc (frn (tk.arr d)) sl xb (2 * J))
69
70/-- No overflow: the clamped depths are the lengths. -/
71theorem done_noovf {tk : TK} {d : DeflateState} {hm J elems maxc L : Nat} {xb : Nat → Nat}
72    {slOpt : Option (Nat → Nat)} {e : DeflateState} (PS : PShape (Hn d) hm J elems maxc) (hL1 : 1 ≤ L) (hL15 : L ≤ 15)
73    (hov : ovP (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) (2 * J) = 0)
74    (hP : P1State tk d hm J elems maxc L xb slOpt (2 * J) e) : GBDone tk d hm J maxc L xb slOpt e := by
75  have hm_eq := PS.hm_eq
76  have hC : Clamped (Hn d) hm J elems L (clK (Hn d) hm elems L (2 * J)) := clK_clamped PS
77  obtain ⟨Tk, Bk, O, S, he, hO, hS, hTs, hBs, hcl, hdad, hfc, hout, hbl⟩ := hP
78  have hcur : ∀ i, i < 2 * J → curL Tk (Hn d (hm + 1 + i)) = clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + i)) := by
79    intro i hi
80    unfold curL
81    rw [hcl (hm + 1 + i) (by omega) (by omega), UInt16.toNat_ofNat']
82    have := hC.le_all PS (hm + 1 + i) (by omega) (by omega)
83    omega
84  have hcl1 : ∀ i, i < 2 * J → 1 ≤ clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + i)) := by
85    intro i hi
86    rw [hC.step i hi]
87    have := hC.dad_le PS i hi
88    omega
89  have hkr := kraft_clamped PS hC hL1
90  have hovC : ovfC (Hn d) hm J elems L (clK (Hn d) hm elems L (2 * J)) = 0 := hov
91  refine ⟨Tk, Bk, O, S, he, hTs, hBs, hfc, hout, fun i hi _ => ?_, ?_, fun b hb => ?_, ?_, hS⟩
92  · rw [hcur i hi]; exact ⟨hcl1 i hi, (hC.le_all PS (hm + 1 + i) (by omega) (by omega))⟩
93  · unfold kraftC at hkr
94    rw [hovC, Nat.pow_succ] at hkr
95    rw [← show (2 : Nat) ^ L = 2 ^ L from rfl]
96    have : rs (fun i => if Hn d (hm + 1 + i) ≤ maxc then 2 ^ (L - curL Tk (Hn d (hm + 1 + i))) else 0) (2 * J) =
97        rs (fun i => if Hn d (hm + 1 + i) ≤ maxc then 2 ^ (L - clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + i))) else 0) (2 * J) :=
98      rs_congr (fun i hi => by rw [hcur i hi])
99    rw [this]; omega
100  · rw [hbl b hb]
101    by_cases e0 : b = 0
102    · subst e0; rw [ite_eq_left rfl]
103      have := blC_zero PS hC hL1
104      unfold blC at this
105      rw [show blP (Hn d) hm maxc (clK (Hn d) hm elems L (2 * J)) (2 * J) 0 = 0 from this]
106    · rw [ite_eq_right e0]
107      have e1 : blP (Hn d) hm maxc (clK (Hn d) hm elems L (2 * J)) (2 * J) b = blP (Hn d) hm maxc (curL Tk) (2 * J) b := by
108        unfold blP; apply rs_congr; intro i hi; rw [hcur i hi]
109      rw [e1]
110  · rw [hO]
111    have e1 : costP (Hn d) hm maxc (frn (tk.arr d)) (clK (Hn d) hm elems L (2 * J)) xb (2 * J) =
112        costP (Hn d) hm maxc (frn (tk.arr d)) (curL Tk) xb (2 * J) := by
113      unfold costP; apply rs_congr; intro i hi; rw [hcur i hi]
114    rw [e1]
115
116
117theorem mkP2_mkP1 (tk : TK) (d Tk Bk O S Tc O') : mkP2 tk (mkP1 tk d Tk Bk O S) Tc O' = mkP1 tk d Tc Bk O' S := by
118  cases tk <;> rfl
119
120@[simp] theorem Hn_mkP1 (tk : TK) (d Tk Bk O S) : Hn (mkP1 tk d Tk Bk O S) = Hn d := by
121  funext q; unfold Hn; rw [mkP1_heap]
122
123/-- The facts about the state `ef` after the repair that the reassignment needs. -/
124theorem rctx_of {tk : TK} {d e2 ef : DeflateState} {hm J elems maxc L : Nat} {c' : Nat → Nat} {ov : Int32} {Tk Bk O S}
125    (he2 : e2 = mkP1 tk d Tk Bk O S) (hTs : Tk.size = (tk.arr d).size)
126    (PS : PShape (Hn d) hm J elems maxc) (hsz : d.heap.size = 573) (hnn : ∀ q, hm ≤ q → q < 573 → 0 ≤ (d.heap[q]!).toInt)
127    (hnc : elems + J ≤ (tk.arr d).size) (htsz : (tk.arr d).size ≤ 600) (hL1 : 1 ≤ L) (hL15 : L ≤ 15)
128    (hfix : FixInvX L (nLeaves (Hn d) hm J maxc) 0 ov c' e2 ef) :
129    RCtx tk ef hm J elems maxc L c' := by
130  obtain ⟨-, -, hc0, -, -, -, htot, Bc, hef⟩ := hfix
131  have hef' : ef = mkP1 tk d Tk Bc O S := by rw [hef, he2, bl_mkP1]
132  have hh : ef.heap = d.heap := by rw [hef', mkP1_heap]
133  have hHn : Hn ef = Hn d := by rw [hef', Hn_mkP1]
134  refine ⟨by rw [hh]; exact hsz, fun q h1 h2 => by rw [hh]; exact hnn q h1 h2, by rw [hHn]; exact PS, ?_, ?_, hL1, hL15, hc0, by rw [hHn]; exact htot⟩
135  · rw [hef', tk_arr_mkP1, hTs]; exact hnc
136  · rw [hef', tk_arr_mkP1, hTs]; exact htsz
137
138
139theorem curL_clK {tk : TK} {d : DeflateState} {hm J elems maxc L : Nat} (PS : PShape (Hn d) hm J elems maxc)
140    {Tk : Array CtData} (hL15 : L ≤ 15)
141    (hcl : ∀ q, hm ≤ q → q ≤ hm + 2 * J → (Tk[Hn d q]!).dl = UInt16.ofNat (clK (Hn d) hm elems L (2 * J) (Hn d q))) :
142    ∀ i, i < 2 * J → curL Tk (Hn d (hm + 1 + i)) = clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + i)) := by
143  have hm_eq := PS.hm_eq
144  have hC : Clamped (Hn d) hm J elems L (clK (Hn d) hm elems L (2 * J)) := clK_clamped PS
145  intro i hi
146  unfold curL
147  rw [hcl (hm + 1 + i) (by omega) (by omega), UInt16.toNat_ofNat']
148  have := hC.le_all PS (hm + 1 + i) (by omega) (by omega)
149  omega
150
151
152theorem reinit {tk : TK} {d e2 ef : DeflateState} {hm J elems maxc L : Nat} {xb : Nat → Nat}
153    {slOpt : Option (Nat → Nat)} {c' : Nat → Nat} {ov : Int32}
154    (PS : PShape (Hn d) hm J elems maxc) (hL15 : L ≤ 15) (hsz : d.heap.size = 573)
155    (hP : P1State tk d hm J elems maxc L xb slOpt (2 * J) e2)
156    (hfix : FixInvX L (nLeaves (Hn d) hm J maxc) 0 ov c' e2 ef) :
157    ReSt tk ef hm J maxc L xb c' d.opt_len 573 L (c' L) ef := by
158  have hm_eq := PS.hm_eq
159  obtain ⟨Tk, Bk, O, S, he2, hO, hS, hTs, hBs, hcl, hdad, hfc, hout, hbl⟩ := hP
160  obtain ⟨-, -, hc0, -, -, -, htot, Bc, hef⟩ := hfix
161  have hef' : ef = mkP1 tk d Tk Bc O S := by rw [hef, he2, bl_mkP1]
162  have hcur := curL_clK (tk := tk) (elems := elems) (L := L) PS hL15 (fun q h1 h2 => hcl q h1 (by omega))
163  have hfr : frn Tk = frn (tk.arr d) := by funext v; unfold frn; rw [hfc v]
164  refine ⟨tk.arr ef, ef.opt_len, by cases tk <;> rfl, rfl, by omega, Nat.le_refl _, Nat.le_refl _, ?_, fun v => rfl,
165    fun v hv => rfl, fun x => ?_, ?_⟩
166  · rw [hef', tk_arr_mkP1, Hn_mkP1]
167    show O = _
168    rw [hO, hfr]
169    congr 2
170    unfold costP; apply rs_congr; intro i hi; rw [hcur i hi]
171  · have h0 : scnt (Hn ef) hm maxc J 573 (curL (tk.arr ef)) x = 0 := by
172      unfold scnt; exact rs_eq_zero (fun i hi => by rw [ite_eq_right (fun h => by omega)])
173    rw [h0]
174    by_cases e1 : L < x ∧ x ≤ L
175    · omega
176    · rw [ite_eq_right e1]; by_cases e2 : x = L
177      · rw [ite_eq_left e2, Nat.sub_self]
178      · rw [ite_eq_right e2]
179  · have h0 : stot (Hn ef) hm maxc J 573 = 0 := by
180      unfold stot; exact rs_eq_zero (fun i hi => by rw [ite_eq_right (fun h => by omega)])
181    rw [h0, Nat.sub_self]
182    unfold Aab
183    rw [rs_eq_zero (fun x hx => by rw [ite_eq_right (by omega)])]
184
185
186/-- Overflow: the lengths after the reassignment. -/
187theorem done_ovf {tk : TK} {d e2 ef efin : DeflateState} {hm J elems maxc L : Nat} {xb : Nat → Nat}
188    {slOpt : Option (Nat → Nat)} {c' : Nat → Nat} {ov : Int32} {hc : Nat}
189    (PS : PShape (Hn d) hm J elems maxc) (hL1 : 1 ≤ L) (hL15 : L ≤ 15)
190    (hP : P1State tk d hm J elems maxc L xb slOpt (2 * J) e2)
191    (hfix : FixInvX L (nLeaves (Hn d) hm J maxc) 0 ov c' e2 ef)
192    (hre : ReSt tk ef hm J maxc L xb c' d.opt_len hc 0 0 efin) : GBDone tk d hm J maxc L xb slOpt efin := by
193  have hm_eq := PS.hm_eq
194  obtain ⟨Tk, Bk, O, S, he2, hO, hS, hTs, hBs, hcl, hdad, hfc, hout, hbl⟩ := hP
195  obtain ⟨hfv, hBcI, hc0, hchi, hkc, -, htot, Bc, hef⟩ := hfix
196  have hef' : ef = mkP1 tk d Tk Bc O S := by rw [hef, he2, bl_mkP1]
197  obtain ⟨Tc, O2, hefin, hTcs, hc1, hc2, -, hO2, hfcc, houtc, hsc, hst⟩ := hre
198  have hefin' : efin = mkP1 tk d Tc Bc O2 S := by rw [hefin, hef', mkP2_mkP1]
199  have hHn : Hn ef = Hn d := by rw [hef', Hn_mkP1]
200  have hTarr : tk.arr ef = Tk := by rw [hef', tk_arr_mkP1]
201  have hfr : frn Tk = frn (tk.arr d) := by funext v; unfold frn; rw [hfc v]
202  rw [hHn] at hsc hst hO2
203  rw [hTarr, hfr] at hO2
204  rw [hTarr] at hTcs
205  have hmL : ∀ i, i < 2 * J → Hn d (hm + 1 + i) ≤ maxc → hc ≤ hm + 1 + i := by
206    intro i hi hl
207    by_cases h : hc ≤ hm + 1 + i
208    · exact h
209    · exfalso
210      have h1 := stot_utot (Hn d) hm maxc J hc
211      rw [hst] at h1
212      simp only [Nat.sub_zero] at h1
213      have h2 : Aab c' L 0 = rs c' (L + 1) := Aab_zero c' L hc0
214      have h3 : 1 ≤ utot (Hn d) hm maxc J hc := by
215        have := le_rs (F := fun j => if hm + 1 + j < hc ∧ Hn d (hm + 1 + j) ≤ maxc then 1 else 0) (n := 2 * J) (i := i) hi
216        unfold utot
217        rw [ite_eq_left ⟨by omega, hl⟩] at this
218        exact this
219      omega
220  have hcnt : ∀ x, blP (Hn d) hm maxc (curL Tc) (2 * J) x = if 0 < x ∧ x ≤ L then c' x else 0 := by
221    intro x
222    have h := hsc x
223    have e1 : scnt (Hn d) hm maxc J hc (curL Tc) x = blP (Hn d) hm maxc (curL Tc) (2 * J) x := by
224      unfold scnt blP; apply rs_congr; intro i hi
225      by_cases hl : Hn d (hm + 1 + i) ≤ maxc
226      · by_cases hx : curL Tc (Hn d (hm + 1 + i)) = x
227        · simp [hl, hx, hmL i hi hl]
228        · simp [hx]
229      · rw [ite_eq_right (fun h => hl h.2.1), ite_eq_right (fun h => hl h.1)]
230    rw [← e1, h]
231    by_cases e : 0 < x ∧ x ≤ L
232    · simp [e]
233    · by_cases e0 : x = 0
234      · subst e0; simp [hc0]
235      · have e' : ¬ (0 < x ∧ x ≤ L) := e
236        simp [e', e0]
237  have hrange : ∀ i, i < 2 * J → Hn d (hm + 1 + i) ≤ maxc →
238      1 ≤ curL Tc (Hn d (hm + 1 + i)) ∧ curL Tc (Hn d (hm + 1 + i)) ≤ L := by
239    intro i hi hl
240    have h1 := hcnt (curL Tc (Hn d (hm + 1 + i)))
241    have h2 : 1 ≤ blP (Hn d) hm maxc (curL Tc) (2 * J) (curL Tc (Hn d (hm + 1 + i))) := by
242      have := le_rs (F := fun j => if Hn d (hm + 1 + j) ≤ maxc ∧ curL Tc (Hn d (hm + 1 + j)) = curL Tc (Hn d (hm + 1 + i)) then 1 else 0)
243        (n := 2 * J) (i := i) hi
244      unfold blP
245      rw [ite_eq_left ⟨hl, rfl⟩] at this
246      exact this
247    by_cases e : 0 < curL Tc (Hn d (hm + 1 + i)) ∧ curL Tc (Hn d (hm + 1 + i)) ≤ L
248    · exact ⟨e.1, e.2⟩
249    · rw [ite_eq_right e] at h1; omega
250  have hBcs : Bc.size = 16 := by have := hBcI.1; rw [hef', mkP1_bl_count] at this; exact this
251  have hBcv : ∀ b, b < 16 → Bc[b]! = UInt16.ofNat (c' b) := by
252    intro b hb; have := hBcI.2 b hb; rw [hef', mkP1_bl_count] at this; exact this
253  refine ⟨Tc, Bc, O2, S, hefin', by rw [hTcs, hTs], hBcs, ?_, ?_, hrange, ?_, fun b hb => ?_, ?_, hS⟩
254  · intro v; rw [hfcc v, hTarr]; exact hfc v
255  · intro v hv; rw [houtc v (fun q h1 h2 => by rw [hHn]; exact hv q h1 h2), hTarr]; exact hout v hv
256  · exact kraft_of_counts (Hn d) hm J maxc L (curL Tc) c' hc0 (by rw [hkc]; rfl) (fun i hi hl => (hrange i hi hl).2) hcnt
257  · rw [hBcv b hb]
258    by_cases e0 : b = 0
259    · subst e0; rw [ite_eq_left rfl, hc0]
260    · rw [ite_eq_right e0, hcnt b]
261      by_cases e : 0 < b ∧ b ≤ L
262      · rw [ite_eq_left e]
263      · rw [ite_eq_right e, hchi b (by omega)]
264  · rw [hO2]
265
266
267@[simp] theorem mkP1_heap_max (tk : TK) (d Tk Bk O S) : (mkP1 tk d Tk Bk O S).heap_max = d.heap_max := by cases tk <;> rfl
268
269theorem ws_ldTreeDesc {h0 : Heap} {id : Nat} {d : DeflateState} (r : TreeDescRef) (dd : TreeDesc)
270    (h : r.get (setD h0 id d) = some dd) : WS h0 id (ldTreeDesc (some r)) d (fun v d' => v = dd ∧ d' = d) :=
271  WS.of_eq (ldTreeDesc_ok h) ⟨rfl, rfl⟩
272
273theorem ws_ldStaticTreeDesc {h0 : Heap} {id : Nat} {d : DeflateState} (sref : StaticTreeDescRef) (sd : StaticTreeDesc)
274    (h : StaticTreeDescRef.get h0 sref = some sd) :
275    WS h0 id (ldStaticTreeDesc (some sref)) d (fun v d' => v = sd ∧ d' = d) :=
276  WS.of_eq (ldStaticTreeDesc_ok (by cases sref <;> simpa [StaticTreeDescRef.get, setD] using h)) ⟨rfl, rfl⟩
277
278/-- **`gen_bitlen`.** -/
279theorem ws_gen_bitlen {h0 : Heap} {id : Nat} {tk : TK} {d : DeflateState} {r : TreeDescRef} {sref : StaticTreeDescRef}
280    {dd : TreeDesc} {sd : StaticTreeDesc} {hm J elems maxc L baseN : Nat} {xb : Nat → Nat}
281    {slOpt : Option (Nat → Nat)}
282    (hdd : r.get (setD h0 id d) = some dd) (hsd : StaticTreeDescRef.get h0 sref = some sd)
283    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = Ptr.ref (tk.ref id) 0)
284    (ctx : P1Ctx h0 id tk d sd.static_tree sd.extra_bits dd.max_code sd.extra_base sd.max_length hm J elems maxc L baseN
285      xb slOpt)
286    (hHM : d.heap_max.toInt = hm) (hel : elems ≤ 2 ^ L) :
287    WS h0 id (gen_bitlen (Sp id) (some r)) d (fun _ d' => GBDone tk d hm J maxc L xb slOpt d') := by
288  have PS := ctx.shape
289  have hm_eq := PS.hm_eq
290  rw [gen_bitlen_eq]
291  unfold gbTop
292  simp only []
293  refine WS.bind' (ws_ldTreeDesc r dd hdd) fun dd' e1 ⟨hdd', he1⟩ => ?_
294  subst e1; subst dd'
295  rw [hstat]
296  refine WS.bind' (ws_ldStaticTreeDesc sref sd hsd) fun sd' e1 ⟨hsd', he1⟩ => ?_
297  subst e1; subst sd'
298  rw [htree]
299  refine WS.bind' (ws_gbZero d ctx.bsz) fun _ e1 ⟨B0, he1, hB0s, hB0z⟩ => ?_
300  subst e1
301  have hhsz := ctx.hsz
302  have hnn0 := ctx.hnn hm (Nat.le_refl _) (by omega)
303  have hnT : Hn d hm < (tk.arr d).size := by
304    rcases PS.kind hm (Nat.le_refl _) (by omega) with h1 | h1
305    · have := PS.maxc_lt; have := ctx.nc; omega
306    · have := ctx.nc; omega
307  have h1i : (1 : Int32).toInt = 1 := rfl
308  refine WS.bind' ws_rd fun dz e1 ⟨hz, he1⟩ => ?_
309  subst e1; subst hz
310  refine WS.bind' (ws_heapAt d.heap_max (by omega) (by show _ < (d.heap.size : Int); omega)) fun r0 e1 ⟨hr0, he1⟩ => ?_
311  subst e1
312  have hr0n : r0.toInt = (Hn d hm : Int) := by
313    rw [hr0]; show (d.heap[d.heap_max.toInt.toNat]!).toInt = _
314    have : d.heap_max.toInt.toNat = hm := by omega
315    rw [this]; unfold Hn; omega
316  refine WS.bind' (ws_setDl tk r0.toInt 0 (by omega) (by rw [tk_arr_bl_count]; omega)) fun _ e1 he1 => ?_
317  have hr0nat : r0.toInt.toNat = Hn d hm := by omega
318  rw [tk_arr_bl_count, hr0nat] at he1
319  change e1 = tk.setArr { d with bl_count := B0 } (setLen (tk.arr d) (Hn d hm) 0) at he1
320  rw [mk_eq] at he1
321  subst e1
322  refine WS.bind' ws_rd fun dz e1 ⟨hz, he1⟩ => ?_
323  subst e1; subst hz
324  refine WS.bind' (ws_iadd _ 1 (by simp only [mkP1_heap_max]; omega) (by simp only [mkP1_heap_max]; omega))
325    fun h0v e1 ⟨hh0, he1⟩ => ?_
326  subst e1
327  simp only [mkP1_heap_max] at hh0
328  have hp1 := ws_gbPass1 ctx h0v (by omega) _ (p1_init ctx B0 hB0s hB0z)
329  refine WS.bind' hp1 fun x e2 ⟨hx1, hx2, hP⟩ => ?_
330  have hC : Clamped (Hn d) hm J elems L (clK (Hn d) hm elems L (2 * J)) := clK_clamped PS
331  have hL1 := ctx.L1
332  have hL15 := ctx.L15
333  have hmlv := ctx.mlv
334  by_cases hov : ovP (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) (2 * J) = 0
335  · refine WS.ite' (fun _ => ?_) (fun hh => absurd (by
336      have : x.snd.toInt = 0 := by rw [hx2, hov]; rfl
337      have : x.snd = 0 := Int32.toInt_inj.mp (by rw [this]; rfl)
338      simp [this]) hh)
339    exact WS.pure' (done_noovf PS hL1 hL15 hov hP)
340  · refine WS.ite' (fun hh => absurd ?_ hov) (fun _ => ?_)
341    · have : x.snd = 0 := by simpa using hh
342      have h1 : x.snd.toInt = 0 := by rw [this]; rfl
343      rw [hx2] at h1; omega
344    · -- overflow: repair, then reassign
345      have hovpos : 0 < ovP (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) (2 * J) := Nat.pos_of_ne_zero hov
346      have hovE := blC_top PS hC hL1
347      have hkr := kraft_clamped PS hC hL1
348      have hex := exactC_pos PS hC hL1 hovpos
349      obtain ⟨R, hR⟩ : ∃ R, ovfC (Hn d) hm J elems L (clK (Hn d) hm elems L (2 * J)) = 2 * (R + 1) :=
350        ⟨ovfC (Hn d) hm J elems L (clK (Hn d) hm elems L (2 * J)) / 2 - 1, by
351          have := hovE.1; have : 0 < ovfC (Hn d) hm J elems L (clK (Hn d) hm elems L (2 * J)) := hovpos
352          omega⟩
353      have hNL := nLeaves_le PS
354      have hmc := PS.maxc_lt
355      have hnc := ctx.nc
356      have htsz := ctx.tsz
357      obtain ⟨Tk, Bk, O, S, he2, hO, hS, hTs, hBs, hcl, hdad, hfc, hout, hbl⟩ := hP
358      have hP' : P1State tk d hm J elems maxc L xb slOpt (2 * J) e2 :=
359        ⟨Tk, Bk, O, S, he2, hO, hS, hTs, hBs, hcl, hdad, hfc, hout, hbl⟩
360      let c0 : Nat → Nat := fun b => blC (Hn d) hm J maxc (clK (Hn d) hm elems L (2 * J)) b
361      have hI : FixInvX L (nLeaves (Hn d) hm J maxc) (R + 1) x.snd c0 e2 e2 := by
362        refine ⟨by rw [hx2]; show ((ovfC (Hn d) hm J elems L (clK (Hn d) hm elems L (2 * J)) : Nat) : Int) = _; rw [hR]; omega, ?_, blC_zero PS hC hL1, fun b hb => blC_high PS hC b hb, ?_, ?_, blC_total PS hC, e2.bl_count, rfl⟩
363        · rw [he2]; simp only [BcIs, mkP1_bl_count]
364          exact ⟨hBs, fun b hb => (hbl b hb).trans rfl⟩
365        · show kc c0 L = _
366          unfold kc
367          have := kraftC_eq PS hC
368          rw [← this]
369          unfold kraftC at hkr ⊢
370          have hp : ovfC (Hn d) hm J elems L (clK (Hn d) hm elems L (2 * J)) = 2 * (R + 1) := hR
371          rw [Nat.pow_succ] at hkr
372          omega
373        · have := hovE.2
374          show R + 1 + 1 ≤ blC (Hn d) hm J maxc (clK (Hn d) hm elems L (2 * J)) L
375          omega
376      have hNLa : nLeaves (Hn d) hm J maxc ≤ 2 ^ L := by omega
377      have hNLb : nLeaves (Hn d) hm J maxc ≤ 1000 := by omega
378      refine WS.bind' (ws_gbFixLoop (h0 := h0) (id := id) e2 sd.max_length L (nLeaves (Hn d) hm J maxc) R hmlv hL1 hL15
379        hNLa hNLb x.snd c0 e2 hI) fun ov' ef hfix => ?_
380      have rctx := rctx_of he2 hTs PS ctx.hsz ctx.hnn ctx.nc ctx.tsz hL1 hL15 hfix
381      have hR0 := reinit PS hL15 ctx.hsz hP' hfix
382      refine WS.bind' (ws_gbOuter rctx hfix.2.1 dd.max_code sd.max_length ctx.mcv hmlv x.fst hx1 ef hR0)
383        fun r efin ⟨hc, hre⟩ => ?_
384      exact WS.pure' (done_ovf PS hL1 hL15 hP' hfix hre)
385
386
387/-- **`gen_bitlen`: correct.** On the heap `h` with the deflate state `id` (the record `d`), called on the tree
388descriptor `r` (one of `l_desc`, `d_desc`, `bl_desc` of the same state) whose `dyn_tree` is the tree array `tk` of
389that state, `max_code = maxc`, and whose static descriptor `sd` has `elems`, `max_length = L`, `extra_base = baseN`:
390
391* the tree is laid out as `build_tree` leaves it (`P1Ctx.shape`: `J ≥ 1` internal nodes `elems .. elems+J-1`, the root
392  at `heap[heap_max]`, `heap_max = hm`, the node `elems + j` stored below its children at `572 - 2j`, `571 - 2j`, the other
393  entries symbols `≤ maxc < elems`, all distinct) and the `Dad` of each non-root node is `dadP elems position`;
394* `1 ≤ L ≤ 15` (`bl_count` has 16 entries), `elems ≤ 2^L` (so a node can always be found below the limit: F8), the tree
395  array has `elems + J ≤ size ≤ 600` entries, the heap array has 573, `bl_count` 16;
396* the extra bits (`xb`) and the static lengths (`slOpt`, none when `static_tree` is null) are read from static arrays
397  that are large enough for the symbols `≤ maxc`.
398
399The call runs to the end without a fault, only the tree array, `bl_count`, `opt_len` and `static_len` change, and
400(`GBDone`) the leaves get lengths in `[1, L]` forming a complete prefix code (`Σ 2^(L - len) = 2^L`), `bl_count[b]` is the number
401of leaves of length `b` (`bl_count[0] = 0`), and `opt_len`, `static_len` grow by `Σ freq * (len + extra bits)`, resp. the same with
402the static lengths (modulo `2^64`). -/
403theorem gen_bitlen_correct {h : Heap} {id : Nat} {d : DeflateState} (hd : h.dstates id = some d) {tk : TK}
404    {r : TreeDescRef} {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc}
405    {hm J elems maxc L baseN : Nat} {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
406    (hdd : r.get h = some dd) (hsd : StaticTreeDescRef.get h sref = some sd)
407    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = Ptr.ref (tk.ref id) 0)
408    (ctx : P1Ctx h id tk d sd.static_tree sd.extra_bits dd.max_code sd.extra_base sd.max_length hm J elems maxc L baseN
409      xb slOpt)
410    (hHM : d.heap_max.toInt = hm) (hel : elems ≤ 2 ^ L) :
411    ∃ d', gen_bitlen (Sp id) (some r) h = .ok ((), setD h id d') ∧ GBDone tk d hm J maxc L xb slOpt d' := by
412  have hdd' : r.get (setD h id d) = some dd := by rw [setD_self hd]; exact hdd
413  obtain ⟨_, d', e, hq⟩ := ws_gen_bitlen (h0 := h) hdd' hsd hstat htree ctx hHM hel
414  rw [setD_self hd] at e
415  exact ⟨d', e, hq⟩
416
417/-- **`gen_bitlen` does not fault.** Same preconditions as `gen_bitlen_correct` (they are what `build_tree` establishes
418before the call): the call returns normally, every index into `heap`, `bl_count` and the tree is inside its array
419(including the search `while (bl_count[bits] == 0) bits--`, which stays at `bits ≥ 1`, and the scan `heap[--h]`, which
420stays above the root). -/
421theorem gen_bitlen_safe {h : Heap} {id : Nat} {d : DeflateState} (hd : h.dstates id = some d) {tk : TK}
422    {r : TreeDescRef} {sref : StaticTreeDescRef} {dd : TreeDesc} {sd : StaticTreeDesc}
423    {hm J elems maxc L baseN : Nat} {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
424    (hdd : r.get h = some dd) (hsd : StaticTreeDescRef.get h sref = some sd)
425    (hstat : dd.stat_desc = some sref) (htree : dd.dyn_tree = Ptr.ref (tk.ref id) 0)
426    (ctx : P1Ctx h id tk d sd.static_tree sd.extra_bits dd.max_code sd.extra_base sd.max_length hm J elems maxc L baseN
427      xb slOpt)
428    (hHM : d.heap_max.toInt = hm) (hel : elems ≤ 2 ^ L) :
429    ∃ h', gen_bitlen (Sp id) (some r) h = .ok ((), h') := by
430  obtain ⟨d', e, -⟩ := gen_bitlen_correct hd hdd hsd hstat htree ctx hHM hel
431  exact ⟨_, e⟩
432
433end Zlib.Trees.Proofs