trees.c.block.lean

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

1import ZlibF.Proof.«trees.c.arrays»
2import ZlibF.Proof.«trees.c.reverse»
3import ZlibF.Proof.«trees.c.bits»
4
5/-!
6# trees.c: `init_block`, `_tr_init`
7-/
8
9namespace Zlib.Trees.Proofs.Out
10open C Zlib.Trees
11
12/-- The loop `for (n = 0; n < M; n++) tree[n].Freq = 0;` over one of the code arrays of the record: after it the
13first `M` entries have `Freq = 0` and nothing else changed. `pS` is the translation's pointer to the array. -/
14theorem zero_freq_loop {h : Heap} {id : Nat} {d : DeflateState} (hd : h.dstates id = some d) (s : Sel)
15    (pS : M CtDataPtr) (hp : ∀ h' : Heap, h'.dstates id ≠ none → pS h' = .ok (.ref (s.ref id) 0, h'))
16    (M0 : Int32) (hM0 : M0.toInt ≤ (s.arr d).size) (hM1 : 0 ≤ M0.toInt) (hMb : M0.toInt ≤ 1000) :
17    Wp (cfor (σ := Int32) (fun n => pure (decide (n.toInt < M0.toInt))) (fun n => iadd n 1)
18        (fun n => do setFc (← pS) n.toInt 0; pure n) 0) h
19      (fun _ h' => ∃ a, h' = setD h id (s.upd d a) ∧ a.size = (s.arr d).size ∧
20        ∀ j, j < a.size → a[j]! = if j < M0.toInt.toNat then { (s.arr d)[j]! with fc := 0 } else (s.arr d)[j]!) := by
21  unfold cfor
22  refine Wp.cwhile (fun n h' => 0 ≤ n.toInt ∧ n.toInt ≤ M0.toInt ∧ ∃ a, h' = setD h id (s.upd d a) ∧
23      a.size = (s.arr d).size ∧ ∀ j, j < a.size →
24        a[j]! = if j < n.toInt.toNat then { (s.arr d)[j]! with fc := 0 } else (s.arr d)[j]!)
25    (fun n => (M0.toInt - n.toInt).toNat) _ ?_ ?_ ?_
26  · rintro n h' ⟨hn0, hn1, a, rfl, hsz, hj⟩
27    have hd' : (setD h id (s.upd d a)).dstates id = some (s.upd d a) := setD_dstates_same _ _ _
28    have hne : (setD h id (s.upd d a)).dstates id ≠ none := by simp
29    by_cases hlt : n.toInt < M0.toInt
30    · right
31      have hn' : n.toInt.toNat < a.size := by omega
32      have hi' : n.toInt.toNat < (s.arr (s.upd d a)).size := by rw [Sel.arr_upd]; exact hn'
33      have hset := setFc_sel hd' s hi' 0
34      rw [Sel.arr_upd] at hset
35      have hadd := iadd_eq (a := n) (b := 1) (by rw [i32_one_toInt]; omega) (by rw [i32_one_toInt]; omega)
36      have hcast : ((n.toInt.toNat : Nat) : Int) = n.toInt := by omega
37      have hnn : (Int32.ofInt (n.toInt + 1)).toInt = n.toInt + 1 := i32_ofInt_toInt (by omega) (by omega)
38      refine ⟨n, setD h id (s.upd d a), Int32.ofInt (n.toInt + 1),
39        setD h id (s.upd d (a.set! n.toInt.toNat { a[n.toInt.toNat]! with fc := 0 })), ?_, ?_, ⟨?_, ?_, ?_⟩, ?_⟩
40      · simp [hlt]
41      · rw [hcast] at hset
42        simp only [bind_app, hp _ hne, hset, pure_app, Sel.arr_upd, Sel.upd_upd, setD_setD]
43        simp only [hadd, i32_one_toInt, pure_app]
44      · rw [hnn]; omega
45      · rw [hnn]; omega
46      · refine ⟨_, rfl, by simp [hsz], ?_⟩
47        intro j hj'
48        simp only [Array.size_set!] at hj'
49        rw [hnn]
50        have e1 : (n.toInt + 1).toNat = n.toInt.toNat + 1 := by omega
51        rw [e1]
52        rw [getElem!_set!]
53        by_cases hjn : n.toInt.toNat = j
54        · subst hjn
55          simp only [hn', and_self, ite_true]
56          rw [hj _ hn']
57          simp
58        · have h1 : ¬ (n.toInt.toNat = j ∧ n.toInt.toNat < a.size) := fun h => hjn h.1
59          simp only [h1, ite_false]
60          rw [hj j (by simpa using hj')]
61          have : (j < n.toInt.toNat + 1) ↔ (j < n.toInt.toNat) := by omega
62          simp only [this]
63      · rw [hnn]; omega
64    · left
65      have hnM : n.toInt = M0.toInt := by omega
66      refine ⟨n, setD h id (s.upd d a), by simp [hlt], ⟨a, rfl, hsz, ?_⟩⟩
67      rw [hnM] at hj
68      exact hj
69  · have h0 : (0 : Int32).toInt = 0 := by decide
70    refine ⟨by rw [h0]; exact Int.le_refl 0, by rw [h0]; exact hM1, s.arr d, ?_, rfl, ?_⟩
71    · rw [Sel.upd_arr, setD_self hd]
72    · intro j hj'
73      simp [h0]
74  · show (M0.toInt - (0 : Int32).toInt).toNat < fuel
75    have h0 : (0 : Int32).toInt = 0 := by decide
76    rw [h0]; unfold fuel; omega
77
78
79theorem L_CODES_toInt : L_CODES.toInt = 286 := by decide
80theorem D_CODES_toInt : D_CODES.toInt = 30 := by decide
81theorem BL_CODES_toInt : BL_CODES.toInt = 19 := by decide
82theorem END_BLOCK_toInt : END_BLOCK.toInt = 256 := by decide
83
84/-- The deflate record after `init_block`, given the three code arrays. -/
85def ibRec (d : DeflateState) (a1 a2 a3 : Array CtData) : DeflateState :=
86  { d with dyn_ltree := a1, dyn_dtree := a2, bl_tree := a3, opt_len := 0, static_len := 0, «matches» := 0, sym_next := 0 }
87
88theorem init_block_inv {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
89    (hb : TreesBase h id d b buf) (hr : TreesRun0 id d) (a1 a2 a3 : Array CtData) (s1 : a1.size = 573)
90    (s2 : a2.size = 61) (s3 : a3.size = 39) :
91    TreesInvAt (setD h id (ibRec d a1 a2 a3)) id (ibRec d a1 a2 a3) b buf := by
92  obtain ⟨w1, w2, w3, w4, w5, w6⟩ := hb.wf
93  refine ⟨hb.stepD _ ⟨s1, s2, s3, w4, w5, w6⟩ rfl rfl rfl rfl rfl hb.pending_le, ?_⟩
94  exact ⟨hr.ldyn, hr.lstat, hr.ddyn, hr.dstat, hr.bldyn, hr.blstat, hr.bi_lo, hr.bi_hi, hr.bi_buf,
95    by show (0 : UInt32).toNat ≤ d.sym_end.toNat; simp, by show (0 : UInt32).toNat % 3 = 0; simp⟩
96
97/-- **`init_block`, safety and specification.** Zeroes the frequencies of the three code arrays
98(`dyn_ltree[0 .. 286)`, `dyn_dtree[0 .. 30)`, `bl_tree[0 .. 19)`), sets `dyn_ltree[END_BLOCK].Freq = 1`,
99`opt_len = static_len = 0`, `sym_next = matches = 0`. Nothing else changes (not the `Len` halves, not the bit
100buffer, not `pending`). Precondition: `TreesBase` and the descriptor and bit-buffer part of `TreesRun`
101(`init_block` does not read `sym_next`). The result is again `TreesInvAt`. -/
102theorem init_block_spec0 {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
103    (hb : TreesBase h id d b buf) (hr : TreesRun0 id d) :
104    ∃ a1 a2 a3 d', init_block (some (.tab id)) h = .ok ((), setD h id d') ∧
105      TreesInvAt (setD h id d') id d' b buf ∧
106      d' = ibRec d a1 a2 a3 ∧
107      a1.size = 573 ∧ a2.size = 61 ∧ a3.size = 39 ∧
108      (∀ n : Nat, n < 286 → n ≠ 256 → (a1[n]!).fc = 0) ∧ (a1[256]!).fc = 1 ∧
109      (∀ n : Nat, n < 30 → (a2[n]!).fc = 0) ∧ (∀ n : Nat, n < 19 → (a3[n]!).fc = 0) ∧
110      (∀ n : Nat, (a1[n]! : CtData).dl = (d.dyn_ltree[n]! : CtData).dl) ∧ (∀ n : Nat, (a2[n]!).dl = (d.dyn_dtree[n]!).dl) ∧
111      (∀ n : Nat, (a3[n]!).dl = (d.bl_tree[n]!).dl) := by
112  have hd := hb.dstate
113  obtain ⟨w1, w2, w3, w4, w5, w6⟩ := hb.wf
114  have hpL : ∀ h' : Heap, h'.dstates id ≠ none → pLtree (some (.tab id)) h' = .ok (.ref (Sel.l.ref id) 0, h') :=
115    fun h' hne => by
116      obtain ⟨dd, hdd⟩ := Option.ne_none_iff_exists'.mp hne
117      exact pLtree_run hdd
118  have hpD : ∀ h' : Heap, h'.dstates id ≠ none → pDtree (some (.tab id)) h' = .ok (.ref (Sel.d.ref id) 0, h') :=
119    fun h' hne => by
120      obtain ⟨dd, hdd⟩ := Option.ne_none_iff_exists'.mp hne
121      exact pDtree_run hdd
122  have hpB : ∀ h' : Heap, h'.dstates id ≠ none → pBltree (some (.tab id)) h' = .ok (.ref (Sel.bl.ref id) 0, h') :=
123    fun h' hne => by
124      obtain ⟨dd, hdd⟩ := Option.ne_none_iff_exists'.mp hne
125      exact pBltree_run hdd
126  obtain ⟨_, h1, e1, a1, rfl, hs1, hel1⟩ := zero_freq_loop hd .l _ hpL L_CODES
127    (by rw [L_CODES_toInt]; show (286 : Int) ≤ d.dyn_ltree.size; omega) (by rw [L_CODES_toInt]; omega)
128    (by rw [L_CODES_toInt]; omega)
129  have hd1 : (setD h id (Sel.l.upd d a1)).dstates id = some (Sel.l.upd d a1) := setD_dstates_same _ _ _
130  obtain ⟨_, h2, e2, a2, rfl, hs2, hel2⟩ := zero_freq_loop hd1 .d _ hpD D_CODES
131    (by rw [D_CODES_toInt]; show (30 : Int) ≤ d.dyn_dtree.size; omega) (by rw [D_CODES_toInt]; omega)
132    (by rw [D_CODES_toInt]; omega)
133  have hd2 : (setD (setD h id (Sel.l.upd d a1)) id (Sel.d.upd (Sel.l.upd d a1) a2)).dstates id
134      = some (Sel.d.upd (Sel.l.upd d a1) a2) := setD_dstates_same _ _ _
135  obtain ⟨_, h3, e3, a3, rfl, hs3, hel3⟩ := zero_freq_loop hd2 .bl _ hpB BL_CODES
136    (by rw [BL_CODES_toInt]; show (19 : Int) ≤ d.bl_tree.size; omega) (by rw [BL_CODES_toInt]; omega)
137    (by rw [BL_CODES_toInt]; omega)
138  have hd3 : (setD (setD (setD h id (Sel.l.upd d a1)) id (Sel.d.upd (Sel.l.upd d a1) a2)) id
139      (Sel.bl.upd (Sel.d.upd (Sel.l.upd d a1) a2) a3)).dstates id
140      = some (Sel.bl.upd (Sel.d.upd (Sel.l.upd d a1) a2) a3) := setD_dstates_same _ _ _
141  unfold init_block
142  rw [bind_app, e1]
143  simp only []
144  rw [bind_app, e2]
145  simp only []
146  rw [bind_app, e3]
147  simp only []
148  have sz1 : a1.size = 573 := by rw [hs1]; exact w1
149  have sz2 : a2.size = 61 := by rw [hs2]; exact w2
150  have sz3 : a3.size = 39 := by rw [hs3]; exact w3
151  have hE : END_BLOCK.toInt = ((256 : Nat) : Int) := by rw [END_BLOCK_toInt]; rfl
152  have hi256 : 256 < (Sel.l.arr (Sel.bl.upd (Sel.d.upd (Sel.l.upd d a1) a2) a3)).size := by
153    show 256 < a1.size
154    rw [hs1]; show 256 < d.dyn_ltree.size; omega
155  have hset : setFc (.ref (CtDataRef.dstate_dyn_ltree id) 0) ((256 : Nat) : Int) 1
156      (setD (setD (setD h id (Sel.l.upd d a1)) id (Sel.d.upd (Sel.l.upd d a1) a2)) id
157        (Sel.bl.upd (Sel.d.upd (Sel.l.upd d a1) a2) a3)) = _ := setFc_sel hd3 .l hi256 1
158  rw [bind_app, pLtree_run hd3]
159  simp only []
160  rw [bind_app, hE, hset]
161  simp (disch := simp) only [bind_app, md_run', rdD_setD_same, setD_setD, pure_app]
162  have ha1 : Sel.l.arr (Sel.bl.upd (Sel.d.upd (Sel.l.upd d a1) a2) a3) = a1 := rfl
163  have hdl1 : ∀ n : Nat, (a1[n]! : CtData).dl = (d.dyn_ltree[n]! : CtData).dl := by
164    intro n
165    by_cases hn : n < a1.size
166    · rw [hel1 n hn]; split <;> rfl
167    · rw [getElem!_ge a1 n (by omega), getElem!_ge d.dyn_ltree n (by omega)]
168  have hdl2 : ∀ n : Nat, (a2[n]! : CtData).dl = (d.dyn_dtree[n]! : CtData).dl := by
169    intro n
170    by_cases hn : n < a2.size
171    · rw [hel2 n hn]; split <;> simp [Sel.arr, Sel.upd]
172    · rw [getElem!_ge a2 n (by omega), getElem!_ge d.dyn_dtree n (by omega)]
173  have hdl3 : ∀ n : Nat, (a3[n]! : CtData).dl = (d.bl_tree[n]! : CtData).dl := by
174    intro n
175    by_cases hn : n < a3.size
176    · rw [hel3 n hn]; split <;> simp [Sel.arr, Sel.upd]
177    · rw [getElem!_ge a3 n (by omega), getElem!_ge d.bl_tree n (by omega)]
178  refine ⟨(Sel.l.arr (Sel.bl.upd (Sel.d.upd (Sel.l.upd d a1) a2) a3)).set! 256
179      { (Sel.l.arr (Sel.bl.upd (Sel.d.upd (Sel.l.upd d a1) a2) a3))[256]! with fc := 1 }, a2, a3, _, rfl, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
180  · suffices H : ∀ D : DeflateState, D = ibRec d ((Sel.l.arr (Sel.bl.upd (Sel.d.upd (Sel.l.upd d a1) a2) a3)).set! 256 { (Sel.l.arr (Sel.bl.upd (Sel.d.upd (Sel.l.upd d a1) a2) a3))[256]! with fc := 1 }) a2 a3 → TreesInvAt (setD h id D) id D b buf from
181      H _ (by simp only [Sel.upd, Sel.arr, ibRec])
182    intro D hD
183    subst hD
184    exact init_block_inv hb hr _ a2 a3 (by rw [Array.size_set!]; rw [ha1]; exact sz1) sz2 sz3
185  · simp only [Sel.upd, Sel.arr, ibRec]
186  · rw [ha1]; simp [sz1]
187  · exact sz2
188  · exact sz3
189  · intro n hn hne
190    rw [ha1, getElem!_set!]
191    have h1 : ¬ (256 = n ∧ 256 < a1.size) := fun h => hne h.1.symm
192    simp only [h1, ite_false]
193    rw [hel1 n (by omega)]
194    simp [L_CODES_toInt, hn]
195  · rw [ha1, getElem!_set!]
196    simp [sz1]
197  · intro n hn
198    rw [hel2 n (by omega)]
199    simp [Sel.arr, Sel.upd, D_CODES_toInt, hn]
200  · intro n hn
201    rw [hel3 n (by omega)]
202    simp [Sel.arr, Sel.upd, BL_CODES_toInt, hn]
203  · intro n
204    rw [ha1, getElem!_set!]
205    by_cases hn : 256 = n
206    · subst hn
207      have h256 : 256 < a1.size := by omega
208      simp only [h256, and_self, ite_true]
209      exact hdl1 256
210    · have h1 : ¬ (256 = n ∧ 256 < a1.size) := fun h => hn h.1
211      simp only [h1, ite_false]; exact hdl1 n
212  · exact hdl2
213  · exact hdl3
214
215
216/-- `init_block_spec0` for a state that satisfies the whole invariant. -/
217theorem init_block_spec {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
218    (hI : TreesInvAt h id d b buf) :
219    ∃ a1 a2 a3 d', init_block (some (.tab id)) h = .ok ((), setD h id d') ∧
220      TreesInvAt (setD h id d') id d' b buf ∧ d' = ibRec d a1 a2 a3 ∧
221      a1.size = 573 ∧ a2.size = 61 ∧ a3.size = 39 := by
222  obtain ⟨a1, a2, a3, d', e, hi, hd, s1, s2, s3, -⟩ := init_block_spec0 hI.base hI.run.to0
223  exact ⟨a1, a2, a3, d', e, hi, hd, s1, s2, s3⟩
224
225
226/-- The record after the stores of `_tr_init` that precede `init_block`. -/
227def trInitRec (id : Nat) (d : DeflateState) : DeflateState :=
228  { d with
229    l_desc := { d.l_desc with dyn_tree := .ref (.dstate_dyn_ltree id) 0, stat_desc := some .st_static_l_desc },
230    d_desc := { d.d_desc with dyn_tree := .ref (.dstate_dyn_dtree id) 0, stat_desc := some .st_static_d_desc },
231    bl_desc := { d.bl_desc with dyn_tree := .ref (.dstate_bl_tree id) 0, stat_desc := some .st_static_bl_desc },
232    bi_buf := 0, bi_valid := 0, bi_used := 0 }
233
234theorem trInitRec_inv {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
235    (hb : TreesBase h id d b buf) :
236    TreesBase (setD h id (trInitRec id d)) id (trInitRec id d) b buf ∧ TreesRun0 id (trInitRec id d) := by
237  refine ⟨hb.stepD _ hb.wf rfl rfl rfl rfl rfl hb.pending_le, ?_⟩
238  refine ⟨rfl, rfl, rfl, rfl, rfl, rfl, ?_, ?_, ?_⟩ <;> simp [trInitRec]
239
240/-- **`_tr_init`, safety and specification.** `_tr_init(s)` points the three tree descriptors at the arrays of the
241record and at the static descriptors, empties the bit buffer (`bi_buf = bi_valid = bi_used = 0`) and calls
242`init_block`. Precondition: `TreesBase` only (what `deflateInit2_` establishes before it calls `deflateReset`, which
243reaches `_tr_init` through `deflateResetKeep`); the result satisfies the whole invariant `TreesInvAt`. `pending`,
244`pending_buf` and the byte block are unchanged. -/
245theorem tr_init_spec {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
246    (hb : TreesBase h id d b buf) :
247    ∃ a1 a2 a3 d', «_tr_init» (some (.tab id)) h = .ok ((), setD h id d') ∧
248      TreesInvAt (setD h id d') id d' b buf ∧ d' = ibRec (trInitRec id d) a1 a2 a3 ∧
249      a1.size = 573 ∧ a2.size = 61 ∧ a3.size = 39 := by
250  obtain ⟨hb6, hr6⟩ := trInitRec_inv hb
251  obtain ⟨a1, a2, a3, d', e, hi, hd, s1, s2, s3, -⟩ := init_block_spec0 hb6 hr6
252  simp only [setD_setD] at e hi
253  refine ⟨a1, a2, a3, d', ?_, hi, hd, s1, s2, s3⟩
254  have hne : h.dstates id ≠ none := by simp [hb.dstate]
255  have hrd : rdD h id = d := by simp [rdD, hb.dstate]
256  unfold «_tr_init»
257  simp (disch := simp [hb.dstate]) only [tr_static_init, bind_app, pure_app, sid_run hb.dstate, md_run', rdD_setD_same, setD_setD, hrd]
258  exact e
259
260end Zlib.Trees.Proofs.Out