trees.c.build.force.lean

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

1import ZlibF.Math.DeflateTreeForce
2import ZlibF.Proof.«trees.c.build.scan»
3
4/-!
5# trees.c: repairing an alphabet with fewer than two used symbols
6
7The fresh-leaf argument follows the reference `BuildTreeB` proof. The
8executions use the actual record and pointer accessors of this translation.
9-/
10
11namespace Zlib.Trees.Proofs
12open C Zlib.Trees
13
14/-- The body of the two-leaf repair, verbatim. -/
15def btForceBody (s : DeflateStatePtr) (tree stree : CtDataPtr) : Int32 → M Int32 :=
16  fun mc => do
17    let mut mc := mc
18    let mut val : Int32 := 0
19    if mc.toInt < 2 then
20      mc ← iadd mc 1
21      val := mc
22    let hl ← iadd (← rd s).heap_len 1
23    md s fun d => { d with heap_len := hl }
24    heapSet s hl val
25    let node := val
26    setFc tree node.toInt 1
27    setAt (← pDepth s) node.toInt 0
28    md s fun d => { d with opt_len := d.opt_len - 1 }
29    if stree != .null then
30      let l ← getDl stree node.toInt
31      md s fun d => { d with static_len := d.static_len - l.toUInt64 }
32    pure mc
33
34/-- The actual `while (s->heap_len < 2)` loop. -/
35def btForce (s : DeflateStatePtr) (tree stree : CtDataPtr) (mc : Int32) : M Int32 :=
36  cwhile (σ := Int32)
37    (fun mc => do pure (decide ((← rd s).heap_len.toInt < 2), mc))
38    (btForceBody s tree stree) mc
39
40/-- A static tree is absent, or it is a readable array unchanged by every
41write to this dynamic state. This is a heap representation fact. -/
42def BTStatic (h0 : Heap) (id : Nat) (stree : CtDataPtr) (N : Nat) (sl : Option (Nat → UInt16)) : Prop :=
43  (stree = .null ∧ sl = none) ∨ ∃ (r : CtDataRef) (T : Array CtData) (f : Nat → UInt16),
44    stree = .ref r 0 ∧ sl = some f ∧
45      (∀ e : DeflateState, Space.get (setD h0 id e) r = some T) ∧
46      ∀ v < N, v < T.size ∧ f v = (T[v]!).dl
47
48/-- The record produced by one repair iteration, including both cost
49adjustments. Unsigned costs may wrap, exactly as in C. -/
50def btForceState (tk : TK) (d : DeflateState) (node hl : Int32) (sl : Option (Nat → UInt16)) : DeflateState :=
51  { tk.setArr d ((tk.arr d).set! node.toInt.toNat { (tk.arr d)[node.toInt.toNat]! with fc := 1 }) with
52    heap_len := hl, heap := d.heap.set! hl.toInt.toNat node, depth := d.depth.set! node.toInt.toNat 0,
53    opt_len := d.opt_len - 1,
54    static_len := match sl with | none => d.static_len | some f => d.static_len - (f node.toInt.toNat).toUInt64 }
55
56/-- The tail after selecting the dummy symbol. It runs in source order. -/
57private theorem btForce_writes {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState)
58    (node mc : Int32) (N : Nat) (stree : CtDataPtr) (sl : Option (Nat → UInt16))
59    (hs : BTStatic h0 id stree N sl) (hn0 : 0 ≤ node.toInt) (hnN : node.toInt < N)
60    (hT : N ≤ (tk.arr d).size) (hD : N ≤ d.depth.size)
61    (hl0 : 0 ≤ d.heap_len.toInt) (hl2 : d.heap_len.toInt < 2) (hH : d.heap.size = 573) :
62    WS h0 id (do
63      let hl ← iadd (← rd (Sp id)).heap_len 1
64      md (Sp id) fun d => { d with heap_len := hl }
65      heapSet (Sp id) hl node
66      setFc (.ref (tk.ref id) 0) node.toInt 1
67      setAt (← pDepth (Sp id)) node.toInt 0
68      md (Sp id) fun d => { d with opt_len := d.opt_len - 1 }
69      if stree != .null then
70        let l ← getDl stree node.toInt
71        md (Sp id) fun d => { d with static_len := d.static_len - l.toUInt64 }
72      pure mc) d (fun r e => ∃ hl : Int32,
73        hl.toInt = d.heap_len.toInt + 1 ∧ r = mc ∧ e = btForceState tk d node hl sl) := by
74  have hi1 : (1 : Int32).toInt = 1 := rfl
75  refine WS.bind' ws_rd fun dz e1 ⟨hdz, he1⟩ => ?_
76  subst e1; subst dz
77  refine WS.bind' (ws_iadd d.heap_len 1 (by omega) (by omega)) fun hl e1 ⟨hhl, he1⟩ => ?_
78  subst e1
79  refine WS.bind' (ws_md (fun e => { e with heap_len := hl })) fun _ e1 he1 => ?_
80  subst e1
81  unfold heapSet
82  simp only [M_bind_assoc]
83  refine WS.bind' ws_pHeap fun p e1 ⟨hp, he1⟩ => ?_
84  subst e1; subst p
85  refine WS.bind' (ws_setAt_heap hl.toInt node (by omega) (by dsimp; omega)) fun _ e1 he1 => ?_
86  subst e1
87  have ht : tk.arr { d with heap_len := hl, heap := d.heap.set! hl.toInt.toNat node } = tk.arr d := by cases tk <;> rfl
88  refine WS.bind' (ws_setFc tk node.toInt 1 hn0 (by rw [ht]; omega)) fun _ e1 he1 => ?_
89  subst e1
90  refine WS.bind' ws_pDepth fun p e1 ⟨hp, he1⟩ => ?_
91  subst e1; subst p
92  refine WS.bind' (ws_setAt_depth node.toInt 0 hn0 (by simp only [tk_setArr_depth]; omega)) fun _ e1 he1 => ?_
93  subst e1
94  refine WS.bind' (ws_md _) fun _ e1 he1 => ?_
95  subst e1
96  rcases hs with ⟨rfl, rfl⟩ | ⟨r, T, f, rfl, rfl, hr, hf⟩
97  · simp only [bne_self_eq_false, Bool.false_eq_true, ite_false, M_pure_bind]
98    refine WS.pure' ⟨hl, by omega, rfl, ?_⟩
99    unfold btForceState
100    rw [ht]
101    cases tk <;> rfl
102  · have hne : (Ptr.ref r 0 != (Ptr.null : CtDataPtr)) = true := by simp
103    simp only [hne, ite_true]
104    have hnN' : node.toInt.toNat < N := by omega
105    have hread : ∀ e : DeflateState,
106        WS h0 id (getDl (.ref r 0) node.toInt) e
107          (fun v e' => v = f node.toInt.toNat ∧ e' = e) := by
108      intro e
109      unfold getDl
110      have hget := index0_ok (hr e) (i := node.toInt) hn0 (by have := (hf _ hnN').1; omega)
111      refine WS.of_eq (by simp only [bind_app, hget]; rfl) ⟨(hf _ hnN').2.symm, rfl⟩
112    refine WS.bind' (hread _) fun v e1 ⟨hv, he1⟩ => ?_
113    subst e1; subst v
114    refine WS.bind' (ws_md _) fun _ e1 he1 => ?_
115    subst e1
116    refine WS.pure' ⟨hl, by omega, rfl, ?_⟩
117    unfold btForceState
118    rw [ht]
119    cases tk <;> rfl
120
121/-- One actual repair step chooses the C symbol and has the exact write
122and unsigned-cost effects. Freshness is derived separately from the leaf
123invariant, rather than assumed by this execution theorem. -/
124theorem btForceBody_run {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState)
125    (mc : Int32) (N : Nat) (stree : CtDataPtr) (sl : Option (Nat → UInt16))
126    (hs : BTStatic h0 id stree N sl) (hN : 3 ≤ N) (hN286 : N ≤ 286)
127    (hm0 : -1 ≤ mc.toInt) (hmN : mc.toInt < N)
128    (hT : N ≤ (tk.arr d).size) (hD : N ≤ d.depth.size)
129    (hl0 : 0 ≤ d.heap_len.toInt) (hl2 : d.heap_len.toInt < 2) (hH : d.heap.size = 573) :
130    WS h0 id (btForceBody (Sp id) (.ref (tk.ref id) 0) stree mc) d (fun r e =>
131      ∃ node hl : Int32, node.toInt = (Math.forceNode mc.toInt : Int) ∧
132        r.toInt = Math.forceMax mc.toInt ∧ hl.toInt = d.heap_len.toInt + 1 ∧
133        e = btForceState tk d node hl sl) := by
134  have hi1 : (1 : Int32).toInt = 1 := rfl
135  unfold btForceBody
136  by_cases hsmall : mc.toInt < 2
137  · simp only [hsmall, ite_true, M_bind_assoc, M_pure_bind]
138    refine WS.bind' (ws_iadd mc 1 (by omega) (by omega)) fun mc' e1 ⟨hmc', he1⟩ => ?_
139    subst e1
140    refine WS.mono (btForce_writes tk d mc' mc' N stree sl hs (by omega) (by omega)
141      hT hD hl0 hl2 hH) ?_
142    intro r e ⟨hl, hhl, hr, he⟩
143    subst r
144    refine ⟨mc', hl, ?_, ?_, hhl, he⟩
145    · simp only [Math.forceNode, ite_eq_left hsmall]; omega
146    · simp only [Math.forceMax, ite_eq_left hsmall]; omega
147  · simp only [hsmall, ite_false, M_bind_assoc, M_pure_bind]
148    refine WS.mono (btForce_writes tk d 0 mc N stree sl hs (by decide +kernel) (by change (0 : Int) < N; omega)
149      hT hD hl0 hl2 hH) ?_
150    intro r e ⟨hl, hhl, hr, he⟩
151    subst r
152    exact ⟨0, hl, by simp only [Math.forceNode, ite_eq_right hsmall]; rfl,
153      by simp only [Math.forceMax, ite_eq_right hsmall], hhl, he⟩
154
155@[simp] theorem btForceState_tree (tk : TK) (d node hl sl) :
156    tk.arr (btForceState tk d node hl sl) =
157      (tk.arr d).set! node.toInt.toNat { (tk.arr d)[node.toInt.toNat]! with fc := 1 } := by cases tk <;> rfl
158
159@[simp] theorem btForceState_heap (tk : TK) (d node hl sl) :
160    (btForceState tk d node hl sl).heap = d.heap.set! hl.toInt.toNat node := rfl
161
162@[simp] theorem btForceState_depth (tk : TK) (d node hl sl) :
163    (btForceState tk d node hl sl).depth = d.depth.set! node.toInt.toNat 0 := rfl
164
165@[simp] theorem btForceState_len (tk : TK) (d node hl sl) :
166    (btForceState tk d node hl sl).heap_len = hl := rfl
167
168/-- Facts needed by heap construction. They are established by the scan and
169preserved by the two-leaf repair, including the all-zero alphabet. -/
170structure BTLeafInv (tk : TK) (N : Nat) (mc : Int32) (d : DeflateState) : Prop where
171  n3 : 3 ≤ N
172  n286 : N ≤ 286
173  tree : N ≤ (tk.arr d).size
174  depth : N ≤ d.depth.size
175  heap : d.heap.size = 573
176  count : d.heap_len.toInt = Math.scanCount (btFreq tk d) N
177  maxCode : mc.toInt = Math.scanMax (btFreq tk d) N
178  valid : ∀ q : Nat, 1 ≤ q → (q : Int) ≤ d.heap_len.toInt →
179    0 ≤ (d.heap[q]!).toInt ∧ (d.heap[q]!).toInt < N ∧ btFreq tk d (d.heap[q]!).toInt.toNat ≠ 0
180  injective : ∀ q q' : Nat, 1 ≤ q → (q : Int) ≤ d.heap_len.toInt →
181    1 ≤ q' → (q' : Int) ≤ d.heap_len.toInt → d.heap[q]! = d.heap[q']! → q = q'
182  complete : ∀ v < N, btFreq tk d v ≠ 0 →
183    ∃ q : Nat, 1 ≤ q ∧ (q : Int) ≤ d.heap_len.toInt ∧ (d.heap[q]!).toInt = v
184  usedDepth : ∀ v < N, btFreq tk d v ≠ 0 → d.depth[v]! = 0
185  unusedLength : ∀ v < N, btFreq tk d v = 0 → ((tk.arr d)[v]!).dl = 0
186
187/-- The initial scan supplies the leaf invariant for the repair loop. -/
188theorem BTLeafInv.of_scan {tk : TK} {d e : DeflateState} {N : Nat} {mc : Int32}
189    (hscan : BTScanInv tk d N mc e) (hN3 : 3 ≤ N) (hN286 : N ≤ 286)
190    (hT : N ≤ (tk.arr d).size) (hD : N ≤ d.depth.size) (hH : d.heap.size = 573) :
191    BTLeafInv tk N mc e := by
192  obtain ⟨T, H, D, hl, rfl, hsT, hsH, hsD, hhl, hmc, ht, hd, hh, hv, hj, hc⟩ := hscan
193  have hfreq : ∀ v < N, btFreq tk (btScanState tk d T H D hl) v = btFreq tk d v := by
194    intro v hv
195    unfold btFreq
196    rw [btScanState_tree, ht v (by omega)]
197    split <;> rfl
198  refine ⟨hN3, hN286, by simp only [btScanState_tree]; omega,
199    by simp only [btScanState_depth]; omega, by simp only [btScanState_heap]; omega,
200    ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
201  · simpa only [btScanState_len, Math.scanCount_congr _ _ N hfreq] using hhl
202  · simpa only [Math.scanMax_congr _ _ N hfreq] using hmc
203  · intro q hq1 hq2
204    obtain ⟨hq0, hqN, hfq⟩ := hv q hq1 (by simp only [btScanState_len] at hq2; omega)
205    refine ⟨hq0, hqN, ?_⟩
206    rw [btScanState_heap, hfreq _ (by omega)]
207    exact hfq
208  · intro q q' hq1 hq2 hq'1 hq'2 heq
209    exact hj q q' hq1 (by simp only [btScanState_len] at hq2; omega)
210      hq'1 (by simp only [btScanState_len] at hq'2; omega) heq
211  · intro v hv hfv
212    rw [hfreq v hv] at hfv
213    obtain ⟨q, hq1, hq2, hqv⟩ := hc v hv hfv
214    exact ⟨q, hq1, by simp only [btScanState_len]; omega, hqv⟩
215  · intro v hv hfv
216    rw [hfreq v hv] at hfv
217    simp only [btScanState_depth]
218    rw [hd v (by omega), ite_eq_left ⟨hv, hfv⟩]
219  · intro v hv hfv
220    rw [hfreq v hv] at hfv
221    simp only [btScanState_tree]
222    rw [ht v (by omega), ite_eq_left ⟨hv, hfv⟩]
223
224/-- The code-cell write is the exact frequency-function update. -/
225theorem btForceState_freq (tk : TK) (d : DeflateState) (node hl : Int32)
226    (sl : Option (Nat → UInt16)) (hn : node.toInt.toNat < (tk.arr d).size) :
227    btFreq tk (btForceState tk d node hl sl) =
228      fun v => if v = node.toInt.toNat then 1 else btFreq tk d v := by
229  funext v
230  unfold btFreq
231  rw [btForceState_tree, getD_set _ node.toInt.toNat v _ hn]
232  split <;> rfl
233
234/-- Every length survives the repair's frequency write. -/
235theorem btForceState_lengths (tk : TK) (d : DeflateState) (node hl : Int32)
236    (sl : Option (Nat → UInt16)) (hn : node.toInt.toNat < (tk.arr d).size) (v : Nat) :
237    ((tk.arr (btForceState tk d node hl sl))[v]!).dl = ((tk.arr d)[v]!).dl := by
238  rw [btForceState_tree, getD_set _ node.toInt.toNat v _ hn]
239  split
240  · rename_i heq; subst v; rfl
241  · rfl
242
243/-- One repair iteration preserves the full leaf representation. In
244particular the new leaf is fresh, so the appended heap entry cannot duplicate
245an existing one. The new maximum and frequency count are derived from the
246actual selected symbol, including `max_code = -1`, `0`, `1` and `≥ 2`. -/
247theorem BTLeafInv.force {tk : TK} {N : Nat} {mc : Int32} {d : DeflateState}
248    (hi : BTLeafInv tk N mc d) (hsmall : d.heap_len.toInt < 2)
249    (node hl mc' : Int32) (sl : Option (Nat → UInt16))
250    (hnode : node.toInt = (Math.forceNode mc.toInt : Int))
251    (hmc : mc'.toInt = Math.forceMax mc.toInt)
252    (hhl : hl.toInt = d.heap_len.toInt + 1) :
253    BTLeafInv tk N mc' (btForceState tk d node hl sl) := by
254  have hcount : Math.scanCount (btFreq tk d) N ≤ 1 := by have := hi.count; omega
255  have hfresh := Math.forceNode_fresh (btFreq tk d) N hi.n3 hcount
256  rw [← hi.maxCode] at hfresh
257  have hn0 : 0 ≤ node.toInt := by omega
258  have hnN : node.toInt.toNat < N := by omega
259  have hnodeN : node.toInt.toNat = Math.forceNode mc.toInt := by omega
260  have hnT : node.toInt.toNat < (tk.arr d).size := by have := hi.tree; omega
261  have hnD : node.toInt.toNat < d.depth.size := by have := hi.depth; omega
262  have hhl0 : 0 ≤ d.heap_len.toInt := by have := hi.count; omega
263  have hhlN : hl.toInt.toNat = d.heap_len.toInt.toNat + 1 := by omega
264  have hhH : hl.toInt.toNat < d.heap.size := by rw [hi.heap]; omega
265  have hfreq : btFreq tk (btForceState tk d node hl sl) = Math.forceFreq (btFreq tk d) mc.toInt := by
266    rw [btForceState_freq tk d node hl sl hnT, hnodeN]
267    rfl
268  have hfreqcount : Math.scanCount (btFreq tk (btForceState tk d node hl sl)) N =
269      Math.scanCount (btFreq tk d) N + 1 := by
270    rw [hfreq, hi.maxCode]
271    exact Math.scanCount_force (btFreq tk d) N hi.n3 hcount
272  have hfreqmax : Math.scanMax (btFreq tk (btForceState tk d node hl sl)) N =
273      Math.forceMax mc.toInt := by
274    rw [hfreq, hi.maxCode]
275    exact Math.scanMax_force (btFreq tk d) N hi.n3 hcount
276  have hvalueNe : ∀ q : Nat, 1 ≤ q → (q : Int) ≤ d.heap_len.toInt → d.heap[q]! ≠ node := by
277    intro q hq1 hq2 heq
278    have hused := (hi.valid q hq1 hq2).2.2
279    rw [heq, hnodeN, hfresh.2] at hused
280    exact hused rfl
281  refine ⟨hi.n3, hi.n286, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
282  · simp only [btForceState_tree, size_set!]; exact hi.tree
283  · simp only [btForceState_depth, size_set!]; exact hi.depth
284  · simp only [btForceState_heap, size_set!]; exact hi.heap
285  · simp only [btForceState_len, hfreqcount]
286    have := hi.count
287    omega
288  · rw [hmc, hfreqmax]
289  · intro q hq1 hq2
290    simp only [btForceState_len] at hq2
291    rw [btForceState_heap, getD_set _ hl.toInt.toNat q node hhH]
292    by_cases hq : q = hl.toInt.toNat
293    · rw [ite_eq_left hq]
294      refine ⟨hn0, by omega, ?_⟩
295      rw [hfreq]
296      simp [Math.forceFreq, hnodeN]
297    · rw [ite_eq_right hq]
298      obtain ⟨h0, hN, hused⟩ := hi.valid q hq1 (by omega)
299      refine ⟨h0, hN, ?_⟩
300      rw [hfreq]
301      unfold Math.forceFreq
302      split
303      · decide +kernel
304      · exact hused
305  · intro q q' hq1 hq2 hq'1 hq'2 heq
306    simp only [btForceState_len] at hq2 hq'2
307    rw [btForceState_heap, getD_set _ hl.toInt.toNat q node hhH,
308      getD_set _ hl.toInt.toNat q' node hhH] at heq
309    by_cases hq : q = hl.toInt.toNat
310    · rw [ite_eq_left hq] at heq
311      by_cases hq' : q' = hl.toInt.toNat
312      · omega
313      · rw [ite_eq_right hq'] at heq
314        exact False.elim (hvalueNe q' hq'1 (by omega) heq.symm)
315    · rw [ite_eq_right hq] at heq
316      by_cases hq' : q' = hl.toInt.toNat
317      · rw [ite_eq_left hq'] at heq
318        exact False.elim (hvalueNe q hq1 (by omega) heq)
319      · rw [ite_eq_right hq'] at heq
320        exact hi.injective q q' hq1 (by omega) hq'1 (by omega) heq
321  · intro v hv hfv
322    rw [hfreq] at hfv
323    by_cases heq : v = node.toInt.toNat
324    · refine ⟨hl.toInt.toNat, by omega, by simp only [btForceState_len]; omega, ?_⟩
325      rw [btForceState_heap, getD_set _ hl.toInt.toNat _ node hhH, ite_eq_left rfl]
326      omega
327    · have hfold : btFreq tk d v ≠ 0 := by
328        simpa only [Math.forceFreq, ite_eq_right (show v ≠ Math.forceNode mc.toInt by omega)] using hfv
329      obtain ⟨q, hq1, hq2, hqv⟩ := hi.complete v hv hfold
330      refine ⟨q, hq1, by simp only [btForceState_len]; omega, ?_⟩
331      rw [btForceState_heap, getD_set _ hl.toInt.toNat q node hhH, ite_eq_right (by omega)]
332      exact hqv
333  · intro v hv hfv
334    rw [hfreq] at hfv
335    rw [btForceState_depth, getD_set _ node.toInt.toNat v 0 hnD]
336    by_cases heq : v = node.toInt.toNat
337    · rw [ite_eq_left heq]
338    · rw [ite_eq_right heq]
339      apply hi.usedDepth v hv
340      simpa only [Math.forceFreq, ite_eq_right (show v ≠ Math.forceNode mc.toInt by omega)] using hfv
341  · intro v hv hfv
342    rw [hfreq] at hfv
343    have heq : v ≠ node.toInt.toNat := by
344      intro heq
345      rw [heq, hnodeN] at hfv
346      simp [Math.forceFreq] at hfv
347    rw [btForceState_lengths tk d node hl sl hnT]
348    apply hi.unusedLength v hv
349    simpa only [Math.forceFreq, ite_eq_right (show v ≠ Math.forceNode mc.toInt by omega)] using hfv
350
351/-- Exact record effects of successive repair iterations. This records data
352updates and symbol choices; it assumes no execution or callee contract. The
353loop theorem below establishes this trace from the actual translated loop. -/
354inductive BTForceTrace (tk : TK) (sl : Option (Nat → UInt16)) :
355    Nat → Int32 → DeflateState → Int32 → DeflateState → Prop where
356  | nil (mc : Int32) (d : DeflateState) : BTForceTrace tk sl 0 mc d mc d
357  | snoc {k : Nat} {mc0 mc mc' : Int32} {d0 d : DeflateState} (node hl : Int32)
358      (before : BTForceTrace tk sl k mc0 d0 mc d)
359      (hnode : node.toInt = (Math.forceNode mc.toInt : Int))
360      (hnodeT : node.toInt.toNat < (tk.arr d).size)
361      (hmc : mc'.toInt = Math.forceMax mc.toInt)
362      (hhl : hl.toInt = d.heap_len.toInt + 1) :
363      BTForceTrace tk sl (k + 1) mc0 d0 mc' (btForceState tk d node hl sl)
364
365/-- The complete actual repair loop terminates after at most two iterations,
366produces exactly `max(2, old heap_len)` distinct live leaves, keeps the leaf
367invariant, and records every source-order memory and cost update. -/
368theorem ws_btForce {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (mc : Int32) (N : Nat)
369    (stree : CtDataPtr) (sl : Option (Nat → UInt16)) (hs : BTStatic h0 id stree N sl)
370    (hi : BTLeafInv tk N mc d) :
371    WS h0 id (btForce (Sp id) (.ref (tk.ref id) 0) stree mc) d (fun r e =>
372      BTLeafInv tk N r e ∧ e.heap_len.toInt = max 2 d.heap_len.toInt ∧
373        ∃ k : Nat, k ≤ 2 ∧ k = (2 - d.heap_len.toInt).toNat ∧ BTForceTrace tk sl k mc d r e) := by
374  have hlen0 : 0 ≤ d.heap_len.toInt := by have := hi.count; omega
375  let Inv : Int32 → DeflateState → Prop := fun r e =>
376    BTLeafInv tk N r e ∧ e.heap_len.toInt ≤ max 2 d.heap_len.toInt ∧
377      ∃ k : Nat, k ≤ 2 ∧ e.heap_len.toInt = d.heap_len.toInt + k ∧ BTForceTrace tk sl k mc d r e
378  let Q : Int32 → DeflateState → Prop := fun r e =>
379    BTLeafInv tk N r e ∧ e.heap_len.toInt = max 2 d.heap_len.toInt ∧
380      ∃ k : Nat, k ≤ 2 ∧ k = (2 - d.heap_len.toInt).toNat ∧ BTForceTrace tk sl k mc d r e
381  unfold btForce
382  refine WS.cwhile2 Inv (fun _ e => (2 - e.heap_len.toInt).toNat) Q ?_
383    ⟨hi, by omega, 0, by omega, by omega, BTForceTrace.nil mc d⟩ (by simp only [fuel]; omega)
384  intro r e ⟨hie, hupper, k, hk, hlen, htrace⟩
385  refine WS.bind' ws_rd fun dz e1 ⟨hdz, he1⟩ => ?_
386  subst e1; subst dz
387  by_cases hsmall : e.heap_len.toInt < 2
388  · refine WS.pure' (Or.inr ⟨by simp only [hsmall, decide_true], ?_⟩)
389    have he0 : 0 ≤ e.heap_len.toInt := by have := hie.count; omega
390    have hm := Math.scanMax_bounds (btFreq tk e) N
391    rw [← hie.maxCode] at hm
392    refine WS.mono (btForceBody_run tk e r N stree sl hs hie.n3 hie.n286 hm.1 hm.2
393      hie.tree hie.depth he0 hsmall hie.heap) ?_
394    intro r' e' ⟨node, hl, hn, hmc', hhl, he'⟩
395    subst e'
396    have hnT : node.toInt.toNat < (tk.arr e).size := by
397      have hfresh := Math.forceNode_fresh (btFreq tk e) N hie.n3 (by have := hie.count; omega)
398      rw [← hie.maxCode] at hfresh
399      have := hie.tree
400      omega
401    refine ⟨⟨hie.force hsmall node hl r' sl hn hmc' hhl, ?_, k + 1, by omega, ?_,
402      BTForceTrace.snoc node hl htrace hn hnT hmc' hhl⟩, ?_⟩
403    · simp only [btForceState_len]; omega
404    · simp only [btForceState_len]; omega
405    · simp only [btForceState_len]; omega
406  · refine WS.pure' (Or.inl ⟨by simp only [hsmall, decide_false], hie, ?_, k, hk, ?_, htrace⟩)
407    · omega
408    · omega
409
410/-- The repair cannot change any tree length. This follows from the exact
411trace of actual iterations, not a frame premise supplied by a caller. -/
412theorem BTForceTrace.lengths {tk : TK} {sl : Option (Nat → UInt16)}
413    {k : Nat} {mc0 mc : Int32} {d0 d : DeflateState} (h : BTForceTrace tk sl k mc0 d0 mc d)
414    (v : Nat) : ((tk.arr d)[v]!).dl = ((tk.arr d0)[v]!).dl := by
415  induction h with
416  | nil => rfl
417  | snoc node hl before hn hnT hm hhl ih =>
418    rw [btForceState_lengths tk _ node hl sl hnT v, ih]
419
420/-- Every field outside the selected tree, heap, depth, heap length and two
421cost counters is unchanged. All other heap records are already framed by
422the actual loop execution theorem's `WS` result. -/
423theorem BTForceTrace.frame {tk : TK} {sl : Option (Nat → UInt16)}
424    {k : Nat} {mc0 mc : Int32} {d0 d : DeflateState} (h : BTForceTrace tk sl k mc0 d0 mc d) :
425    ∃ (T : Array CtData) (H : Array Int32) (D : Array UInt8) (hl : Int32) (O S : UInt64),
426      d = { btScanState tk d0 T H D hl with opt_len := O, static_len := S } := by
427  induction h with
428  | nil mc d =>
429    refine ⟨tk.arr d, d.heap, d.depth, d.heap_len, d.opt_len, d.static_len, ?_⟩
430    cases tk <;> rfl
431  | snoc node hl before hn hnT hm hhl ih =>
432    obtain ⟨T, H, D, hl0, O, S, he⟩ := ih
433    subst he
434    refine ⟨T.set! node.toInt.toNat { T[node.toInt.toNat]! with fc := 1 },
435      H.set! hl.toInt.toNat node, D.set! node.toInt.toNat 0, hl, O - 1,
436      (match sl with | none => S | some f => S - (f node.toInt.toNat).toUInt64), ?_⟩
437    cases sl <;> cases tk <;> rfl
438
439/-- The repair subtracts exactly one from the unsigned optimal-bit counter
440per iteration. No non-underflow assumption is needed. -/
441theorem BTForceTrace.opt_len {tk : TK} {sl : Option (Nat → UInt16)}
442    {k : Nat} {mc0 mc : Int32} {d0 d : DeflateState} (h : BTForceTrace tk sl k mc0 d0 mc d)
443    (hk : k ≤ 2) : d.opt_len = d0.opt_len - UInt64.ofNat k := by
444  induction h with
445  | nil => simp
446  | @snoc k' mc0 mc mc' d0' d' node hl before hn hnT hm hhl ih =>
447    change _ - 1 = _
448    rw [ih (by omega)]
449    apply UInt64.toNat_inj.mp
450    simp only [UInt64.toNat_sub, UInt64.toNat_ofNat', show (1 : UInt64).toNat = 1 from rfl]
451    have hlt := d0'.opt_len.toNat_lt
452    omega
453
454end Zlib.Trees.Proofs