theory VSpace_R

lemma find_pd_for_asid_assert_eq:
  "\<lbrakk> vspace_at_asid asid pd s; valid_vspace_objs s;
         asid \<noteq> 0; pspace_aligned s \<rbrakk>
    \<Longrightarrow> find_pd_for_asid_assert asid s = return pd s" apply (drule(3) find_pd_for_asid_eq_helper) apply (simp add: find_pd_for_asid_assert_def
                   catch_def bind_assoc) apply (clarsimp simp: returnOk_def obj_at_def
                        a_type_def
                  cong: bind_apply_cong) apply (clarsimp split: Structures_A.kernel_object.splits
                         arch_kernel_obj.splits if_split_asm) apply (simp add: get_pde_def get_pd_def get_object_def
                   bind_assoc is_aligned_neg_mask_eq
                   pd_bits_def pdBits_def pdeBits_def pageBits_def) apply (simp add: exec_gets) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vspace_at_asid asid pd s; valid_vspace_objs s; asid \<noteq> 0; pspace_aligned s\<rbrakk> \<Longrightarrow> find_pd_for_asid_assert asid s = return pd s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; asid \<noteq> 0; pspace_aligned s; find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits\<rbrakk> \<Longrightarrow> find_pd_for_asid_assert asid s = return pd s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; asid \<noteq> 0; pspace_aligned s; find_pd_for_asid asid s = returnOk pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pdBits\<rbrakk> \<Longrightarrow> (do x <- find_pd_for_asid asid;
pd <- case x of Inl e \<Rightarrow> fail | Inr x \<Rightarrow> return x;
y <- get_pde pd;
return pd
od) s = return pd s proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_vspace_objs s; asid \<noteq> 0; pspace_aligned s; find_pd_for_asid asid s = return (Inr pd) s; is_aligned pd pdBits; kheap s pd = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory\<rbrakk> \<Longrightarrow> (do rv <- get_pde pd;
return pd
od) s = return pd s proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>valid_vspace_objs s; asid \<noteq> 0; pspace_aligned s; find_pd_for_asid asid s = return (Inr pd) s; is_aligned pd pdBits; kheap s pd = Some (ArchObj (PageDirectory x3))\<rbrakk> \<Longrightarrow> (do rv <- get_pde pd;
return pd
od) s = return pd s proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>valid_vspace_objs s; asid \<noteq> 0; pspace_aligned s; find_pd_for_asid asid s = return (Inr pd) s; is_aligned pd 14; kheap s pd = Some (ArchObj (PageDirectory x3))\<rbrakk> \<Longrightarrow> (do x <- gets kheap;
xa <- assert (\<exists>y. x pd = Some y);
pda <- case the (x pd) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return pd
od) s = return pd s proof (prove)
goal:
No subgoals!