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