trees.c.send-tree.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.scan-tree»
2import ZlibF.Proof.«trees.c.emit-state»
3
4/-! # trees.c: actual run-length tree-description output -/
5
6namespace Zlib.Trees.Proofs
7open C Zlib.Trees Out
8
9/-- The actual direct-code repeat, including the final decrement. -/
10def stRepeat (s : DeflateStatePtr) (cur count : Int32) : M Int32 :=
11  cdoWhile
12    (fun c => do send_code s cur.toInt (← pBltree s); pure c)
13    (fun c => do let c ← isub c 1; pure (c != 0, c)) count
14
15/-- One actual bit-length-code call, including its pointer read. -/
16def stCode (s : DeflateStatePtr) (c : Int) : M Unit := do
17  send_code s c (← pBltree s)
18
19/-- Every output branch of the actual send_tree body, in source order. -/
20def stSend (s : DeflateStatePtr) (cur prev count0 minc : Int32) : M Int32 := do
21  let mut count := count0
22  if count.toInt < minc.toInt then
23    count ← stRepeat s cur count
24  else if cur != 0 then
25    if cur != prev then
26      stCode s cur.toInt
27      count ← isub count 1
28    stCode s REP_3_6.toInt
29    send_bits s (← isub count 3) 2
30  else if count.toInt ≤ 10 then
31    stCode s REPZ_3_10.toInt
32    send_bits s (← isub count 3) 3
33  else
34    stCode s REPZ_11_138.toInt
35    send_bits s (← isub count 11) 7
36  pure count
37
38/-- The actual body, including the source early continue and local tail. -/
39def stBody (s : DeflateStatePtr) (tree : CtDataPtr) : SCLocals → M SCLocals :=
40  fun (n, prevlen, nextlen, count, max_count, min_count, _) => do
41    let curlen := nextlen
42    let nextlen := u16i (← getDl tree (← iadd n 1).toInt)
43    let count ← iadd count 1
44    if count.toInt < max_count.toInt ∧ curlen == nextlen then
45      return (n, prevlen, nextlen, count, max_count, min_count, 0)
46    let _ ← stSend s curlen prevlen count min_count
47    pure (scTail n curlen nextlen)
48
49def stLoop (s : DeflateStatePtr) (tree : CtDataPtr) (mc : Int32) (r : SCLocals) : M SCLocals :=
50  cfor (fun (n, _) => pure (decide (n.toInt ≤ mc.toInt)))
51    (fun (n, rest) => do pure (← iadd n 1, rest)) (stBody s tree) r
52
53/-- Complete source equality, independent of the execution proofs below. -/
54theorem send_tree_eq (s : DeflateStatePtr) (tree : CtDataPtr) (mc : Int32) :
55    send_tree s tree mc = (do
56      let nextlen0 := u16i (← getDl tree 0)
57      let (mx0, mn0) : Int32 × Int32 := if nextlen0 == 0 then (138, 3) else (7, 4)
58      let _ ← stLoop s tree mc (0, -1, nextlen0, 0, mx0, mn0, 0)
59      pure ()) := by
60  unfold send_tree stLoop stBody stSend stRepeat stCode scTail
61  simp only [M_bind_assoc, M_pure_bind, merge_ite_bind]
62
63/-- Scalar checked arithmetic used by the actual output loops. -/
64theorem st_isub (a b : Int32) (hlo : -2147483648 ≤ a.toInt - b.toInt)
65    (hhi : a.toInt - b.toInt ≤ 2147483647) :
66    isub a b = pure (Int32.ofInt (a.toInt - b.toInt)) := by
67  simp only [isub, ck, hlo, hhi, and_self, ite_true]
68
69theorem st_iadd (a b : Int32) (hlo : -2147483648 ≤ a.toInt + b.toInt)
70    (hhi : a.toInt + b.toInt ≤ 2147483647) :
71    iadd a b = pure (Int32.ofInt (a.toInt + b.toInt)) := by
72  simp only [iadd, ck, hlo, hhi, and_self, ite_true]
73
74theorem st_v16 (a : Int32) (A : Nat) (ha : a.toInt = A) (hA : A < 65536) : v16 a = A := by
75  unfold v16 i2us
76  rw [ha]
77  have hm : ((A : Int) % 65536).toNat = A := by omega
78  rw [UInt16.toNat_ofNat', hm]
79  exact Nat.mod_eq_of_lt hA
80
81theorem st_rep_succ {α : Type} (n : Nat) (xs : List α) :
82    (List.replicate (n + 1) xs).flatten = (List.replicate n xs).flatten ++ xs := by
83  rw [List.replicate_succ', List.flatten_append]
84  simp
85
86theorem st_rep_length {α : Type} (n : Nat) (xs : List α) :
87    (List.replicate n xs).flatten.length = n * xs.length := by
88  induction n with
89  | zero => simp
90  | succ n ih => rw [st_rep_succ, List.length_append, ih, Nat.succ_mul]
91
92/-- The actual direct-repeat loop emits exactly count copies and executes
93its final signed decrement. The loop measure proves termination. -/
94theorem stRepeat_run {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
95    {w : List Bool} (ht : EmitState id b h0 d0 buf0 w h d buf)
96    (cur count : Int32) (C K total : Nat) (hcur : cur.toInt = C) (hc : C < 19)
97    (hk : count.toInt = K) (hK0 : 1 ≤ K) (hK : K ≤ 138)
98    (hfit : CodeFits (blWords d0) C)
99    (hp : w.length + K * (codeBits (blWords d0) C).length ≤ total)
100    (hr : 8 * d0.pending.toNat + d0.bi_valid.toInt.toNat + total ≤ 8 * buf0.size) :
101    EWP (stRepeat (some (.tab id)) cur count) h (fun c h' => c = 0 ∧ ∃ d' buf',
102      EmitState id b h0 d0 buf0 (w ++ (List.replicate K (codeBits (blWords d0) C)).flatten) h' d' buf') := by
103  let bits := codeBits (blWords d0) C
104  change w.length + K * bits.length ≤ total at hp
105  let P := fun k (c : Int32) H => k < K ∧ c.toInt = (k + 1 : Nat) ∧ ∃ D B,
106    EmitState id b h0 d0 buf0 (w ++ (List.replicate (K - 1 - k) bits).flatten) H D B
107  let Q := fun (c : Int32) H => c = 0 ∧ ∃ D B,
108    EmitState id b h0 d0 buf0 (w ++ (List.replicate K bits).flatten) H D B
109  have step : ∀ k c H, P (k + 1) c H → ∃ c1 H1 c2 H2,
110      (do send_code (some (.tab id)) cur.toInt (← pBltree (some (.tab id))); pure c) H = .ok (c1, H1) ∧
111      (do let c ← isub c1 1; pure (c != 0, c)) H1 = .ok ((true, c2), H2) ∧ P k c2 H2 := by
112    rintro k c H ⟨hkl, hcv, D, B, htrace⟩
113    have hs : (K - 1 - (k + 1)) + 1 ≤ K := by omega
114    have hmul := Nat.mul_le_mul_right bits.length hs
115    have hlen : (w ++ (List.replicate (K - 1 - (k + 1)) bits).flatten).length + bits.length ≤ total := by
116      rw [List.length_append, st_rep_length]
117      rw [Nat.succ_mul] at hmul
118      omega
119    have hroom := htrace.room bits.length total hlen hr
120    have hbitslen : bits.length = (blWords d0 C).2.toNat := by simp [bits, codeBits, natBits]
121    rw [hbitslen] at hroom
122    obtain ⟨a, H1, hsnd, D1, B1, htrace1⟩ := htrace.bl_code C hc hfit hroom
123    have ha : a = () := Subsingleton.elim _ _
124    subst a
125    have hbody : (do send_code (some (.tab id)) cur.toInt (← pBltree (some (.tab id))); pure c) H = .ok (c, H1) := by
126      rw [hcur, ← M_bind_assoc, bind_app, hsnd]
127      rfl
128    let cv := Int32.ofInt (c.toInt - 1)
129    have hsub : isub c 1 = pure cv := st_isub c 1 (by change -2147483648 ≤ c.toInt - 1; omega)
130      (by change c.toInt - 1 ≤ 2147483647; omega)
131    have hcv' : cv.toInt = (k + 1 : Nat) := by
132      dsimp [cv]
133      rw [ofInt_toInt' _ (by omega) (by omega)]
134      omega
135    have hne : (cv != 0) = true := by
136      rw [bne_iff_ne, ne_eq, ← Int32.toInt_inj, hcv']
137      change ¬ (k + 1 : Int) = 0
138      omega
139    refine ⟨c, H1, cv, H1, hbody, ?_, by omega, hcv', D1, B1, ?_⟩
140    · rw [hsub]
141      simp only [M_pure_bind, hne]
142      rfl
143    · have he : K - 1 - k = (K - 1 - (k + 1)) + 1 := by omega
144      rw [he, st_rep_succ, ← List.append_assoc]
145      exact htrace1
146  have last : ∀ c H, P 0 c H → ∃ c1 H1 c2 H2,
147      (do send_code (some (.tab id)) cur.toInt (← pBltree (some (.tab id))); pure c) H = .ok (c1, H1) ∧
148      (do let c ← isub c1 1; pure (c != 0, c)) H1 = .ok ((false, c2), H2) ∧ Q c2 H2 := by
149    rintro c H ⟨hkl, hcv, D, B, htrace⟩
150    have hlen : (w ++ (List.replicate (K - 1 - 0) bits).flatten).length + bits.length ≤ total := by
151      rw [List.length_append, st_rep_length]
152      have hm : (K - 1) * bits.length + bits.length = K * bits.length := by
153        rw [← Nat.succ_mul, Nat.succ_eq_add_one, Nat.sub_add_cancel hK0]
154      simp only [Nat.sub_zero]
155      omega
156    have hroom := htrace.room bits.length total hlen hr
157    have hbitslen : bits.length = (blWords d0 C).2.toNat := by simp [bits, codeBits, natBits]
158    rw [hbitslen] at hroom
159    obtain ⟨a, H1, hsnd, D1, B1, htrace1⟩ := htrace.bl_code C hc hfit hroom
160    have ha : a = () := Subsingleton.elim _ _
161    subst a
162    refine ⟨c, H1, 0, H1, ?_, ?_, rfl, D1, B1, ?_⟩
163    · rw [hcur, ← M_bind_assoc, bind_app, hsnd]
164      rfl
165    · rw [st_isub c 1 (by change -2147483648 ≤ c.toInt - 1; omega)
166        (by change c.toInt - 1 ≤ 2147483647; omega)]
167      have he : Int32.ofInt (c.toInt - (1 : Int32).toInt) = 0 := by
168        rw [hcv]
169        rfl
170      rw [he]
171      rfl
172    · have he : K = (K - 1 - 0) + 1 := by omega
173      rw [he, st_rep_succ, ← List.append_assoc]
174      exact htrace1
175  have hstart : P (K - 1) count h := by
176    refine ⟨by omega, by omega, d, buf, ?_⟩
177    simpa using ht
178  obtain ⟨c, H, hrun, hQ⟩ := _root_.C.cdoWhile_run P Q step last hstart (by unfold fuel; omega)
179  exact ⟨c, H, hrun, hQ⟩
180
181/-- A repetition symbol followed by its checked extra-bit subtraction. -/
182theorem stCode_extra {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
183    {w : List Bool} (ht : EmitState id b h0 d0 buf0 w h d buf)
184    (code count off len : Int32) (K V L total : Nat)
185    (hcode : code.toInt = K) (hK : K < 19)
186    (hV : count.toInt - off.toInt = V) (hV16 : V < 65536)
187    (hL : len.toInt = L) (hL15 : L ≤ 15) (hfit : V < 2 ^ L)
188    (hc : CodeFits (blWords d0) K)
189    (hp : w.length + (codeBits (blWords d0) K).length + L ≤ total)
190    (hr : 8 * d0.pending.toNat + d0.bi_valid.toInt.toNat + total ≤ 8 * buf0.size) :
191    EWP (do stCode (some (.tab id)) code.toInt
192            send_bits (some (.tab id)) (← isub count off) len) h
193      (fun _ h' => ∃ d' buf', EmitState id b h0 d0 buf0
194        (w ++ codeBits (blWords d0) K ++ natBits V L) h' d' buf') := by
195  have hbl : (codeBits (blWords d0) K).length = (blWords d0 K).2.toNat := by simp [codeBits, natBits]
196  have hroom := ht.room (blWords d0 K).2.toNat total (by omega) hr
197  unfold stCode
198  rw [hcode]
199  refine EWP.bind (ht.bl_code K hK hc hroom) ?_
200  rintro _ H ⟨D, B, hs⟩
201  rw [st_isub count off (by omega) (by omega)]
202  refine EWP.bind (EWP.pure (Q := fun v H' => v = Int32.ofInt (count.toInt - off.toInt) ∧ H' = H) ⟨rfl, rfl⟩) ?_
203  rintro _ _ ⟨rfl, rfl⟩
204  have hv : (Int32.ofInt (count.toInt - off.toInt)).toInt = V := by
205    rw [ofInt_toInt' _ (by omega) (by omega), hV]
206  exact hs.extra_bits _ len V L (st_v16 _ V hv hV16) (by rw [hL]; simp) (by omega) (by omega) hfit
207    (hs.room L total (by simpa only [List.length_append] using hp) hr)
208
209theorem Out.EWP.keep {α : Type} {h : Heap} {m : M Unit} {Q : Heap → Prop}
210    (hm : EWP m h (fun _ H => Q H)) (a : α) :
211    EWP (m >>= fun _ => (Pure.pure a : M α)) h (fun _ H => Q H) :=
212  EWP.bind hm (by intro _ H hq; exact EWP.pure hq)
213
214/-- Exact output for a finished run in the actual send_tree body. The
215code premises describe only entries used by this run. -/
216theorem stSend_run {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
217    {w : List Bool} (ht : EmitState id b h0 d0 buf0 w h d buf)
218    (cur prev count minc : Int32) (s : RunSt) (total : Nat)
219    (hc : cur.toInt = s.next) (hpv : prev.toInt = s.prev)
220    (hcnt : count.toInt = (s.cnt + 1 : Nat)) (hmn : minc.toInt = s.mn)
221    (hi : RunInv s) (hcur : s.next ≤ 15)
222    (hcodes : ∀ k < 19, 0 < runFreq (some (s.next, s.prev, s.cnt + 1, s.mn)) k →
223      CodeFits (blWords d0) k)
224    (hp : w.length + (runBits (blWords d0) (some (s.next, s.prev, s.cnt + 1, s.mn))).length ≤ total)
225    (hr : 8 * d0.pending.toNat + d0.bi_valid.toInt.toNat + total ≤ 8 * buf0.size) :
226    EWP (stSend (some (.tab id)) cur prev count minc) h (fun _ h' => ∃ d' buf',
227      EmitState id b h0 d0 buf0 (w ++ runBits (blWords d0) (some (s.next, s.prev, s.cnt + 1, s.mn))) h' d' buf') := by
228  have hmx : s.mx ≤ 138 := by
229    by_cases hz : s.next = 0
230    · rw [(hi.2.1 hz).1]
231      omega
232    · rcases hi.2.2.1 hz with ⟨h, rest⟩ | ⟨h, rest⟩ <;> omega
233  have hmn3 : 3 ≤ s.mn := by
234    by_cases hz : s.next = 0
235    · rw [(hi.2.1 hz).2]
236      omega
237    · rcases hi.2.2.1 hz with ⟨h, h', rest⟩ | ⟨h, h', rest⟩ <;> omega
238  have hsmall : count.toInt < minc.toInt ↔ s.cnt + 1 < s.mn := by omega
239  have hzero : ((cur != 0) = true) ↔ s.next ≠ 0 := by
240    rw [bne_iff_ne, ne_eq, ← Int32.toInt_inj, hc]
241    change ¬ (s.next : Int) = 0 ↔ s.next ≠ 0
242    omega
243  have hprev : ((cur != prev) = true) ↔ (s.next : Int) ≠ s.prev := by
244    rw [bne_iff_ne, ne_eq, ← Int32.toInt_inj, hc, hpv]
245  unfold stSend
246  simp only [hsmall, hzero, hprev]
247  by_cases hs : s.cnt + 1 < s.mn
248  · simp only [hs, ite_true]
249    have hfit : CodeFits (blWords d0) s.next := hcodes s.next (by omega) (by
250      simp only [runFreq, ite_eq_left hs, ite_true]
251      omega)
252    have hp' : w.length + (s.cnt + 1) * (codeBits (blWords d0) s.next).length ≤ total := by
253      simpa only [runBits, ite_eq_left hs, st_rep_length] using hp
254    refine EWP.bind (stRepeat_run ht cur count s.next (s.cnt + 1) total hc (by omega) hcnt
255      (by omega) (by have := hi.1; omega) hfit hp' hr) ?_
256    rintro c H ⟨hc0, D, B, htrace⟩
257    refine EWP.pure ⟨D, B, ?_⟩
258    simpa only [runBits, ite_eq_left hs] using htrace
259  · simp only [hs, ite_false]
260    by_cases hz : s.next ≠ 0
261    · simp only [ite_eq_left hz]
262      have h16 := hcodes 16 (by omega) (by
263        simp only [runFreq, ite_eq_right hs, ite_eq_left hz, ite_true]
264        omega)
265      by_cases hneq : (s.next : Int) ≠ s.prev
266      · simp only [ite_eq_left hneq]
267        have h7 : s.mx = 7 ∧ s.mn = 4 := by
268          rcases hi.2.2.1 hz with h | h
269          · exact False.elim (hneq h.2.2)
270          · exact ⟨h.1, h.2.1⟩
271        have hf := hcodes s.next (by omega) (by
272          simp only [runFreq, ite_eq_right hs, ite_eq_left hz, and_true, ite_eq_left hneq]
273          omega)
274        simp only [runBits, ite_eq_right hs, ite_eq_left hz, ite_eq_left hneq,
275          List.length_append, codeBits, natBits, List.length_map, List.length_range] at hp
276        have hrC := ht.room (blWords d0 s.next).2.toNat total (by omega) hr
277        rw [hc]
278        refine EWP.bind (ht.bl_code s.next (by omega) hf hrC) ?_
279        rintro _ H ⟨D, B, ht1⟩
280        rw [st_isub count 1 (by change -2147483648 ≤ count.toInt - 1; omega)
281          (by change count.toInt - 1 ≤ 2147483647; have := hi.1; omega), M_pure_bind]
282        let cv := Int32.ofInt (count.toInt - (1 : Int32).toInt)
283        have hcv : cv.toInt = s.cnt := by
284          dsimp [cv]
285          rw [ofInt_toInt' _ (by have := hi.1; omega) (by have := hi.1; omega)]
286          change count.toInt - 1 = (s.cnt : Int)
287          omega
288        have he := stCode_extra ht1 REP_3_6 cv 3 2 16 (s.cnt + 1 - 1 - 3) 2 total
289          rfl (by omega) (by change cv.toInt - 3 = _; rw [hcv]; omega)
290          (by have := hi.1; omega) rfl (by omega) (by change _ < 4; have := hi.1; omega) h16
291          (by simp only [List.length_append, codeBits, natBits, List.length_map, List.length_range]; omega) hr
292        apply EWP.mono (by simpa only [M_bind_assoc] using he.keep cv)
293        rintro _ H' ⟨D', B', ht2⟩
294        refine ⟨D', B', ?_⟩
295        simpa only [runBits, ite_eq_right hs, ite_eq_left hz, ite_eq_left hneq, List.append_assoc] using ht2
296      · simp only [ite_eq_right hneq]
297        have heq : (s.next : Int) = s.prev := by omega
298        have h6 : s.mx = 6 ∧ s.mn = 3 := by
299          rcases hi.2.2.1 hz with h | h
300          · exact ⟨h.1, h.2.1⟩
301          · exact False.elim (h.2.2 heq)
302        have hlen : w.length + (codeBits (blWords d0) 16).length + 2 ≤ total := by
303          simpa only [runBits, ite_eq_right hs, ite_eq_left hz, ite_eq_right hneq,
304            List.length_append, natBits, List.length_map, List.length_range, Nat.add_assoc] using hp
305        have he := stCode_extra ht REP_3_6 count 3 2 16 (s.cnt + 1 - 3) 2 total rfl (by omega)
306          (by change count.toInt - 3 = _; omega) (by have := hi.1; omega) rfl (by omega)
307          (by change _ < 4; have := hi.1; omega) h16 hlen hr
308        apply EWP.mono (by simpa only [M_bind_assoc] using he.keep count)
309        rintro _ H' ⟨D', B', ht2⟩
310        refine ⟨D', B', ?_⟩
311        simpa only [runBits, ite_eq_right hs, ite_eq_left hz, ite_eq_right hneq, List.append_assoc] using ht2
312    · simp only [hz, ite_false]
313      have hcount0 : 3 ≤ s.cnt + 1 := by omega
314      have hcond : count.toInt ≤ 10 ↔ s.cnt + 1 ≤ 10 := by omega
315      simp only [hcond]
316      by_cases h10 : s.cnt + 1 ≤ 10
317      · simp only [h10, ite_true]
318        have hf := hcodes 17 (by omega) (by simp only [runFreq, ite_eq_right hs, ite_eq_right hz, ite_eq_left h10, ite_true]; omega)
319        have hlen : w.length + (codeBits (blWords d0) 17).length + 3 ≤ total := by
320          simpa only [runBits, ite_eq_right hs, ite_eq_right hz, ite_eq_left h10,
321            List.length_append, natBits, List.length_map, List.length_range, Nat.add_assoc] using hp
322        have he := stCode_extra ht REPZ_3_10 count 3 3 17 (s.cnt + 1 - 3) 3 total rfl (by omega)
323          (by change count.toInt - 3 = _; omega) (by omega) rfl (by omega) (by change _ < 8; omega) hf hlen hr
324        apply EWP.mono (by simpa only [M_bind_assoc] using he.keep count)
325        rintro _ H' ⟨D', B', ht2⟩
326        refine ⟨D', B', ?_⟩
327        simpa only [runBits, ite_eq_right hs, ite_eq_right hz, ite_eq_left h10, List.append_assoc] using ht2
328      · simp only [h10, ite_false]
329        have hf := hcodes 18 (by omega) (by simp only [runFreq, ite_eq_right hs, ite_eq_right hz, ite_eq_right h10, ite_true]; omega)
330        have hlen : w.length + (codeBits (blWords d0) 18).length + 7 ≤ total := by
331          simpa only [runBits, ite_eq_right hs, ite_eq_right hz, ite_eq_right h10,
332            List.length_append, natBits, List.length_map, List.length_range, Nat.add_assoc] using hp
333        have he := stCode_extra ht REPZ_11_138 count 11 7 18 (s.cnt + 1 - 11) 7 total rfl (by omega)
334          (by change count.toInt - 11 = _; omega) (by have := hi.1; omega) rfl (by omega)
335          (by change _ < 128; have := hi.1; omega) hf hlen hr
336        apply EWP.mono (by simpa only [M_bind_assoc] using he.keep count)
337        rintro _ H' ⟨D', B', ht2⟩
338        refine ⟨D', B', ?_⟩
339        simpa only [runBits, ite_eq_right hs, ite_eq_right hz, ite_eq_right h10, List.append_assoc] using ht2
340
341/-- Every dynamic-tree array is outside the bit-output write footprint. -/
342theorem emitState_tk_arr {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
343    {w : List Bool} (ht : EmitState id b h0 d0 buf0 w h d buf) (tk : TK) : tk.arr d = tk.arr d0 := by
344  cases tk
345  · exact ht.tree_arrays.1
346  · exact ht.tree_arrays.2.1
347  · exact ht.tree_arrays.2.2
348
349/-- One actual body preserves the local/model correspondence and emits
350exactly this iteration's model bits, including an empty early continue. -/
351theorem stBody_run {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
352    {w : List Bool} (ht : EmitState id b h0 d0 buf0 w h d buf)
353    (tk : TK) (L : Nat → Nat) (n : Nat) (s : RunSt) (r : SCLocals) (total : Nat)
354    (hcorr : SCCorr r n s) (hi : RunInv s) (hn : n ≤ 285)
355    (hread : n + 1 < (tk.arr d0).size) (hl : (tk.arr d0)[n + 1]!.dl.toNat = L (n + 1))
356    (hcur : s.next ≤ 15)
357    (hcodes : ∀ k < 19, 0 < runFreq (runStep L n s).2 k → CodeFits (blWords d0) k)
358    (hp : w.length + (runBits (blWords d0) (runStep L n s).2).length ≤ total)
359    (hr : 8 * d0.pending.toNat + d0.bi_valid.toInt.toNat + total ≤ 8 * buf0.size) :
360    EWP (stBody (some (.tab id)) (.ref (tk.ref id) 0) r) h (fun r' H =>
361      SCCorr r' n (runStep L n s).1 ∧ ∃ D B,
362        EmitState id b h0 d0 buf0 (w ++ runBits (blWords d0) (runStep L n s).2) H D B) := by
363  rcases r with ⟨ni, pi, ci, ki, mi, mni, unused⟩
364  obtain ⟨hnc, hpc, hcc, hkc, hmc, hmnc⟩ := hcorr
365  dsimp only at hnc hpc hcc hkc hmc hmnc
366  have hone : (1 : Int32).toInt = 1 := rfl
367  have hmx : s.mx ≤ 138 := by
368    by_cases hz : s.next = 0
369    · rw [(hi.2.1 hz).1]
370      omega
371    · rcases hi.2.2.1 hz with ⟨hh, rest⟩ | ⟨hh, rest⟩ <;> omega
372  have hn1 : (Int32.ofInt (ni.toInt + (1 : Int32).toInt)).toInt = (n + 1 : Nat) := by
373    rw [ofInt_toInt' _ (by omega) (by omega)]
374    change ni.toInt + 1 = _
375    omega
376  have htarr := emitState_tk_arr ht tk
377  have hg := tk_get (h0 := h) (id := id) (d := d) tk
378  rw [Zlib.Trees.Proofs.setD_self ht.inv.base.dstate] at hg
379  have hidx : (Int32.ofInt (ni.toInt + (1 : Int32).toInt)).toInt = ((n + 1 : Nat) : Int) := hn1
380  have hload : getDl (.ref (tk.ref id) 0) (Int32.ofInt (ni.toInt + (1 : Int32).toInt)).toInt h =
381      .ok ((tk.arr d0)[n + 1]!.dl, h) := by
382    rw [hidx]
383    have hs := getDl_gen hg (by rw [htarr]; exact hread)
384    simpa only [getElem!_pos, htarr, hread] using hs
385  have hk1 : (Int32.ofInt (ki.toInt + (1 : Int32).toInt)).toInt = (s.cnt + 1 : Nat) := by
386    rw [ofInt_toInt' _ (by have := hi.1; omega) (by have := hi.1; omega)]
387    change ki.toInt + 1 = _
388    omega
389  have hnx : (u16i (tk.arr d0)[n + 1]!.dl).toInt = L (n + 1) := by rw [u16i_toInt, hl]
390  have hsame : ((ci == u16i (tk.arr d0)[n + 1]!.dl) = true) ↔ s.next = L (n + 1) := by
391    rw [beq_iff_eq, ← Int32.toInt_inj, hcc, hnx, Int.natCast_inj]
392  have hcond : (Int32.ofInt (ki.toInt + (1 : Int32).toInt)).toInt < mi.toInt ∧
393      (ci == u16i (tk.arr d0)[n + 1]!.dl) = true ↔ s.cnt + 1 < s.mx ∧ s.next = L (n + 1) := by
394    rw [hk1, hmc, hsame]
395    omega
396  unfold stBody
397  dsimp only
398  rw [st_iadd ni 1 (by change -2147483648 ≤ ni.toInt + 1; omega)
399    (by change ni.toInt + 1 ≤ 2147483647; omega), M_pure_bind]
400  refine EWP.read hload ?_
401  rw [st_iadd ki 1 (by change -2147483648 ≤ ki.toInt + 1; omega)
402    (by change ki.toInt + 1 ≤ 2147483647; have := hi.1; omega), M_pure_bind]
403  simp only [hcond]
404  by_cases ha : s.cnt + 1 < s.mx ∧ s.next = L (n + 1)
405  · simp only [ite_eq_left ha]
406    refine EWP.pure ⟨?_, d, buf, ?_⟩
407    · simp only [runStep, ite_eq_left ha, SCCorr]
408      exact ⟨hnc, hpc, hnx, hk1, hmc, hmnc⟩
409    · simpa only [runStep, ite_eq_left ha, runBits, List.append_nil] using ht
410  · simp only [ite_eq_right ha]
411    have hcodes' : ∀ k < 19, 0 < runFreq (some (s.next, s.prev, s.cnt + 1, s.mn)) k → CodeFits (blWords d0) k := by
412      simpa only [runStep, ite_eq_right ha] using hcodes
413    have hp' : w.length + (runBits (blWords d0) (some (s.next, s.prev, s.cnt + 1, s.mn))).length ≤ total := by
414      simpa only [runStep, ite_eq_right ha] using hp
415    refine EWP.bind (stSend_run ht ci pi _ mni s total hcc hpc hk1 hmnc hi hcur hcodes' hp' hr) ?_
416    rintro _ H ⟨D, B, htrace⟩
417    refine EWP.pure ⟨?_, D, B, ?_⟩
418    · simp only [runStep, ite_eq_right ha]
419      exact scTail_corr _ _ _ _ _ _ hnc hcc hnx
420    · simpa only [runStep, ite_eq_right ha] using htrace
421
422theorem st_scanFreq_mono (L : Nat → Nat) (k : Nat) {i j : Nat} (hij : i ≤ j) :
423    scanFreqUpTo L i k ≤ scanFreqUpTo L j k := by
424  induction j with
425  | zero => have he : i = 0 := by omega
426            subst he
427            exact Nat.le_refl _
428  | succ j ih =>
429    by_cases he : i = j + 1
430    · subst he
431      exact Nat.le_refl _
432    · have hb := ih (by omega)
433      simp only [scanFreqUpTo]
434      omega
435
436theorem st_runFreq_le (L : Nat → Nat) (n m k : Nat) (hn : n < m) :
437    runFreq (runStep L n (runAt L n)).2 k ≤ scanFreqUpTo L m k := by
438  have hm := st_scanFreq_mono L k (i := n + 1) (j := m) (by omega)
439  simp only [scanFreqUpTo] at hm
440  omega
441
442/-- A whole actual iteration, including n++, preserves the emitted prefix.
443Required code entries derive from the complete source scan's used symbols. -/
444theorem stIteration_run {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
445    (tk : TK) (L : Nat → Nat) (n M : Nat) (r : SCLocals)
446    (ht : EmitState id b h0 d0 buf0 (treeBitsUpTo (blWords d0) L n) h d buf)
447    (hn : n ≤ M) (hM : M ≤ 285) (hT : M + 1 < (tk.arr d0).size)
448    (hread : ∀ i ≤ M + 1, (tk.arr d0)[i]!.dl.toNat = L i)
449    (h16 : ∀ i, L i < 65536) (h15 : ∀ i ≤ M, L i ≤ 15)
450    (hcodes : ∀ k < 19, 0 < scanFreqUpTo L (M + 1) k → CodeFits (blWords d0) k)
451    (hr : 8 * d0.pending.toNat + d0.bi_valid.toInt.toNat + (sendTreeBits (blWords d0) L M).length ≤ 8 * buf0.size)
452    (hcorr : SCCorr r n (runAt L n)) :
453    EWP (do let (ni, rest) ← stBody (some (.tab id)) (.ref (tk.ref id) 0) r
454            pure (← iadd ni 1, rest)) h (fun r' H =>
455      SCCorr r' (n + 1) (runAt L (n + 1)) ∧ ∃ D B,
456        EmitState id b h0 d0 buf0 (treeBitsUpTo (blWords d0) L (n + 1)) H D B) := by
457  have hcur : (runAt L n).next ≤ 15 := by rw [runAt_next]; exact h15 n hn
458  have hfit : ∀ k < 19, 0 < runFreq (runStep L n (runAt L n)).2 k → CodeFits (blWords d0) k := by
459    intro k hk hused
460    have hb := st_runFreq_le L n (M + 1) k (by omega)
461    exact hcodes k hk (by omega)
462  have hprefix : (treeBitsUpTo (blWords d0) L n).length +
463      (runBits (blWords d0) (runStep L n (runAt L n)).2).length ≤ (sendTreeBits (blWords d0) L M).length := by
464    have hm := treeBitsUpTo_mono (blWords d0) L (i := n + 1) (j := M + 1) (by omega)
465    simpa only [sendTreeBits, treeBitsUpTo, List.length_append] using hm
466  refine EWP.bind (stBody_run ht tk L n (runAt L n) r _ hcorr (runInv_runAt L h16 n) (by omega)
467    (by omega) (hread (n + 1) (by omega)) hcur hfit hprefix hr) ?_
468  rintro ⟨ni, rest⟩ H ⟨hc, D, B, htrace⟩
469  have hni := hc.1
470  dsimp only at hni ⊢
471  have hone : (1 : Int32).toInt = 1 := rfl
472  rw [st_iadd ni 1 (by omega) (by omega), M_pure_bind]
473  refine EWP.pure ⟨?_, D, B, ?_⟩
474  · exact ⟨by rw [ofInt_toInt' _ (by omega) (by omega) ]; omega, hc.2⟩
475  · simpa only [treeBitsUpTo] using htrace
476
477/-- The complete actual for loop terminates and emits its whole model
478prefix. The source arrays and code words are retained at every iteration. -/
479theorem stLoop_run {h0 h : Heap} {id b : Nat} {d0 d : DeflateState} {buf0 buf : Array UInt8}
480    (tk : TK) (L : Nat → Nat) (M : Nat) (mc : Int32) (r : SCLocals)
481    (ht : EmitState id b h0 d0 buf0 [] h d buf)
482    (hmc : mc.toInt = M) (hM : M ≤ 285) (hT : M + 1 < (tk.arr d0).size)
483    (hread : ∀ i ≤ M + 1, (tk.arr d0)[i]!.dl.toNat = L i)
484    (h16 : ∀ i, L i < 65536) (h15 : ∀ i ≤ M, L i ≤ 15)
485    (hcodes : ∀ k < 19, 0 < scanFreqUpTo L (M + 1) k → CodeFits (blWords d0) k)
486    (hr : 8 * d0.pending.toNat + d0.bi_valid.toInt.toNat + (sendTreeBits (blWords d0) L M).length ≤ 8 * buf0.size)
487    (hcorr : SCCorr r 0 (runAt L 0)) :
488    EWP (stLoop (some (.tab id)) (.ref (tk.ref id) 0) mc r) h (fun _ H => ∃ D B,
489      EmitState id b h0 d0 buf0 (sendTreeBits (blWords d0) L M) H D B) := by
490  let cond := fun r : SCLocals => do
491    pure (← (pure (decide (r.1.toInt ≤ mc.toInt)) : _root_.C.M Bool), r)
492  let body := fun r : SCLocals => do
493    let (ni, rest) ← stBody (some (.tab id)) (.ref (tk.ref id) 0) r
494    pure (← iadd ni 1, rest)
495  let P := fun k r H => k ≤ M + 1 ∧ SCCorr r (M + 1 - k) (runAt L (M + 1 - k)) ∧ ∃ D B,
496    EmitState id b h0 d0 buf0 (treeBitsUpTo (blWords d0) L (M + 1 - k)) H D B
497  let Q := fun (_ : SCLocals) H => ∃ D B, EmitState id b h0 d0 buf0 (sendTreeBits (blWords d0) L M) H D B
498  have step : ∀ k r H, P (k + 1) r H → ∃ r1 H1 r2 H2,
499      cond r H = .ok ((true, r1), H1) ∧ body r1 H1 = .ok (r2, H2) ∧ P k r2 H2 := by
500    rintro k rr H ⟨hk, hc, D, B, htrace⟩
501    have hle : rr.1.toInt ≤ mc.toInt := by rw [hc.1, hmc]; omega
502    obtain ⟨r2, H2, hbody, hcorr2, D2, B2, htrace2⟩ :=
503      stIteration_run tk L (M + 1 - (k + 1)) M rr htrace (by omega) hM hT hread h16 h15 hcodes hr hc
504    refine ⟨rr, H, r2, H2, ?_, hbody, by omega, ?_, D2, B2, ?_⟩
505    · simp only [cond, bind_app, pure_app, hle, decide_true]
506    · have he : M + 1 - k = M + 1 - (k + 1) + 1 := by omega
507      rw [he]
508      exact hcorr2
509    · have he : M + 1 - k = M + 1 - (k + 1) + 1 := by omega
510      rw [he]
511      exact htrace2
512  have stop : ∀ r H, P 0 r H → ∃ r1 H1, cond r H = .ok ((false, r1), H1) ∧ Q r1 H1 := by
513    rintro rr H ⟨hk, hc, D, B, htrace⟩
514    have hno : ¬ rr.1.toInt ≤ mc.toInt := by rw [hc.1, hmc]; omega
515    refine ⟨rr, H, ?_, D, B, ?_⟩
516    · simp only [cond, bind_app, pure_app, hno, decide_false]
517    · simpa only [Nat.sub_zero, sendTreeBits] using htrace
518  have hstart : P (M + 1) r h := by
519    refine ⟨Nat.le_refl _, ?_, d, buf, ?_⟩
520    · simpa only [Nat.sub_self] using hcorr
521    · simpa only [Nat.sub_self, treeBitsUpTo] using ht
522  obtain ⟨rf, Hf, hrun, hQ⟩ := _root_.C.cwhile_run P Q step stop hstart (by unfold fuel; omega)
523  exact ⟨rf, Hf, hrun, hQ⟩
524
525/-- `local void send_tree(deflate_state *s, ct_data *tree, int max_code)`.
526The internal alphabet maximum is at most 285. Actual lengths are at most
52715; only entries with positive complete-scan frequency require fitted code
528data. Exact total bit room remains an internal caller obligation. -/
529theorem send_tree_emit {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
530    (hI : TreesInvAt h id d b buf) (tk : TK) (L : Nat → Nat) (M : Nat) (mc : Int32)
531    (hmc : mc.toInt = M) (hM : M ≤ 285) (hT : M + 1 < (tk.arr d).size)
532    (hread : ∀ i ≤ M + 1, (tk.arr d)[i]!.dl.toNat = L i)
533    (h16 : ∀ i, L i < 65536) (h15 : ∀ i ≤ M, L i ≤ 15)
534    (hcodes : ∀ k < 19, 0 < scanFreqUpTo L (M + 1) k → CodeFits (blWords d) k)
535    (hr : 8 * d.pending.toNat + d.bi_valid.toInt.toNat + (sendTreeBits (blWords d) L M).length ≤ 8 * buf.size) :
536    Emit id b (send_tree (some (.tab id)) (.ref (tk.ref id) 0) mc) h d buf
537      (sendTreeBits (blWords d) L M) (d.bi_valid.toInt.toNat + (sendTreeBits (blWords d) L M).length) := by
538  have hget := tk_get (h0 := h) (id := id) (d := d) tk
539  rw [Zlib.Trees.Proofs.setD_self hI.base.dstate] at hget
540  have hread0 := getDl_gen hget (i := 0) (by omega)
541  have hload : getDl (.ref (tk.ref id) 0) 0 h = .ok ((tk.arr d)[0]!.dl, h) := by
542    simpa only [getElem!_pos, show 0 < (tk.arr d).size by omega, Int.natCast_zero] using hread0
543  let nx := u16i (tk.arr d)[0]!.dl
544  have hnx : nx.toInt = L 0 := by rw [u16i_toInt, hread 0 (by omega)]
545  have hz : ((nx == 0) = true) ↔ L 0 = 0 := by
546    rw [beq_iff_eq, ← Int32.toInt_inj, hnx]
547    change (L 0 : Int) = 0 ↔ L 0 = 0
548    omega
549  let mxmn : Int32 × Int32 := if nx == 0 then (138, 3) else (7, 4)
550  have hc : SCCorr (0, -1, nx, 0, mxmn.1, mxmn.2, 0) 0 (runAt L 0) := by
551    dsimp only [mxmn]
552    simp only [hz, runAt, runInit]
553    by_cases h0 : L 0 = 0
554    · simp only [ite_eq_left h0]
555      exact ⟨rfl, rfl, hnx, rfl, rfl, rfl⟩
556    · simp only [ite_eq_right h0]
557      exact ⟨rfl, rfl, hnx, rfl, rfl, rfl⟩
558  obtain ⟨rf, H, hloop, D, B, ht⟩ := stLoop_run tk L M mc (0, -1, nx, 0, mxmn.1, mxmn.2, 0)
559    (EmitState.start hI) hmc hM hT hread h16 h15 hcodes hr hc
560  apply ht.emit
561  rw [send_tree_eq, bind_app, hload]
562  change (stLoop (some (.tab id)) (.ref (tk.ref id) 0) mc
563    (0, -1, nx, 0, mxmn.1, mxmn.2, 0) >>= fun _ => pure ()) h = .ok ((), H)
564  rw [bind_app, hloop]
565  rfl
566
567end Zlib.Trees.Proofs