trees.c.build.scan.lean

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

1import ZlibF.Math.DeflateTreeScan
2import ZlibF.Proof.«trees.c.monad»
3import ZlibF.Proof.«trees.c.heap.gbdef»
4
5/-! # trees.c: the first `build_tree` scan -/
6
7namespace Zlib.Trees.Proofs
8open C Zlib.Trees
9
10/-- The first scan's body, in the actual source order. -/
11def btScanBody (s : DeflateStatePtr) (tree : CtDataPtr) : Int32 × Int32 → M (Int32 × Int32) :=
12  fun (n, mc) => do
13    if (← getFc tree n.toInt) != 0 then
14      let hl ← iadd (← rd s).heap_len 1
15      md s fun d => { d with heap_len := hl }
16      heapSet s hl n
17      setAt (← pDepth s) n.toInt 0
18      pure (n, n)
19    else
20      setDl tree n.toInt 0
21      pure (n, mc)
22
23/-- The first scan, including the separate increment. -/
24def btScan (s : DeflateStatePtr) (tree : CtDataPtr) (elems : Int32) : M (Int32 × Int32) :=
25  cfor (σ := Int32 × Int32)
26    (fun (n, _) => pure (decide (n.toInt < elems.toInt)))
27    (fun (n, mc) => do pure (← iadd n 1, mc))
28    (btScanBody s tree) (0, -1)
29
30/-- Exact state frame of the scan. -/
31def btScanState (tk : TK) (d : DeflateState) (T : Array CtData) (H : Array Int32)
32    (D : Array UInt8) (hl : Int32) : DeflateState :=
33  { tk.setArr d T with heap := H, depth := D, heap_len := hl }
34
35@[simp] theorem btScanState_tree (tk : TK) (d T H D hl) :
36    tk.arr (btScanState tk d T H D hl) = T := by cases tk <;> rfl
37
38@[simp] theorem btScanState_heap (tk : TK) (d T H D hl) :
39    (btScanState tk d T H D hl).heap = H := rfl
40
41@[simp] theorem btScanState_depth (tk : TK) (d T H D hl) :
42    (btScanState tk d T H D hl).depth = D := rfl
43
44@[simp] theorem btScanState_len (tk : TK) (d T H D hl) :
45    (btScanState tk d T H D hl).heap_len = hl := rfl
46
47/-- One actual positive-frequency iteration writes the next heap slot and
48zeroes the leaf depth. It keeps the code-tree entry unchanged. -/
49theorem btScanBody_used {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (n mc : Int32)
50    (hn0 : 0 ≤ n.toInt) (hnT : n.toInt < (tk.arr d).size)
51    (hnD : n.toInt < d.depth.size) (hl0 : 0 ≤ d.heap_len.toInt)
52    (hlH : d.heap_len.toInt + 1 < d.heap.size) (hbig : d.heap.size ≤ 573)
53    (hf : ((tk.arr d)[n.toInt.toNat]!).fc ≠ 0) :
54    WS h0 id (btScanBody (Sp id) (.ref (tk.ref id) 0) (n, mc)) d
55      (fun r e => ∃ hl : Int32, hl.toInt = d.heap_len.toInt + 1 ∧ r = (n, n) ∧
56        e = { d with
57          heap_len := hl, heap := d.heap.set! hl.toInt.toNat n, depth := d.depth.set! n.toInt.toNat 0 }) := by
58  unfold btScanBody
59  refine WS.bind' (ws_getFc tk n.toInt hn0 hnT) fun v e1 ⟨hv, he1⟩ => ?_
60  subst e1; subst v
61  have hb : (((tk.arr d)[n.toInt.toNat]!).fc != 0) = true := by simpa using hf
62  simp only [hb, Bool.true_eq, ite_true]
63  refine WS.bind' ws_rd fun dz e1 ⟨hdz, he1⟩ => ?_
64  subst e1; subst dz
65  have hi1 : (1 : Int32).toInt = 1 := rfl
66  refine WS.bind' (ws_iadd d.heap_len 1 (by omega) (by omega)) fun hl e1 ⟨hhl, he1⟩ => ?_
67  subst e1
68  refine WS.bind' (ws_md (fun e => { e with heap_len := hl })) fun _ e1 he1 => ?_
69  subst e1
70  unfold heapSet
71  simp only [M_bind_assoc]
72  refine WS.bind' ws_pHeap fun p e1 ⟨hp, he1⟩ => ?_
73  subst e1; subst p
74  refine WS.bind' (ws_setAt_heap hl.toInt n (by omega) (by dsimp; omega)) fun _ e1 he1 => ?_
75  subst e1
76  refine WS.bind' ws_pDepth fun p e1 ⟨hp, he1⟩ => ?_
77  subst e1; subst p
78  refine WS.bind' (ws_setAt_depth n.toInt 0 hn0 (by dsimp; exact hnD)) fun _ e1 he1 => ?_
79  subst e1
80  exact WS.pure' ⟨hl, by omega, rfl, rfl⟩
81
82/-- One actual zero-frequency iteration only clears that leaf's length. -/
83theorem btScanBody_unused {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (n mc : Int32)
84    (hn0 : 0 ≤ n.toInt) (hnT : n.toInt < (tk.arr d).size)
85    (hf : ((tk.arr d)[n.toInt.toNat]!).fc = 0) :
86    WS h0 id (btScanBody (Sp id) (.ref (tk.ref id) 0) (n, mc)) d
87      (fun r e => r = (n, mc) ∧
88        e = tk.setArr d ((tk.arr d).set! n.toInt.toNat { (tk.arr d)[n.toInt.toNat]! with dl := 0 })) := by
89  unfold btScanBody
90  refine WS.bind' (ws_getFc tk n.toInt hn0 hnT) fun v e1 ⟨hv, he1⟩ => ?_
91  subst e1; subst v
92  simp only [hf, bne_self_eq_false, Bool.false_eq_true, ite_false]
93  refine WS.bind' (ws_setDl tk n.toInt 0 hn0 hnT) fun _ e1 he1 => ?_
94  subst e1
95  exact WS.pure' ⟨rfl, by simp only [hf]⟩
96
97/-- Frequencies before the scan; the scan preserves these code cells. -/
98def btFreq (tk : TK) (d : DeflateState) (v : Nat) : UInt16 := ((tk.arr d)[v]!).fc
99
100/-- The first scan's derived state: exact writes, one occurrence of every
101used symbol, no other heap entries, and the exact largest used symbol. -/
102def BTScanInv (tk : TK) (d : DeflateState) (k : Nat) (mc : Int32) (e : DeflateState) : Prop :=
103  let fr := btFreq tk d
104  ∃ (T : Array CtData) (H : Array Int32) (D : Array UInt8) (hl : Int32),
105    e = btScanState tk d T H D hl ∧ T.size = (tk.arr d).size ∧ H.size = d.heap.size ∧
106    D.size = d.depth.size ∧ hl.toInt = Math.scanCount fr k ∧ mc.toInt = Math.scanMax fr k ∧
107    (∀ j < T.size, T[j]! = if j < k ∧ fr j = 0 then { (tk.arr d)[j]! with dl := 0 } else (tk.arr d)[j]!) ∧
108    (∀ j < D.size, D[j]! = if j < k ∧ fr j ≠ 0 then 0 else d.depth[j]!) ∧
109    (∀ q, ¬ (1 ≤ q ∧ q ≤ Math.scanCount fr k) → H[q]! = d.heap[q]!) ∧
110    (∀ q, 1 ≤ q → q ≤ Math.scanCount fr k →
111      0 ≤ H[q]!.toInt ∧ H[q]!.toInt < k ∧ fr H[q]!.toInt.toNat ≠ 0) ∧
112    (∀ q q', 1 ≤ q → q ≤ Math.scanCount fr k → 1 ≤ q' → q' ≤ Math.scanCount fr k →
113      H[q]! = H[q']! → q = q') ∧
114    ∀ v < k, fr v ≠ 0 → ∃ q, 1 ≤ q ∧ q ≤ Math.scanCount fr k ∧ H[q]!.toInt = v
115
116/-- The scan invariant is established by an empty heap, independently of
117the old lengths and depths. -/
118theorem btScan_init (tk : TK) (d : DeflateState) (hl : d.heap_len.toInt = 0) :
119    BTScanInv tk d 0 (-1) d := by
120  refine ⟨tk.arr d, d.heap, d.depth, d.heap_len, ?_, rfl, rfl, rfl, hl, rfl,
121    ?_, ?_, ?_, ?_, ?_, ?_⟩
122  · cases tk <;> rfl
123  · intro j hj; simp
124  · intro j hj; simp
125  · intro q hq; rfl
126  · intro q hq1 hq2; simp only [Math.scanCount] at hq2; omega
127  · intro q q' hq1 hq2; simp only [Math.scanCount] at hq2; omega
128  · intro v hv; omega
129
130/-- One complete scan iteration, including the separate checked increment. -/
131theorem btScan_step {h0 : Heap} {id : Nat} (tk : TK) (d e : DeflateState) (k N : Nat)
132    (n mc : Int32) (hn : n.toInt = k) (hk : k < N) (hN : N ≤ 286)
133    (hT : N ≤ (tk.arr d).size) (hD : N ≤ d.depth.size)
134    (hH : N < d.heap.size) (hbig : d.heap.size ≤ 573)
135    (hi : BTScanInv tk d k mc e) :
136    WS h0 id (do
137      let (n, mc) ← btScanBody (Sp id) (.ref (tk.ref id) 0) (n, mc)
138      pure (← iadd n 1, mc)) e (fun r e' => r.1.toInt = k + 1 ∧ BTScanInv tk d (k + 1) r.2 e') := by
139  obtain ⟨T, H, D, hl, he, hsT, hsH, hsD, hhl, hmc, ht, hd, hh, hv, hj, hc⟩ := hi
140  subst e
141  have hcount := Math.scanCount_le (btFreq tk d) k
142  have hnN : n.toInt.toNat = k := by omega
143  have hkT : k < T.size := by omega
144  have hkD : k < D.size := by omega
145  have hcur : (T[k]!).fc = (btFreq tk d) k := by rw [ht k hkT]; split <;> rfl
146  have hfcur : ((tk.arr (btScanState tk d T H D hl))[n.toInt.toNat]!).fc = (btFreq tk d) k := by
147    simpa only [btScanState_tree, hnN] using hcur
148  have hi1 : (1 : Int32).toInt = 1 := rfl
149  by_cases hf : (btFreq tk d) k ≠ 0
150  · refine WS.bind' (btScanBody_used tk (btScanState tk d T H D hl) n mc
151      (by omega) (by simp only [btScanState_tree]; omega)
152      (by simp only [btScanState_depth]; omega) (by simp only [btScanState_len]; omega)
153      (by simp only [btScanState_len, btScanState_heap]; omega)
154      (by simp only [btScanState_heap]; omega) (by rw [hfcur]; exact hf))
155      fun r e1 ⟨hl', hhl', hr, he1⟩ => ?_
156    subst r; subst e1
157    dsimp only
158    refine WS.bind' (ws_iadd n 1 (by omega) (by omega)) fun n' e1 ⟨hn', he1⟩ => ?_
159    subst e1
160    have hhl' : hl'.toInt = Math.scanCount (btFreq tk d) k + 1 := by simpa only [btScanState_len, hhl] using hhl'
161    have hhlN : hl'.toInt.toNat = Math.scanCount (btFreq tk d) k + 1 := by omega
162    have hnewH : Math.scanCount (btFreq tk d) k + 1 < H.size := by omega
163    have hnext : Math.scanCount (btFreq tk d) (k + 1) = Math.scanCount (btFreq tk d) k + 1 := by simp only [Math.scanCount, ite_eq_left hf]
164    have hnextmc : Math.scanMax (btFreq tk d) (k + 1) = k := by simp only [Math.scanMax, ite_eq_left hf]
165    refine WS.pure' ⟨by dsimp; omega,
166      T, H.set! (Math.scanCount (btFreq tk d) k + 1) n, D.set! k 0, hl', ?_, hsT,
167      by simpa only [size_set!] using hsH, by simpa only [size_set!] using hsD,
168      by rw [hnext]; omega, by dsimp; rw [hnextmc]; exact hn, ?_, ?_, ?_, ?_, ?_, ?_⟩
169    · simp only [btScanState_heap, btScanState_depth, hnN, hhlN]
170      rfl
171    · intro j hjT
172      rw [ht j hjT]
173      by_cases hjk : j = k
174      · subst j; simp [hf]
175      · have hcut : (j < k) ↔ (j < k + 1) := by omega
176        simp only [hcut]
177    · intro j hjD
178      have hjD' : j < D.size := by simpa only [size_set!] using hjD
179      rw [getD_set D k j 0 hkD]
180      by_cases hjk : j = k
181      · subst j; simp [hf]
182      · rw [ite_eq_right hjk, hd j hjD']
183        have hcut : (j < k) ↔ (j < k + 1) := by omega
184        simp only [hcut]
185    · intro q hq
186      rw [hnext] at hq
187      rw [getD_set H (Math.scanCount (btFreq tk d) k + 1) q n hnewH, ite_eq_right (by omega)]
188      exact hh q (by omega)
189    · intro q hq1 hq2
190      rw [hnext] at hq2
191      rw [getD_set H (Math.scanCount (btFreq tk d) k + 1) q n hnewH]
192      by_cases hq : q = Math.scanCount (btFreq tk d) k + 1
193      · rw [ite_eq_left hq]
194        exact ⟨by omega, by omega, by simpa only [hnN] using hf⟩
195      · rw [ite_eq_right hq]
196        obtain ⟨h0, hlt, hfq⟩ := hv q hq1 (by omega)
197        exact ⟨h0, by omega, hfq⟩
198    · intro q q' hq1 hq2 hq'1 hq'2 heq
199      rw [hnext] at hq2 hq'2
200      rw [getD_set H (Math.scanCount (btFreq tk d) k + 1) q n hnewH,
201        getD_set H (Math.scanCount (btFreq tk d) k + 1) q' n hnewH] at heq
202      by_cases hq : q = Math.scanCount (btFreq tk d) k + 1
203      · rw [ite_eq_left hq] at heq
204        by_cases hq' : q' = Math.scanCount (btFreq tk d) k + 1
205        · omega
206        · rw [ite_eq_right hq'] at heq
207          have hlt := (hv q' hq'1 (by omega)).2.1
208          rw [← heq] at hlt
209          omega
210      · rw [ite_eq_right hq] at heq
211        by_cases hq' : q' = Math.scanCount (btFreq tk d) k + 1
212        · rw [ite_eq_left hq'] at heq
213          have hlt := (hv q hq1 (by omega)).2.1
214          rw [heq] at hlt
215          omega
216        · rw [ite_eq_right hq'] at heq
217          exact hj q q' hq1 (by omega) hq'1 (by omega) heq
218    · intro v hvk hfv
219      rw [hnext]
220      by_cases hvk' : v = k
221      · subst v
222        refine ⟨Math.scanCount (btFreq tk d) k + 1, by omega, by omega, ?_⟩
223        rw [getD_set H (Math.scanCount (btFreq tk d) k + 1) _ n hnewH, ite_eq_left rfl]
224        exact hn
225      · obtain ⟨q, hq1, hq2, hqv⟩ := hc v (by omega) hfv
226        refine ⟨q, hq1, by omega, ?_⟩
227        rw [getD_set H (Math.scanCount (btFreq tk d) k + 1) q n hnewH, ite_eq_right (by omega)]
228        exact hqv
229  · have hf0 : (btFreq tk d) k = 0 := by simpa using hf
230    refine WS.bind' (btScanBody_unused tk (btScanState tk d T H D hl) n mc
231      (by omega) (by simp only [btScanState_tree]; omega) (by rw [hfcur]; exact hf0))
232      fun r e1 ⟨hr, he1⟩ => ?_
233    subst r; subst e1
234    dsimp only
235    refine WS.bind' (ws_iadd n 1 (by omega) (by omega)) fun n' e1 ⟨hn', he1⟩ => ?_
236    subst e1
237    have hnext : Math.scanCount (btFreq tk d) (k + 1) = Math.scanCount (btFreq tk d) k := by simp only [Math.scanCount, hf0, ne_eq, not_true_eq_false, ite_false, Nat.add_zero]
238    have hnextmc : Math.scanMax (btFreq tk d) (k + 1) = Math.scanMax (btFreq tk d) k := by simp only [Math.scanMax, hf0, ne_eq, not_true_eq_false, ite_false]
239    refine WS.pure' ⟨by dsimp; omega,
240      T.set! k { T[k]! with dl := 0 }, H, D, hl, ?_,
241      by simpa only [size_set!] using hsT, hsH, hsD,
242      by simpa only [hnext] using hhl, by simpa only [hnextmc] using hmc, ?_, ?_,
243      by simpa only [hnext] using hh, ?_, by simpa only [hnext] using hj, ?_⟩
244    · simp only [btScanState_tree, hnN]
245      cases tk <;> rfl
246    · intro j hjT
247      have hjT' : j < T.size := by simpa only [size_set!] using hjT
248      rw [getD_set T k j _ hkT]
249      by_cases hjk : j = k
250      · subst j
251        rw [ite_eq_left rfl, ht k hkT]
252        simp [hf0]
253      · rw [ite_eq_right hjk, ht j hjT']
254        have hcut : (j < k) ↔ (j < k + 1) := by omega
255        simp only [hcut]
256    · intro j hjD
257      rw [hd j hjD]
258      by_cases hjk : j = k
259      · subst j; simp [hf0]
260      · have hcut : (j < k) ↔ (j < k + 1) := by omega
261        simp only [hcut]
262    · intro q hq1 hq2
263      rw [hnext] at hq2
264      obtain ⟨h0, hlt, hfq⟩ := hv q hq1 hq2
265      exact ⟨h0, by omega, hfq⟩
266    · intro v hvk hfv
267      rw [hnext]
268      have hvk' : v < k := by
269        by_cases heq : v = k
270        · subst v; exact False.elim (hfv hf0)
271        · omega
272      exact hc v hvk' hfv
273
274/-- The complete first scan terminates, keeps each used symbol exactly once
275in the heap, computes the exact largest used symbol, clears unused lengths,
276and preserves all cells outside its explicit write set. The caller must supply
277the empty heap written immediately before the loop. -/
278theorem ws_btScan {h0 : Heap} {id : Nat} (tk : TK) (d : DeflateState) (elems : Int32)
279    (he0 : 0 ≤ elems.toInt) (he286 : elems.toInt ≤ 286)
280    (hT : elems.toInt ≤ (tk.arr d).size) (hD : elems.toInt ≤ d.depth.size)
281    (hH : elems.toInt < d.heap.size) (hbig : d.heap.size ≤ 573)
282    (hlen : d.heap_len.toInt = 0) :
283    WS h0 id (btScan (Sp id) (.ref (tk.ref id) 0) elems) d
284      (fun r e => r.1.toInt = elems.toInt ∧ BTScanInv tk d elems.toInt.toNat r.2 e) := by
285  let N := elems.toInt.toNat
286  have heN : elems.toInt = N := by dsimp [N]; omega
287  let Inv : Int32 × Int32 → DeflateState → Prop := fun r e =>
288    ∃ k : Nat, k ≤ N ∧ r.1.toInt = k ∧ BTScanInv tk d k r.2 e
289  unfold btScan
290  refine WS.cfor2 Inv (fun r _ => N - r.1.toInt.toNat) _ ?_
291    ⟨0, by omega, rfl, btScan_init tk d hlen⟩ (by simp only [fuel]; omega)
292  rintro ⟨n, mc⟩ e ⟨k, hk, hn, hi⟩
293  change n.toInt = (k : Int) at hn
294  refine WS.pure' ?_
295  by_cases hlt : k < N
296  · refine Or.inr ⟨by simp only [decide_eq_true_eq]; omega, ?_⟩
297    dsimp only
298    refine WS.mono (btScan_step tk d e k N n mc hn hlt (by omega) (by omega)
299      (by omega) (by omega) hbig hi) ?_
300    intro r e' ⟨hr, hi'⟩
301    exact ⟨⟨k + 1, by omega, hr, hi'⟩, by omega⟩
302  · refine Or.inl ⟨by simp only [decide_eq_false_iff_not]; omega, ?_⟩
303    have hkN : k = N := by omega
304    exact ⟨by dsimp; omega, by simpa only [hkN] using hi⟩
305
306/-- Any scanned symbol absent from the resulting heap has length zero.
307This derives the inactive-symbol condition needed after tree construction. -/
308theorem BTScanInv.absent_zero {tk : TK} {d e : DeflateState} {k : Nat} {mc : Int32}
309    (hi : BTScanInv tk d k mc e) (hT : k ≤ (tk.arr d).size) (v : Nat) (hv : v < k)
310    (habsent : ∀ q : Nat, 1 ≤ q → (q : Int) ≤ e.heap_len.toInt → (e.heap[q]!).toInt ≠ v) :
311    ((tk.arr e)[v]!).dl = 0 := by
312  obtain ⟨T, H, D, hl, rfl, hsT, hsH, hsD, hhl, hmc, ht, hd, hh, hvalid, hinj, hcomplete⟩ := hi
313  have hfreq : btFreq tk d v = 0 := by
314    apply Classical.byContradiction
315    intro hf
316    obtain ⟨q, hq1, hq2, hqv⟩ := hcomplete v hv hf
317    exact habsent q hq1 (by simp only [btScanState_len]; omega) hqv
318  simp only [btScanState_tree]
319  rw [ht v (by omega), ite_eq_left ⟨hv, hfreq⟩]
320
321end Zlib.Trees.Proofs