trees.c.scan-tree.lean

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

1import ZlibF.Proof.«trees.c.build.frame»
2import ZlibF.Proof.«trees.c.runs»
3
4/-! # trees.c: actual code-length scanning
5
6The run model and the frequency-by-iteration argument follow the reference
7EmitScanTree proof. Executions use this translation's arrays and source order.
8-/
9
10namespace Zlib.Trees.Proofs
11open C Zlib.Trees
12
13abbrev SCLocals := Int32 × Int32 × Int32 × Int32 × Int32 × Int32 × Int32
14
15/-- The frequency-writing branch of the actual scan body. -/
16def scCounts (s : DeflateStatePtr) (curlen prevlen count min_count : Int32) : M Unit := do
17  let blt ← pBltree s
18  if count.toInt < min_count.toInt then
19    setFc blt curlen.toInt ((← getFc blt curlen.toInt) + i2us count)
20  else if curlen != 0 then
21    if curlen != prevlen then setFc blt curlen.toInt ((← getFc blt curlen.toInt) + 1)
22    setFc blt REP_3_6.toInt ((← getFc blt REP_3_6.toInt) + 1)
23  else if count.toInt ≤ 10 then
24    setFc blt REPZ_3_10.toInt ((← getFc blt REPZ_3_10.toInt) + 1)
25  else
26    setFc blt REPZ_11_138.toInt ((← getFc blt REPZ_11_138.toInt) + 1)
27
28/-- The local-variable tail of the actual scan. -/
29def scTail (n curlen nextlen : Int32) : SCLocals :=
30  let (mx, mn) : Int32 × Int32 :=
31    if nextlen == 0 then (138, 3) else if curlen == nextlen then (6, 3) else (7, 4)
32  (n, curlen, nextlen, 0, mx, mn, 0)
33
34/-- The actual loop body, retaining its early continue. -/
35def scBody (s : DeflateStatePtr) (tree : CtDataPtr) : SCLocals → M SCLocals :=
36  fun (n, prevlen, nextlen, count, max_count, min_count, _) => do
37    let curlen := nextlen
38    let nextlen := u16i (← getDl tree (← iadd n 1).toInt)
39    let count ← iadd count 1
40    if count.toInt < max_count.toInt ∧ curlen == nextlen then
41      return (n, prevlen, nextlen, count, max_count, min_count, 0)
42    scCounts s curlen prevlen count min_count
43    return scTail n curlen nextlen
44
45def scLoop (s : DeflateStatePtr) (tree : CtDataPtr) (mc : Int32) (r : SCLocals) : M SCLocals :=
46  cfor (fun (n, _) => pure (decide (n.toInt ≤ mc.toInt)))
47    (fun (n, rest) => do pure (← iadd n 1, rest)) (scBody s tree) r
48
49/-- Naming fragments does not change the actual function. -/
50theorem scan_tree_eq (s : DeflateStatePtr) (tree : CtDataPtr) (mc : Int32) :
51    scan_tree s tree mc = (do
52      let nextlen0 := u16i (← getDl tree 0)
53      let (mx0, mn0) : Int32 × Int32 := if nextlen0 == 0 then (138, 3) else (7, 4)
54      setDl tree (← iadd mc 1).toInt 0xffff
55      let _ ← scLoop s tree mc (0, -1, nextlen0, 0, mx0, mn0, 0)
56      pure ()) := by
57  unfold scan_tree scLoop scBody scCounts scTail
58  simp only [M_bind_assoc, merge_ite_bind]
59
60/-- Array effects of a finished run. This data model leaves 16-bit frequency
61addition wrapping, exactly as the actual stores do. -/
62def scFreqUpdate (B : Array CtData) (cur : Nat) (prev : Int) (cnt mn : Nat) : Array CtData :=
63  if cnt < mn then Out.addFc B cur (UInt16.ofNat cnt)
64  else if cur ≠ 0 then
65    Out.addFc (if (cur : Int) ≠ prev then Out.addFc B cur 1 else B) 16 1
66  else if cnt ≤ 10 then Out.addFc B 17 1
67  else Out.addFc B 18 1
68
69theorem scFreqUpdate_size (B : Array CtData) (cur : Nat) (prev : Int) (cnt mn : Nat) :
70    (scFreqUpdate B cur prev cnt mn).size = B.size := by
71  unfold scFreqUpdate
72  split
73  · simp
74  · split
75    · split <;> simp
76    · split <;> simp
77
78theorem scFreqUpdate_dl (B : Array CtData) (cur : Nat) (prev : Int) (cnt mn k : Nat) :
79    (scFreqUpdate B cur prev cnt mn)[k]!.dl = B[k]!.dl := by
80  unfold scFreqUpdate
81  split
82  · exact Out.addFc_dl _ _ _ _
83  · split
84    · rw [Out.addFc_dl]; split <;> simp [Out.addFc_dl]
85    · split <;> exact Out.addFc_dl _ _ _ _
86
87theorem scFreqUpdate_fc (B : Array CtData) (cur : Nat) (prev : Int) (cnt mn k : Nat)
88    (hcur : cur ≤ 15) (hB : 19 ≤ B.size) :
89    (scFreqUpdate B cur prev cnt mn)[k]!.fc =
90      B[k]!.fc + UInt16.ofNat (Out.runFreq (some (cur, prev, cnt, mn)) k) := by
91  by_cases hs : cnt < mn
92  · simp only [scFreqUpdate, Out.runFreq, ite_eq_left hs]
93    rw [Out.addFc_fc _ _ _ (by omega)]
94    split <;> simp_all
95  · by_cases hz : cur ≠ 0
96    · simp only [scFreqUpdate, Out.runFreq, ite_eq_right hs, ite_eq_left hz]
97      by_cases hp : (cur : Int) ≠ prev
98      · rw [ite_eq_left hp, Out.addFc_fc _ _ _ (by simp; omega), Out.addFc_fc _ _ _ (by omega)]
99        by_cases hk : k = cur <;> by_cases hk16 : k = 16 <;>
100          simp_all [UInt16.add_assoc]
101      · rw [ite_eq_right hp, Out.addFc_fc _ _ _ (by omega)]
102        by_cases hk16 : k = 16 <;> simp_all
103    · simp only [scFreqUpdate, Out.runFreq, ite_eq_right hs, ite_eq_right hz]
104      by_cases hc : cnt ≤ 10
105      · rw [ite_eq_left hc, Out.addFc_fc _ _ _ (by omega)]
106        split <;> simp_all
107      · rw [ite_eq_right hc, Out.addFc_fc _ _ _ (by omega)]
108        split <;> simp_all
109
110/-- A single actual frequency read/add/store has its exact array effect. -/
111theorem ws_scAdd {h0 : Heap} {id : Nat} {d : DeflateState} (i : Int) (v : UInt16)
112    (hi0 : 0 ≤ i) (hiB : i < d.bl_tree.size) :
113    WS h0 id (do
114      setFc (.ref (.dstate_bl_tree id) 0) i ((← getFc (.ref (.dstate_bl_tree id) 0) i) + v)) d
115      (fun _ e => e = { d with bl_tree := Out.addFc d.bl_tree i.toNat v }) := by
116  refine WS.bind' (ws_getFc .bl i hi0 hiB) fun f e ⟨hf, he⟩ => ?_
117  subst e; subst f
118  refine WS.mono (ws_setFc .bl i _ hi0 hiB) ?_
119  intro _ e he
120  exact he
121
122/-- All finished-run frequency branches execute with exact array effects.
123Only bounds on real scalar values and array storage are assumed. -/
124theorem ws_scCounts {h0 : Heap} {id : Nat} {d : DeflateState}
125    (cur prev count minc : Int32) (c cnt mn : Nat) (p : Int)
126    (hc : cur.toInt = c) (hp : prev.toInt = p) (hcnt : count.toInt = cnt) (hmn : minc.toInt = mn)
127    (hc15 : c ≤ 15) (hcnt16 : cnt < 65536) (hB : 19 ≤ d.bl_tree.size) :
128    WS h0 id (scCounts (Sp id) cur prev count minc) d
129      (fun _ e => e = { d with bl_tree := scFreqUpdate d.bl_tree c p cnt mn }) := by
130  have hcur0 : ((cur != 0) = true) ↔ c ≠ 0 := by
131    simp only [bne_iff_ne, ne_eq, ← Int32.toInt_inj, hc]
132    change ¬ (c : Int) = 0 ↔ c ≠ 0
133    omega
134  have hcurprev : ((cur != prev) = true) ↔ (c : Int) ≠ p := by
135    simp only [bne_iff_ne, ne_eq, ← Int32.toInt_inj, hc, hp]
136  have hcast : i2us count = UInt16.ofNat cnt := by
137    apply UInt16.toNat_inj.mp
138    simp only [i2us, hcnt, UInt16.toNat_ofNat']
139    omega
140  have hsmall : count.toInt < minc.toInt ↔ cnt < mn := by omega
141  have hten : count.toInt ≤ 10 ↔ cnt ≤ 10 := by omega
142  unfold scCounts pBltree
143  simp only [M_bind_assoc, M_pure_bind]
144  refine WS.bind' ws_sid fun i e ⟨hi, he⟩ => ?_
145  subst i; subst e
146  simp only [hsmall, hten, hc, hcur0, hcurprev, hcast]
147  unfold scFreqUpdate
148  split
149  · rename_i hs
150    refine WS.mono (ws_scAdd (c : Int) (UInt16.ofNat cnt) (by omega) (by omega)) ?_
151    intro _ e he; simpa [hs] using he
152  · rename_i hs
153    split
154    · rename_i hz
155      split
156      · rename_i hp
157        refine WS.bind' (ws_getFc .bl (c : Int) (by omega) (by change (c : Int) < d.bl_tree.size; omega))
158          fun f e ⟨hf, he⟩ => ?_
159        subst e; subst f
160        refine WS.bind' (ws_setFc .bl (c : Int) _ (by omega) (by change (c : Int) < d.bl_tree.size; omega))
161          fun _ e he => ?_
162        subst e
163        refine WS.mono (ws_scAdd REP_3_6.toInt 1 (by decide +kernel)
164          (by change (16 : Int) < (Out.addFc d.bl_tree c 1).size; simp; omega)) ?_
165        intro _ e he; simpa [hs, hz, hp, REP_3_6, Out.addFc, TK.setArr, TK.arr] using he
166      · rename_i hp
167        refine WS.mono (ws_scAdd REP_3_6.toInt 1 (by decide +kernel) (by change (16 : Int) < d.bl_tree.size; omega)) ?_
168        intro _ e he; simpa [hs, hz, hp, REP_3_6, Out.addFc, TK.setArr, TK.arr] using he
169    · rename_i hz
170      split
171      · rename_i ht
172        refine WS.mono (ws_scAdd REPZ_3_10.toInt 1 (by decide +kernel) (by change (17 : Int) < d.bl_tree.size; omega)) ?_
173        intro _ e he; simpa [hs, hz, ht, REPZ_3_10, REPZ_11_138] using he
174      · rename_i ht
175        refine WS.mono (ws_scAdd REPZ_11_138.toInt 1 (by decide +kernel) (by change (18 : Int) < d.bl_tree.size; omega)) ?_
176        intro _ e he; simpa [hs, hz, ht, REPZ_3_10, REPZ_11_138] using he
177
178/-- Correspondence between the actual seven scalar locals and the pure run
179state. The final unused scalar has no semantic constraint. -/
180def SCCorr (r : SCLocals) (n : Nat) (s : Out.RunSt) : Prop :=
181  r.1.toInt = n ∧ r.2.1.toInt = s.prev ∧ r.2.2.1.toInt = s.next ∧
182  r.2.2.2.1.toInt = s.cnt ∧ r.2.2.2.2.1.toInt = s.mx ∧ r.2.2.2.2.2.1.toInt = s.mn
183
184/-- A pure run changes the frequency array only when it finishes a group. -/
185def scStepTree (B : Array CtData) (L : Nat → Nat) (n : Nat) (s : Out.RunSt) : Array CtData :=
186  if s.cnt + 1 < s.mx ∧ s.next = L (n + 1) then B
187  else scFreqUpdate B s.next s.prev (s.cnt + 1) s.mn
188
189theorem scStepTree_size (B : Array CtData) (L : Nat → Nat) (n : Nat) (s : Out.RunSt) :
190    (scStepTree B L n s).size = B.size := by
191  unfold scStepTree
192  split
193  · rfl
194  · exact scFreqUpdate_size _ _ _ _ _
195
196theorem scStepTree_dl (B : Array CtData) (L : Nat → Nat) (n k : Nat) (s : Out.RunSt) :
197    (scStepTree B L n s)[k]!.dl = B[k]!.dl := by
198  unfold scStepTree
199  split
200  · rfl
201  · exact scFreqUpdate_dl _ _ _ _ _ _
202
203theorem scStepTree_fc (B : Array CtData) (L : Nat → Nat) (n k : Nat) (s : Out.RunSt)
204    (hcur : s.next ≤ 15) (hB : 19 ≤ B.size) :
205    (scStepTree B L n s)[k]!.fc = B[k]!.fc + UInt16.ofNat (Out.runFreq (Out.runStep L n s).2 k) := by
206  unfold scStepTree Out.runStep
207  by_cases ha : s.cnt + 1 < s.mx ∧ s.next = L (n + 1)
208  · simp only [ite_eq_left ha, Out.runFreq, show UInt16.ofNat 0 = 0 from rfl, UInt16.add_zero]
209  · simp only [ite_eq_right ha]
210    exact scFreqUpdate_fc _ _ _ _ _ _ hcur hB
211
212/-- Scalar tail assignment agrees with the model's finished-run state. -/
213theorem scTail_corr (n cur nx : Int32) (N C X : Nat)
214    (hn : n.toInt = N) (hc : cur.toInt = C) (hx : nx.toInt = X) :
215    SCCorr (scTail n cur nx) N
216      (if X = 0 then ⟨C, X, 0, 138, 3⟩ else if C = X then ⟨C, X, 0, 6, 3⟩ else ⟨C, X, 0, 7, 4⟩) := by
217  have hz : ((nx == 0) = true) ↔ X = 0 := by
218    simp only [beq_iff_eq, ← Int32.toInt_inj, hx]
219    change (X : Int) = 0 ↔ X = 0
220    omega
221  have he : ((cur == nx) = true) ↔ C = X := by
222    simp only [beq_iff_eq, ← Int32.toInt_inj, hc, hx, Int.natCast_inj]
223  simp only [scTail, hz, he]
224  split
225  · exact ⟨hn, hc, hx, rfl, rfl, rfl⟩
226  · split <;> exact ⟨hn, hc, hx, rfl, rfl, rfl⟩
227
228/-- One actual scan body agrees with runStep, including the early continue
229and every frequency branch. No loop or callee behavior is assumed. -/
230theorem ws_scBody {h0 : Heap} {id : Nat} {d : DeflateState}
231    (tk : TK) (L : Nat → Nat) (n : Nat) (s : Out.RunSt) (r : SCLocals)
232    (hcorr : SCCorr r n s) (hi : Out.RunInv s) (hn : n ≤ 285)
233    (hread : n + 1 < (tk.arr d).size)
234    (hl : (tk.arr d)[n + 1]!.dl.toNat = L (n + 1))
235    (hcur : s.next ≤ 15) (hB : 19 ≤ d.bl_tree.size) :
236    WS h0 id (scBody (Sp id) (.ref (tk.ref id) 0) r) d (fun r' e =>
237      SCCorr r' n (Out.runStep L n s).1 ∧
238      e = { d with bl_tree := scStepTree d.bl_tree L n s }) := by
239  rcases r with ⟨ni, pi, ci, ki, mi, mni, unused⟩
240  obtain ⟨hnc, hpc, hcc, hkc, hmc, hmnc⟩ := hcorr
241  dsimp only at hnc hpc hcc hkc hmc hmnc
242  have hmx : s.mx ≤ 138 := by
243    by_cases hz : s.next = 0
244    · exact (hi.2.1 hz).1 ▸ Nat.le_refl _
245    · rcases hi.2.2.1 hz with ⟨h, rest⟩ | ⟨h, rest⟩ <;> omega
246  have hc0 : 0 ≤ s.cnt := Nat.zero_le _
247  have hcnt := hi.1
248  have hone : (1 : Int32).toInt = 1 := rfl
249  unfold scBody
250  refine WS.bind' (ws_iadd ni 1 (by omega) (by omega)) fun ni1 e ⟨hn1, he⟩ => ?_
251  subst e
252  have hn1N : ni1.toInt.toNat = n + 1 := by omega
253  refine WS.bind' (ws_getDl tk ni1.toInt (by omega) (by omega)) fun len e ⟨hlen, he⟩ => ?_
254  subst e; subst len
255  have hnx : (u16i (tk.arr d)[ni1.toInt.toNat]!.dl).toInt = L (n + 1) := by
256    rw [Out.u16i_toInt, hn1N, hl]
257  refine WS.bind' (ws_iadd ki 1 (by omega) (by omega)) fun ki1 e ⟨hk1, he⟩ => ?_
258  subst e
259  have hk1N : ki1.toInt = (s.cnt + 1 : Nat) := by omega
260  have hsame : ((ci == u16i (tk.arr d)[ni1.toInt.toNat]!.dl) = true) ↔ s.next = L (n + 1) := by
261    simp only [beq_iff_eq, ← Int32.toInt_inj, hcc, hnx, Int.natCast_inj]
262  have hcond : (ki1.toInt < mi.toInt ∧ (ci == u16i (tk.arr d)[ni1.toInt.toNat]!.dl) = true) ↔
263      s.cnt + 1 < s.mx ∧ s.next = L (n + 1) := by
264    rw [hsame, hk1N, hmc]
265    omega
266  simp only [hcond]
267  by_cases ha : s.cnt + 1 < s.mx ∧ s.next = L (n + 1)
268  · simp only [ha]
269    refine WS.pure' ⟨?_, ?_⟩
270    · simp only [Out.runStep, ite_eq_left ha, SCCorr]
271      exact ⟨hnc, hpc, hnx, hk1N, hmc, hmnc⟩
272    · unfold scStepTree
273      rw [ite_eq_left ha]
274  · simp only [ha, ite_false]
275    refine WS.bind' (ws_scCounts ci pi ki1 mni s.next (s.cnt + 1) s.mn s.prev
276      hcc hpc hk1N hmnc hcur (by omega) hB) fun _ e he => ?_
277    refine WS.pure' ⟨?_, ?_⟩
278    · simp only [Out.runStep, ite_eq_right ha]
279      exact scTail_corr _ _ _ _ _ _ hnc hcc hnx
280    · simpa only [scStepTree, ite_eq_right ha] using he
281
282/-- Frequency state after exactly n iterations. Every length and all record
283fields except the bit-length tree are retained. -/
284def SCFreqState (d : DeflateState) (L : Nat → Nat) (n : Nat) (e : DeflateState) : Prop :=
285  ∃ B : Array CtData, e = { d with bl_tree := B } ∧ B.size = d.bl_tree.size ∧
286    (∀ k : Nat, B[k]!.dl = d.bl_tree[k]!.dl) ∧
287    ∀ k : Nat, B[k]!.fc = d.bl_tree[k]!.fc + UInt16.ofNat (Out.scanFreqUpTo L n k)
288
289theorem scFreqState_init (d : DeflateState) (L : Nat → Nat) : SCFreqState d L 0 d := by
290  refine ⟨d.bl_tree, rfl, rfl, fun _ => rfl, ?_⟩
291  intro k
292  change d.bl_tree[k]!.fc = d.bl_tree[k]!.fc + 0
293  exact (UInt16.add_zero _).symm
294
295theorem tk_arr_bl (tk : TK) (d : DeflateState) (B : Array CtData) (hne : tk ≠ .bl) :
296    tk.arr { d with bl_tree := B } = tk.arr d := by
297  cases tk
298  · rfl
299  · rfl
300  · exact False.elim (hne rfl)
301
302/-- Actual n++ after a body with unchanged loop index. -/
303theorem ws_scIncrement {h0 : Heap} {id : Nat} {d : DeflateState}
304    (r : SCLocals) (n : Nat) (s : Out.RunSt) (hc : SCCorr r n s) (hn : n ≤ 285) :
305    WS h0 id (do let (ni, rest) := r; pure (← iadd ni 1, rest)) d
306      (fun r' e => SCCorr r' (n + 1) s ∧ e = d) := by
307  rcases r with ⟨ni, rest⟩
308  obtain ⟨hni, hrest⟩ := hc
309  dsimp only at hni hrest
310  have hone : (1 : Int32).toInt = 1 := rfl
311  refine WS.bind' (ws_iadd ni 1 (by omega) (by omega)) fun ni1 e ⟨hni1, he⟩ => ?_
312  subst e
313  exact WS.pure' ⟨⟨by dsimp only; omega, hrest⟩, rfl⟩
314
315/-- One whole actual iteration, including n++, preserves the exact frequency
316history. The next length read follows from the unchanged source alphabet. -/
317theorem ws_scIteration {h0 : Heap} {id : Nat} {base e : DeflateState}
318    (tk : TK) (hne : tk ≠ .bl) (L : Nat → Nat) (n mc : Nat) (r : SCLocals)
319    (hn : n ≤ mc) (hmc : mc ≤ 285) (hT : mc + 1 < (tk.arr base).size)
320    (hB : 19 ≤ base.bl_tree.size)
321    (hread : ∀ i ≤ mc + 1, (tk.arr base)[i]!.dl.toNat = L i)
322    (h16 : ∀ i, L i < 65536) (h15 : ∀ i ≤ mc, L i ≤ 15)
323    (hcorr : SCCorr r n (Out.runAt L n)) (hfreq : SCFreqState base L n e) :
324    WS h0 id (do
325      let (ni, rest) ← scBody (Sp id) (.ref (tk.ref id) 0) r
326      pure (← iadd ni 1, rest)) e
327      (fun r' e' => SCCorr r' (n + 1) (Out.runAt L (n + 1)) ∧ SCFreqState base L (n + 1) e') := by
328  obtain ⟨B, rfl, hBs, hdl, hfc⟩ := hfreq
329  have hcur : (Out.runAt L n).next ≤ 15 := by rw [Out.runAt_next]; exact h15 n hn
330  have hB' : 19 ≤ B.size := by omega
331  refine WS.bind' (ws_scBody tk L n (Out.runAt L n) r hcorr (Out.runInv_runAt L h16 n)
332    (by omega) (by rw [tk_arr_bl tk base B hne]; omega)
333    (by rw [tk_arr_bl tk base B hne]; exact hread (n + 1) (by omega)) hcur hB')
334    fun r' e' ⟨hcorr', he'⟩ => ?_
335  subst e'
336  refine WS.mono (ws_scIncrement r' n (Out.runStep L n (Out.runAt L n)).1 hcorr' (by omega)) ?_
337  intro r'' e'' ⟨hcorr'', he''⟩
338  subst e''
339  refine ⟨hcorr'', scStepTree B L n (Out.runAt L n), rfl, ?_, ?_, ?_⟩
340  · exact (scStepTree_size _ _ _ _).trans hBs
341  · intro k
342    exact (scStepTree_dl _ _ _ _ _).trans (hdl k)
343  · intro k
344    rw [scStepTree_fc B L n k _ hcur hB', hfc k]
345    simp only [Out.scanFreqUpTo, UInt16.ofNat_add, UInt16.add_assoc]
346
347/-- Complete actual loop: every iteration and its increment execute, the
348measure decreases, and the accumulated frequencies equal the run model. -/
349theorem ws_scLoop {h0 : Heap} {id : Nat} {d : DeflateState}
350    (tk : TK) (hne : tk ≠ .bl) (L : Nat → Nat) (mc : Int32) (M : Nat) (r : SCLocals)
351    (hmc : mc.toInt = M) (hM : M ≤ 285) (hT : M + 1 < (tk.arr d).size)
352    (hB : 19 ≤ d.bl_tree.size)
353    (hread : ∀ i ≤ M + 1, (tk.arr d)[i]!.dl.toNat = L i)
354    (h16 : ∀ i, L i < 65536) (h15 : ∀ i ≤ M, L i ≤ 15)
355    (hstart : SCCorr r 0 (Out.runAt L 0)) :
356    WS h0 id (scLoop (Sp id) (.ref (tk.ref id) 0) mc r) d
357      (fun r' e => SCCorr r' (M + 1) (Out.runAt L (M + 1)) ∧ SCFreqState d L (M + 1) e) := by
358  let Inv : SCLocals → DeflateState → Prop := fun r' e =>
359    ∃ n : Nat, n ≤ M + 1 ∧ SCCorr r' n (Out.runAt L n) ∧ SCFreqState d L n e
360  unfold scLoop
361  refine WS.cfor2 Inv (fun r' _ => M + 1 - r'.1.toInt.toNat) _ ?_
362    ⟨0, by omega, hstart, scFreqState_init d L⟩ (by simp only [fuel]; omega)
363  intro r' e hi
364  obtain ⟨n, hn, hcorr, hfreq⟩ := hi
365  have hni := hcorr.1
366  refine WS.pure' ?_
367  by_cases hlt : n ≤ M
368  · refine Or.inr ⟨by simp only [decide_eq_true_eq]; omega, ?_⟩
369    refine WS.mono (ws_scIteration tk hne L n M r' hlt hM hT hB hread h16 h15 hcorr hfreq) ?_
370    intro r'' e' ⟨hc, hf⟩
371    exact ⟨⟨n + 1, by omega, hc, hf⟩, by have := hc.1; omega⟩
372  · refine Or.inl ⟨by simp only [decide_eq_false_iff_not]; omega, ?_⟩
373    have hnM : n = M + 1 := by omega
374    exact ⟨by simpa only [hnM] using hcorr, by simpa only [hnM] using hfreq⟩
375
376theorem bl_tree_setArr (tk : TK) (d : DeflateState) (T : Array CtData) (hne : tk ≠ .bl) :
377    (tk.setArr d T).bl_tree = d.bl_tree := by
378  cases tk
379  · rfl
380  · rfl
381  · exact False.elim (hne rfl)
382
383/-- The actual sentinel array, with its full entry retained except for Len. -/
384def scGuard (T : Array CtData) (M : Nat) : Array CtData :=
385  T.set! (M + 1) { T[M + 1]! with dl := 0xffff }
386
387theorem scGuard_lengths (T : Array CtData) (M : Nat) (hT : M + 1 < T.size) (i : Nat) :
388    (scGuard T M)[i]!.dl.toNat = Out.guarded (fun n => T[n]!.dl.toNat) M i := by
389  unfold scGuard Out.guarded
390  rw [getD_set T (M + 1) i _ hT]
391  split <;> rfl
392
393/-- `local void scan_tree(deflate_state *s, ct_data *tree, int max_code)`.
394For an internal literal or distance alphabet, the actual complete function
395terminates, writes the sentinel and adds exactly the modeled run frequencies.
396The explicit internal bounds are obtained from actual tree construction in
397the composition theorem. No public API domain restriction is proposed. -/
398theorem ws_scan_tree {h0 : Heap} {id : Nat} {d : DeflateState}
399    (tk : TK) (hne : tk ≠ .bl) (mc : Int32) (hmc0 : 0 ≤ mc.toInt) (hmc285 : mc.toInt ≤ 285)
400    (hT : mc.toInt.toNat + 1 < (tk.arr d).size) (hB : 19 ≤ d.bl_tree.size)
401    (h15 : ∀ i ≤ mc.toInt.toNat, (tk.arr d)[i]!.dl.toNat ≤ 15) :
402    WS h0 id (scan_tree (Sp id) (.ref (tk.ref id) 0) mc) d (fun _ e =>
403      ∃ B : Array CtData,
404        e = { tk.setArr d (scGuard (tk.arr d) mc.toInt.toNat) with bl_tree := B } ∧
405        B.size = d.bl_tree.size ∧ (∀ k : Nat, B[k]!.dl = d.bl_tree[k]!.dl) ∧
406        ∀ k : Nat, B[k]!.fc = d.bl_tree[k]!.fc + UInt16.ofNat
407          (Out.scanFreqUpTo (Out.guarded (fun i => (tk.arr d)[i]!.dl.toNat) mc.toInt.toNat)
408            (mc.toInt.toNat + 1) k)) := by
409  let M := mc.toInt.toNat
410  let L := Out.guarded (fun i => (tk.arr d)[i]!.dl.toNat) M
411  have hm : mc.toInt = M := by dsimp [M]; omega
412  have hone : (1 : Int32).toInt = 1 := rfl
413  rw [scan_tree_eq]
414  refine WS.bind' (ws_getDl tk 0 (by decide +kernel) (by omega)) fun len e ⟨hlen, he⟩ => ?_
415  subst e; subst len
416  refine WS.bind' (ws_iadd mc 1 (by omega) (by omega)) fun mc1 e ⟨hmc1, he⟩ => ?_
417  subst e
418  have hmc1N : mc1.toInt.toNat = M + 1 := by omega
419  refine WS.bind' (ws_setDl tk mc1.toInt 0xffff (by omega) (by omega)) fun _ e he => ?_
420  subst e
421  rw [hmc1N]
422  let base := tk.setArr d (scGuard (tk.arr d) M)
423  have hbaseB : base.bl_tree = d.bl_tree := bl_tree_setArr tk d _ hne
424  have hbaseT : tk.arr base = scGuard (tk.arr d) M := tk_arr_setArr tk _
425  have hread : ∀ i ≤ M + 1, (tk.arr base)[i]!.dl.toNat = L i := by
426    intro i hi
427    rw [hbaseT]
428    exact scGuard_lengths _ M hT i
429  have h16 : ∀ i, L i < 65536 := by
430    intro i
431    unfold L Out.guarded
432    split
433    · decide +kernel
434    · exact UInt16.toNat_lt _
435  have h15' : ∀ i ≤ M, L i ≤ 15 := by
436    intro i hi
437    simp only [L, Out.guarded, ite_eq_right (show i ≠ M + 1 by omega)]
438    exact h15 i hi
439  have hl0 : (u16i (tk.arr d)[Int.toNat 0]!.dl).toInt = L 0 := by
440    rw [Out.u16i_toInt]
441    simp only [L, Out.guarded, ite_eq_right (show 0 ≠ M + 1 by omega)]
442    rfl
443  have hz : ((u16i (tk.arr d)[Int.toNat 0]!.dl == 0) = true) ↔ L 0 = 0 := by
444    simp only [beq_iff_eq, ← Int32.toInt_inj, hl0]
445    change (L 0 : Int) = 0 ↔ L 0 = 0
446    omega
447  have hstart : SCCorr
448      (0, -1, u16i (tk.arr d)[Int.toNat 0]!.dl, 0,
449        (if u16i (tk.arr d)[Int.toNat 0]!.dl == 0 then ((138, 3) : Int32 × Int32) else (7, 4)).1,
450        (if u16i (tk.arr d)[Int.toNat 0]!.dl == 0 then ((138, 3) : Int32 × Int32) else (7, 4)).2, 0)
451      0 (Out.runAt L 0) := by
452    simp only [Out.runAt, Out.runInit, hz]
453    split <;> exact ⟨rfl, rfl, hl0, rfl, rfl, rfl⟩
454  refine WS.bind' (ws_scLoop (d := base) tk hne L mc M _ hm (by omega)
455    (by rw [hbaseT]; simp only [scGuard, Array.size_set!]; exact hT)
456    (by rw [hbaseB]; exact hB) hread h16 h15' hstart) fun r e ⟨hc, hf⟩ => ?_
457  obtain ⟨B, he, hBs, hdl, hfc⟩ := hf
458  exact WS.pure' ⟨B, he, by rw [← hbaseB]; exact hBs,
459    by rw [← hbaseB]; exact hdl, by rw [← hbaseB]; exact hfc⟩
460
461/-- Actual scanning on the live caller heap preserves its output invariant
462and pending bits. The descriptor-alphabet bound supplies sentinel capacity. -/
463theorem scan_tree_preserves {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
464    (hI : Out.TreesInvAt h id d b buf) (tk : TK) (hne : tk ≠ .bl) (mc : Int32)
465    (hmc0 : 0 ≤ mc.toInt) (hmcN : mc.toInt < tk.buildDesc.elems.toInt)
466    (h15 : ∀ i ≤ mc.toInt.toNat, (tk.arr d)[i]!.dl.toNat ≤ 15) :
467    ∃ (e : DeflateState) (B : Array CtData),
468      scan_tree (Sp id) (.ref (tk.ref id) 0) mc h = .ok ((), setD h id e) ∧
469      e = { tk.setArr d (scGuard (tk.arr d) mc.toInt.toNat) with bl_tree := B } ∧
470      Out.TreesInvAt (setD h id e) id e b buf ∧ Out.outBits buf e = Out.outBits buf d ∧
471      B.size = d.bl_tree.size ∧ (∀ k : Nat, B[k]!.dl = d.bl_tree[k]!.dl) ∧
472      ∀ k : Nat, B[k]!.fc = d.bl_tree[k]!.fc + UInt16.ofNat
473        (Out.scanFreqUpTo (Out.guarded (fun i => (tk.arr d)[i]!.dl.toNat) mc.toInt.toNat)
474          (mc.toInt.toNat + 1) k) := by
475  have hwf := hI.base.wf
476  obtain ⟨hLT, hDT, hBT, hBC, hH, hD⟩ := hwf
477  have hmc285 : mc.toInt ≤ 285 := by
478    cases tk
479    · change mc.toInt < 286 at hmcN; omega
480    · change mc.toInt < 30 at hmcN; omega
481    · exact False.elim (hne rfl)
482  have hT : mc.toInt.toNat + 1 < (tk.arr d).size := by
483    cases tk
484    · change mc.toInt.toNat + 1 < d.dyn_ltree.size; omega
485    · change mc.toInt < 30 at hmcN
486      change mc.toInt.toNat + 1 < d.dyn_dtree.size; omega
487    · exact False.elim (hne rfl)
488  obtain ⟨a, e, he, B, heB, hBs, hdl, hfc⟩ := ws_scan_tree (h0 := h) tk hne mc hmc0 hmc285 hT
489    (by omega) h15
490  have ha : a = () := Subsingleton.elim _ _
491  subst a
492  rw [setD_self hI.base.dstate] at he
493  let guard := tk.setArr d (scGuard (tk.arr d) mc.toInt.toNat)
494  have hguard := BTBuildFrame.codes tk tk d (scGuard (tk.arr d) mc.toInt.toNat)
495    (by simp only [scGuard, Array.size_set!])
496  have hguardB : guard.bl_tree = d.bl_tree := bl_tree_setArr tk d _ hne
497  have hBframe := BTBuildFrame.codes .bl .bl guard B
498    (by change B.size = guard.bl_tree.size; rw [hguardB]; exact hBs)
499  have hIe := hBframe.treesInvAt (hguard.treesInvAt hI)
500  have hout := (hBframe.outBits buf).trans (hguard.outBits buf)
501  rw [setD_setD] at hIe
502  have hee : e = TK.bl.setArr guard B := heB
503  refine ⟨e, B, he, heB, ?_, ?_, hBs, hdl, hfc⟩
504  · rw [hee]; exact hIe
505  · rw [hee]; exact hout
506
507/-- Independent accepted lengths supply the real scan's code-length bound. -/
508theorem acceptable_scan_lengths (tk : TK) (d : DeflateState) (M : Nat)
509    (ha : ZlibF.Spec.Acceptable .codeLength
510      (Zlib.Inftrees.Proofs.lensOf (fun i => (tk.arr d)[i]!.dl.toNat) (M + 1))) :
511    ∀ i ≤ M, (tk.arr d)[i]!.dl.toNat ≤ 15 := by
512  intro i hi
513  apply ha.1 _
514  unfold Zlib.Inftrees.Proofs.lensOf
515  exact List.mem_map.mpr ⟨i, List.mem_range.mpr (by omega), rfl⟩
516
517/-- The actual tree constructor supplies every scalar, length and capacity
518premise of actual scan_tree. Both calls run on one heap. This bridges tree
519construction to description-frequency scanning, rather than assuming the
520scan's precondition as a callee contract. -/
521theorem build_tree_scan {h : Heap} {id b : Nat} {d : DeflateState} {buf : Array UInt8}
522    (hI : Out.TreesInvAt h id d b buf) (tk : TK) (hne : tk ≠ .bl) :
523    ∃ (built e : DeflateState) (B : Array CtData),
524      build_tree (Sp id) (some (tk.descRef id)) h = .ok ((), setD h id built) ∧
525      (do build_tree (Sp id) (some (tk.descRef id))
526          scan_tree (Sp id) (.ref (tk.ref id) 0) (tk.getDesc (← rd (Sp id))).max_code) h =
527        .ok ((), setD h id e) ∧
528      scan_tree (Sp id) (.ref (tk.ref id) 0) (tk.getDesc built).max_code (setD h id built) =
529        .ok ((), setD h id e) ∧
530      e = { tk.setArr built (scGuard (tk.arr built) (tk.getDesc built).max_code.toInt.toNat) with bl_tree := B } ∧
531      Out.TreesInvAt (setD h id e) id e b buf ∧ Out.outBits buf e = Out.outBits buf d ∧
532      B.size = built.bl_tree.size ∧
533      ∀ k : Nat, B[k]!.fc = built.bl_tree[k]!.fc + UInt16.ofNat
534        (Out.scanFreqUpTo
535          (Out.guarded (fun i => (tk.arr built)[i]!.dl.toNat) (tk.getDesc built).max_code.toInt.toNat)
536          ((tk.getDesc built).max_code.toInt.toNat + 1) k) := by
537  obtain ⟨a, built, hbuild, hframe, M, hM, hmax, haccept, hdecode⟩ := merge_ws_and
538    (ws_build_tree_frame_initialized (h0 := h) tk hI.base.wf hI.base.static hI.run.to0)
539    (ws_build_tree_decodable_initialized (h0 := h) tk hI.base.wf hI.base.static hI.run.to0)
540  have ha : a = () := Subsingleton.elim _ _
541  subst a
542  rw [setD_self hI.base.dstate] at hbuild
543  have hmc0 : 0 ≤ (tk.getDesc built).max_code.toInt := by omega
544  have hmcN : (tk.getDesc built).max_code.toInt < tk.buildDesc.elems.toInt := by
545    have hN0 : 0 ≤ tk.buildDesc.elems.toInt := by cases tk <;> decide +kernel
546    omega
547  have hlens := acceptable_scan_lengths tk built M (haccept .codeLength)
548  have hlens' : ∀ i ≤ (tk.getDesc built).max_code.toInt.toNat, (tk.arr built)[i]!.dl.toNat ≤ 15 := by
549    intro i hi
550    exact hlens i (by omega)
551  obtain ⟨e, B, hscan, heB, hIe, hout, hBs, hdl, hfc⟩ :=
552    scan_tree_preserves (hframe.treesInvAt hI) tk hne (tk.getDesc built).max_code hmc0 hmcN hlens'
553  rw [setD_setD] at hscan hIe
554  refine ⟨built, e, B, hbuild, ?_, hscan, heB, hIe, hout.trans (hframe.outBits buf), hBs, hfc⟩
555  have hrd : rd (Sp id) (setD h id built) = .ok (built, setD h id built) :=
556    Out.rd_run (setD_dstates_same h id built)
557  rw [bind_app, hbuild]
558  simp only []
559  rw [bind_app, hrd]
560  exact hscan
561
562/-- A finished run contributes at most its consumed length to any one
563frequency. Repeated nonzero lengths use at most two symbols and require at
564least three consumed lengths. -/
565theorem scRunFreq_le (cur cnt mn k : Nat) (prev : Int) (hc : 1 ≤ cnt) (hm : 3 ≤ mn) :
566    Out.runFreq (some (cur, prev, cnt, mn)) k ≤ cnt := by
567  simp only [Out.runFreq]
568  split
569  · split <;> omega
570  · rename_i hs
571    split
572    · split <;> split <;> omega
573    · split <;> split <;> omega
574
575/-- Finished counts plus the unfinished run never exceed the number of
576scanned lengths. This supplies the non-wrapping bound for a real alphabet. -/
577theorem scanFreq_with_pending_le (L : Nat → Nat) (hL : ∀ i, L i < 65536) (n k : Nat) :
578    Out.scanFreqUpTo L n k + (Out.runAt L n).cnt ≤ n := by
579  induction n with
580  | zero =>
581    simp only [Out.scanFreqUpTo, Out.runAt, Out.runInit]
582    split <;> simp
583  | succ n ih =>
584    have hi := Out.runInv_runAt L hL n
585    have hmn : 3 ≤ (Out.runAt L n).mn := by
586      by_cases hz : (Out.runAt L n).next = 0
587      · have := (hi.2.1 hz).2; omega
588      · rcases hi.2.2.1 hz with ⟨h, h', rest⟩ | ⟨h, h', rest⟩ <;> omega
589    have hb := scRunFreq_le (Out.runAt L n).next ((Out.runAt L n).cnt + 1)
590      (Out.runAt L n).mn k (Out.runAt L n).prev (by omega) hmn
591    simp only [Out.scanFreqUpTo, Out.runAt]
592    unfold Out.runStep
593    by_cases ha : (Out.runAt L n).cnt + 1 < (Out.runAt L n).mx ∧ (Out.runAt L n).next = L (n + 1)
594    · simp only [ite_eq_left ha, Out.runFreq, Nat.add_zero]
595      omega
596    · simp only [ite_eq_right ha]
597      split
598      · dsimp only; omega
599      · split <;> (dsimp only; omega)
600
601theorem scanFreq_le (L : Nat → Nat) (hL : ∀ i, L i < 65536) (n k : Nat) :
602    Out.scanFreqUpTo L n k ≤ n := by
603  have := scanFreq_with_pending_le L hL n k
604  omega
605
606/-- The two scans' counts fit exactly in a 16-bit frequency cell when their
607combined alphabet size is below 65536. No input-length restriction is used. -/
608theorem scan_frequency_pair_exact (L D : Nat → Nat)
609    (hL : ∀ i, L i < 65536) (hD : ∀ i, D i < 65536) (n m k : Nat) (hsize : n + m < 65536) :
610    (UInt16.ofNat (Out.scanFreqUpTo L n k) + UInt16.ofNat (Out.scanFreqUpTo D m k)).toNat =
611      Out.scanFreqUpTo L n k + Out.scanFreqUpTo D m k := by
612  have h1 := scanFreq_le L hL n k
613  have h2 := scanFreq_le D hD m k
614  rw [← UInt16.ofNat_add, UInt16.toNat_ofNat']
615  exact Nat.mod_eq_of_lt (by omega)
616
617/-- The sentinel forces the last pending run to be counted. -/
618theorem scan_guard_finishes (L : Nat → Nat) (M : Nat) (h15 : ∀ i ≤ M, L i ≤ 15) :
619    (Out.runAt (Out.guarded L M) (M + 1)).cnt = 0 := by
620  have hcur : (Out.runAt (Out.guarded L M) M).next ≤ 15 := by
621    rw [Out.runAt_next]
622    simp only [Out.guarded, ite_eq_right (show M ≠ M + 1 by omega)]
623    exact h15 M (Nat.le_refl _)
624  have hnx : Out.guarded L M (M + 1) = 65535 := by simp [Out.guarded]
625  have hnot : ¬ ((Out.runAt (Out.guarded L M) M).cnt + 1 < (Out.runAt (Out.guarded L M) M).mx ∧
626      (Out.runAt (Out.guarded L M) M).next = Out.guarded L M (M + 1)) := by
627    rw [hnx]
628    omega
629  simp only [Out.runAt, Out.runStep, ite_eq_right hnot]
630  split
631  · rfl
632  · split <;> rfl
633
634end Zlib.Trees.Proofs