kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_DR

lemma store_pte_non_sense_wp:
  "\<lbrace>\<lambda>s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s
    \<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pt_bits >> 2)) = ARM_A.pte.InvalidPTE)) \<rbrace>
  store_pte x ARM_A.pte.InvalidPTE
   \<lbrace>\<lambda>r s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s
    \<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pt_bits >> 2)) = ARM_A.pte.InvalidPTE))\<rbrace>" apply (simp add:store_pte_def get_object_def get_pte_def set_pt_def set_object_def) apply wp apply (clarsimp simp:obj_at_def split: Structures_A.kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST('b \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)\<rbrace> store_pte x InvalidPTE \<lbrace>\<lambda>r s. \<exists>f. ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST('b \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>f. ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST('b \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)\<rbrace> do pt <- get_pt (x && ~~ mask pt_bits);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh (x && ~~ mask pt_bits) = Some y);
return (the (kh (x && ~~ mask pt_bits)))
od;
y <- assert (a_type kobj = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE)))));
s <- get;
put (update_kheap ((kheap s)(x && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE))))) s)
od \<lbrace>\<lambda>r s. \<exists>f. ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST('b \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>f. ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) s \<and> (\<forall>slot\<in>set xs. f (UCAST('b \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE) \<Longrightarrow> \<forall>pt. ako_at (arch_kernel_obj.PageTable pt) (x && ~~ mask pt_bits) s \<longrightarrow> (\<exists>y. kheap s (x && ~~ mask pt_bits) = Some y) \<longrightarrow> a_type (the (kheap s (x && ~~ mask pt_bits))) = a_type (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE)))) \<longrightarrow> (\<exists>f. ako_at (arch_kernel_obj.PageTable f) (slot && ~~ mask pt_bits) (update_kheap ((kheap s)(x && ~~ mask pt_bits \<mapsto> ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (x && mask pt_bits >> 2) := InvalidPTE))))) s) \<and> (\<forall>slot\<in>set xs. f (UCAST('b \<rightarrow> 8) (slot && mask pt_bits >> 2)) = InvalidPTE)) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma pt_page_relation_weaken:
  "\<lbrakk> pt_page_relation a b c S s; S \<subseteq> T \<rbrakk> \<Longrightarrow> pt_page_relation a b c T s" apply (clarsimp simp: pt_page_relation_def) apply (auto split: ARM_A.pte.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pt_page_relation a b c S s; S \<subseteq> T\<rbrakk> \<Longrightarrow> pt_page_relation a b c T s proof (prove)
goal (1 subgoal):
 1. \<And>fun. \<lbrakk>S \<subseteq> T; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (c && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> b = ptrFromPAddr ref \<and> ARMLargePage \<in> S | SmallPagePTE ref fun1 fun2 \<Rightarrow> b = ptrFromPAddr ref \<and> ARMSmallPage \<in> S\<rbrakk> \<Longrightarrow> case fun (UCAST(32 \<rightarrow> 8) (c && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> b = ptrFromPAddr ref \<and> ARMLargePage \<in> T | SmallPagePTE ref fun1 fun2 \<Rightarrow> b = ptrFromPAddr ref \<and> ARMSmallPage \<in> T proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma pt_page_relation_univ:
  "pt_page_relation a b c {ARMLargePage} s
  \<Longrightarrow> pt_page_relation a b c UNIV s" apply (clarsimp simp:pt_page_relation_def) apply (clarsimp split: ARM_A.pte.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pt_page_relation a b c {ARMLargePage} s \<Longrightarrow> pt_page_relation a b c UNIV s proof (prove)
goal (1 subgoal):
 1. \<And>fun. \<lbrakk>kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun)); case fun (UCAST(32 \<rightarrow> 8) (c && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> b = ptrFromPAddr ref \<and> ARMLargePage \<in> {ARMLargePage} | SmallPagePTE ref fun1 fun2 \<Rightarrow> b = ptrFromPAddr ref \<and> ARMSmallPage \<in> {ARMLargePage}\<rbrakk> \<Longrightarrow> case fun (UCAST(32 \<rightarrow> 8) (c && mask pt_bits >> 2)) of InvalidPTE \<Rightarrow> False | LargePagePTE ref fun1 fun2 \<Rightarrow> b = ptrFromPAddr ref \<and> ARMLargePage \<in> UNIV | SmallPagePTE ref fun1 fun2 \<Rightarrow> b = ptrFromPAddr ref \<and> ARMSmallPage \<in> UNIV proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma (in pspace_update_eq) pd_pt_relation_update[iff]:
  "pd_pt_relation a b c (f s) = pd_pt_relation a b c s" by (simp add: pd_pt_relation_def pspace)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pd_pt_relation a b c (f s) = pd_pt_relation a b c s
theory Finalise_DR

lemma check_mapping_pptr_section_relation:
  "\<lbrace>\<top>\<rbrace> check_mapping_pptr w ARMSection (Inr (lookup_pd_slot rv' b))
   \<lbrace>\<lambda>rv s. rv \<longrightarrow>
    pd_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s\<rbrace>" apply (rule hoare_vcg_precond_imp) apply (simp add:check_mapping_pptr_def) apply (wp get_pde_wp) apply (clarsimp simp: obj_at_def) apply (clarsimp simp: pd_section_relation_def pd_super_section_relation_def
                 split: ARM_A.pde.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> check_mapping_pptr w ARMSection (Inr (lookup_pd_slot rv' b)) \<lbrace>\<lambda>rv s. rv \<longrightarrow> pd_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> check_mapping_pptr w ARMSection (Inr (lookup_pd_slot rv' b)) \<lbrace>\<lambda>rv s. rv \<longrightarrow> pd_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do pde <- get_pde (lookup_pd_slot rv' b);
return (case pde of SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr w \<and> ARMSection = ARMSection | SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr w \<and> ARMSection = ARMSuperSection | _ \<Rightarrow> False)
od \<lbrace>\<lambda>rv s. rv \<longrightarrow> pd_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>pd. ako_at (arch_kernel_obj.PageDirectory pd) (lookup_pd_slot rv' b && ~~ mask pd_bits) s \<longrightarrow> (case pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv' b && mask pd_bits >> 2)) of SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr w \<and> ARMSection = ARMSection | SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr w \<and> ARMSection = ARMSuperSection | _ \<Rightarrow> False) \<longrightarrow> pd_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>kheap s (lookup_pd_slot rv' b && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); case pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv' b && mask pd_bits >> 2)) of SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr w \<and> ARMSection = ARMSection | SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr w \<and> ARMSection = ARMSuperSection | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> pd_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma check_mapping_pptr_super_section_relation:
  "\<lbrace>\<top>\<rbrace> check_mapping_pptr w ARMSuperSection (Inr (lookup_pd_slot rv' b))
   \<lbrace>\<lambda>rv s. rv \<longrightarrow> pd_super_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s\<rbrace>" apply (rule hoare_vcg_precond_imp) apply (simp add:check_mapping_pptr_def) apply (wp get_pde_wp) apply (clarsimp simp: obj_at_def) apply (clarsimp simp: pd_section_relation_def pd_super_section_relation_def
                 split: ARM_A.pde.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> check_mapping_pptr w ARMSuperSection (Inr (lookup_pd_slot rv' b)) \<lbrace>\<lambda>rv s. rv \<longrightarrow> pd_super_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> check_mapping_pptr w ARMSuperSection (Inr (lookup_pd_slot rv' b)) \<lbrace>\<lambda>rv s. rv \<longrightarrow> pd_super_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do pde <- get_pde (lookup_pd_slot rv' b);
return (case pde of SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr w \<and> ARMSuperSection = ARMSection | SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr w \<and> ARMSuperSection = ARMSuperSection | _ \<Rightarrow> False)
od \<lbrace>\<lambda>rv s. rv \<longrightarrow> pd_super_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>pd. ako_at (arch_kernel_obj.PageDirectory pd) (lookup_pd_slot rv' b && ~~ mask pd_bits) s \<longrightarrow> (case pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv' b && mask pd_bits >> 2)) of SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr w \<and> ARMSuperSection = ARMSection | SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr w \<and> ARMSuperSection = ARMSuperSection | _ \<Rightarrow> False) \<longrightarrow> pd_super_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd. \<lbrakk>kheap s (lookup_pd_slot rv' b && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory pd)); case pd (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv' b && mask pd_bits >> 2)) of SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr w \<and> ARMSuperSection = ARMSection | SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr w \<and> ARMSuperSection = ARMSuperSection | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> pd_super_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma lookup_pt_slot_aligned:
  "\<lbrace>invs and \<exists>\<rhd> pd and K (is_aligned pd pd_bits \<and> is_aligned vptr 16 \<and> vptr < kernel_base)\<rbrace>
        lookup_pt_slot pd vptr \<lbrace>\<lambda>rb s. is_aligned rb 6\<rbrace>, -" apply (rule hoare_gen_asmE)+ apply (rule hoare_pre, rule hoare_post_imp_R, rule lookup_pt_slot_cap_to) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits \<and> is_aligned vptr 16 \<and> vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rb s. is_aligned rb 6\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<and> is_aligned vptr 16 \<and> vptr < kernel_base \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rb s. is_aligned rb 6\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>is_aligned pd pd_bits \<and> is_aligned vptr 16 \<and> vptr < kernel_base; \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> local.is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrakk> \<Longrightarrow> is_aligned rv 6
 2. \<And>s. \<lbrakk>is_aligned pd pd_bits \<and> is_aligned vptr 16 \<and> vptr < kernel_base; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s)) s\<rbrakk> \<Longrightarrow> (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)) s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma get_pde_pd_relation:
  "\<lbrace>P\<rbrace> get_pde x
           \<lbrace>\<lambda>r s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (x && ~~ mask pd_bits) s
           \<and> r = f (ucast (x && mask pd_bits >> 2))\<rbrace>" apply (simp add:get_pde_def) apply wp apply (clarsimp simp:obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_pde x \<lbrace>\<lambda>r s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (x && ~~ mask pd_bits) s \<and> r = f (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do pd <- get_pd (x && ~~ mask pd_bits);
