theory ArchADT_AC

lemma pd_of_thread_same_agent:
  "\<lbrakk> pas_refined aag s; is_subject aag tcb_ptr;
     get_pd_of_thread (kheap s) (arch_state s) tcb_ptr = pd; pd \<noteq> arm_global_pd (arch_state s) \<rbrakk>
     \<Longrightarrow> pasObjectAbs aag tcb_ptr = pasObjectAbs aag pd" apply (rule_tac aag="pasPolicy aag" in aag_wellformed_Control[rotated]) apply (fastforce simp: pas_refined_def) apply (rule pas_refined_mem[rotated], simp) apply (clarsimp simp: get_pd_of_thread_eq) apply (cut_tac ptr="(tcb_ptr, tcb_cnode_index 1)" in sbta_caps) prefer 4 apply (simp add: state_objs_to_policy_def) apply (subst caps_of_state_tcb_cap_cases) apply (simp add: get_tcb_def) apply (simp add: dom_tcb_cap_cases[simplified]) apply simp apply (simp add: obj_refs_def) apply (simp add: cap_auth_conferred_def arch_cap_auth_conferred_def is_page_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; get_pd_of_thread (kheap s) (arch_state s) tcb_ptr = pd; pd \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> pasObjectAbs aag tcb_ptr = pasObjectAbs aag pd proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; get_pd_of_thread (kheap s) (arch_state s) tcb_ptr = pd; pd \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> policy_wellformed (pasPolicy aag) ?mirqs ?irqs (pasObjectAbs aag tcb_ptr)
 2. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; get_pd_of_thread (kheap s) (arch_state s) tcb_ptr = pd; pd \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb_ptr, Control, pasObjectAbs aag pd) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; get_pd_of_thread (kheap s) (arch_state s) tcb_ptr = pd; pd \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb_ptr, Control, pasObjectAbs aag pd) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; get_pd_of_thread (kheap s) (arch_state s) tcb_ptr = pd; pd \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (tcb_ptr, Control, pd) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> (tcb_ptr, Control, pd) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> ?caps23 tcb asid (tcb_ptr, tcb_cnode_index 1) = Some (?cap23 tcb asid)
 2. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> ?oref23 tcb asid \<in> obj_refs_ac (?cap23 tcb asid)
 3. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> ?auth23 tcb asid \<in> cap_auth_conferred (?cap23 tcb asid)
 4. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid)); (fst (tcb_ptr, tcb_cnode_index 1), ?auth23 tcb asid, ?oref23 tcb asid) \<in> state_bits_to_policy (?caps23 tcb asid) (?thread_sts23 tcb asid) (?thread_bas23 tcb asid) (?cdt23 tcb asid) (?vrefs23 tcb asid)\<rbrakk> \<Longrightarrow> (tcb_ptr, Control, pd) \<in> state_objs_to_policy s proof (prove)
goal (4 subgoals):
 1. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid)); (fst (tcb_ptr, tcb_cnode_index 1), ?auth23 tcb asid, ?oref23 tcb asid) \<in> state_bits_to_policy (?caps23 tcb asid) (?thread_sts23 tcb asid) (?thread_bas23 tcb asid) (?cdt23 tcb asid) (?vrefs23 tcb asid)\<rbrakk> \<Longrightarrow> (tcb_ptr, Control, pd) \<in> state_objs_to_policy s
 2. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> ?caps23 tcb asid (tcb_ptr, tcb_cnode_index 1) = Some (?cap23 tcb asid)
 3. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> ?oref23 tcb asid \<in> obj_refs_ac (?cap23 tcb asid)
 4. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> ?auth23 tcb asid \<in> cap_auth_conferred (?cap23 tcb asid) proof (prove)
goal (3 subgoals):
 1. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> caps_of_state s (tcb_ptr, tcb_cnode_index 1) = Some (?cap23 tcb asid)
 2. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> pd \<in> obj_refs_ac (?cap23 tcb asid)
 3. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> Control \<in> cap_auth_conferred (?cap23 tcb asid) proof (prove)
goal (5 subgoals):
 1. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> get_tcb tcb_ptr s = Some (?tcb26 tcb asid)
 2. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> tcb_cnode_index 1 \<in> dom tcb_cap_cases
 3. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 1))) (?tcb26 tcb asid)) = Some (?cap26 tcb asid (?tcba26 tcb asid) (?asid26 tcb asid))
 4. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> pd \<in> obj_refs_ac (?cap26 tcb asid (?tcba26 tcb asid) (?asid26 tcb asid))
 5. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> Control \<in> cap_auth_conferred (?cap26 tcb asid (?tcba26 tcb asid) (?asid26 tcb asid)) proof (prove)
goal (4 subgoals):
 1. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> tcb_cnode_index 1 \<in> dom tcb_cap_cases
 2. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 1))) tcb) = Some (?cap26 tcb asid (?tcba26 tcb asid) (?asid26 tcb asid))
 3. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> pd \<in> obj_refs_ac (?cap26 tcb asid (?tcba26 tcb asid) (?asid26 tcb asid))
 4. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> Control \<in> cap_auth_conferred (?cap26 tcb asid (?tcba26 tcb asid) (?asid26 tcb asid)) proof (prove)
goal (3 subgoals):
 1. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> Some (the (map_option fst (tcb_cap_cases (tcb_cnode_index 1))) tcb) = Some (?cap26 tcb asid (?tcba26 tcb asid) (?asid26 tcb asid))
 2. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> pd \<in> obj_refs_ac (?cap26 tcb asid (?tcba26 tcb asid) (?asid26 tcb asid))
 3. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> Control \<in> cap_auth_conferred (?cap26 tcb asid (?tcba26 tcb asid) (?asid26 tcb asid)) proof (prove)
goal (2 subgoals):
 1. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> pd \<in> obj_refs_ac (ArchObjectCap (PageDirectoryCap pd (Some asid)))
 2. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> Control \<in> cap_auth_conferred (ArchObjectCap (PageDirectoryCap pd (Some asid))) proof (prove)
goal (1 subgoal):
 1. \<And>tcb asid. \<lbrakk>pas_refined aag s; is_subject aag tcb_ptr; pd \<noteq> arm_global_pd (arch_state s); kheap s tcb_ptr = Some (TCB tcb); ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s; tcb_vtable tcb = ArchObjectCap (PageDirectoryCap pd (Some asid))\<rbrakk> \<Longrightarrow> Control \<in> cap_auth_conferred (ArchObjectCap (PageDirectoryCap pd (Some asid))) proof (prove)
goal:
No subgoals!