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