trees.c.heap.gbp1.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.gbdef»
2import ZlibF.Proof.«trees.c.heap.gbclk»
3
4/-!
5# trees.c: `gen_bitlen`, the first pass
6
7The loop `for (h = heap_max + 1; h < HEAP_SIZE; h++)` stores in `tree[n].Len` the depth of each node clamped to
8`max_length`, counts the leaves into `bl_count`, counts the clamped nodes in `overflow`, and adds each leaf's
9cost to `opt_len` and `static_len`. The invariant and the clamped depths `clK` are those of the earlier attempt
10(`GenBitlenPass1.lean`, `GenBitlenBase.lean`).
11-/
12
13namespace Zlib.Trees.Proofs
14open C Zlib.Trees
15
16theorem i2u_u64 (t : Int32) (h : 0 ≤ t.toInt) : (i2u t).toUInt64 = UInt64.ofNat t.toInt.toNat := by
17  have h2 : t.toInt < 2147483648 := by
18    have := t.toInt_le
19    have e : Int32.maxValue.toInt = 2147483647 := by decide
20    omega
21  apply UInt64.toNat_inj.mp
22  unfold i2u
23  rw [UInt32.toNat_toUInt64, UInt32.toNat_ofNat', UInt64.toNat_ofNat']
24  omega
25
26theorem u16_u64 (f : UInt16) : f.toUInt64 = UInt64.ofNat f.toNat := by
27  apply UInt64.toNat_inj.mp
28  rw [UInt16.toNat_toUInt64, UInt64.toNat_ofNat']
29  have := f.toNat_lt
30  omega
31
32theorem u16i_toInt (x : UInt16) : (u16i x).toInt = x.toNat := by
33  unfold u16i
34  have := x.toNat_lt
35  rw [Int32.toInt_ofInt]
36  have : Int32.size = 4294967296 := rfl
37  rw [this, Int.bmod_eq_of_le] <;> omega
38
39/-- `s0` with `c` added, when there is a static tree. -/
40def addOpt (s0 : UInt64) : Option Nat → UInt64
41  | none => s0
42  | some c => s0 + UInt64.ofNat c
43
44/-- The record after the cost of a leaf with `fv` occurrences is added. -/
45def costAdd (e : DeflateState) (fv bits xbv : Nat) (slv : Option Nat) : DeflateState :=
46  { e with opt_len := e.opt_len + UInt64.ofNat (fv * (bits + xbv)),
47           static_len := addOpt e.static_len (slv.map fun l => fv * (l + xbv)) }
48
49
50theorem opt_add (o : UInt64) (f : UInt16) (t : Int32) (ht : 0 ≤ t.toInt) (b x : Nat) (hb : t.toInt.toNat = b + x) :
51    o + f.toUInt64 * (i2u t).toUInt64 = o + UInt64.ofNat (f.toNat * (b + x)) := by
52  rw [u16_u64, i2u_u64 t ht, hb, UInt64.ofNat_mul]
53
54theorem ws_gbTail2_null {h0 : Heap} {id : Nat} (tk : TK) (e : DeflateState) (h n bits ov xbits : Int32)
55    (hn : 0 ≤ n.toInt ∧ n.toInt < (tk.arr e).size) (hb : 0 ≤ bits.toInt ∧ bits.toInt ≤ 15)
56    (hx : 0 ≤ xbits.toInt ∧ xbits.toInt ≤ 1000) :
57    WS h0 id (gbTail2 (Sp id) (Ptr.ref (tk.ref id) 0) Ptr.null h n bits ov xbits) e (fun r e' =>
58      r = (h, ov) ∧ e' = costAdd e ((tk.arr e)[n.toInt.toNat]!).fc.toNat bits.toInt.toNat xbits.toInt.toNat none) := by
59  unfold gbTail2
60  refine WS.bind' (ws_getFc tk n.toInt hn.1 hn.2) fun f e1 ⟨hf, he1⟩ => ?_
61  subst e1; subst hf
62  refine WS.bind' (ws_iadd bits xbits (by omega) (by omega)) fun t e1 ⟨ht, he1⟩ => ?_
63  subst e1
64  refine WS.bind' (ws_md _) fun _ e1 he1 => ?_
65  subst he1
66  simp only [bne_self_eq_false, Bool.false_eq_true, ite_false]
67  refine WS.pure' ⟨rfl, ?_⟩
68  unfold costAdd
69  rw [opt_add _ _ t (by omega) bits.toInt.toNat xbits.toInt.toNat (by omega)]
70  rfl
71
72theorem ws_gbTail2_ref {h0 : Heap} {id : Nat} (tk : TK) (e : DeflateState) (r : CtDataRef) (st : Array CtData)
73    (h n bits ov xbits : Int32)
74    (hn : 0 ≤ n.toInt ∧ n.toInt < (tk.arr e).size) (hb : 0 ≤ bits.toInt ∧ bits.toInt ≤ 15)
75    (hx : 0 ≤ xbits.toInt ∧ xbits.toInt ≤ 1000) (hr : ∀ e', Space.get (setD h0 id e') r = some st)
76    (hs : n.toInt < st.size) (hl : (st[n.toInt.toNat]!).dl.toNat ≤ 15) :
77    WS h0 id (gbTail2 (Sp id) (Ptr.ref (tk.ref id) 0) (Ptr.ref r 0) h n bits ov xbits) e (fun res e' =>
78      res = (h, ov) ∧ e' = costAdd e ((tk.arr e)[n.toInt.toNat]!).fc.toNat bits.toInt.toNat xbits.toInt.toNat
79        (some ((st[n.toInt.toNat]!).dl.toNat))) := by
80  unfold gbTail2
81  refine WS.bind' (ws_getFc tk n.toInt hn.1 hn.2) fun f e1 ⟨hf, he1⟩ => ?_
82  subst e1; subst hf
83  refine WS.bind' (ws_iadd bits xbits (by omega) (by omega)) fun t e1 ⟨ht, he1⟩ => ?_
84  subst e1
85  refine WS.bind' (ws_md _) fun _ e1 he1 => ?_
86  subst he1
87  have hne : (Ptr.ref r 0 != (Ptr.null : CtDataPtr)) = true := by simp
88  simp only [hne, ite_true]
89  have hdl : WS h0 id (getDl (Ptr.ref r 0) n.toInt) { e with opt_len := e.opt_len + ((tk.arr e)[n.toInt.toNat]!).fc.toUInt64 * (i2u t).toUInt64 }
90      (fun v e' => v = (st[n.toInt.toNat]!).dl ∧ e' = { e with opt_len := e.opt_len + ((tk.arr e)[n.toInt.toNat]!).fc.toUInt64 * (i2u t).toUInt64 }) := by
91    unfold getDl
92    have := index0_ok (h := setD h0 id { e with opt_len := e.opt_len + ((tk.arr e)[n.toInt.toNat]!).fc.toUInt64 * (i2u t).toUInt64 })
93      (hr _) (i := n.toInt) hn.1 hs
94    exact WS.of_eq (by simp only [bind_app, this]; rfl) ⟨rfl, rfl⟩
95  refine WS.bind' hdl fun dl e1 ⟨hdl1, he1⟩ => ?_
96  subst e1; subst hdl1
97  refine WS.bind' (ws_iadd (u16i _) xbits (by rw [u16i_toInt]; omega) (by rw [u16i_toInt]; omega)) fun t2 e1 ⟨ht2, he1⟩ => ?_
98  subst e1
99  refine WS.bind' (ws_md _) fun _ e1 he1 => ?_
100  subst he1
101  refine WS.pure' ⟨rfl, ?_⟩
102  unfold costAdd
103  rw [u16i_toInt] at ht2
104  simp only [addOpt, Option.map, opt_add _ _ t (by omega) bits.toInt.toNat xbits.toInt.toNat (by omega),
105    opt_add _ _ t2 (by omega) (st[n.toInt.toNat]!).dl.toNat xbits.toInt.toNat (by omega)]
106
107/-- `Ptr.index` through a static array (found by `setD h0 id e` for every `e`). -/
108theorem ws_index_static {R T : Type} [Space Heap R T] [Inhabited T] {h0 : Heap} {id : Nat} (e : DeflateState)
109    (r : R) (a : Array T) (hr : ∀ e', Space.get (setD h0 id e') r = some a) (i : Int) (h1 : 0 ≤ i)
110    (h2 : i < a.size) :
111    WS h0 id (Ptr.index (Ptr.ref r 0) i) e (fun v e' => v = a[i.toNat]! ∧ e' = e) :=
112  WS.of_eq (index0_ok (hr e) h1 h2) ⟨rfl, rfl⟩
113
114@[simp] theorem tk_arr_bl_count (tk : TK) (d : DeflateState) (a : Array UInt16) :
115    tk.arr { d with bl_count := a } = tk.arr d := by cases tk <;> rfl
116
117/-- The result of the tail of the first-pass body for a leaf. -/
118def leafEff (tk : TK) (e : DeflateState) (n bits : Nat) (xbv : Nat) (slv : Option Nat) : DeflateState :=
119  costAdd { e with bl_count := e.bl_count.set! bits (e.bl_count[bits]! + 1) } ((tk.arr e)[n]!).fc.toNat bits xbv slv
120
121theorem ws_gbTail1 {h0 : Heap} {id : Nat} (tk : TK) (e : DeflateState) (stree : CtDataPtr) (extra : IPtr)
122    (mc base h n bits ov : Int32) (xbv : Nat) (slv : Option Nat) (hbase : 0 ≤ base.toInt)
123    (hn : 0 ≤ n.toInt ∧ n.toInt < (tk.arr e).size) (hb : 0 ≤ bits.toInt ∧ bits.toInt ≤ 15)
124    (hbc : e.bl_count.size = 16)
125    (hxb : (base.toInt ≤ n.toInt → n.toInt ≤ mc.toInt → ∃ (r : IRef) (ex : Array Int32), extra = Ptr.ref r 0 ∧
126        (∀ e', Space.get (setD h0 id e') r = some ex) ∧ 0 ≤ n.toInt - base.toInt ∧ n.toInt - base.toInt < ex.size ∧
127        0 ≤ (ex[(n.toInt - base.toInt).toNat]!).toInt ∧ (ex[(n.toInt - base.toInt).toNat]!).toInt ≤ 1000 ∧
128        xbv = (ex[(n.toInt - base.toInt).toNat]!).toInt.toNat) ∧
129      (n.toInt < base.toInt → xbv = 0))
130    (hst : n.toInt ≤ mc.toInt → (stree = Ptr.null ∧ slv = none) ∨ (∃ (r : CtDataRef) (st : Array CtData),
131      stree = Ptr.ref r 0 ∧
132      (∀ e', Space.get (setD h0 id e') r = some st) ∧ n.toInt < st.size ∧ (st[n.toInt.toNat]!).dl.toNat ≤ 15 ∧
133      slv = some ((st[n.toInt.toNat]!).dl.toNat)))
134    (hxsz : xbv ≤ 1000) :
135    WS h0 id (gbTail1 (Sp id) (Ptr.ref (tk.ref id) 0) stree extra mc base h n bits ov) e (fun r e' =>
136      r = (h, ov) ∧ (n.toInt ≤ mc.toInt → e' = leafEff tk e n.toInt.toNat bits.toInt.toNat xbv slv) ∧
137        (¬ n.toInt ≤ mc.toInt → e' = e)) := by
138  unfold gbTail1
139  have hnb : n.toInt ≤ 2147483647 := by
140    have := n.toInt_le
141    have e : Int32.maxValue.toInt = 2147483647 := by decide
142    omega
143  by_cases hmc : n.toInt > mc.toInt
144  · refine WS.ite' (fun _ => ?_) (fun hh => absurd hmc hh)
145    exact WS.pure' ⟨rfl, fun h' => by omega, fun _ => rfl⟩
146  · refine WS.ite' (fun hh => absurd hh hmc) (fun _ => ?_)
147    refine WS.bind' ws_pBlCount fun bc e1 ⟨hbc1, he1⟩ => ?_
148    subst e1; subst hbc1
149    refine WS.bind' (ws_index_blc bits.toInt hb.1 (by omega)) fun v e1 ⟨hv, he1⟩ => ?_
150    subst e1; subst hv
151    refine WS.bind' (ws_setAt_blc bits.toInt _ hb.1 (by omega)) fun _ e1 he1 => ?_
152    subst he1
153    have hmc' : n.toInt ≤ mc.toInt := by omega
154    have hn' : 0 ≤ n.toInt ∧ n.toInt < (tk.arr { e with bl_count := e.bl_count.set! bits.toInt.toNat (e.bl_count[bits.toInt.toNat]! + 1) }).size := by
155      rw [tk_arr_bl_count]; exact hn
156    -- the tail2 call, for a given extra-bits value
157    have fin : ∀ (x : Int32), 0 ≤ x.toInt → x.toInt ≤ 1000 → x.toInt.toNat = xbv →
158        WS h0 id (gbTail2 (Sp id) (Ptr.ref (tk.ref id) 0) stree h n bits ov x)
159          { e with bl_count := e.bl_count.set! bits.toInt.toNat (e.bl_count[bits.toInt.toNat]! + 1) }
160          (fun r e' => r = (h, ov) ∧ (n.toInt ≤ mc.toInt → e' = leafEff tk e n.toInt.toNat bits.toInt.toNat xbv slv) ∧
161            (¬ n.toInt ≤ mc.toInt → e' = e)) := by
162      intro x hx1 hx2 hx3
163      rcases hst hmc' with ⟨hs, hsl⟩ | ⟨r, st, hs, hrr, hs1, hs2, hsl⟩
164      · subst hs; subst hsl
165        refine WS.mono (ws_gbTail2_null (h0 := h0) (id := id) tk _ h n bits ov x hn' hb ⟨hx1, hx2⟩) ?_
166        intro res e' ⟨h1, h2⟩
167        refine ⟨h1, fun _ => ?_, fun hh => absurd hmc' hh⟩
168        rw [h2, tk_arr_bl_count, hx3]; rfl
169      · subst hs; subst hsl
170        refine WS.mono (ws_gbTail2_ref (h0 := h0) (id := id) tk _ r st h n bits ov x hn' hb ⟨hx1, hx2⟩ hrr hs1 hs2) ?_
171        intro res e' ⟨h1, h2⟩
172        refine ⟨h1, fun _ => ?_, fun hh => absurd hmc' hh⟩
173        rw [h2, tk_arr_bl_count, hx3]; rfl
174    by_cases hge : n.toInt ≥ base.toInt
175    · refine WS.ite' (fun _ => ?_) (fun hh => absurd hge hh)
176      obtain ⟨r, ex, hex, hrr, h0', h1', h2', h3', hxv⟩ := hxb.1 hge hmc'
177      refine WS.bind' (ws_isub n base (by omega) (by omega)) fun d' e1 ⟨hd', he1⟩ => ?_
178      subst e1
179      have hidx : d'.toInt = n.toInt - base.toInt := hd'
180      rw [hex]
181      refine WS.bind' (ws_index_static _ r ex hrr d'.toInt (by omega) (by omega)) fun x e1 ⟨hx, he1⟩ => ?_
182      subst e1; subst hx
183      refine fin _ (by rw [hidx]; exact h2') (by rw [hidx]; exact h3') (by rw [hidx]; exact hxv.symm)
184    · refine WS.ite' (fun hh => absurd hh hge) (fun _ => ?_)
185      have := hxb.2 (by omega)
186      exact fin 0 (by decide) (by decide) (by rw [this]; rfl)
187/-! ### The state of the first pass -/
188
189open Zlib.Trees.Proofs.GB
190
191/-- The record `d` with the tree array replaced and `bl_count`, `opt_len`, `static_len` set. -/
192def mkP1 (tk : TK) (d : DeflateState) (Tk : Array CtData) (Bk : Array UInt16) (O S : UInt64) : DeflateState :=
193  { tk.setArr d Tk with bl_count := Bk, opt_len := O, static_len := S }
194
195@[simp] theorem tk_arr_mkP1 (tk : TK) (d Tk Bk O S) : tk.arr (mkP1 tk d Tk Bk O S) = Tk := by
196  cases tk <;> rfl
197theorem setArr_mkP1 (tk : TK) (d Tk Bk O S A) : tk.setArr (mkP1 tk d Tk Bk O S) A = mkP1 tk d A Bk O S := by
198  cases tk <;> rfl
199theorem costAdd_mkP1 (tk : TK) (d Tk Bk O S fv bits xbv slv) :
200    costAdd (mkP1 tk d Tk Bk O S) fv bits xbv slv = mkP1 tk d Tk Bk (O + UInt64.ofNat (fv * (bits + xbv)))
201      (addOpt S (slv.map fun l => fv * (l + xbv))) := by
202  cases slv <;> rfl
203theorem bl_mkP1 (tk : TK) (d Tk Bk O S B) : ({ mkP1 tk d Tk Bk O S with bl_count := B } : DeflateState) =
204    mkP1 tk d Tk B O S := by
205  cases tk <;> rfl
206
207/-- `Tk` with the `Len` of node `v` set to `c`. -/
208def setLen (Tk : Array CtData) (v c : Nat) : Array CtData := Tk.set! v { Tk[v]! with dl := UInt16.ofNat c }
209
210/-- The nodes of the heap array, as numbers. -/
211def Hn (d : DeflateState) (q : Nat) : Nat := (d.heap[q]!).toInt.toNat
212/-- The frequency of a symbol. -/
213def frn (T : Array CtData) (v : Nat) : Nat := (T[v]!).fc.toNat
214
215/-- The state after `k` non-root positions of the first pass. -/
216def P1State (tk : TK) (d : DeflateState) (hm J elems maxc L : Nat) (xb : Nat → Nat) (slOpt : Option (Nat → Nat))
217    (k : Nat) (e : DeflateState) : Prop :=
218  ∃ (Tk : Array CtData) (Bk : Array UInt16) (O S : UInt64), e = mkP1 tk d Tk Bk O S ∧
219    O = d.opt_len + UInt64.ofNat (costP (Hn d) hm maxc (frn (tk.arr d)) (clK (Hn d) hm elems L (2 * J)) xb k) ∧
220    S = addOpt d.static_len (slOpt.map fun sl => costP (Hn d) hm maxc (frn (tk.arr d)) sl xb k) ∧
221    Tk.size = (tk.arr d).size ∧ Bk.size = 16 ∧
222    (∀ q, hm ≤ q → q ≤ hm + k → (Tk[Hn d q]!).dl = UInt16.ofNat (clK (Hn d) hm elems L (2 * J) (Hn d q))) ∧
223    (∀ i, k ≤ i → i < 2 * J → (Tk[Hn d (hm + 1 + i)]!).dl = UInt16.ofNat (dadP elems (hm + 1 + i))) ∧
224    (∀ v : Nat, (Tk[v]!).fc = ((tk.arr d)[v]!).fc) ∧
225    (∀ v : Nat, (∀ q, hm ≤ q → q < 573 → Hn d q ≠ v) → (Tk[v]!).dl = ((tk.arr d)[v]!).dl) ∧
226    (∀ b, b < 16 → Bk[b]! = UInt16.ofNat (blP (Hn d) hm maxc (clK (Hn d) hm elems L (2 * J)) k b))
227
228@[simp] theorem mkP1_bl_count (tk : TK) (d Tk Bk O S) : (mkP1 tk d Tk Bk O S).bl_count = Bk := by cases tk <;> rfl
229
230theorem mkP1_heap (tk : TK) (d Tk Bk O S) : (mkP1 tk d Tk Bk O S).heap = d.heap := by cases tk <;> rfl
231
232/-- All the preconditions of the first pass. -/
233structure P1Ctx (h0 : Heap) (id : Nat) (tk : TK) (d : DeflateState) (stree : CtDataPtr) (extra : IPtr)
234    (mc base ml : Int32) (hm J elems maxc L baseN : Nat) (xb : Nat → Nat) (slOpt : Option (Nat → Nat)) : Prop where
235  hsz : d.heap.size = 573
236  bsz : d.bl_count.size = 16
237  hnn : ∀ q, hm ≤ q → q < 573 → 0 ≤ (d.heap[q]!).toInt
238  shape : PShape (Hn d) hm J elems maxc
239  nc : elems + J ≤ (tk.arr d).size
240  tsz : (tk.arr d).size ≤ 600
241  mcv : mc.toInt = maxc
242  basev : base.toInt = baseN
243  mlv : ml.toInt = L
244  L1 : 1 ≤ L
245  L15 : L ≤ 15
246  dad : ∀ i, i < 2 * J → ((tk.arr d)[Hn d (hm + 1 + i)]!).dl = UInt16.ofNat (dadP elems (hm + 1 + i))
247  xbOK : ∀ n, n ≤ maxc → (baseN ≤ n → ∃ (r : IRef) (ex : Array Int32), extra = Ptr.ref r 0 ∧
248      (∀ e, Space.get (setD h0 id e) r = some ex) ∧ n - baseN < ex.size ∧ 0 ≤ (ex[n - baseN]!).toInt ∧
249      (ex[n - baseN]!).toInt ≤ 1000 ∧ xb n = (ex[n - baseN]!).toInt.toNat) ∧ (n < baseN → xb n = 0)
250  stOK : (stree = Ptr.null ∧ slOpt = none) ∨ ∃ (r : CtDataRef) (st : Array CtData) (sl : Nat → Nat),
251    stree = Ptr.ref r 0 ∧ slOpt = some sl ∧ (∀ e, Space.get (setD h0 id e) r = some st) ∧
252    ∀ n, n ≤ maxc → n < st.size ∧ (st[n]!).dl.toNat ≤ 15 ∧ sl n = (st[n]!).dl.toNat
253
254theorem ws_gbBody1 {h0 : Heap} {id : Nat} {tk : TK} {d : DeflateState} {stree : CtDataPtr} {extra : IPtr}
255    {mc base ml : Int32} {hm J elems maxc L baseN : Nat} {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
256    (ctx : P1Ctx h0 id tk d stree extra mc base ml hm J elems maxc L baseN xb slOpt) (k : Nat) (hk : k < 2 * J)
257    (h o : Int32) (hh : h.toInt = (hm + 1 + k : Nat)) (ho : o.toInt = ovP (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) k)
258    (e : DeflateState) (hst : P1State tk d hm J elems maxc L xb slOpt k e) :
259    WS h0 id (gbBody1 (Sp id) (Ptr.ref (tk.ref id) 0) stree extra mc base ml (h, o)) e (fun r e' =>
260      r.1.toInt = (hm + 1 + k : Nat) ∧ r.2.toInt = ovP (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) (k + 1) ∧
261      P1State tk d hm J elems maxc L xb slOpt (k + 1) e') := by
262  have PS := ctx.shape
263  have hm_eq := PS.hm_eq
264  have hC : Clamped (Hn d) hm J elems L (clK (Hn d) hm elems L (2 * J)) := clK_clamped PS
265  obtain ⟨Tk, Bk, O, S, rfl, hO, hS, hTs, hBs, hcl, hdad, hfc, hout, hbl⟩ := hst
266  have hq1 : hm + 1 + k < 573 := by omega
267  have hnn := ctx.hnn (hm + 1 + k) (by omega) hq1
268  have hnode : Hn d (hm + 1 + k) < elems + J := by
269    rcases PS.kind (hm + 1 + k) (by omega) hq1 with h1 | h1
270    · have := PS.maxc_lt; omega
271    · omega
272  have hdv : dadP elems (hm + 1 + k) < elems + J := by unfold dadP; omega
273  obtain ⟨q', hq'1, hq'2, hq'e⟩ := dad_pos PS k hk
274  have hCd := hC.dad_le PS k hk
275  have hsz573 := ctx.hsz
276  have hTn := ctx.nc
277  have htsz := ctx.tsz
278  have hL1 := ctx.L1
279  have hL15 := ctx.L15
280  have hmlv := ctx.mlv
281  have hbasev := ctx.basev
282  have hmcv := ctx.mcv
283  have hTk : (tk.arr (mkP1 tk d Tk Bk O S)).size = (tk.arr d).size := by rw [tk_arr_mkP1]; exact hTs
284  unfold gbBody1
285  refine WS.bind' (ws_heapAt h (by omega) (by rw [mkP1_heap]; omega)) fun n e1 ⟨hn, he1⟩ => ?_
286  subst e1
287  have hnv : n.toInt = (Hn d (hm + 1 + k) : Int) := by
288    rw [mkP1_heap] at hn
289    have : h.toInt.toNat = hm + 1 + k := by omega
290    rw [this] at hn
291    rw [hn]; unfold Hn; omega
292  have hdn := hdad k (Nat.le_refl _) hk
293  refine WS.bind' (ws_getDl tk n.toInt (by omega) (by rw [hTk]; omega)) fun a1 e1 ⟨ha1, he1⟩ => ?_
294  subst e1
295  have ha1' : a1 = UInt16.ofNat (dadP elems (hm + 1 + k)) := by
296    rw [ha1, tk_arr_mkP1]
297    have : n.toInt.toNat = Hn d (hm + 1 + k) := by omega
298    rw [this]; exact hdn
299  have hdvlt : dadP elems (hm + 1 + k) < 65536 := by omega
300  have hu1 : (u16i a1).toInt = (dadP elems (hm + 1 + k) : Int) := by
301    rw [u16i_toInt, ha1', UInt16.toNat_ofNat']; omega
302  refine WS.bind' (ws_getDl tk (u16i a1).toInt (by omega) (by rw [hTk]; omega)) fun a2 e1 ⟨ha2, he1⟩ => ?_
303  subst e1
304  have ha2' : a2 = UInt16.ofNat (clK (Hn d) hm elems L (2 * J) (dadP elems (hm + 1 + k))) := by
305    rw [ha2, tk_arr_mkP1]
306    have : (u16i a1).toInt.toNat = Hn d q' := by omega
307    rw [this]
308    have := hcl q' hq'1 (by omega)
309    rw [this, hq'e]
310  have hCdv : (u16i a2).toInt = (clK (Hn d) hm elems L (2 * J) (dadP elems (hm + 1 + k)) : Int) := by
311    rw [u16i_toInt, ha2', UInt16.toNat_ofNat']; omega
312  refine WS.bind' (ws_iadd (u16i a2) 1 (by have : (1 : Int32).toInt = 1 := rfl; omega)
313    (by have : (1 : Int32).toInt = 1 := rfl; omega)) fun bits e1 ⟨hbits, he1⟩ => ?_
314  subst e1
315  have h1i : (1 : Int32).toInt = 1 := rfl
316  have hCn : clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k)) =
317      min (clK (Hn d) hm elems L (2 * J) (dadP elems (hm + 1 + k)) + 1) L := hC.step k hk
318  have hCnL : 1 ≤ clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k)) ∧
319      clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k)) ≤ L := by omega
320  have hnT : Hn d (hm + 1 + k) < (tk.arr d).size := by omega
321  have hnvn : n.toInt.toNat = Hn d (hm + 1 + k) := by omega
322  have hleaf : n.toInt ≤ mc.toInt ↔ Hn d (hm + 1 + k) ≤ maxc := by rw [hnv, ctx.mcv]; omega
323  -- everything after `Len` is stored
324  have fin : ∀ (bitsv ov' : Int32), bitsv.toInt = (clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k)) : Int) →
325      ov'.toInt = (ovP (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) (k + 1) : Int) →
326      WS h0 id (do setDl (Ptr.ref (tk.ref id) 0) n.toInt (i2us bitsv)
327                   gbTail1 (Sp id) (Ptr.ref (tk.ref id) 0) stree extra mc base h n bitsv ov')
328        (mkP1 tk d Tk Bk O S) (fun r e' => r.1.toInt = (hm + 1 + k : Nat) ∧
329          r.2.toInt = (ovP (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) (k + 1) : Int) ∧
330          P1State tk d hm J elems maxc L xb slOpt (k + 1) e') := by
331    intro bitsv ov' hbv hov
332    have hbvn : 0 ≤ bitsv.toInt ∧ bitsv.toInt ≤ 15 := by omega
333    have hi2us : i2us bitsv = UInt16.ofNat (clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k))) := by
334      unfold i2us; rw [hbv]; congr 1; omega
335    refine WS.bind' (ws_setDl tk n.toInt (i2us bitsv) (by omega) (by rw [hTk]; omega)) fun _ e2 he2 => ?_
336    rw [setArr_mkP1, tk_arr_mkP1, hnvn, hi2us] at he2
337    change e2 = mkP1 tk d (setLen Tk (Hn d (hm + 1 + k)) (clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k)))) Bk O S at he2
338    subst he2
339    have hTk's : (setLen Tk (Hn d (hm + 1 + k)) (clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k)))).size = Tk.size :=
340      size_set! _ _ _
341    have hnTk : Hn d (hm + 1 + k) < Tk.size := by omega
342    obtain ⟨xbv, hxbv⟩ : ∃ x : Nat, x = (if Hn d (hm + 1 + k) ≤ maxc then xb (Hn d (hm + 1 + k)) else 0) := ⟨_, rfl⟩
343    obtain ⟨slv, hslv⟩ : ∃ x : Option Nat, x = slOpt.map (fun sl => if Hn d (hm + 1 + k) ≤ maxc then sl (Hn d (hm + 1 + k)) else 0) := ⟨_, rfl⟩
344    obtain ⟨Tn, hTn'⟩ : ∃ T2, T2 = setLen Tk (Hn d (hm + 1 + k)) (clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k))) := ⟨_, rfl⟩
345    rw [← hTn'] at hTk's ⊢
346    have hTns : Tn.size = (tk.arr d).size := by rw [hTk's]; exact hTs
347    -- facts about the new tree array
348    have getTn : ∀ v, Tn[v]! = if v = Hn d (hm + 1 + k) then
349        { Tk[Hn d (hm + 1 + k)]! with dl := UInt16.ofNat (clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k))) } else Tk[v]! := by
350      intro v; rw [hTn']; exact getD_set Tk _ v _ hnTk
351    have hinj : ∀ q2, hm ≤ q2 → q2 < 573 → Hn d q2 = Hn d (hm + 1 + k) → q2 = hm + 1 + k :=
352      fun q2 h1 h2 h3 => PS.inj q2 (hm + 1 + k) h1 h2 (by omega) hq1 h3
353    have Tn_cl : ∀ q2, hm ≤ q2 → q2 ≤ hm + (k + 1) → (Tn[Hn d q2]!).dl =
354        UInt16.ofNat (clK (Hn d) hm elems L (2 * J) (Hn d q2)) := by
355      intro q2 h1 h2
356      rw [getTn]
357      by_cases e : Hn d q2 = Hn d (hm + 1 + k)
358      · rw [ite_eq_left e, e]
359      · rw [ite_eq_right e]
360        have hne : q2 ≠ hm + 1 + k := fun h' => e (by rw [h'])
361        exact hcl q2 h1 (by omega)
362    have Tn_dad : ∀ i, k + 1 ≤ i → i < 2 * J → (Tn[Hn d (hm + 1 + i)]!).dl = UInt16.ofNat (dadP elems (hm + 1 + i)) := by
363      intro i h1 h2
364      rw [getTn, ite_eq_right]
365      · exact hdad i (by omega) h2
366      · intro e; have := hinj (hm + 1 + i) (by omega) (by omega) e; omega
367    have Tn_fc : ∀ v : Nat, (Tn[v]!).fc = ((tk.arr d)[v]!).fc := by
368      intro v; rw [getTn]; split
369      · rename_i e; subst e; exact hfc _
370      · exact hfc v
371    have Tn_out : ∀ v : Nat, (∀ q, hm ≤ q → q < 573 → Hn d q ≠ v) → (Tn[v]!).dl = ((tk.arr d)[v]!).dl := by
372      intro v hv; rw [getTn, ite_eq_right]
373      · exact hout v hv
374      · intro e; exact hv (hm + 1 + k) (by omega) hq1 e.symm
375    have hCn' : clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k)) ≤ 15 := by omega
376    have hnTn : 0 ≤ n.toInt ∧ n.toInt < (tk.arr (mkP1 tk d Tn Bk O S)).size := by
377      rw [tk_arr_mkP1, hTns]; omega
378    have hxb1000 : xbv ≤ 1000 := by
379      rw [hxbv]; split
380      · rename_i hl
381        by_cases hb : baseN ≤ Hn d (hm + 1 + k)
382        · obtain ⟨r, ex, -, -, -, -, h1, h2⟩ := (ctx.xbOK _ hl).1 hb
383          omega
384        · rw [(ctx.xbOK _ hl).2 (by omega)]; omega
385      · omega
386    have hbase0 : 0 ≤ base.toInt := by have := ctx.basev; omega
387    have tail := ws_gbTail1 (h0 := h0) (id := id) tk (mkP1 tk d Tn Bk O S) stree extra mc base h n bitsv ov' xbv slv
388      hbase0 hnTn hbvn (by rw [mkP1_bl_count]; exact hBs)
389      (by
390        constructor
391        · intro hb hl
392          have hl' : Hn d (hm + 1 + k) ≤ maxc := hleaf.mp hl
393          obtain ⟨r, ex, h1, h2, h3, h4, h5, h7⟩ := (ctx.xbOK _ hl').1 (by omega)
394          refine ⟨r, ex, h1, h2, by omega, ?_, ?_, ?_, ?_⟩
395          · have : n.toInt - base.toInt = ((Hn d (hm + 1 + k) - baseN : Nat) : Int) := by omega
396            rw [this]; omega
397          · have : (n.toInt - base.toInt).toNat = Hn d (hm + 1 + k) - baseN := by omega
398            rw [this]; exact h4
399          · have : (n.toInt - base.toInt).toNat = Hn d (hm + 1 + k) - baseN := by omega
400            rw [this]; exact h5
401          · have : (n.toInt - base.toInt).toNat = Hn d (hm + 1 + k) - baseN := by omega
402            rw [this, hxbv, ite_eq_left hl']; exact h7
403        · intro hb
404          rw [hxbv]; split
405          · rename_i hl'; exact (ctx.xbOK _ hl').2 (by omega)
406          · rfl)
407      (by
408        intro hl
409        have hl' : Hn d (hm + 1 + k) ≤ maxc := hleaf.mp hl
410        rcases ctx.stOK with ⟨h1, h2⟩ | ⟨r, st, sl, h1, h2, h3, h4⟩
411        · left; refine ⟨h1, ?_⟩; rw [hslv, h2]; rfl
412        · right
413          obtain ⟨g1, g2, g3⟩ := h4 _ hl'
414          refine ⟨r, st, h1, h3, by omega, by rw [hnvn]; exact g2, ?_⟩
415          rw [hslv, h2, hnvn]; simp [hl', g3])
416      hxb1000
417    refine WS.mono tail ?_
418    rintro r e' ⟨hr, hl1, hl2⟩
419    subst hr
420    refine ⟨by omega, hov, ?_⟩
421    have hbn : bitsv.toInt.toNat = clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k)) := by omega
422    have hcs := costP_succ (Hn d) hm maxc (frn (tk.arr d)) (clK (Hn d) hm elems L (2 * J)) xb k
423    have hcs2 : ∀ sl, costP (Hn d) hm maxc (frn (tk.arr d)) sl xb (k + 1) = costP (Hn d) hm maxc (frn (tk.arr d)) sl xb k +
424        (if Hn d (hm + 1 + k) ≤ maxc then frn (tk.arr d) (Hn d (hm + 1 + k)) * (sl (Hn d (hm + 1 + k)) + xb (Hn d (hm + 1 + k))) else 0) :=
425      fun sl => costP_succ (Hn d) hm maxc (frn (tk.arr d)) sl xb k
426    have hfv : ((tk.arr (mkP1 tk d Tn Bk O S))[n.toInt.toNat]!).fc.toNat = frn (tk.arr d) (Hn d (hm + 1 + k)) := by
427      rw [tk_arr_mkP1, hnvn]; unfold frn; rw [Tn_fc]
428    by_cases hl : Hn d (hm + 1 + k) ≤ maxc
429    · have he' := hl1 (hleaf.mpr hl)
430      unfold leafEff at he'
431      rw [bl_mkP1, costAdd_mkP1, hfv, hbn] at he'
432      simp only [mkP1_bl_count] at he'
433      refine ⟨Tn, Bk.set! (clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k))) (Bk[clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k))]! + 1),
434        O + UInt64.ofNat (frn (tk.arr d) (Hn d (hm + 1 + k)) * (clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k)) + xbv)),
435        (addOpt S (slv.map fun l => frn (tk.arr d) (Hn d (hm + 1 + k)) * (l + xbv))),
436        he', ?_, ?_, hTns, ?_, Tn_cl, Tn_dad, Tn_fc, Tn_out, ?_⟩
437      · rw [hO, hcs, ite_eq_left hl, hxbv, ite_eq_left hl, UInt64.ofNat_add]; ac_rfl
438      · rw [hS, hslv]
439        cases slOpt with
440        | none => rfl
441        | some sl =>
442          simp only [Option.map, addOpt, hcs2, ite_eq_left hl, hxbv, UInt64.ofNat_add, UInt64.add_assoc]
443      · rw [size_set!]; exact hBs
444      · intro b hb
445        rw [getD_set Bk _ b _ (by omega), blP_succ]
446        by_cases e : b = clK (Hn d) hm elems L (2 * J) (Hn d (hm + 1 + k))
447        · subst e; rw [ite_eq_left rfl, hbl _ hb, ite_eq_left ⟨hl, rfl⟩, UInt16.ofNat_add]; rfl
448        · rw [ite_eq_right e, hbl b hb, ite_eq_right (fun hh => e hh.2.symm)]; simp
449    · have he' := hl2 (fun hh => hl (hleaf.mp hh))
450      refine ⟨Tn, Bk, O, S, he', ?_, ?_, hTns, hBs, Tn_cl, Tn_dad, Tn_fc, Tn_out, ?_⟩
451      · rw [hO, hcs, ite_eq_right hl]; simp
452      · rw [hS]; cases slOpt with
453        | none => rfl
454        | some sl => simp only [Option.map, addOpt, hcs2, ite_eq_right hl, Nat.add_zero]
455      · intro b hb
456        rw [hbl b hb, blP_succ, ite_eq_right (fun hh => hl hh.1)]; simp
457  have hovs : ovP (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) (k + 1) =
458      ovP (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) k +
459        (if clK (Hn d) hm elems L (2 * J) (dadP elems (hm + 1 + k)) = L then 1 else 0) := rfl
460  have hovle := ovP_le (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) k
461  refine WS.ite' (fun hgt => ?_) (fun hle => ?_)
462  · refine WS.bind' (ws_iadd o 1 (by omega) (by omega)) fun ov e1 ⟨hov, he1⟩ => ?_
463    subst e1
464    have hcd : clK (Hn d) hm elems L (2 * J) (dadP elems (hm + 1 + k)) = L := by omega
465    refine fin ml ov (by omega) (by rw [hovs, ite_eq_left hcd]; omega)
466  · have hcd : ¬ clK (Hn d) hm elems L (2 * J) (dadP elems (hm + 1 + k)) = L := by omega
467    refine fin bits o (by omega) (by rw [hovs, ite_eq_right hcd]; omega)
468
469/-- **The first pass.** From the state after `Len` of the root is zero, the pass ends with `h = HEAP_SIZE`, `overflow` the
470number of clamped nodes, and the state of `k = 2J` positions processed. -/
471theorem ws_gbPass1 {h0 : Heap} {id : Nat} {tk : TK} {d : DeflateState} {stree : CtDataPtr} {extra : IPtr}
472    {mc base ml : Int32} {hm J elems maxc L baseN : Nat} {xb : Nat → Nat} {slOpt : Option (Nat → Nat)}
473    (ctx : P1Ctx h0 id tk d stree extra mc base ml hm J elems maxc L baseN xb slOpt)
474    (h0v : Int32) (hh0 : h0v.toInt = (hm + 1 : Nat)) (e : DeflateState)
475    (hst : P1State tk d hm J elems maxc L xb slOpt 0 e) :
476    WS h0 id (gbPass1 (Sp id) (Ptr.ref (tk.ref id) 0) stree extra mc base ml h0v) e (fun r e' =>
477      r.1.toInt = 573 ∧ r.2.toInt = (ovP (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) (2 * J) : Int) ∧
478      P1State tk d hm J elems maxc L xb slOpt (2 * J) e') := by
479  have PS := ctx.shape
480  have hm_eq := PS.hm_eq
481  unfold gbPass1
482  refine WS.cfor2 (id := id)
483    (fun (st : Int32 × Int32) e => ∃ k, k ≤ 2 * J ∧ st.1.toInt = (hm + 1 + k : Nat) ∧
484      st.2.toInt = (ovP (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) k : Int) ∧
485      P1State tk d hm J elems maxc L xb slOpt k e)
486    (fun (st : Int32 × Int32) _ => (573 : Nat) - st.1.toInt.toNat)
487    (fun (r : Int32 × Int32) e' => r.1.toInt = 573 ∧ r.2.toInt = (ovP (Hn d) hm elems L (clK (Hn d) hm elems L (2 * J)) (2 * J) : Int) ∧
488      P1State tk d hm J elems maxc L xb slOpt (2 * J) e') ?_
489    ⟨0, by omega, by show h0v.toInt = _; omega, ?_, hst⟩ (by simp only [fuel]; omega)
490  · rintro ⟨h, o⟩ e ⟨k, hk, hh, ho, hs⟩
491    simp only at hh ho
492    refine WS.pure' ?_
493    have hH : HEAP_SIZE.toInt = 573 := rfl
494    by_cases hlt : k < 2 * J
495    · refine Or.inr ⟨?_, ?_⟩
496      · simp only [gbCond1, decide_eq_true_eq]; omega
497      · refine WS.bind' (ws_gbBody1 ctx k hlt h o hh ho e hs) fun r e1 ⟨h1, h2, h3⟩ => ?_
498        have h1i : (1 : Int32).toInt = 1 := rfl
499        refine WS.bind' (ws_iadd r.1 1 (by omega) (by omega)) fun h' e2 ⟨hh', he2⟩ => ?_
500        subst e2
501        refine WS.pure' ⟨⟨k + 1, by omega, ?_, ?_, h3⟩, ?_⟩
502        · show h'.toInt = _; omega
503        · exact h2
504        · show 573 - h'.toInt.toNat < 573 - h.toInt.toNat; omega
505    · refine Or.inl ⟨?_, ?_⟩
506      · simp only [gbCond1, decide_eq_false_iff_not]; show ¬ h.toInt < 573; omega
507      · have hk2 : k = 2 * J := by omega
508        subst hk2
509        exact ⟨by show h.toInt = 573; omega, ho, hs⟩
510  · show (0 : Int32).toInt = _
511    simp [ovP]
512
513end Zlib.Trees.Proofs