return (pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)))
od \<lbrace>\<lambda>r s. \<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (x && ~~ mask pd_bits) s \<and> r = f (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> \<forall>pd. ako_at (arch_kernel_obj.PageDirectory pd) (x && ~~ mask pd_bits) s \<longrightarrow> (\<exists>f. ako_at (arch_kernel_obj.PageDirectory f) (x && ~~ mask pd_bits) s \<and> pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)) = f (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2))) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma hoare_post_Some_conj:
  "\<lbrakk> \<lbrace>P\<rbrace>f\<lbrace>\<lambda>r s. case r of Some a \<Rightarrow> Q a s | _ \<Rightarrow> S \<rbrace>;
    \<lbrace>P'\<rbrace>f\<lbrace>\<lambda>r s. case r of Some a \<Rightarrow> R a s | _ \<Rightarrow> S \<rbrace>
   \<rbrakk> \<Longrightarrow>\<lbrace>P and P'\<rbrace>f\<lbrace>\<lambda>r s. case r of Some a \<Rightarrow> Q a s \<and> R a s | _ \<Rightarrow> S\<rbrace>" apply (clarsimp simp:valid_def) apply (drule_tac x = s in spec)+ apply clarsimp apply (drule_tac x= "(a,b)" in bspec,simp)+ apply (clarsimp split:option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. case r of None \<Rightarrow> S | Some a \<Rightarrow> Q a s\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>r s. case r of None \<Rightarrow> S | Some a \<Rightarrow> R a s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r s. case r of None \<Rightarrow> S | Some a \<Rightarrow> Q a s \<and> R a s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (None, s') \<Rightarrow> S | (Some a, s') \<Rightarrow> Q a s'); \<forall>s. P' s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (None, s') \<Rightarrow> S | (Some a, s') \<Rightarrow> R a s'); (a, b) \<in> fst (f s); P s; P' s\<rbrakk> \<Longrightarrow> case a of None \<Rightarrow> S | Some a \<Rightarrow> Q a b \<and> R a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s; P' s; P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (None, s') \<Rightarrow> S | (Some a, s') \<Rightarrow> Q a s'); P' s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (None, s') \<Rightarrow> S | (Some a, s') \<Rightarrow> R a s')\<rbrakk> \<Longrightarrow> case a of None \<Rightarrow> S | Some a \<Rightarrow> Q a b \<and> R a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s; P' s; \<forall>x\<in>fst (f s). case x of (None, s') \<Rightarrow> S | (Some a, s') \<Rightarrow> Q a s'; \<forall>x\<in>fst (f s). case x of (None, s') \<Rightarrow> S | (Some a, s') \<Rightarrow> R a s'\<rbrakk> \<Longrightarrow> case a of None \<Rightarrow> S | Some a \<Rightarrow> Q a b \<and> R a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P s; P' s; case (a, b) of (None, s') \<Rightarrow> S | (Some a, s') \<Rightarrow> Q a s'; case (a, b) of (None, s') \<Rightarrow> S | (Some a, s') \<Rightarrow> R a s'\<rbrakk> \<Longrightarrow> case a of None \<Rightarrow> S | Some a \<Rightarrow> Q a b \<and> R a b proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma cleanByVA_PoU_underlying_memory[wp]: " \<lbrace>\<lambda>m'. underlying_memory m' = m\<rbrace> cleanByVA_PoU w q \<lbrace>\<lambda>_ m'. underlying_memory m' = m\<rbrace>" apply(clarsimp simp: cleanByVA_PoU_def, wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m'. underlying_memory m' = m\<rbrace> cleanByVA_PoU w q \<lbrace>\<lambda>_ m'. underlying_memory m' = m\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma cdl_asid_table_transform:
  "cdl_asid_table (transform sa) x
  =  unat_map (Some \<circ> transform_asid_table_entry \<circ> arm_asid_table (arch_state sa)) x" by (simp add:transform_def transform_asid_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_asid_table (transform sa) x = unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table sa) x
theory Finalise_DR

lemma unat_pd_bits_less_4096_helper[simp]:
  "\<And>x. unat (x && mask pd_bits >> 2 :: word32) < 4096" apply (rule order_less_le_trans[where y="2^12"]) apply (rule unat_less_power[rotated]) apply (rule shiftr_less_t2n) apply (rule order_less_le_trans, rule and_mask_less') apply (simp_all add: pd_bits_def pageBits_def word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x. unat (x && mask pd_bits >> 2) < 4096 proof (prove)
goal (2 subgoals):
 1. \<And>x. unat (x && mask pd_bits >> 2) < 2 ^ 12
 2. \<And>x. 2 ^ 12 \<le> 4096 proof (prove)
goal (3 subgoals):
 1. \<And>x. x && mask pd_bits >> 2 < 2 ^ 12
 2. \<And>x. 12 < LENGTH(32)
 3. \<And>x. 2 ^ 12 \<le> 4096 proof (prove)
goal (3 subgoals):
 1. \<And>x. x && mask pd_bits < 2 ^ (2 + 12)
 2. \<And>x. 12 < LENGTH(32)
 3. \<And>x. 2 ^ 12 \<le> 4096 proof (prove)
goal (4 subgoals):
 1. \<And>x. pd_bits < LENGTH(32)
 2. \<And>x. 2 ^ pd_bits \<le> 2 ^ (2 + 12)
 3. \<And>x. 12 < LENGTH(32)
 4. \<And>x. 2 ^ 12 \<le> 4096 proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma pd_at_cdl_pd_at:
  "\<lbrakk>valid_idle s ; ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots;
  kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk>
  \<Longrightarrow> opt_cap (transform_pd_slot_ref ptr) (transform s) =
  Some (transform_pde (fun (of_nat (unat (ptr && mask pd_bits >> 2)))))" apply (clarsimp simp:opt_cap_def transform_pd_slot_ref_def transform_def
    slots_of_def transform_objects_def pred_tcb_def2
    valid_idle_def restrict_map_def object_slots_def
    transform_page_directory_contents_def unat_map_def
     dest!:get_tcb_SomeD split:option.splits) apply (simp add: below_kernel_base) apply (auto simp:transform_page_directory_contents_def unat_map_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk> \<Longrightarrow> opt_cap (transform_pd_slot_ref ptr) (transform s) = Some (transform_pde (fun (word_of_nat (unat (ptr && mask pd_bits >> 2))))) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> (ptr && ~~ mask pd_bits \<noteq> idle_thread_ptr \<longrightarrow> transform_pde (kernel_pde_mask fun (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2))) = transform_pde (fun (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2)))) \<and> ptr && ~~ mask pd_bits \<noteq> idle_thread_ptr proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> ptr && ~~ mask pd_bits \<noteq> idle_thread_ptr proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma dcorres_get_pde:
  "dcorres (\<lambda>r r'. r = transform_pde r') \<top>
  (valid_idle and K (ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots))
  (cdl_get_pde (transform_pd_slot_ref ptr)) (get_pde ptr)" apply (rule corres_guard_imp[OF corres_gen_asm2]) apply (rule dcorres_get_pde_helper) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>r r'. r = transform_pde r') (\<lambda>_. True) (valid_idle and K (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) (cdl_get_pde (transform_pd_slot_ref ptr)) (get_pde ptr) proof (prove)
