trees.c.arrays.lean

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

1import ZlibF.Proof.«trees.c.inv»
2
3/-!
4# trees.c: reading and writing the tree arrays of the deflate record
5
6Run lemmas for `getFc`, `setFc`, `getDl`, `setDl` on `s->dyn_ltree`, `s->dyn_dtree`, `s->bl_tree`, and the facts
7that such a write keeps the record well formed (array sizes) and `TreesBase`.
8-/
9
10namespace Zlib.Trees.Proofs.Out
11open C Zlib.Trees
12
13section generic
14variable {h : Heap} {r : CtDataRef} {a : Array CtData} {i : Nat}
15
16theorem getFc_gen (hg : Space.get h r = some a) (hi : i < a.size) :
17    getFc (.ref r 0) (i : Int) h = .ok ((a[i]).fc, h) := by
18  have e := Ptr.index_ok (off := 0) (i := i) hg (by omega)
19  unfold OkOn at e
20  unfold getFc
21  rw [bind_app, e]
22  simp
23
24theorem getDl_gen (hg : Space.get h r = some a) (hi : i < a.size) :
25    getDl (.ref r 0) (i : Int) h = .ok ((a[i]).dl, h) := by
26  have e := Ptr.index_ok (off := 0) (i := i) hg (by omega)
27  unfold OkOn at e
28  unfold getDl
29  rw [bind_app, e]
30  simp
31
32theorem setFc_gen (hg : Space.get h r = some a) (hro : Space.ro h r = false) (hi : i < a.size) (v : UInt16) :
33    setFc (.ref r 0) (i : Int) v h = .ok ((), Space.put h r (a.set! i { a[i] with fc := v })) := by
34  have e1 := Ptr.add_nat_ok (off := 0) (n := i) hg (by omega)
35  have e2 := Ptr.load_ok (off := 0 + i) hg (by omega)
36  have e3 := Ptr.store_ok (v := ({ a[0 + i] with fc := v } : CtData)) (off := 0 + i) hg hro (by omega)
37  unfold OkOn at e1 e2
38  unfold setFc
39  rw [bind_app, e1]
40  simp only []
41  rw [bind_app, e2]
42  simp only []
43  rw [e3]
44  simp
45
46theorem setDl_gen (hg : Space.get h r = some a) (hro : Space.ro h r = false) (hi : i < a.size) (v : UInt16) :
47    setDl (.ref r 0) (i : Int) v h = .ok ((), Space.put h r (a.set! i { a[i] with dl := v })) := by
48  have e1 := Ptr.add_nat_ok (off := 0) (n := i) hg (by omega)
49  have e2 := Ptr.load_ok (off := 0 + i) hg (by omega)
50  have e3 := Ptr.store_ok (v := ({ a[0 + i] with dl := v } : CtData)) (off := 0 + i) hg hro (by omega)
51  unfold OkOn at e1 e2
52  unfold setDl
53  rw [bind_app, e1]
54  simp only []
55  rw [bind_app, e2]
56  simp only []
57  rw [e3]
58  simp
59
60end generic
61
62
63theorem getElem!_set! {α : Type} [Inhabited α] (a : Array α) (i j : Nat) (v : α) :
64    (a.set! i v)[j]! = if i = j ∧ i < a.size then v else a[j]! := by
65  rw [Array.getElem!_eq_getD, Array.getElem!_eq_getD, Array.set!_eq_setIfInBounds, Array.getD_eq_getD_getElem?,
66    Array.getD_eq_getD_getElem?, Array.getElem?_setIfInBounds]
67  by_cases h1 : i = j
68  · subst h1; by_cases h2 : i < a.size <;> simp [h2]
69  · simp [h1]
70
71theorem getElem!_ge {α : Type} [Inhabited α] (a : Array α) (n : Nat) (h : a.size ≤ n) : a[n]! = default := by
72  rw [Array.getElem!_eq_getD, Array.getD_eq_getD_getElem?, Array.getElem?_eq_none h]; rfl
73
74/-- The three code arrays of the deflate record. -/
75inductive Sel where
76  | l | d | bl
77  deriving DecidableEq
78
79/-- The reference to the array. -/
80def Sel.ref (s : Sel) (id : Nat) : CtDataRef :=
81  match s with
82  | .l => .dstate_dyn_ltree id
83  | .d => .dstate_dyn_dtree id
84  | .bl => .dstate_bl_tree id
85
86/-- The array in the record. -/
87def Sel.arr (s : Sel) (d : DeflateState) : Array CtData :=
88  match s with
89  | .l => d.dyn_ltree
90  | .d => d.dyn_dtree
91  | .bl => d.bl_tree
92
93/-- The record with the array replaced. -/
94def Sel.upd (s : Sel) (d : DeflateState) (a : Array CtData) : DeflateState :=
95  match s with
96  | .l => { d with dyn_ltree := a }
97  | .d => { d with dyn_dtree := a }
98  | .bl => { d with bl_tree := a }
99
100/-- The size of the array in the C declaration. -/
101def Sel.size (s : Sel) : Nat :=
102  match s with
103  | .l => 573
104  | .d => 61
105  | .bl => 39
106
107theorem Sel.get_ref {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) (s : Sel) :
108    Space.get h (s.ref id) = some (s.arr d) := by
109  cases s <;> simp [Sel.ref, Sel.arr, Space.get, e]
110
111theorem Sel.ro_ref (h : Heap) (id : Nat) (s : Sel) : Space.ro h (s.ref id) = false := by
112  cases s <;> rfl
113
114theorem Sel.put_ref {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) (s : Sel) (a : Array CtData) :
115    Space.put h (s.ref id) a = setD h id (s.upd d a) := by
116  cases s <;> simp [Sel.ref, Sel.upd, Space.put, e, setD]
117
118theorem Sel.size_arr {d : DeflateState} (hw : d.WellFormed) (s : Sel) : (s.arr d).size = s.size := by
119  obtain ⟨h1, h2, h3, -⟩ := hw
120  cases s <;> simp [Sel.arr, Sel.size, h1, h2, h3]
121
122theorem Sel.wf_upd {d : DeflateState} (hw : d.WellFormed) (s : Sel) (a : Array CtData) (ha : a.size = s.size) :
123    (s.upd d a).WellFormed := by
124  obtain ⟨h1, h2, h3, h4, h5, h6⟩ := hw
125  cases s <;> simp_all [Sel.upd, Sel.size, DeflateState.WellFormed]
126
127theorem Sel.arr_upd (s : Sel) (d : DeflateState) (a : Array CtData) : s.arr (s.upd d a) = a := by
128  cases s <;> rfl
129
130theorem Sel.upd_arr (s : Sel) (d : DeflateState) : s.upd d (s.arr d) = d := by
131  cases s <;> rfl
132
133theorem Sel.upd_upd (s : Sel) (d : DeflateState) (a a' : Array CtData) : s.upd (s.upd d a) a' = s.upd d a' := by
134  cases s <;> rfl
135
136theorem getFc_sel {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) (s : Sel) {i : Nat}
137    (hi : i < (s.arr d).size) :
138    getFc (.ref (s.ref id) 0) (i : Int) h = .ok (((s.arr d)[i]!).fc, h) := by
139  rw [getElem!_pos (s.arr d) i hi]; exact getFc_gen (Sel.get_ref e s) hi
140
141theorem getDl_sel {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) (s : Sel) {i : Nat}
142    (hi : i < (s.arr d).size) :
143    getDl (.ref (s.ref id) 0) (i : Int) h = .ok (((s.arr d)[i]!).dl, h) := by
144  rw [getElem!_pos (s.arr d) i hi]; exact getDl_gen (Sel.get_ref e s) hi
145
146theorem setFc_sel {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) (s : Sel) {i : Nat}
147    (hi : i < (s.arr d).size) (v : UInt16) :
148    setFc (.ref (s.ref id) 0) (i : Int) v h =
149      .ok ((), setD h id (s.upd d ((s.arr d).set! i { (s.arr d)[i]! with fc := v }))) := by
150  rw [getElem!_pos (s.arr d) i hi, setFc_gen (Sel.get_ref e s) (Sel.ro_ref h id s) hi, Sel.put_ref e]
151
152theorem setDl_sel {h : Heap} {id : Nat} {d : DeflateState} (e : h.dstates id = some d) (s : Sel) {i : Nat}
153    (hi : i < (s.arr d).size) (v : UInt16) :
154    setDl (.ref (s.ref id) 0) (i : Int) v h =
155      .ok ((), setD h id (s.upd d ((s.arr d).set! i { (s.arr d)[i]! with dl := v }))) := by
156  rw [getElem!_pos (s.arr d) i hi, setDl_gen (Sel.get_ref e s) (Sel.ro_ref h id s) hi, Sel.put_ref e]
157
158theorem TreesBase.treeUpd {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
159    (hb : TreesBase h id d b buf) (s : Sel) (a : Array CtData) (ha : a.size = s.size) :
160    TreesBase (setD h id (s.upd d a)) id (s.upd d a) b buf := by
161  refine ⟨setD_dstates_same _ _ _, Sel.wf_upd hb.wf s a ha, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
162  all_goals first
163    | (cases s <;> simpa [Sel.upd] using hb.static)
164    | (cases s <;> simpa [Sel.upd] using hb.pbuf)
165    | (cases s <;> simpa [Sel.upd] using hb.bytes)
166    | (cases s <;> simpa [Sel.upd] using hb.rw)
167    | (cases s <;> simpa [Sel.upd] using hb.size)
168    | (cases s <;> simpa [Sel.upd] using hb.psize)
169    | (cases s <;> simpa [Sel.upd] using hb.sym)
170    | (cases s <;> simpa [Sel.upd] using hb.lit_lo)
171    | (cases s <;> simpa [Sel.upd] using hb.lit_hi)
172    | (cases s <;> simpa [Sel.upd] using hb.sym_end)
173    | (cases s <;> simpa [Sel.upd] using hb.pending_le)
174
175theorem TreesRun.treeUpd {id : Nat} {d : DeflateState} (hr : TreesRun id d) (s : Sel) (a : Array CtData) :
176    TreesRun id (s.upd d a) := by
177  cases s <;> exact ⟨hr.ldyn, hr.lstat, hr.ddyn, hr.dstat, hr.bldyn, hr.blstat, hr.bi_lo, hr.bi_hi, hr.bi_buf,
178    hr.sym_next_le, hr.sym_next_mod⟩
179
180theorem TreesInvAt.treeUpd {h : Heap} {id : Nat} {d : DeflateState} {b : Nat} {buf : Array UInt8}
181    (hI : TreesInvAt h id d b buf) (s : Sel) (a : Array CtData) (ha : a.size = s.size) :
182    TreesInvAt (setD h id (s.upd d a)) id (s.upd d a) b buf :=
183  ⟨hI.base.treeUpd s a ha, hI.run.treeUpd s a⟩
184
185end Zlib.Trees.Proofs.Out