theory ArchArch_AC

lemma delete_asid_pas_refined[wp]:
  "delete_asid asid pd \<lbrace>pas_refined aag\<rbrace>" apply (simp add: delete_asid_def) apply (wp | wpc)+ apply (clarsimp simp add: split_def Ball_def obj_at_def) apply (rule conjI) apply (clarsimp dest!: auth_graph_map_memD graph_ofD) apply (erule pas_refined_mem[OF sta_vref, rotated]) apply (fastforce simp: state_vrefs_def vs_refs_no_global_pts_def
                         image_def graph_of_def split: if_split_asm) apply (clarsimp simp: pas_refined_def dest!: graph_ofD) apply (erule subsetD, erule state_asids_to_policy_aux.intros) apply (fastforce simp: state_vrefs_def vs_refs_no_global_pts_def
                        graph_of_def image_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> delete_asid asid pd \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag\<rbrace> do asid_table <- gets (arm_asid_table \<circ> arch_state);
case asid_table (asid_high_bits_of asid) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) asid) = Some pd) (do y <- flush_space asid;
y <- invalidate_asid_entry asid;
y <- set_asid_pool pool_ptr (pool(UCAST(32 \<rightarrow> 10) asid := None));
gets cur_thread >>= set_vm_root
od)
od
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<Longrightarrow> ((arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = None \<longrightarrow> pas_refined aag s) \<and> (\<forall>x. (arm_asid_table \<circ> arch_state) s (asid_high_bits_of asid) = Some x \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) x s \<longrightarrow> (if pool (UCAST(32 \<rightarrow> 10) asid) = Some pd then \<lambda>s. pas_refined aag s \<and> (\<forall>a\<in>graph_of (pool(UCAST(32 \<rightarrow> 10) asid := None)). case a of (xa, y) \<Rightarrow> auth_graph_map (pasObjectAbs aag) {(x, Control, y)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some x \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) xa \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag y) \<in> pasPolicy aag)) else pas_refined aag) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x pool a b. \<lbrakk>pas_refined aag s; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; kheap s x = Some (ArchObj (ASIDPool pool)); (a, b) \<in> graph_of (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) asid then None else pool a)\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(x, Control, b)} \<subseteq> pasPolicy aag \<and> (\<forall>asid. asid_table s (asid_high_bits_of asid) = Some x \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag b) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>s x pool a b. \<lbrakk>pas_refined aag s; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; kheap s x = Some (ArchObj (ASIDPool pool)); (a, b) \<in> graph_of (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) asid then None else pool a)\<rbrakk> \<Longrightarrow> auth_graph_map (pasObjectAbs aag) {(x, Control, b)} \<subseteq> pasPolicy aag
 2. \<And>s x pool a b. \<lbrakk>pas_refined aag s; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; kheap s x = Some (ArchObj (ASIDPool pool)); (a, b) \<in> graph_of (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) asid then None else pool a)\<rbrakk> \<Longrightarrow> \<forall>asid. asid_table s (asid_high_bits_of asid) = Some x \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag b) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s x pool a b. \<lbrakk>pas_refined aag s; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; kheap s x = Some (ArchObj (ASIDPool pool)); (if a = UCAST(32 \<rightarrow> 10) asid then None else pool a) = Some b\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Control, pasObjectAbs aag b) \<in> pasPolicy aag
 2. \<And>s x pool a b. \<lbrakk>pas_refined aag s; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; kheap s x = Some (ArchObj (ASIDPool pool)); (a, b) \<in> graph_of (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) asid then None else pool a)\<rbrakk> \<Longrightarrow> \<forall>asid. asid_table s (asid_high_bits_of asid) = Some x \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag b) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s x pool a b. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; kheap s x = Some (ArchObj (ASIDPool pool)); (if a = UCAST(32 \<rightarrow> 10) asid then None else pool a) = Some b\<rbrakk> \<Longrightarrow> (b, ?uu86 s x pool a b, ?uv86 s x pool a b, Control) \<in> state_vrefs s x
 2. \<And>s x pool a b. \<lbrakk>pas_refined aag s; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; kheap s x = Some (ArchObj (ASIDPool pool)); (a, b) \<in> graph_of (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) asid then None else pool a)\<rbrakk> \<Longrightarrow> \<forall>asid. asid_table s (asid_high_bits_of asid) = Some x \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag b) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s x pool a b. \<lbrakk>pas_refined aag s; asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; kheap s x = Some (ArchObj (ASIDPool pool)); (a, b) \<in> graph_of (\<lambda>a. if a = UCAST(32 \<rightarrow> 10) asid then None else pool a)\<rbrakk> \<Longrightarrow> \<forall>asid. asid_table s (asid_high_bits_of asid) = Some x \<and> asid && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag b) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s x pool a b asida. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; kheap s x = Some (ArchObj (ASIDPool pool)); (if a = UCAST(32 \<rightarrow> 10) asid then None else pool a) = Some b; pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; asid_table s (asid_high_bits_of asida) = Some x; asida && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a\<rbrakk> \<Longrightarrow> (pasASIDAbs aag asida, Control, pasObjectAbs aag b) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s x pool a b asida. \<lbrakk>asid_table s (asid_high_bits_of asid) = Some x; pool (UCAST(32 \<rightarrow> 10) asid) = Some pd; kheap s x = Some (ArchObj (ASIDPool pool)); (if a = UCAST(32 \<rightarrow> 10) asid then None else pool a) = Some b; pas_wellformed aag; irq_map_wellformed aag s; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; asida && mask local.asid_low_bits = UCAST(10 \<rightarrow> 32) a\<rbrakk> \<Longrightarrow> (b, asida && mask local.asid_low_bits, AASIDPool, Control) \<in> state_vrefs s x proof (prove)
goal:
No subgoals!