trees.c.heap.gbre.lean

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

1import ZlibF.Proof.«trees.c.heap.gbfix»
2
3/-!
4# trees.c: `gen_bitlen`, reassignment of the lengths
5
6`for (bits = max_length; bits != 0; bits--) { n = bl_count[bits]; while (n != 0) { m = heap[--h]; if (m > max_code)
7continue; if (tree[m].Len != bits) { opt_len += (bits - tree[m].Len) * tree[m].Freq; tree[m].Len = bits; } n--; } }`.
8The counting facts (`scnt`, `stot`, `utot`, `Aab`) and `kraft_of_counts` are copied from the earlier attempt
9(`GenBitlenRe.lean`).
10-/
11
12namespace Zlib.Trees.Proofs
13open C Zlib.Trees Zlib.Trees.Proofs.GB
14
15/-- Scanned leaves (positions `≥ hc`) of length `x`. -/
16def scnt (H : Nat → Nat) (hm maxc J hc : Nat) (len : Nat → Nat) (x : Nat) : Nat :=
17  rs (fun i => if hc ≤ hm + 1 + i ∧ H (hm + 1 + i) ≤ maxc ∧ len (H (hm + 1 + i)) = x then 1 else 0) (2 * J)
18
19/-- Scanned leaves. -/
20def stot (H : Nat → Nat) (hm maxc J hc : Nat) : Nat :=
21  rs (fun i => if hc ≤ hm + 1 + i ∧ H (hm + 1 + i) ≤ maxc then 1 else 0) (2 * J)
22
23/-- Unscanned leaves. -/
24def utot (H : Nat → Nat) (hm maxc J hc : Nat) : Nat :=
25  rs (fun i => if hm + 1 + i < hc ∧ H (hm + 1 + i) ≤ maxc then 1 else 0) (2 * J)
26
27/-- `Σ_{b < x ≤ L} c x`. -/
28def Aab (c : Nat → Nat) (L b : Nat) : Nat := rs (fun x => if b < x then c x else 0) (L + 1)
29
30theorem stot_utot (H : Nat → Nat) (hm maxc J hc : Nat) :
31    stot H hm maxc J hc + utot H hm maxc J hc = nLeaves H hm J maxc := by
32  unfold stot utot nLeaves; rw [← rs_add]; apply rs_congr; intro i _
33  by_cases a : H (hm + 1 + i) ≤ maxc
34  · by_cases b : hc ≤ hm + 1 + i
35    · rw [ite_eq_left ⟨b, a⟩, ite_eq_right (fun h => by omega), ite_eq_left a]
36    · rw [ite_eq_right (fun h => b h.1), ite_eq_left ⟨by omega, a⟩, ite_eq_left a]
37  · rw [ite_eq_right (fun h => a h.2), ite_eq_right (fun h => a h.2), ite_eq_right a]
38
39theorem Aab_pred (c : Nat → Nat) (L b : Nat) (hb : 1 ≤ b) (hbL : b ≤ L) :
40    Aab c L (b - 1) = Aab c L b + c b := by
41  unfold Aab
42  rw [← rs_single' c b (L + 1) (by omega), ← rs_add]
43  apply rs_congr; intro x _
44  by_cases e : b = x
45  · subst e; rw [ite_eq_left (by omega), ite_eq_right (Nat.lt_irrefl _), ite_eq_left rfl]; omega
46  · rw [ite_eq_right e]
47    by_cases f : b < x
48    · rw [ite_eq_left (by omega), ite_eq_left f]; omega
49    · rw [ite_eq_right (by omega), ite_eq_right f]
50
51theorem Aab_zero (c : Nat → Nat) (L : Nat) (h0 : c 0 = 0) : Aab c L 0 = rs c (L + 1) := by
52  unfold Aab; apply rs_congr; intro x _
53  by_cases e : x = 0
54  · subst e; rw [ite_eq_right (Nat.lt_irrefl _), h0]
55  · rw [ite_eq_left (by omega)]
56
57theorem Aab_le (c : Nat → Nat) (L b : Nat) (hb : b ≤ L) : Aab c L b + c b ≤ rs c (L + 1) := by
58  have := rs_le (n := L + 1) (F := fun x => (if b < x then c x else 0) + (if x = b then c x else 0)) (G := c)
59    (fun x _ => by split <;> split <;> omega)
60  rw [rs_add, rs_single, ite_eq_left (by omega)] at this
61  unfold Aab; omega
62
63theorem ite_iff {p q : Prop} [Decidable p] [Decidable q] {α : Type} (a b : α) (h : p ↔ q) :
64    (if p then a else b) = (if q then a else b) := by
65  by_cases hp : p
66  · rw [ite_eq_left hp, ite_eq_left (h.mp hp)]
67  · rw [ite_eq_right hp, ite_eq_right (fun hq => hp (h.mpr hq))]
68
69
70/-- Kraft equality of the reassigned lengths (by position). -/
71theorem kraft_of_counts (H : Nat → Nat) (hm J maxc L : Nat) (len c : Nat → Nat) (hc0 : c 0 = 0)
72    (hkc : kc c L = 2 ^ L)
73    (hle : ∀ i < 2 * J, H (hm + 1 + i) ≤ maxc → len (H (hm + 1 + i)) ≤ L)
74    (hcnt : ∀ x, blP H hm maxc len (2 * J) x = if 0 < x ∧ x ≤ L then c x else 0) :
75    rs (fun i => if H (hm + 1 + i) ≤ maxc then 2 ^ (L - len (H (hm + 1 + i))) else 0) (2 * J) = 2 ^ L := by
76  rw [rs_regroup (fun i => H (hm + 1 + i) ≤ maxc) (fun i => len (H (hm + 1 + i))) (fun b => 2 ^ (L - b))
77    (2 * J) (L + 1) (fun i hi hl => by have := hle i hi hl; omega)]
78  rw [← hkc]; unfold kc; apply rs_congr; intro x hx
79  have := hcnt x; unfold blP at this; rw [this]
80  by_cases e : x = 0
81  · subst e; rw [ite_eq_right (fun h => by omega), hc0]
82  · rw [ite_eq_left ⟨by omega, by omega⟩]
83
84
85
86/-! ### One scan step on the counts -/
87
88theorem scnt_step (H : Nat → Nat) (hm maxc J hc : Nat) (len len' : Nat → Nat) (x : Nat) (hc2 : hm + 2 ≤ hc)
89    (hcJ : hc ≤ hm + 1 + 2 * J)
90    (hsame : ∀ i, i < 2 * J → hc ≤ hm + 1 + i → len' (H (hm + 1 + i)) = len (H (hm + 1 + i))) :
91    scnt H hm maxc J (hc - 1) len' x = scnt H hm maxc J hc len x +
92      (if H (hc - 1) ≤ maxc ∧ len' (H (hc - 1)) = x then 1 else 0) := by
93  unfold scnt
94  have key : ∀ i < 2 * J, (if hc - 1 ≤ hm + 1 + i ∧ H (hm + 1 + i) ≤ maxc ∧ len' (H (hm + 1 + i)) = x then 1 else 0) =
95      (if hc ≤ hm + 1 + i ∧ H (hm + 1 + i) ≤ maxc ∧ len (H (hm + 1 + i)) = x then 1 else 0) +
96      (if i = hc - 2 - hm then (if H (hc - 1) ≤ maxc ∧ len' (H (hc - 1)) = x then 1 else 0) else 0) := by
97    intro i hi
98    by_cases e : i = hc - 2 - hm
99    · have hA : hm + 1 + i = hc - 1 := by omega
100      have hn : ¬ hc ≤ hc - 1 := by omega
101      rw [ite_eq_left e]; simp [hA, hn]
102    · by_cases h1 : hc ≤ hm + 1 + i
103      · have h1' : hc - 1 ≤ hm + 1 + i := by omega
104        simp [e, h1, h1', hsame i hi h1]
105      · have h1' : ¬ hc - 1 ≤ hm + 1 + i := by omega
106        simp [e, h1, h1']
107  rw [rs_congr key, rs_add, rs_single, ite_eq_left (by omega)]
108
109theorem stot_step (H : Nat → Nat) (hm maxc J hc : Nat) (hc2 : hm + 2 ≤ hc) (hcJ : hc ≤ hm + 1 + 2 * J) :
110    stot H hm maxc J (hc - 1) = stot H hm maxc J hc + (if H (hc - 1) ≤ maxc then 1 else 0) := by
111  unfold stot
112  have key : ∀ i < 2 * J, (if hc - 1 ≤ hm + 1 + i ∧ H (hm + 1 + i) ≤ maxc then 1 else 0) =
113      (if hc ≤ hm + 1 + i ∧ H (hm + 1 + i) ≤ maxc then 1 else 0) +
114      (if i = hc - 2 - hm then (if H (hc - 1) ≤ maxc then 1 else 0) else 0) := by
115    intro i hi
116    by_cases e : i = hc - 2 - hm
117    · have hA : hm + 1 + i = hc - 1 := by omega
118      have hn : ¬ hc ≤ hc - 1 := by omega
119      rw [ite_eq_left e]; simp [hA, hn]
120    · by_cases h1 : hc ≤ hm + 1 + i
121      · have h1' : hc - 1 ≤ hm + 1 + i := by omega
122        simp [e, h1, h1']
123      · have h1' : ¬ hc - 1 ≤ hm + 1 + i := by omega
124        simp [e, h1, h1']
125  rw [rs_congr key, rs_add, rs_single, ite_eq_left (by omega)]
126
127theorem costP_set (H : Nat → Nat) (hm maxc J : Nat) (fr len : Nat → Nat) (xb : Nat → Nat) (ip b : Nat)
128    (hip : ip < 2 * J) (hleaf : H (hm + 1 + ip) ≤ maxc)
129    (hinj : ∀ i, i < 2 * J → i ≠ ip → H (hm + 1 + i) ≠ H (hm + 1 + ip)) :
130    costP H hm maxc fr (fun v => if v = H (hm + 1 + ip) then b else len v) xb (2 * J) +
131        fr (H (hm + 1 + ip)) * len (H (hm + 1 + ip)) =
132      costP H hm maxc fr len xb (2 * J) + fr (H (hm + 1 + ip)) * b := by
133  unfold costP
134  have key : ∀ i < 2 * J, (if H (hm + 1 + i) ≤ maxc then fr (H (hm + 1 + i)) *
135        ((fun v => if v = H (hm + 1 + ip) then b else len v) (H (hm + 1 + i)) + xb (H (hm + 1 + i))) else 0) +
136      (if i = ip then fr (H (hm + 1 + ip)) * len (H (hm + 1 + ip)) else 0) =
137      (if H (hm + 1 + i) ≤ maxc then fr (H (hm + 1 + i)) * (len (H (hm + 1 + i)) + xb (H (hm + 1 + i))) else 0) +
138      (if i = ip then fr (H (hm + 1 + ip)) * b else 0) := by
139    intro i hi
140    by_cases e : i = ip
141    · subst e; simp only [ite_true, hleaf]
142      rw [Nat.mul_add, Nat.mul_add]; ac_rfl
143    · simp only [ite_eq_right e, Nat.add_zero, hinj i hi e, ite_false]
144  have := rs_congr key
145  rw [rs_add, rs_add, rs_single, rs_single, ite_eq_left hip, ite_eq_left hip] at this
146  exact this
147
148
149theorem opt_upd (opt0 : UInt64) (cOld cNew fr lm b : Nat) (hN : cNew + fr * lm = cOld + fr * b) :
150    opt0 + UInt64.ofNat cOld + (UInt64.ofNat b - UInt64.ofNat lm) * UInt64.ofNat fr = opt0 + UInt64.ofNat cNew := by
151  have hN' : cNew + lm * fr = cOld + b * fr := by rw [Nat.mul_comm lm, Nat.mul_comm b]; exact hN
152  have h1 : (UInt64.ofNat b - UInt64.ofNat lm) * UInt64.ofNat fr + UInt64.ofNat (lm * fr) = UInt64.ofNat (b * fr) := by
153    rw [UInt64.ofNat_mul, UInt64.ofNat_mul, ← UInt64.add_mul, UInt64.sub_add_cancel]
154  have h2 : UInt64.ofNat cNew + UInt64.ofNat (lm * fr) = UInt64.ofNat cOld + UInt64.ofNat (b * fr) := by
155    rw [← UInt64.ofNat_add, ← UInt64.ofNat_add, hN']
156  rw [UInt64.add_assoc]
157  congr 1
158  have h3 : (UInt64.ofNat cOld + (UInt64.ofNat b - UInt64.ofNat lm) * UInt64.ofNat fr) + UInt64.ofNat (lm * fr)
159      = UInt64.ofNat cNew + UInt64.ofNat (lm * fr) := by
160    rw [UInt64.add_assoc, h1, h2]
161  have h4 := congrArg (fun z => z - UInt64.ofNat (lm * fr)) h3
162  simp only [UInt64.add_sub_cancel] at h4
163  exact h4
164
165/-! ### The state of the reassignment -/
166
167open Zlib.Trees.Proofs.GB
168
169/-- `tree[v].Len`. -/
170def curL (T : Array CtData) (v : Nat) : Nat := (T[v]!).dl.toNat
171
172/-- The record `e0` with the tree array replaced and `opt_len` set. -/
173def mkP2 (tk : TK) (e0 : DeflateState) (Tc : Array CtData) (O : UInt64) : DeflateState :=
174  { tk.setArr e0 Tc with opt_len := O }
175
176@[simp] theorem tk_arr_mkP2 (tk : TK) (e0 Tc O) : tk.arr (mkP2 tk e0 Tc O) = Tc := by cases tk <;> rfl
177@[simp] theorem mkP2_opt_len (tk : TK) (e0 Tc O) : (mkP2 tk e0 Tc O).opt_len = O := by cases tk <;> rfl
178@[simp] theorem mkP2_heap (tk : TK) (e0 Tc O) : (mkP2 tk e0 Tc O).heap = e0.heap := by cases tk <;> rfl
179@[simp] theorem mkP2_bl_count (tk : TK) (e0 Tc O) : (mkP2 tk e0 Tc O).bl_count = e0.bl_count := by cases tk <;> rfl
180theorem setArr_mkP2 (tk : TK) (e0 Tc O A) : tk.setArr (mkP2 tk e0 Tc O) A = mkP2 tk e0 A O := by cases tk <;> rfl
181theorem optlen_mkP2 (tk : TK) (e0 Tc O O') : ({ mkP2 tk e0 Tc O with opt_len := O' } : DeflateState) = mkP2 tk e0 Tc O' := by
182  cases tk <;> rfl
183
184/-- Preconditions of the reassignment. -/
185structure RCtx (tk : TK) (e0 : DeflateState) (hm J elems maxc L : Nat) (c : Nat → Nat) : Prop where
186  hsz : e0.heap.size = 573
187  hnn : ∀ q, hm ≤ q → q < 573 → 0 ≤ (e0.heap[q]!).toInt
188  shape : PShape (Hn e0) hm J elems maxc
189  nc : elems + J ≤ (tk.arr e0).size
190  tsz : (tk.arr e0).size ≤ 600
191  L1 : 1 ≤ L
192  L15 : L ≤ 15
193  c0 : c 0 = 0
194  ctot : rs c (L + 1) = nLeaves (Hn e0) hm J maxc
195
196/-- The state of the scan: positions `≥ hc` scanned, lengths `L .. b + 1` all given out, `c b - n` leaves of length `b`. -/
197def ReSt (tk : TK) (e0 : DeflateState) (hm J maxc L : Nat) (xb : Nat → Nat) (c : Nat → Nat) (opt0 : UInt64)
198    (hc b n : Nat) (e : DeflateState) : Prop :=
199  ∃ (Tc : Array CtData) (O : UInt64), e = mkP2 tk e0 Tc O ∧ Tc.size = (tk.arr e0).size ∧ hm + 1 ≤ hc ∧ hc ≤ 573 ∧
200    n ≤ c b ∧
201    O = opt0 + UInt64.ofNat (costP (Hn e0) hm maxc (frn (tk.arr e0)) (curL Tc) xb (2 * J)) ∧
202    (∀ v : Nat, (Tc[v]!).fc = ((tk.arr e0)[v]!).fc) ∧
203    (∀ v : Nat, (∀ q, hm ≤ q → q < 573 → Hn e0 q ≠ v) → (Tc[v]!).dl = ((tk.arr e0)[v]!).dl) ∧
204    (∀ x, scnt (Hn e0) hm maxc J hc (curL Tc) x = if b < x ∧ x ≤ L then c x else if x = b then c b - n else 0) ∧
205    stot (Hn e0) hm maxc J hc = Aab c L b + (c b - n)
206
207
208theorem i2u_toNat (x : Int32) (h : 0 ≤ x.toInt) (hb : x.toInt < 65536) : (i2u x).toNat = x.toInt.toNat := by
209  unfold i2u
210  rw [UInt32.toNat_ofNat']
211  omega
212
213theorem i2ul_eq (x : Int32) (h : 0 ≤ x.toInt) (hb : x.toInt < 65536) : i2ul x = UInt64.ofNat x.toInt.toNat := by
214  unfold i2ul; congr 1; omega
215
216theorem i2us_eq (x : Int32) (h : 0 ≤ x.toInt) (hb : x.toInt < 65536) : i2us x = UInt16.ofNat x.toInt.toNat := by
217  unfold i2us; congr 1; omega
218
219theorem bne_u32 (lm : UInt16) (x : Int32) (h : 0 ≤ x.toInt) (hb : x.toInt < 65536) :
220    ((lm.toUInt32 != i2u x) = true) ↔ lm.toNat ≠ x.toInt.toNat := by
221  rw [bne_iff_ne, ne_eq, ne_eq, ← UInt32.toNat_inj, UInt16.toNat_toUInt32, i2u_toNat x h hb]
222
223theorem curL_setLen (T : Array CtData) (v c : Nat) (hv : v < T.size) (hc : c < 65536) :
224    curL (setLen T v c) = fun w => if w = v then c else curL T w := by
225  funext w
226  unfold curL setLen
227  rw [getD_set T v w _ hv]
228  by_cases e : w = v
229  · subst e; simp [UInt16.toNat_ofNat']; omega
230  · simp [e]
231
232theorem ws_gbInner {h0 : Heap} {id : Nat} {tk : TK} {e0 : DeflateState} {hm J elems maxc L : Nat}
233    {xb : Nat → Nat} {c : Nat → Nat} {opt0 : UInt64} (ctx : RCtx tk e0 hm J elems maxc L c)
234    (mc bitsv : Int32) (hmc : mc.toInt = maxc) (b : Nat) (hb1 : 1 ≤ b) (hbL : b ≤ L) (hbv : bitsv.toInt = b)
235    (n hc : Nat) (nI hI : Int32) (hnI : nI.toInt = n) (hhI : hI.toInt = hc) (hn : 1 ≤ n) (e : DeflateState)
236    (hR : ReSt tk e0 hm J maxc L xb c opt0 hc b n e) :
237    WS h0 id (gbInner (Sp id) (Ptr.ref (tk.ref id) 0) mc bitsv (nI, hI)) e (fun r e' =>
238      ∃ (hc' n' : Nat), r.1.toInt = (n' : Int) ∧ r.2.toInt = (hc' : Int) ∧ hc' < hc ∧ ReSt tk e0 hm J maxc L xb c opt0 hc' b n' e') := by
239  obtain ⟨Tc, O, rfl, hTs, hc1, hc2, hnc, hO, hfc, hout, hsc, hst⟩ := hR
240  have PS := ctx.shape
241  have hm_eq := PS.hm_eq
242  have hsz := ctx.hsz
243  have hL15 := ctx.L15
244  have hL1 := ctx.L1
245  have hcb : c b ≤ 600 := by
246    have h1 := le_rs (F := c) (n := L + 1) (i := b) (by omega)
247    have h2 := nLeaves_le ctx.shape
248    have h3 := ctx.shape.maxc_lt
249    have h4 := ctx.nc; have h5 := ctx.tsz
250    rw [ctx.ctot] at h1; omega
251  have hut : 1 ≤ utot (Hn e0) hm maxc J hc := by
252    have := stot_utot (Hn e0) hm maxc J hc
253    have := Aab_le c L b hbL
254    have := ctx.ctot
255    omega
256  have hcp : hm + 2 ≤ hc := by
257    by_cases hx : hm + 2 ≤ hc
258    · exact hx
259    · exfalso
260      have : utot (Hn e0) hm maxc J hc = 0 := rs_eq_zero (fun i _ => by rw [ite_eq_right (fun h => by omega)])
261      omega
262  have hp573 : hc - 1 < 573 := by omega
263  have hnn := ctx.hnn (hc - 1) (by omega) hp573
264  have hnode : Hn e0 (hc - 1) < elems + J := by
265    rcases PS.kind (hc - 1) (by omega) hp573 with h1 | h1
266    · have := PS.maxc_lt; omega
267    · omega
268  have hnc' := ctx.nc
269  have h1i : (1 : Int32).toInt = 1 := rfl
270  have hinj : ∀ i, i < 2 * J → hc ≤ hm + 1 + i → Hn e0 (hm + 1 + i) ≠ Hn e0 (hc - 1) := by
271    intro i hi h1 e
272    have := PS.inj (hm + 1 + i) (hc - 1) (by omega) (by omega) (by omega) hp573 e; omega
273  unfold gbInner
274  simp only []
275  refine WS.bind' (ws_isub hI 1 (by omega) (by omega)) fun h' e1 ⟨hh', he1⟩ => ?_
276  subst e1
277  have hh'v : h'.toInt = (hc - 1 : Nat) := by omega
278  refine WS.bind' (ws_heapAt h' (by omega) (by rw [mkP2_heap]; omega)) fun m e1 ⟨hmv, he1⟩ => ?_
279  subst e1
280  have hmI : m.toInt = (Hn e0 (hc - 1) : Int) := by
281    rw [mkP2_heap] at hmv
282    have : h'.toInt.toNat = hc - 1 := by omega
283    rw [this] at hmv; rw [hmv]; unfold Hn; omega
284  have hcJ : hc ≤ hm + 1 + 2 * J := by omega
285  -- the common ending: isub n 1, then the result
286  have fin : ∀ (Tn : Array CtData) (On : UInt64), Tn.size = (tk.arr e0).size →
287      On = opt0 + UInt64.ofNat (costP (Hn e0) hm maxc (frn (tk.arr e0)) (curL Tn) xb (2 * J)) →
288      (curL Tn = fun v => if v = Hn e0 (hc - 1) then b else curL Tc v) →
289      (∀ v : Nat, (Tn[v]!).fc = ((tk.arr e0)[v]!).fc) →
290      (∀ v : Nat, (∀ q, hm ≤ q → q < 573 → Hn e0 q ≠ v) → (Tn[v]!).dl = ((tk.arr e0)[v]!).dl) →
291      Hn e0 (hc - 1) ≤ maxc →
292      WS h0 id (do let r ← isub nI 1; pure (r, h')) (mkP2 tk e0 Tn On) (fun r e' =>
293        ∃ (hc' n' : Nat), r.1.toInt = (n' : Int) ∧ r.2.toInt = (hc' : Int) ∧ hc' < hc ∧ ReSt tk e0 hm J maxc L xb c opt0 hc' b n' e') := by
294    intro Tn On hTn hOn hcur hfcn houtn hleaf
295    refine WS.bind' (ws_isub nI 1 (by omega) (by omega)) fun r e1 ⟨hr, he1⟩ => ?_
296    subst e1
297    refine WS.pure' ⟨hc - 1, n - 1, by simp only; omega, by simp only; omega, by omega, Tn, On, rfl, hTn, by omega,
298      by omega, by omega, hOn, hfcn, houtn, ?_, ?_⟩
299    · intro x
300      have hs := scnt_step (Hn e0) hm maxc J hc (curL Tc) (curL Tn) x hcp hcJ (fun i hi h1 => by
301        rw [hcur]; simp [hinj i hi h1])
302      rw [hs, hsc x, hcur]
303      simp only [ite_true, hleaf]
304      by_cases e1 : b < x ∧ x ≤ L
305      · rw [ite_eq_left e1, ite_eq_left e1]; have : x ≠ b := by omega
306        simp [this, Ne.symm this]
307      · rw [ite_eq_right e1, ite_eq_right e1]
308        by_cases e2 : x = b
309        · subst e2; simp; omega
310        · simp [e2, Ne.symm e2]
311    · rw [stot_step (Hn e0) hm maxc J hc hcp hcJ, hst, ite_eq_left hleaf]; omega
312  have hmt : m.toInt.toNat = Hn e0 (hc - 1) := by omega
313  have hmlt : 0 ≤ m.toInt ∧ m.toInt < ((tk.arr (mkP2 tk e0 Tc O)).size : Int) := by
314    rw [tk_arr_mkP2, hTs]; omega
315  by_cases hleaf : Hn e0 (hc - 1) ≤ maxc
316  · refine WS.ite' (fun hh => absurd hh (by omega)) (fun _ => ?_)
317    refine WS.bind' (ws_getDl tk m.toInt hmlt.1 hmlt.2) fun lm e1 ⟨hlm, he1⟩ => ?_
318    subst e1
319    have hlm' : lm = (Tc[Hn e0 (hc - 1)]!).dl := by rw [hlm, tk_arr_mkP2, hmt]
320    refine WS.ite' (fun hch => ?_) (fun hnch => ?_)
321    · -- the length changes
322      have hne := (bne_u32 lm bitsv (by omega) (by omega)).mp hch
323      refine WS.bind' (ws_getFc tk m.toInt hmlt.1 hmlt.2) fun fm e1 ⟨hfm, he1⟩ => ?_
324      subst e1
325      have hfm' : fm.toNat = frn (tk.arr e0) (Hn e0 (hc - 1)) := by
326        rw [hfm, tk_arr_mkP2, hmt, hfc]; rfl
327      refine WS.bind' (ws_md _) fun _ e1 he1 => ?_
328      subst e1
329      rw [optlen_mkP2]
330      refine WS.bind' (ws_setDl tk m.toInt (i2us bitsv) hmlt.1 (by rw [tk_arr_mkP2, hTs]; omega)) fun _ e1 he1 => ?_
331      subst e1
332      rw [setArr_mkP2, tk_arr_mkP2, hmt, i2us_eq bitsv (by omega) (by omega)]
333      have hbn : bitsv.toInt.toNat = b := by omega
334      rw [hbn]
335      have hvT : Hn e0 (hc - 1) < Tc.size := by omega
336      have hcur := curL_setLen Tc (Hn e0 (hc - 1)) b hvT (by omega)
337      refine fin (setLen Tc (Hn e0 (hc - 1)) b) _ (by unfold setLen; rw [size_set!]; exact hTs) ?_ hcur ?_ ?_ hleaf
338      · simp only [mkP2_opt_len]
339        rw [hcur, i2ul_eq bitsv (by omega) (by omega), hbn, u16_u64 lm, u16_u64 fm, hfm', hlm', hO]
340        have hcs := costP_set (Hn e0) hm maxc J (frn (tk.arr e0)) (curL Tc) xb (hc - 2 - hm) b (by omega)
341          (by have : hm + 1 + (hc - 2 - hm) = hc - 1 := by omega
342              rw [this]; exact hleaf)
343          (fun i hi hne => by
344            have : hm + 1 + (hc - 2 - hm) = hc - 1 := by omega
345            rw [this]
346            intro e; have := PS.inj (hm + 1 + i) (hc - 1) (by omega) (by omega) (by omega) hp573 e; omega)
347        have e5 : hm + 1 + (hc - 2 - hm) = hc - 1 := by omega
348        rw [e5] at hcs
349        have := opt_upd opt0 (costP (Hn e0) hm maxc (frn (tk.arr e0)) (curL Tc) xb (2 * J))
350          (costP (Hn e0) hm maxc (frn (tk.arr e0)) (fun v => if v = Hn e0 (hc - 1) then b else curL Tc v) xb (2 * J))
351          (frn (tk.arr e0) (Hn e0 (hc - 1))) (curL Tc (Hn e0 (hc - 1))) b hcs
352        have e6 : curL Tc (Hn e0 (hc - 1)) = (Tc[Hn e0 (hc - 1)]!).dl.toNat := rfl
353        rw [e6] at this; rw [this]
354      · intro v
355        unfold setLen; rw [getD_set Tc _ v _ hvT]
356        by_cases e : v = Hn e0 (hc - 1)
357        · subst e; simp [hfc]
358        · simp [e, hfc v]
359      · intro v hv
360        unfold setLen; rw [getD_set Tc _ v _ hvT, ite_eq_right]
361        · exact hout v hv
362        · intro e; exact hv (hc - 1) (by omega) hp573 e.symm
363    · have heq : lm.toNat = b := by
364        have hh : lm.toNat = bitsv.toInt.toNat := by
365          by_cases e : lm.toNat = bitsv.toInt.toNat
366          · exact e
367          · exact absurd ((bne_u32 lm bitsv (by omega) (by omega)).mpr e) hnch
368        omega
369      have hcm : curL Tc (Hn e0 (hc - 1)) = b := by unfold curL; rw [← hlm']; exact heq
370      refine fin Tc O hTs hO ?_ hfc hout hleaf
371      funext v
372      by_cases e : v = Hn e0 (hc - 1)
373      · subst e; simp [hcm]
374      · simp [e]
375  · refine WS.ite' (fun _ => ?_) (fun hh => absurd (by omega) hh)
376    refine WS.pure' ⟨hc - 1, n, hnI, hh'v, by omega, Tc, O, rfl, hTs, by omega, by omega, hnc, hO, hfc, hout, ?_, ?_⟩
377    · intro x
378      have hs := scnt_step (Hn e0) hm maxc J hc (curL Tc) (curL Tc) x hcp hcJ (fun i hi h1 => rfl)
379      have hz : ¬ (Hn e0 (hc - 1) ≤ maxc ∧ curL Tc (Hn e0 (hc - 1)) = x) := fun h => hleaf h.1
380      rw [hs, hsc x, ite_eq_right hz, Nat.add_zero]
381    · rw [stot_step (Hn e0) hm maxc J hc hcp hcJ, hst, ite_eq_right hleaf]; rfl
382
383
384theorem bne_zero_iff (n : Int32) : (n != 0) = true ↔ n.toInt ≠ 0 := by
385  rw [bne_iff_ne, ne_eq, ne_eq, ← Int32.toInt_inj]
386  have : (0 : Int32).toInt = 0 := rfl
387  rw [this]
388
389/-- The inner loop: `n` leaves of length `b` are taken from the heap, going down. -/
390theorem ws_gbInnerLoop {h0 : Heap} {id : Nat} {tk : TK} {e0 : DeflateState} {hm J elems maxc L : Nat}
391    {xb : Nat → Nat} {c : Nat → Nat} {opt0 : UInt64} (ctx : RCtx tk e0 hm J elems maxc L c)
392    (mc bitsv : Int32) (hmc : mc.toInt = maxc) (b : Nat) (hb1 : 1 ≤ b) (hbL : b ≤ L) (hbv : bitsv.toInt = b)
393    (n hc : Nat) (nI hI : Int32) (hnI : nI.toInt = n) (hhI : hI.toInt = hc) (e : DeflateState)
394    (hR : ReSt tk e0 hm J maxc L xb c opt0 hc b n e) :
395    WS h0 id (cwhile (σ := Int32 × Int32) (fun (n, h) => pure (n != 0, (n, h)))
396      (gbInner (Sp id) (Ptr.ref (tk.ref id) 0) mc bitsv) (nI, hI)) e (fun r e' =>
397      ∃ hc' : Nat, r.2.toInt = (hc' : Int) ∧ r.1.toInt = 0 ∧ ReSt tk e0 hm J maxc L xb c opt0 hc' b 0 e') := by
398  refine WS.cwhile2 (id := id)
399    (fun (st : Int32 × Int32) e' => ∃ n hc : Nat, st.1.toInt = (n : Int) ∧ st.2.toInt = (hc : Int) ∧ ReSt tk e0 hm J maxc L xb c opt0 hc b n e')
400    (fun (st : Int32 × Int32) _ => st.2.toInt.toNat)
401    (fun (st : Int32 × Int32) e' => ∃ hc' : Nat, st.2.toInt = (hc' : Int) ∧ st.1.toInt = 0 ∧ ReSt tk e0 hm J maxc L xb c opt0 hc' b 0 e')
402    ?_ ⟨n, hc, hnI, hhI, hR⟩ (by
403      have := ctx.hsz; simp only [fuel]
404      have := hI.toInt_le
405      have e : Int32.maxValue.toInt = 2147483647 := by decide
406      omega)
407  rintro ⟨n1, h1⟩ e' ⟨n2, hc2, hn2, hh2, hR2⟩
408  simp only at hn2 hh2
409  refine WS.pure' ?_
410  by_cases hz : n2 = 0
411  · refine Or.inl ⟨?_, hc2, hh2, by show n1.toInt = 0; omega, by subst hz; exact hR2⟩
412    have : ¬ n1.toInt ≠ 0 := by omega
413    have h' := mt (bne_zero_iff n1).mp this
414    simpa using h'
415  · refine Or.inr ⟨?_, ?_⟩
416    · exact (bne_zero_iff n1).mpr (by omega)
417    · refine WS.mono (ws_gbInner ctx mc bitsv hmc b hb1 hbL hbv n2 hc2 n1 h1 hn2 hh2 (by omega) e' hR2) ?_
418      rintro r e'' ⟨hc', n', hr1, hr2, hlt, hR'⟩
419      exact ⟨⟨n', hc', hr1, hr2, hR'⟩, by show r.2.toInt.toNat < h1.toInt.toNat; omega⟩
420
421
422theorem ReSt_down {tk : TK} {e0 : DeflateState} {hm J maxc L : Nat} {xb : Nat → Nat} {c : Nat → Nat} {opt0 : UInt64}
423    {hc b : Nat} {e : DeflateState} (hb1 : 1 ≤ b) (hbL : b ≤ L)
424    (hR : ReSt tk e0 hm J maxc L xb c opt0 hc b 0 e) : ReSt tk e0 hm J maxc L xb c opt0 hc (b - 1) (c (b - 1)) e := by
425  obtain ⟨Tc, O, he, hTs, hc1, hc2, hnc, hO, hfc, hout, hsc, hst⟩ := hR
426  refine ⟨Tc, O, he, hTs, hc1, hc2, Nat.le_refl _, hO, hfc, hout, fun x => ?_, ?_⟩
427  · rw [hsc x]
428    by_cases e1 : b < x ∧ x ≤ L
429    · rw [ite_eq_left e1, ite_eq_left (show b - 1 < x ∧ x ≤ L from ⟨by omega, e1.2⟩)]
430    · by_cases e2 : x = b
431      · rw [ite_eq_right e1, ite_eq_left e2, ite_eq_left (show b - 1 < x ∧ x ≤ L from ⟨by omega, by omega⟩), Nat.sub_zero, e2]
432      · by_cases e3 : x = b - 1
433        · rw [ite_eq_right e1, ite_eq_right e2, ite_eq_right (show ¬ (b - 1 < x ∧ x ≤ L) from fun h => by omega), ite_eq_left e3, Nat.sub_self]
434        · rw [ite_eq_right e1, ite_eq_right e2, ite_eq_right (show ¬ (b - 1 < x ∧ x ≤ L) from fun h => by omega), ite_eq_right e3]
435  · rw [hst, Aab_pred c L b hb1 hbL, Nat.sub_zero, Nat.sub_self]; omega
436
437/-- The reassignment loop. -/
438theorem ws_gbOuter {h0 : Heap} {id : Nat} {tk : TK} {e0 : DeflateState} {hm J elems maxc L : Nat}
439    {xb : Nat → Nat} {c : Nat → Nat} {opt0 : UInt64} (ctx : RCtx tk e0 hm J elems maxc L c) (hB : BcIs e0 c)
440    (mc ml : Int32) (hmc : mc.toInt = maxc) (hml : ml.toInt = L) (hI : Int32) (hhI : hI.toInt = 573) (e : DeflateState)
441    (hR : ReSt tk e0 hm J maxc L xb c opt0 573 L (c L) e) :
442    WS h0 id (cfor (σ := Int32 × Int32) (fun (bits, _) => pure (bits != 0))
443      (fun (bits, h) => do pure (← isub bits 1, h)) (gbOuter (Sp id) (Ptr.ref (tk.ref id) 0) mc) (ml, hI)) e
444      (fun r e' => ∃ hc, ReSt tk e0 hm J maxc L xb c opt0 hc 0 0 e') := by
445  have hL15 := ctx.L15
446  have hL1 := ctx.L1
447  have hcL : ∀ x, x ≤ L → c x ≤ 600 := by
448    intro x hx
449    have h1 := le_rs (F := c) (n := L + 1) (i := x) (by omega)
450    have h2 := nLeaves_le ctx.shape
451    have h3 := ctx.shape.maxc_lt
452    have h4 := ctx.nc; have h5 := ctx.tsz
453    rw [ctx.ctot] at h1; omega
454  have h1i : (1 : Int32).toInt = 1 := rfl
455  have hfuel : ml.toInt.toNat < fuel := by
456    have := ml.toInt_le
457    have e : Int32.maxValue.toInt = 2147483647 := by decide
458    simp only [fuel]; omega
459  refine WS.cfor2 (id := id)
460    (fun (st : Int32 × Int32) e' => ∃ b hc : Nat, st.1.toInt = (b : Int) ∧ st.2.toInt = (hc : Int) ∧ b ≤ L ∧
461      ReSt tk e0 hm J maxc L xb c opt0 hc b (c b) e')
462    (fun (st : Int32 × Int32) _ => st.1.toInt.toNat)
463    (fun (st : Int32 × Int32) e' => ∃ hc, ReSt tk e0 hm J maxc L xb c opt0 hc 0 0 e') ?_
464    ⟨L, 573, hml, hhI, Nat.le_refl _, hR⟩ hfuel
465  rintro ⟨bits, h⟩ e' ⟨b, hc, hb, hh, hbL, hR2⟩
466  simp only at hb hh
467  refine WS.pure' ?_
468  by_cases hz : b = 0
469  · subst hz
470    refine Or.inl ⟨?_, hc, ?_⟩
471    · have : ¬ bits.toInt ≠ 0 := by omega
472      simpa using mt (bne_zero_iff bits).mp this
473    · rw [ctx.c0] at hR2; exact hR2
474  · refine Or.inr ⟨?_, ?_⟩
475    · exact (bne_zero_iff bits).mpr (by omega)
476    · -- the body, then the step
477      have hbody : WS h0 id (gbOuter (Sp id) (Ptr.ref (tk.ref id) 0) mc (bits, h)) e'
478          (fun r e'' => r.1 = bits ∧ ∃ hc' : Nat, r.2.toInt = (hc' : Int) ∧
479            ReSt tk e0 hm J maxc L xb c opt0 hc' b 0 e'') := by
480        unfold gbOuter
481        simp only []
482        refine WS.bind' ws_pBlCount fun bc e1 ⟨hbc, he1⟩ => ?_
483        subst e1; subst hbc
484        obtain ⟨Tc, O, he, hTs, hc1, hc2, hnc, hO, hfc, hout, hsc, hst⟩ := hR2
485        subst he
486        have hcb := hcL b hbL
487        refine WS.bind' (ws_index_blc bits.toInt (by omega) (by rw [mkP2_bl_count, hB.1]; omega)) fun v e1 ⟨hv, he1⟩ => ?_
488        subst e1
489        have hv' : v = UInt16.ofNat (c b) := by
490          rw [hv, mkP2_bl_count, show bits.toInt.toNat = b by omega]; exact hB.2 b (by omega)
491        have hu : (u16i v).toInt = (c b : Int) := by
492          rw [u16i_toInt, hv', UInt16.toNat_ofNat']; omega
493        refine WS.bind' (ws_gbInnerLoop ctx mc bits hmc b (by omega) hbL hb (c b) hc (u16i v) h hu hh _
494          ⟨Tc, O, rfl, hTs, hc1, hc2, hnc, hO, hfc, hout, hsc, hst⟩) fun r e1 ⟨hc', hr2, hr1, hR3⟩ => ?_
495        obtain ⟨n3, h3⟩ := r
496        exact WS.pure' ⟨rfl, hc', hr2, hR3⟩
497      refine WS.bind' hbody fun r e1 ⟨hr1, hc', hr2, hR3⟩ => ?_
498      have hr1' : r.1.toInt = bits.toInt := by rw [hr1]
499      refine WS.bind' (ws_isub r.1 1 (by omega) (by omega)) fun b2 e2 ⟨hb2, he2⟩ => ?_
500      subst e2
501      refine WS.pure' ⟨⟨b - 1, hc', by show b2.toInt = ((b - 1 : Nat) : Int); omega, hr2, by omega, ReSt_down (by omega) hbL hR3⟩, ?_⟩
502      show b2.toInt.toNat < bits.toInt.toNat
503      omega
504
505end Zlib.Trees.Proofs