1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8 * Proofs regarding the State Translation.
9 *)
10
11theory StateTranslationProofs_DR
12imports StateTranslation_D
13begin
14
15context begin interpretation Arch . (*FIXME: arch_split*)
16
17declare transform_current_domain_def [simp]
18
19lemma asid_high_bits [simp]:
20  "Types_D.asid_high_bits = asid_high_bits"
21  by (simp add:Types_D.asid_high_bits_def asid_high_bits_def)
22
23lemma asid_low_bits [simp]:
24  "Types_D.asid_low_bits = asid_low_bits"
25  by (simp add:Types_D.asid_low_bits_def asid_low_bits_def)
26
27lemma asid_bits [simp]:
28  "Types_D.asid_bits = asid_bits"
29  by (simp add:Types_D.asid_bits_def asid_bits_def)
30
31lemma get_obj_simps [simp]:
32  "get_obj (s\<lparr>cur_thread := a\<rparr>) = get_obj s"
33  apply (rule ext)
34  apply (clarsimp simp: get_obj_def)
35  done
36
37lemma transform_objects_simps [simp]:
38  "transform_objects (s\<lparr>cur_thread := a\<rparr>) = transform_objects s"
39  apply (rule ext)
40  apply (clarsimp simp: transform_objects_def transform_object_def)
41  done
42
43lemma transform_cdt_simps [simp]:
44  "transform_cdt (s\<lparr>cur_thread := a\<rparr>) = transform_cdt s"
45  apply (rule ext)+
46  apply (clarsimp simp: transform_cdt_def split_def)
47  done
48
49(* Aggressive simp rules, using explictly *)
50abbreviation
51"update_machine ms s \<equiv> machine_state_update (\<lambda>_. ms) s"
52
53abbreviation
54"update_kheap kh s \<equiv> kheap_update (\<lambda>_. kh) s"
55
56abbreviation
57"tcb_set_mi tcb msg \<equiv> tcb \<lparr>tcb_context := (tcb_context tcb)(msg_info_register := msg)\<rparr>"
58
59abbreviation
60"update_tcb_cxt_badge msg tcb\<equiv> tcb \<lparr>tcb_context := (tcb_context tcb)(badge_register := msg)\<rparr>"
61
62abbreviation
63"update_tcb_state state tcb \<equiv> tcb \<lparr>tcb_state := state\<rparr>"
64
65abbreviation
66"update_tcb_boundntfn ntfn_opt tcb \<equiv> tcb \<lparr>tcb_bound_notification := ntfn_opt\<rparr>"
67
68abbreviation
69"dupdate_cdl_object ptr obj s \<equiv>  cdl_objects_update (\<lambda>_. cdl_objects s(ptr \<mapsto> obj)) s"
70
71abbreviation
72"dupdate_tcb_intent intent tcb\<equiv> tcb \<lparr>cdl_tcb_intent := intent\<rparr>"
73
74lemma update_kheap_triv[simp]:
75  "kheap s y = Some obj\<Longrightarrow> update_kheap ((kheap s)(y \<mapsto> obj)) s = s"
76  apply (case_tac s,clarsimp)
77  apply (rule ext,clarsimp)
78done
79
80lemma msg_registers_lt_msg_max_length [simp]:
81  "length msg_registers < msg_max_length"
82  by (simp add: msg_registers_def msgRegisters_def upto_enum_def
83                fromEnum_def enum_register msg_max_length_def)
84
85lemma get_tcb_mrs_update_state :
86  "get_tcb_mrs ms (tcb_state_update f tcb) = get_tcb_mrs ms tcb"
87  by (clarsimp simp:get_tcb_mrs_def Suc_le_eq get_tcb_message_info_def get_ipc_buffer_words_def)
88
89lemma msg_info_badge_register_no_overlap:
90  "badge_register \<noteq> msg_info_register"
91  by (clarsimp simp:badge_register_def msg_info_register_def
92    ARM.badgeRegister_def
93                  ARM.msgInfoRegister_def)
94
95lemma badge_cap_register_overlap:
96  "badge_register = cap_register"
97by (clarsimp simp:badge_register_def cap_register_def
98                  ARM.badgeRegister_def
99                  ARM.capRegister_def)
100
101lemma cap_msg_info_register_no_overlap:
102  "cap_register \<noteq> msg_info_register"
103by (clarsimp simp:msg_info_register_def cap_register_def
104                  ARM.msgInfoRegister_def
105                  ARM.capRegister_def)
106
107lemmas register_overlap_check = msg_info_badge_register_no_overlap
108                                cap_msg_info_register_no_overlap
109                                badge_cap_register_overlap
110
111lemma transform_full_intent_cong:
112  "\<lbrakk>ms = ms'; ptr = ptr';
113    arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb');
114    tcb_ipc_buffer tcb = tcb_ipc_buffer tcb'; tcb_ipcframe tcb = tcb_ipcframe tcb'\<rbrakk>
115  \<Longrightarrow> transform_full_intent ms ptr tcb = transform_full_intent ms' ptr' tcb'"
116  by (simp add: transform_full_intent_def get_tcb_message_info_def get_tcb_mrs_def Suc_le_eq get_ipc_buffer_words_def)
117
118lemma caps_of_state_eq_lift:
119  "\<forall>cap. cte_wp_at ((=) cap) p s = cte_wp_at ((=) cap) p s' \<Longrightarrow>  caps_of_state s p = caps_of_state s' p"
120  apply (simp add:cte_wp_at_def caps_of_state_def)
121  done
122
123lemma caps_of_state_irrelavent_simp:
124  "ref \<noteq> epptr \<Longrightarrow> caps_of_state (update_kheap (kh(epptr \<mapsto> obj)) s) (ref, cref) = caps_of_state (update_kheap kh s) (ref, cref)"
125  apply (rule caps_of_state_eq_lift)
126  apply (clarsimp simp: cte_wp_at_cases)
127  done
128
129(* This doesn't satisfy the obvious transformation into capDL because of
130   pagetables etc. *)
131fun
132   caps_of_object :: "kernel_object \<Rightarrow> (bool list \<rightharpoonup> cap)"
133where
134    "caps_of_object (Structures_A.CNode sz c) = (if well_formed_cnode_n sz c then c else Map.empty)"
135  | "caps_of_object (Structures_A.TCB t) = (\<lambda>n. option_map (\<lambda>(f, _). f t) (tcb_cap_cases n))"
136  | "caps_of_object _                    = Map.empty"
137
138lemma caps_of_state_def2:
139  "caps_of_state s = (\<lambda>ptr. case (option_map caps_of_object (kheap s (fst ptr))) of
140                                None \<Rightarrow> None
141                              | Some f \<Rightarrow> f (snd ptr))"
142  unfolding caps_of_state_def get_cap_def tcb_cnode_map_def
143  apply (rule ext)
144  apply (clarsimp simp add: split_def get_object_def bind_def gets_def get_def return_def assert_def fail_def)
145  apply (case_tac y, simp_all add: bind_def assert_def return_def assert_opt_def fail_def tcb_cap_cases_def
146                              split: option.splits)
147  done
148
149lemma caps_of_state_update_same_caps:
150  assumes kh: "kh ptr = Some ko"
151  and    coo: "caps_of_object ko' = caps_of_object ko"
152  shows  "caps_of_state (update_kheap (kh(ptr \<mapsto> ko')) s) = caps_of_state (update_kheap kh s)"
153  using kh coo
154  apply -
155  apply (rule ext)
156  apply (clarsimp simp add: caps_of_state_def2)
157  done
158
159lemma caps_of_state_update_tcb:
160  "\<lbrakk> kh thread = Some (TCB tcb);
161     (tcb_ctable tcb) =  (tcb_ctable (f tcb));
162     (tcb_vtable tcb) =  (tcb_vtable (f tcb));
163     (tcb_reply tcb) =  (tcb_reply (f tcb));
164     (tcb_caller tcb) =  (tcb_caller (f tcb));
165     (tcb_ipcframe tcb) =  (tcb_ipcframe (f tcb)) \<rbrakk>
166    \<Longrightarrow>
167      caps_of_state (update_kheap (kh(thread \<mapsto> (TCB (f tcb)))) s) =
168      caps_of_state (update_kheap kh s)"
169  apply (erule caps_of_state_update_same_caps)
170  apply (rule ext)
171  apply (simp add: tcb_cap_cases_def split: if_split)
172  done
173
174lemmas caps_of_state_upds = caps_of_state_update_tcb caps_of_state_update_same_caps
175
176lemma transform_cdt_kheap_update [simp]:
177  "transform_cdt (kheap_update f s) = transform_cdt s"
178  by (clarsimp simp: transform_cdt_def)
179
180lemma transform_cdt_update_machine [simp]:
181  "transform_cdt (update_machine ms s) = transform_cdt s "
182  by (clarsimp simp: transform_cdt_def)
183
184lemma transform_cdt_update_original_cap [simp]:
185  "transform_cdt (b\<lparr>is_original_cap := x\<rparr>) = transform_cdt b"
186  by (clarsimp simp: transform_cdt_def)
187
188lemma transform_asid_table_kheap_update [simp]:
189  "transform_asid_table (kheap_update f s) = transform_asid_table s"
190  by (clarsimp simp: transform_asid_table_def)
191
192lemma transform_asid_table_update_machine [simp]:
193  "transform_asid_table (update_machine ms s) = transform_asid_table s "
194  by (clarsimp simp: transform_asid_table_def)
195
196lemma transform_asid_table_update_original_cap [simp]:
197  "transform_asid_table (b\<lparr>is_original_cap := x\<rparr>) = transform_asid_table b"
198  by (clarsimp simp: transform_asid_table_def)
199
200lemma transform_objects_update_kheap_same_caps:
201  "\<lbrakk> kh ptr = Some ko; caps_of_object ko' = caps_of_object ko; a_type ko' = a_type ko\<rbrakk> \<Longrightarrow>
202  transform_objects (update_kheap (kh(ptr \<mapsto> ko')) s) =
203  (if ptr = idle_thread s then
204         transform_objects (update_kheap kh s)
205  else
206         (transform_objects (update_kheap kh s))(ptr \<mapsto> transform_object (machine_state s) ptr (ekheap s ptr) ko'))"
207  unfolding transform_objects_def
208  apply (rule ext)
209  apply (simp add: map_option_case restrict_map_def map_add_def )
210  done
211
212lemma transform_objects_update_same:
213  "\<lbrakk> kheap s ptr = Some ko; transform_object (machine_state s) ptr (ekheap s ptr) ko = ko'; ptr \<noteq> idle_thread s \<rbrakk>
214  \<Longrightarrow> (transform_objects s)(ptr \<mapsto> ko') = transform_objects s"
215  unfolding transform_objects_def
216  by (rule ext) (simp)
217
218text \<open>Facts about map_lift_over\<close>
219
220lemma map_lift_over_eq_Some:
221  "(map_lift_over f m x = Some y)
222         = (\<exists>x' y'. x = f x' \<and> y = f y' \<and> inj_on f (dom m \<union> ran m)
223                   \<and> m x' = Some y')"
224proof -
225  have P: "inj_on f (dom m \<union> ran m) \<longrightarrow> inj_on f (dom m)"
226    by (auto elim: subset_inj_on)
227  have Q: "\<And>x y. \<lbrakk> m x = Some y; inj_on f (dom m \<union> ran m) \<rbrakk>
228                  \<Longrightarrow> inv_into (dom m) f (f x) = x"
229    using P
230    by (blast intro: inv_into_f_f)
231  show ?thesis
232    by (auto simp add: map_lift_over_def Q)
233qed
234
235lemma map_lift_over_eq_None:
236  "(map_lift_over f m x = None)
237         = (inj_on f (dom m \<union> ran m) \<longrightarrow>
238                (\<forall>x'. x = f x' \<longrightarrow> m x' = None))"
239proof -
240  have P: "inj_on f (dom m \<union> ran m) \<Longrightarrow> inj_on f (dom m)"
241    by (auto elim: subset_inj_on)
242  show ?thesis
243    by (auto simp add: map_lift_over_def P[THEN inv_into_f_f] domI
244                       inj_on_eq_iff[where f=f]
245           | rule ccontr[where P="v = None" for v])+
246qed
247
248lemma map_lift_over_f_eq:
249  "inj_on f ({x} \<union> dom m \<union> ran m) \<Longrightarrow>
250   (map_lift_over f m (f x) = v) = (v = map_option f (m x))"
251  apply (cases v, simp_all add: map_lift_over_eq_None map_lift_over_eq_Some)
252   apply (auto simp: option_map_def split: option.split)
253  done
254
255lemma map_lift_over_eq_cases[unfolded map_lift_over_eq_None map_lift_over_eq_Some]:
256  "(map_lift_over f m x = v)
257       = (case v of None \<Rightarrow> map_lift_over f m x = None
258                | Some z \<Rightarrow> map_lift_over f m x = Some z)"
259  by (simp split: option.split)
260
261lemma map_lift_over_upd:
262  assumes inj_f: "inj_on f ({x} \<union> set_option y \<union> dom m \<union> ran m)"
263  shows "(map_lift_over f (m(x := y)))
264           = ((map_lift_over f m) (f x := map_option f y))"
265proof -
266  have Q: "inj_on f (dom m \<union> ran m)"
267      "inj_on f (insert x (dom m \<union> ran (m(x := y))))"
268      "inj_on f (dom m)"
269      "inj_on f (insert x (dom m))"
270      "inj_on f (dom m - {x} \<union> ran (m(x := None)))"
271      "inj_on f (dom m - {x})"
272    apply (safe intro!: subset_inj_on[OF inj_f])
273    apply (auto simp: ran_def split: if_split_asm)
274    done
275  show ?thesis
276    apply (simp add: map_lift_over_def Q del: inj_on_insert)
277    apply (safe; rule ext; simp add: Q[THEN inv_into_f_f] domI cong del: imp_cong)
278     apply (auto simp add: Q[THEN inv_into_f_f] domI inj_on_eq_iff[OF inj_f] ranI
279                 simp del: inj_on_insert)
280    done
281qed
282
283lemma map_lift_over_if_eq_twice:
284  assumes inj_f: "inj_on f (dom m \<union> ran m \<union> {y, y'} \<union> set_option z \<union> set_option z')"
285  shows
286  "map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y' then z' else m x)
287       = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z
288              else if map_lift_over f m x = Some (f y') then map_option f z'
289              else map_lift_over f m x)"
290  (is "map_lift_over f ?ifeq = ?rhs")
291proof -
292  from inj_f
293  have 1: "inj_on f (dom m \<union> ran m)" "inj_on f (dom m)"
294    by (auto simp: inj_on_Un)
295  have "dom ?ifeq \<subseteq> dom m"
296    by (auto split: if_split_asm)
297  with inj_f
298  have 2: "inj_on f (dom ?ifeq)"
299    by (auto elim!: subset_inj_on)
300  have "dom ?ifeq \<union> ran ?ifeq \<subseteq> dom m \<union> ran m \<union> set_option z \<union> set_option z'"
301    by (auto simp: ran_def)
302  with inj_f
303  have "inj_on f (dom ?ifeq \<union> ran ?ifeq)"
304    by (auto elim!: subset_inj_on)
305  note Q = 1 2 this
306  note if_split[split del] if_cong[cong]
307  show ?thesis
308    apply (simp add: map_lift_over_def Q)
309    apply (rule ext)
310    apply (case_tac "x \<in> f ` dom ?ifeq")
311     apply clarsimp
312     apply (subst if_P, fastforce split: if_split_asm)+
313     apply (simp add: Q[THEN inv_into_f_f] domI ranI inj_on_eq_iff[OF inj_f]
314               split: if_split_asm)
315    apply (subst if_not_P, simp, rule allI, fastforce)+
316    apply (auto simp: option_map_def Q[THEN inv_into_f_f] domI ranI
317                      inj_on_eq_iff[OF inj_f]
318               split: if_split option.split)
319    done
320qed
321
322lemma map_lift_over_if_eq:
323  assumes inj_f: "inj_on f (dom m \<union> ran m \<union> {y} \<union> set_option z)"
324  shows
325  "map_lift_over f (\<lambda>x. if m x = Some y then z else m x)
326       = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z
327              else map_lift_over f m x)"
328  using inj_f map_lift_over_if_eq_twice[where f=f and m=m and y=y and z=z and y'=y and z'=z]
329  apply (simp del: inj_on_insert)
330  done
331
332end
333
334end
335