theory VSpace_R

lemma find_pd_for_asid_valids:
  "\<lbrace> vspace_at_asid asid pd and valid_vspace_objs
         and pspace_aligned and K (asid \<noteq> 0) \<rbrace>
     find_pd_for_asid asid \<lbrace>\<lambda>rv s. pde_at rv s\<rbrace>,-"
  "\<lbrace> vspace_at_asid asid pd and valid_vspace_objs
         and pspace_aligned and K (asid \<noteq> 0)
         and K (is_aligned pd pdBits \<longrightarrow> P pd) \<rbrace>
     find_pd_for_asid asid \<lbrace>\<lambda>rv s. P rv\<rbrace>,-"
  "\<lbrace> vspace_at_asid asid pd and valid_vspace_objs
         and pspace_aligned and K (asid \<noteq> 0)
         and pd_at_uniq asid pd \<rbrace>
     find_pd_for_asid asid \<lbrace>\<lambda>rv s. pd_at_uniq asid rv s\<rbrace>,-"
  "\<lbrace> vspace_at_asid asid pd and valid_vspace_objs
         and pspace_aligned and K (asid \<noteq> 0) \<rbrace>
     find_pd_for_asid asid -,\<lbrace>\<bottom>\<bottom>\<rbrace>" apply (simp_all add: validE_def validE_R_def validE_E_def
                       valid_def split: sum.split) apply (auto simp: returnOk_def return_def pdeBits_def
                    pde_at_def pd_bits_def pdBits_def
                    pageBits_def is_aligned_neg_mask_eq
             dest!: find_pd_for_asid_eq_helper
             elim!: is_aligned_weaken) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)\<rbrace> find_pd_for_asid asid \<lbrace>pde_at\<rbrace>, - &&& \<lbrace>vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> P pd)\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. P rv\<rbrace>, -) &&& \<lbrace>vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and pd_at_uniq asid pd\<rbrace> find_pd_for_asid asid \<lbrace>pd_at_uniq asid\<rbrace>, - &&& \<lbrace>vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)\<rbrace> find_pd_for_asid asid -, \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<forall>s. vspace_at_asid asid pd s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0 \<longrightarrow> (\<forall>x\<in>fst (find_pd_for_asid asid s). case x of (r, s') \<Rightarrow> \<forall>ra. r = Inr ra \<longrightarrow> pde_at ra s')
 2. \<forall>s. vspace_at_asid asid pd s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0 \<and> (is_aligned pd pdBits \<longrightarrow> P pd) \<longrightarrow> (\<forall>x\<in>fst (find_pd_for_asid asid s). case x of (r, s') \<Rightarrow> \<forall>b. r = Inr b \<longrightarrow> P b)
 3. \<forall>s. vspace_at_asid asid pd s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0 \<and> pd_at_uniq asid pd s \<longrightarrow> (\<forall>x\<in>fst (find_pd_for_asid asid s). case x of (r, s') \<Rightarrow> \<forall>ra. r = Inr ra \<longrightarrow> pd_at_uniq asid ra s')
 4. \<forall>s. vspace_at_asid asid pd s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> asid \<noteq> 0 \<longrightarrow> (\<forall>x\<in>fst (find_pd_for_asid asid s). case x of (Inl e, s') \<Rightarrow> False | (Inr ra, s') \<Rightarrow> True) proof (prove)
goal:
No subgoals!