Space.lean

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

1/-!
2# Runtime: the parts that do not mention the heap
3
4Trusted base of every translation; see `docs/trusted-base.md`. The heap itself is generated
5(`Schema.lean`, from the C headers). This file holds what the generated file builds on:
6
7* `upd`, the update of a table (a function from block numbers);
8* `Ptr R`, a pointer into an array: null, or the array (`R` says where it lives) and an index;
9* `Space`, which says how the heap stores the arrays of a reference type `R`;
10* `FnPtr`, a function pointer as a name;
11* `Junk`, the value of an uninitialised integer.
12-/
13
14namespace C
15
16/-- A table of the heap: the objects of one kind by block number, as an `Array`, so that code which uses the heap
17linearly updates it in place (`Tbl.modify`). Proofs see it as the function `Tbl.get t : Nat → α` (a coercion): entry
18`k` is `t.arr[k]` if that exists and `default` otherwise (`none` for a table of objects, `false` for the read-only
19flags). `upd` is the update; `upd_same`, `upd_ne`, `upd_upd`, `upd_self` are its rules. -/
20structure Tbl (α : Type) [Inhabited α] where
21  arr : Array α
22
23namespace Tbl
24variable {α : Type} [Inhabited α]
25
26/-- The entry `k`: `t.arr[k]`, or `default` beyond the end. -/
27def get (t : Tbl α) (k : Nat) : α := t.arr.getD k default
28instance : CoeFun (Tbl α) (fun _ => Nat → α) := ⟨Tbl.get⟩
29
30/-- The table with every entry `default`. -/
31def empty : Tbl α := ⟨#[]⟩
32
33instance : Inhabited (Tbl α) := ⟨empty⟩
34/-- `t` with the entry `k` replaced by `v` (the table grows when `k` is beyond its end). -/
35def set (t : Tbl α) (k : Nat) (v : α) : Tbl α :=
36  if k < t.arr.size then ⟨t.arr.set! k v⟩ else ⟨(t.arr ++ Array.replicate (k - t.arr.size) default).push v⟩
37/-- `t` with the entry `k` changed by `f`. The entry is taken out of the array, changed and put back, so it is
38updated in place when `t` and the entry are not shared. No change when `k` is beyond the end. -/
39def modify (t : Tbl α) (k : Nat) (f : α → α) : Tbl α := ⟨t.arr.modify k f⟩
40
41theorem get_eq (t : Tbl α) (k : Nat) : t.get k = (t.arr[k]?).getD default := by
42  simp [get, Array.getD_eq_getD_getElem?]
43
44theorem get_set (t : Tbl α) (k : Nat) (v : α) (x : Nat) :
45    (t.set k v).get x = if x = k then v else t.get x := by
46  unfold set
47  split
48  · rename_i h
49    simp [get_eq, Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds]
50    split <;> simp_all [eq_comm]
51  · rename_i h
52    simp only [get_eq]
53    simp [Array.getElem?_push, Array.getElem?_append, Array.getElem?_replicate]
54    by_cases h1 : x < t.arr.size
55    · have : x ≠ k := by omega
56      simp [h1, this]
57    · by_cases h2 : x = k
58      · subst h2; simp [h1]
59      · simp [h1, h2]
60        have h3 : x - t.arr.size ≠ k - t.arr.size := by omega
61        simp [h3]
62        split <;> simp
63
64theorem get_empty (k : Nat) : (empty : Tbl α).get k = default := by
65  simp [get_eq, empty]
66
67@[simp] theorem get_empty_opt {β : Type} (k : Nat) : (empty : Tbl (Option β)).get k = none := by
68  simp [get_eq, empty]
69  rfl
70
71@[simp] theorem get_empty_bool (k : Nat) : (empty : Tbl Bool).get k = false := by
72  simp [get_eq, empty]
73
74theorem lt_size_of_get_ne (t : Tbl α) (k : Nat) (h : t.get k ≠ default) : k < t.arr.size := by
75  by_cases hc : k < t.arr.size
76  · exact hc
77  · exfalso
78    apply h
79    simp [get_eq, Array.getElem?_eq_none (by omega : t.arr.size ≤ k)]
80
81theorem modify_eq (t : Tbl α) (k : Nat) (f : α → α) (hk : k < t.arr.size) :
82    t.modify k f = t.set k (f (t.get k)) := by
83  unfold modify set
84  simp only [hk, ite_true]
85  congr 1
86  apply Array.ext_getElem?
87  intro i
88  simp [Array.getElem?_modify, Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds, get_eq, hk]
89  split
90  · rename_i hki
91    subst hki
92    simp [Array.getElem?_eq_getElem hk]
93  · simp_all
94
95theorem set_self (t : Tbl α) (k : Nat) (hk : k < t.arr.size) : t.set k (t.get k) = t := by
96  obtain ⟨arr⟩ := t
97  have hk' : k < arr.size := hk
98  unfold set
99  simp only [hk', ite_true]
100  simp only [Tbl.mk.injEq]
101  apply Array.ext_getElem?
102  intro i
103  simp [Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds, get_eq]
104  intro hki
105  subst hki
106  simp [hk', Array.getElem?_eq_getElem hk']
107
108theorem set_set (t : Tbl α) (k : Nat) (v v' : α) : (t.set k v).set k v' = t.set k v' := by
109  unfold set
110  split
111  · rename_i h
112    simp only [h, ite_true, Array.size_setIfInBounds, Array.set!_eq_setIfInBounds]
113    congr 1
114    apply Array.ext_getElem?
115    intro i
116    simp [Array.getElem?_setIfInBounds]
117  · rename_i h
118    have h2 : k < ((t.arr ++ Array.replicate (k - t.arr.size) default).push v).size := by simp; omega
119    simp only [h2, ite_true, Array.set!_eq_setIfInBounds]
120    congr 1
121    apply Array.ext_getElem?
122    intro i
123    simp [Array.getElem?_setIfInBounds, Array.getElem?_push, Array.getElem?_append]
124    by_cases hki : k = i
125    · subst hki
126      have h4 : k < t.arr.size + (k - t.arr.size + 1) := by omega
127      simp [h4, h]
128    · simp only [hki, ite_false]
129      by_cases h1 : i < t.arr.size
130      · simp [h1]
131      · have h3 : i - t.arr.size ≠ k - t.arr.size := by omega
132        simp [h1, h3]
133
134end Tbl
135/-- `t` with the entry `k` replaced by `v`: the update of a table of the heap. -/
136def upd {α : Type} [Inhabited α] (t : Tbl α) (k : Nat) (v : α) : Tbl α := t.set k v
137
138@[simp] theorem upd_same {α : Type} [Inhabited α] (t : Tbl α) (k : Nat) (v : α) : upd t k v k = v := by
139  have := Tbl.get_set t k v k
140  simpa [upd] using this
141@[simp] theorem upd_ne {α : Type} [Inhabited α] (t : Tbl α) (k : Nat) (v : α) (x : Nat) (h : x ≠ k) :
142    upd t k v x = t x := by
143  have := Tbl.get_set t k v x
144  simpa [upd, h] using this
145/-- The update as a function: the new value at `k`, the old table elsewhere. -/
146theorem upd_apply {α : Type} [Inhabited α] (t : Tbl α) (k : Nat) (v : α) (x : Nat) :
147    upd t k v x = if x = k then v else t x := by
148  have := Tbl.get_set t k v x
149  simpa [upd] using this
150
151theorem upd_upd {α : Type} [Inhabited α] (t : Tbl α) (k : Nat) (v v' : α) : upd (upd t k v) k v' = upd t k v' :=
152  Tbl.set_set t k v v'
153theorem upd_self {α : Type} (t : Tbl (Option α)) (k : Nat) (a : α) (hf : t k = some a) :
154    upd t k (some a) = t := by
155  have hk : k < t.arr.size := Tbl.lt_size_of_get_ne t k (by simp [Tbl.get] at hf ⊢; simp [hf])
156  have := Tbl.set_self t k hk
157  rw [show t.get k = some a from hf] at this
158  exact this
159
160/-- Changing an entry that holds `a` in place is the same as replacing it. -/
161theorem Tbl.modify_opt {β : Type} (t : Tbl (Option β)) (k : Nat) (g : β → β) (a : β) (hg : t k = some a) :
162    t.modify k (Option.map g) = upd t k (some (g a)) := by
163  have hk : k < t.arr.size := Tbl.lt_size_of_get_ne t k (by simp [Tbl.get] at hg ⊢; simp [hg])
164  rw [Tbl.modify_eq t k _ hk]
165  simp [upd, show t.get k = some a from hg]
166
167
168/-- A pointer into an array: null, or the array (`R` says where it lives: a heap block, an array inside a
169struct, a static table) and an index. There is no address. One past the end is a valid pointer. -/
170inductive Ptr (R : Type) where
171  | null
172  | ref (r : R) (off : Nat)
173  deriving DecidableEq
174
175instance {R : Type} : Inhabited (Ptr R) := ⟨.null⟩
176
177/-- How the heap stores the arrays that the reference type `R` denotes. `get h r` is the array (if it is live),
178`put h r a` the heap with that array replaced, `ro h r` says that the array is read-only. `modify h r f` is the heap
179with the array changed by `f`: the same as `put h r (f a)` (`modify_eq`) for a live array `a`, and it is what the
180primitives that write (`Ptr.store`, `Ptr.memcpy`, `Ptr.fill`) use, because it takes the array out of its table, so
181that `f` updates it in place when the heap is not shared. -/
182class Space (H : Type) (R : Type) (T : outParam Type) where
183  get : H → R → Option (Array T)
184  put : H → R → Array T → H
185  ro : H → R → Bool
186  modify : H → R → (Array T → Array T) → H
187  modify_eq : ∀ h r a f, get h r = some a → modify h r f = put h r (f a)
188
189/-- A function pointer: null, or the name of the function. -/
190inductive FnPtr where
191  | null
192  | fn (name : String)
193  deriving DecidableEq, Inhabited
194
195/-- The value of an uninitialised integer of type `T`, given an arbitrary 64-bit pattern. -/
196class Junk (T : Type) where
197  of : UInt64 → T
198
199instance : Junk UInt8 := ⟨UInt64.toUInt8⟩
200instance : Junk UInt16 := ⟨UInt64.toUInt16⟩
201instance : Junk UInt32 := ⟨UInt64.toUInt32⟩
202instance : Junk UInt64 := ⟨id⟩
203instance : Junk Int8 := ⟨fun x => x.toUInt8.toInt8⟩
204instance : Junk Int16 := ⟨fun x => x.toUInt16.toInt16⟩
205instance : Junk Int32 := ⟨fun x => x.toUInt32.toInt32⟩
206instance : Junk Int64 := ⟨UInt64.toInt64⟩
207
208end C