theory ArchArch_AC

lemma create_mapping_entries_authorised_slots [wp]:
  "\<lbrace>\<exists>\<rhd> pd and invs and pas_refined aag and
    K (is_subject aag pd \<and> is_aligned pd pd_bits \<and>
       vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and>
       (\<forall>a\<in>vspace_cap_rights_to_auth rights.
          \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). aag_has_auth_to aag a p))\<rbrace>
   create_mapping_entries base vptr vmpage_size rights attrib pd
   \<lbrace>\<lambda>rv _. authorised_slots aag rv\<rbrace>, -" unfolding authorised_slots_def apply (rule hoare_gen_asmE) apply (cases vmpage_size) apply (wp lookup_pt_slot_authorised | simp add: pte_ref_simps | fold validE_R_def)+ apply (auto simp: pd_bits_def pageBits_def)[1] apply (wp lookup_pt_slot_authorised2
           | simp add: pte_ref_simps largePagePTE_offsets_def
           | fold validE_R_def)+ apply (auto simp: pd_bits_def pageBits_def vmsz_aligned_def)[1] apply (wp | simp)+ apply (auto simp: pde_ref2_def lookup_pd_slot_pd)[1] apply (wp | simp add: superSectionPDE_offsets_def)+ apply (auto simp: pde_ref2_def vmsz_aligned_def lookup_pd_slot_add_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag and K (is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag))\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. authorised_slots aag rv\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag and K (is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag))\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSmallPage\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, -
 2. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, -
 3. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, -
 4. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr ARMSmallPage \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) 12. (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSmallPage; (\<exists>ref. (ref \<rhd> pd) s) \<and> invs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> valid_vspace_objs s \<and> pspace_aligned s \<and> is_aligned pd 14
 2. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, -
 3. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, -
 4. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, -
 2. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, -
 3. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr ARMLargePage \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) 16. (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMLargePage; (\<exists>ref. (ref \<rhd> pd) s) \<and> invs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> is_aligned pd 14 \<and> is_aligned vptr 16 \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> equal_kernel_mappings s \<and> valid_global_objs s \<and> pspace_aligned s
 2. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, -
 3. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, -
 2. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr ARMSection \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) 20. (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> invs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>a aa b. pde_ref2 (SectionPDE base (attrib - {Global}) 0 rights) = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> is_subject aag (lookup_pd_slot pd vptr && ~~ mask pd_bits)
 2. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr vmpage_size \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and invs and pas_refined aag\<rbrace> create_mapping_entries base vptr vmpage_size rights attrib pd \<lbrace>\<lambda>rv _. case rv of Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pt_bits)) | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a\<in>snd (snd x). \<forall>p\<in>ptr_range (fst x) (fst (snd x)). (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set slots. is_subject aag (x && ~~ mask pd_bits))\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag pd \<and> is_aligned pd pd_bits \<and> vmsz_aligned vptr ARMSuperSection \<and> vptr < kernel_base \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. \<forall>p\<in>ptr_range (ptrFromPAddr base) 24. (pasSubject aag, a, pasObjectAbs aag p) \<in> pasPolicy aag); vmpage_size = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> invs s \<and> pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>a aa b. pde_ref2 (SuperSectionPDE base (attrib - {Global}) rights) = Some (a, aa, b) \<longrightarrow> (\<forall>ab\<in>b. \<forall>p\<in>ptr_range a aa. (pasSubject aag, ab, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. is_subject aag (x + lookup_pd_slot pd vptr && ~~ mask pd_bits)) proof (prove)
goal:
No subgoals!