theory ArchADT_AC

lemma user_op_access[ADT_AC_assms]:
  "\<lbrakk> invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr;
     auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x) \<rbrakk>
     \<Longrightarrow> abs_has_auth_to aag auth tcb (ptrFromPAddr ptr)" apply (case_tac "x \<in> kernel_mappings") apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
                          ptable_lift_def ptable_rights_def vspace_cap_rights_to_auth_def
                    dest: some_get_page_info_kmapsD split: option.splits) apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) tcb =
                   arm_global_pd (arch_state s)") apply (fastforce simp: invs_valid_global_objs invs_arch_state
                          ptable_lift_def ptable_rights_def
                   split: option.splits
                    dest: get_page_info_gpd_kmaps[rotated 2]) apply (subst pd_of_thread_same_agent) apply fastforce+ apply (cases "\<exists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj))
                                                (get_pd_of_thread (kheap s) (arch_state s) tcb) x =
                                   Some (PageTablePDE word1 set1 word2)") apply (clarsimp simp: ptable_lift_def ptable_rights_def split: option.splits) apply (frule pd_of_thread_same_agent) apply fastforce+ apply (subst pt_in_pd_same_agent) apply fastforce+ apply (rule pas_refined_mem[rotated], simp) apply (rule get_page_info_state_objs_to_policy) apply fastforce+ apply (rule pas_refined_mem[rotated], simp) apply (rule ptable_state_objs_to_policy) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag
 2. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag
 2. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (5 subgoals):
 1. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> pas_refined aag ?s60
 2. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> is_subject aag tcb
 3. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> get_pd_of_thread (kheap ?s60) (arch_state ?s60) tcb = ?pd60
 4. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ?pd60 \<noteq> arm_global_pd (arch_state ?s60)
 5. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag ?pd60, auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<exists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag
 2. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr (a + (x && mask aa)))) \<in> pasPolicy aag
 2. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (5 subgoals):
 1. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa)\<rbrakk> \<Longrightarrow> is_subject aag (?tcb_ptr95 a aa ab b word1 set1 word2)
 2. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa)\<rbrakk> \<Longrightarrow> get_pd_of_thread (kheap s) (arch_state s) (?tcb_ptr95 a aa ab b word1 set1 word2) = ?pd95 a aa ab b word1 set1 word2
 3. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa)\<rbrakk> \<Longrightarrow> ?pd95 a aa ab b word1 set1 word2 \<noteq> arm_global_pd (arch_state s)
 4. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag (?tcb_ptr95 a aa ab b word1 set1 word2) = pasObjectAbs aag (?pd95 a aa ab b word1 set1 word2)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr (a + (x && mask aa)))) \<in> pasPolicy aag
 5. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr (a + (x && mask aa)))) \<in> pasPolicy aag
 2. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (6 subgoals):
 1. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> pas_refined aag (?s108 a aa ab b word1 set1 word2)
 2. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> is_subject aag (get_pd_of_thread (kheap s) (arch_state s) tcb)
 3. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> ?vptr108 a aa ab b word1 set1 word2 \<notin> kernel_mappings
 4. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> get_pd_entry (\<lambda>obj. get_arch_obj (kheap (?s108 a aa ab b word1 set1 word2) obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) (?vptr108 a aa ab b word1 set1 word2) = Some (PageTablePDE (?p108 a aa ab b word1 set1 word2) (?x108 a aa ab b word1 set1 word2) (?xa108 a aa ab b word1 set1 word2))
 5. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (ptrFromPAddr (?p108 a aa ab b word1 set1 word2)), auth, pasObjectAbs aag (ptrFromPAddr (a + (x && mask aa)))) \<in> pasPolicy aag
 6. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (ptrFromPAddr word1), auth, pasObjectAbs aag (ptrFromPAddr (a + (x && mask aa)))) \<in> pasPolicy aag
 2. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> (ptrFromPAddr word1, auth, ptrFromPAddr (a + (x && mask aa))) \<in> state_objs_to_policy s
 2. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (7 subgoals):
 1. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> invs s
 2. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> auth \<in> vspace_cap_rights_to_auth (?r128 a aa ab b word1 set1 word2)
 3. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (?tcb128 a aa ab b word1 set1 word2)) x = Some (a, aa, ?attr128 a aa ab b word1 set1 word2, ?r128 a aa ab b word1 set1 word2)
 4. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> get_pd_of_thread (kheap s) (arch_state s) (?tcb128 a aa ab b word1 set1 word2) \<noteq> arm_global_pd (arch_state s)
 5. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (?tcb128 a aa ab b word1 set1 word2)) x = Some (PageTablePDE word1 (?set1.128 a aa ab b word1 set1 word2) (?word2.128 a aa ab b word1 set1 word2))
 6. \<And>a aa ab b word1 set1 word2. \<lbrakk>auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); invs s; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (a, aa, ab, b); get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2); ptr = a + (x && mask aa); pasObjectAbs aag tcb = pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb)\<rbrakk> \<Longrightarrow> x \<notin> kernel_mappings
 7. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (get_pd_of_thread (kheap s) (arch_state s) tcb), auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> (get_pd_of_thread (kheap s) (arch_state s) tcb, auth, ptrFromPAddr ptr) \<in> state_objs_to_policy s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> invs s
 2. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> ptable_lift tcb s ?x153 = Some ptr
 3. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s ?x153)
 4. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s)
 5. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) ?x153 \<noteq> Some (PageTablePDE word1 set1 word2)
 6. \<lbrakk>invs s; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x); x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s); \<nexists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (PageTablePDE word1 set1 word2)\<rbrakk> \<Longrightarrow> ?x153 \<notin> kernel_mappings proof (prove)
goal:
No subgoals!