goal (3 subgoals):
 1. ?F1 \<Longrightarrow> dcorres (\<lambda>r r'. r = transform_pde r') ?Q ?P'1 (cdl_get_pde (transform_pd_slot_ref ptr)) (get_pde ptr)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_idle and K (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> (?P'1 and (\<lambda>s. ?F1)) s proof (prove)
goal (3 subgoals):
 1. ?F1 \<Longrightarrow> UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. \<And>s. True \<Longrightarrow> True
 3. \<And>s. (valid_idle and K (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> (valid_idle and (\<lambda>s. ?F1)) s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma PPtrPAddr:
  "(addrFromPPtr w = v) = (ptrFromPAddr v = w)" by (auto simp:addrFromPPtr_def ptrFromPAddr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (addrFromPPtr w = v) = (ptrFromPAddr v = w)
theory Finalise_DR

lemma lookup_pd_slot_aligned_simp:
 "is_aligned pd pd_bits
  \<Longrightarrow> lookup_pd_slot pd vptr && mask pd_bits >> 2 = vptr >> 20" by (simp add:lookup_pd_slot_def mask_add_aligned
    shiftr_shiftl_mask_pd_bits vptr_shifting_3_ways)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> lookup_pd_slot pd vptr && mask pd_bits >> 2 = vptr >> 20
theory Finalise_DR

lemma dcorres_option:
  "\<lbrakk> x = None \<Longrightarrow> dcorres sr T P g (C None);
    \<And>z. x = Some z \<Longrightarrow> dcorres sr T (Q z) g (C (Some z))\<rbrakk> \<Longrightarrow>
  dcorres sr T (\<lambda>s. case x of None \<Rightarrow> P s | Some z \<Rightarrow> Q z s) g (C x)" by (case_tac x ,auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = None \<Longrightarrow> dcorres sr T P g (C None); \<And>z. x = Some z \<Longrightarrow> dcorres sr T (Q z) g (C (Some z))\<rbrakk> \<Longrightarrow> dcorres sr T (\<lambda>s. case x of None \<Rightarrow> P s | Some z \<Rightarrow> Q z s) g (C x)