theory ArchUserOp_IF

lemma user_op_access_data_at:
  "\<lbrakk> invs s; valid_pdpt_objs s;pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr;
     data_at sz ((ptrFromPAddr ptr) && ~~ mask (pageBitsForSize sz)) s;
     auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x) \<rbrakk>
     \<Longrightarrow> (pasObjectAbs aag tcb, auth,
          pasObjectAbs aag (ptrFromPAddr (ptr && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag" apply (case_tac "x \<in> kernel_mappings") apply (clarsimp simp: ptable_lift_def ptable_rights_def split: option.splits) apply (frule some_get_page_info_kmapsD) apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
                             vspace_cap_rights_to_auth_def)+ apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) tcb = arm_global_pd (arch_state s)") apply (clarsimp simp: ptable_lift_def ptable_rights_def split: option.splits) apply (frule get_page_info_gpd_kmaps[rotated, rotated]) apply (fastforce simp: invs_valid_global_objs invs_arch_state)+ apply (frule (3) ptable_lift_data_consistant[rotated 2]) apply fastforce apply fastforce apply (frule (3) ptable_rights_data_consistant[rotated 2]) apply fastforce apply fastforce apply (erule (3) user_op_access) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr (ptr && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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 && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag
 2. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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 && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b. \<lbrakk>data_at sz (ptrFromPAddr (a + (x && mask aa)) && ~~ mask (pageBitsForSize sz)) s; auth \<in> vspace_cap_rights_to_auth b; x \<in> kernel_mappings; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; 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); ptr = a + (x && mask aa)\<rbrakk> \<Longrightarrow> (pasSubject aag, auth, pasObjectAbs aag (ptrFromPAddr (a + (x && mask aa) && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag
 2. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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 && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (5 subgoals):
 1. \<And>a aa ab b. \<lbrakk>data_at sz (ptrFromPAddr (a + (x && mask aa)) && ~~ mask (pageBitsForSize sz)) s; auth \<in> vspace_cap_rights_to_auth b; x \<in> kernel_mappings; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; 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); ptr = a + (x && mask aa)\<rbrakk> \<Longrightarrow> x \<in> kernel_mappings
 2. \<And>a aa ab b. \<lbrakk>data_at sz (ptrFromPAddr (a + (x && mask aa)) && ~~ mask (pageBitsForSize sz)) s; auth \<in> vspace_cap_rights_to_auth b; x \<in> kernel_mappings; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; 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); ptr = a + (x && mask aa)\<rbrakk> \<Longrightarrow> valid_global_vspace_mappings s
 3. \<And>a aa ab b. \<lbrakk>data_at sz (ptrFromPAddr (a + (x && mask aa)) && ~~ mask (pageBitsForSize sz)) s; auth \<in> vspace_cap_rights_to_auth b; x \<in> kernel_mappings; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; 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); ptr = a + (x && mask aa)\<rbrakk> \<Longrightarrow> equal_kernel_mappings s
 4. \<And>a aa ab b. \<lbrakk>data_at sz (ptrFromPAddr (a + (x && mask aa)) && ~~ mask (pageBitsForSize sz)) s; auth \<in> vspace_cap_rights_to_auth b; x \<in> kernel_mappings; invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; 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); ptr = a + (x && mask aa); (\<exists>sz. pageBitsForSize sz = aa) \<and> b = {}\<rbrakk> \<Longrightarrow> (pasSubject aag, auth, pasObjectAbs aag (ptrFromPAddr (a + (x && mask aa) && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag
 5. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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 && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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 && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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 && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag
 2. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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 && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b. \<lbrakk>data_at sz (ptrFromPAddr (a + (x && mask aa)) && ~~ mask (pageBitsForSize sz)) s; auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb = arm_global_pd (arch_state s); invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); ptr = a + (x && mask aa)\<rbrakk> \<Longrightarrow> (pasSubject aag, auth, pasObjectAbs aag (ptrFromPAddr (a + (x && mask aa) && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag
 2. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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 && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (4 subgoals):
 1. \<And>a aa ab b. \<lbrakk>data_at sz (ptrFromPAddr (a + (x && mask aa)) && ~~ mask (pageBitsForSize sz)) s; auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb = arm_global_pd (arch_state s); invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); ptr = a + (x && mask aa)\<rbrakk> \<Longrightarrow> valid_global_objs s
 2. \<And>a aa ab b. \<lbrakk>data_at sz (ptrFromPAddr (a + (x && mask aa)) && ~~ mask (pageBitsForSize sz)) s; auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb = arm_global_pd (arch_state s); invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); ptr = a + (x && mask aa)\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<And>a aa ab b. \<lbrakk>data_at sz (ptrFromPAddr (a + (x && mask aa)) && ~~ mask (pageBitsForSize sz)) s; auth \<in> vspace_cap_rights_to_auth b; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) tcb = arm_global_pd (arch_state s); invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); ptr = a + (x && mask aa); x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> (pasSubject aag, auth, pasObjectAbs aag (ptrFromPAddr (a + (x && mask aa) && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag
 4. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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 && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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 && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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> valid_state s
 2. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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> \<forall>x\<in>ran (kheap s). obj_valid_pdpt x
 3. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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); ptable_lift tcb s (x && ~~ mask (pageBitsForSize sz)) = Some (ptr && ~~ mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr (ptr && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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> \<forall>x\<in>ran (kheap s). obj_valid_pdpt x
 2. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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); ptable_lift tcb s (x && ~~ mask (pageBitsForSize sz)) = Some (ptr && ~~ mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr (ptr && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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); ptable_lift tcb s (x && ~~ mask (pageBitsForSize sz)) = Some (ptr && ~~ mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr (ptr && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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); ptable_lift tcb s (x && ~~ mask (pageBitsForSize sz)) = Some (ptr && ~~ mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> valid_state s
 2. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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); ptable_lift tcb s (x && ~~ mask (pageBitsForSize sz)) = Some (ptr && ~~ mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran (kheap s). obj_valid_pdpt x
 3. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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); ptable_lift tcb s (x && ~~ mask (pageBitsForSize sz)) = Some (ptr && ~~ mask (pageBitsForSize sz)); ptable_rights tcb s (x && ~~ mask (pageBitsForSize sz)) = ptable_rights tcb s x\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr (ptr && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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); ptable_lift tcb s (x && ~~ mask (pageBitsForSize sz)) = Some (ptr && ~~ mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran (kheap s). obj_valid_pdpt x
 2. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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); ptable_lift tcb s (x && ~~ mask (pageBitsForSize sz)) = Some (ptr && ~~ mask (pageBitsForSize sz)); ptable_rights tcb s (x && ~~ mask (pageBitsForSize sz)) = ptable_rights tcb s x\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr (ptr && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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); ptable_lift tcb s (x && ~~ mask (pageBitsForSize sz)) = Some (ptr && ~~ mask (pageBitsForSize sz)); ptable_rights tcb s (x && ~~ mask (pageBitsForSize sz)) = ptable_rights tcb s x\<rbrakk> \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr (ptr && ~~ mask (pageBitsForSize sz)))) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>ran (kheap s). obj_valid_pdpt x; pas_refined aag s; is_subject aag tcb; ptable_lift tcb s x = Some ptr; data_at sz (ptrFromPAddr ptr && ~~ mask (pageBitsForSize sz)) s; 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); ptable_lift tcb s (x && ~~ mask (pageBitsForSize sz)) = Some (ptr && ~~ mask (pageBitsForSize sz)); ptable_rights tcb s (x && ~~ mask (pageBitsForSize sz)) = ptable_rights tcb s x\<rbrakk> \<Longrightarrow> auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s (x && ~~ mask (pageBitsForSize sz))) proof (prove)
goal:
No subgoals!