theory ArchAcc_R

lemma getObject_PDE_corres [corres]:
  "p = p' \<Longrightarrow> corres (pde_relation_aligned (p >> 2)) (pde_at p) (pde_at' p')
     (get_pde p) (getObject p')" apply (simp add: getObject_def get_pde_def get_pd_def get_object_def split_def bind_assoc) apply (rule corres_no_failI) apply (rule no_fail_pre, wp) apply (clarsimp simp: ko_wp_at'_def typ_at'_def lookupAround2_known1) apply (case_tac ko; simp) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object; simp add: projectKOs) apply (clarsimp simp: objBits_def cong: option.case_cong) apply (erule (1) ps_clear_lookupAround2) apply simp apply (erule is_aligned_no_overflow) apply (simp add: objBits_simps archObjSize_def word_bits_def) apply simp apply (clarsimp simp: in_monad loadObject_default_def projectKOs) apply (simp add: bind_assoc exec_gets) apply (clarsimp simp: pde_at_def obj_at_def) apply (clarsimp simp add: a_type_def return_def
                  split: if_split_asm Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (clarsimp simp: typ_at'_def ko_wp_at'_def) apply (simp add: in_magnitude_check objBits_simps archObjSize_def pageBits_def pdeBits_def) apply (clarsimp simp: state_relation_def pspace_relation_def) apply (drule bspec, blast) apply (clarsimp simp: other_obj_relation_def pde_relation_def) apply (erule_tac x="(ucast (p && mask pd_bits >> 2))" in allE) apply (clarsimp simp: mask_pd_bits_inner_beauty) apply (clarsimp simp: obj_at_def pde_relation_aligned_simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p = p' \<Longrightarrow> corres (pde_relation_aligned (p >> 2)) (pde_at p) (pde_at' p') (get_pde p) (getObject p') proof (prove)
goal (1 subgoal):
 1. p = p' \<Longrightarrow> corres (pde_relation_aligned (p' >> 2)) (pde_at p') (pde_at' p') (do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) (do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p = p'; True\<rbrakk> \<Longrightarrow> no_fail (pde_at' p') (do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od)
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pde_at p' s \<and> pde_at' p' s' \<longrightarrow> (\<forall>(r', t')\<in>fst ((do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) s'). \<exists>(r, t)\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>p = p'; True; pde_at' p' s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. fst (lookupAround2 p' (ksPSpace s)) \<noteq> None) and (\<lambda>sa. fst (lookupAround2 p' (ksPSpace s)) \<noteq> None \<longrightarrow> (\<exists>obj. projectKO_opt (snd (the (fst (lookupAround2 p' (ksPSpace s))))) = Some obj \<and> is_aligned p' (objBits obj) \<and> fst (the (fst (lookupAround2 p' (ksPSpace s)))) = p' \<and> (case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits obj \<le> x - p')))) s)) s
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pde_at p' s \<and> pde_at' p' s' \<longrightarrow> (\<forall>(r', t')\<in>fst ((do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) s'). \<exists>(r, t)\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>p = p'; ksPSpace s p' = Some ko; is_aligned p' (objBitsKO ko); koTypeOf ko = ArchT PDET; ps_clear p' (objBitsKO ko) s\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt ko = Some obj \<and> is_aligned p' (objBits obj) \<and> (case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits obj \<le> x - p')
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pde_at p' s \<and> pde_at' p' s' \<longrightarrow> (\<forall>(r', t')\<in>fst ((do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) s'). \<exists>(r, t)\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s ko x8. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch x8); is_aligned p' (objBitsKO (KOArch x8)); archTypeOf x8 = PDET; ps_clear p' (objBitsKO (KOArch x8)) s; ko = KOArch x8\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt (KOArch x8) = Some obj \<and> is_aligned p' (objBits obj) \<and> (case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits obj \<le> x - p')
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pde_at p' s \<and> pde_at' p' s' \<longrightarrow> (\<forall>(r', t')\<in>fst ((do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) s'). \<exists>(r, t)\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s ko arch_kernel_object. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch arch_kernel_object); is_aligned p' (objBitsKO (KOArch arch_kernel_object)); archTypeOf arch_kernel_object = PDET; ps_clear p' (objBitsKO (KOArch arch_kernel_object)) s; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> \<exists>obj. projectKO_opt (KOArch arch_kernel_object) = Some obj \<and> is_aligned p' (objBits obj) \<and> (case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits obj \<le> x - p')
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pde_at p' s \<and> pde_at' p' s' \<longrightarrow> (\<forall>(r', t')\<in>fst ((do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) s'). \<exists>(r, t)\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s ko arch_kernel_object x3. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPDE x3)); is_aligned p' (objBitsKO (KOArch (KOPDE x3))); ps_clear p' (objBitsKO (KOArch (KOPDE x3))) s; ko = KOArch (KOPDE x3); arch_kernel_object = KOPDE x3\<rbrakk> \<Longrightarrow> is_aligned p' (objBits x3) \<and> (case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits x3 \<le> x - p')
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pde_at p' s \<and> pde_at' p' s' \<longrightarrow> (\<forall>(r', t')\<in>fst ((do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) s'). \<exists>(r, t)\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s x3. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPDE x3)); is_aligned p' (objBitsKO (KOArch (KOPDE x3))); ps_clear p' (objBitsKO (KOArch (KOPDE x3))) s\<rbrakk> \<Longrightarrow> case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPDE x3)) \<le> x - p'
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pde_at p' s \<and> pde_at' p' s' \<longrightarrow> (\<forall>(r', t')\<in>fst ((do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) s'). \<exists>(r, t)\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r r') proof (prove)
goal (4 subgoals):
 1. \<And>s x3. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPDE x3)); is_aligned p' (objBitsKO (KOArch (KOPDE x3)))\<rbrakk> \<Longrightarrow> p' \<le> p'
 2. \<And>s x3. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPDE x3)); is_aligned p' (objBitsKO (KOArch (KOPDE x3)))\<rbrakk> \<Longrightarrow> p' \<le> p' + 2 ^ objBitsKO (KOArch (KOPDE x3)) - 1
 3. \<And>s x3. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPDE x3)); is_aligned p' (objBitsKO (KOArch (KOPDE x3))); fst (lookupAround2 p' (ksPSpace s)) = Some (p', KOArch (KOPDE x3)); case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPDE x3)) \<le> x - p'\<rbrakk> \<Longrightarrow> case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPDE x3)) \<le> x - p'
 4. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pde_at p' s \<and> pde_at' p' s' \<longrightarrow> (\<forall>(r', t')\<in>fst ((do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) s'). \<exists>(r, t)\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r r') proof (prove)
goal (3 subgoals):
 1. \<And>s x3. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPDE x3)); is_aligned p' (objBitsKO (KOArch (KOPDE x3)))\<rbrakk> \<Longrightarrow> p' \<le> p' + 2 ^ objBitsKO (KOArch (KOPDE x3)) - 1
 2. \<And>s x3. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPDE x3)); is_aligned p' (objBitsKO (KOArch (KOPDE x3))); fst (lookupAround2 p' (ksPSpace s)) = Some (p', KOArch (KOPDE x3)); case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPDE x3)) \<le> x - p'\<rbrakk> \<Longrightarrow> case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPDE x3)) \<le> x - p'
 3. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pde_at p' s \<and> pde_at' p' s' \<longrightarrow> (\<forall>(r', t')\<in>fst ((do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) s'). \<exists>(r, t)\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s x3. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPDE x3)); is_aligned p' (objBitsKO (KOArch (KOPDE x3))); fst (lookupAround2 p' (ksPSpace s)) = Some (p', KOArch (KOPDE x3)); case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPDE x3)) \<le> x - p'\<rbrakk> \<Longrightarrow> case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPDE x3)) \<le> x - p'
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pde_at p' s \<and> pde_at' p' s' \<longrightarrow> (\<forall>(r', t')\<in>fst ((do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) s'). \<exists>(r, t)\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r r') proof (prove)
goal (1 subgoal):
 1. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pde_at p' s \<and> pde_at' p' s' \<longrightarrow> (\<forall>(r', t')\<in>fst ((do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) s'). \<exists>(r, t)\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r r') proof (prove)
goal (1 subgoal):
 1. p = p' \<Longrightarrow> \<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> pde_at p' s \<and> pde_at' p' s' \<longrightarrow> (\<forall>x\<in>fst ((do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 p' map));
loadObject_default p' (fst p) (snd (lookupAround2 p' map)) (snd p)
od) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) s). case x of (r, t) \<Rightarrow> (t, t') \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r r') proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>p = p'; (a, b) \<in> state_relation; pde_at p' a; pde_at' p' b; ksPSpace b p' = Some (KOArch (KOPDE aa)); is_aligned p' (objBits aa); ((), ba) \<in> fst (magnitudeCheck p' (snd (lookupAround2 p' (ksPSpace b))) (objBits aa) b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pd_bits) = Some y);
pd <- case the (x (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>p = p'; (a, b) \<in> state_relation; pde_at p' a; pde_at' p' b; ksPSpace b p' = Some (KOArch (KOPDE aa)); is_aligned p' (objBits aa); ((), ba) \<in> fst (magnitudeCheck p' (snd (lookupAround2 p' (ksPSpace b))) (objBits aa) b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do x <- assert (\<exists>y. kheap a (p' && ~~ mask pd_bits) = Some y);
pd <- case the (kheap a (p' && ~~ mask pd_bits)) of ArchObj (PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)))
od) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba pd. \<lbrakk>p = p'; (a, b) \<in> state_relation; pde_at' p' b; ksPSpace b p' = Some (KOArch (KOPDE aa)); is_aligned p' (objBits aa); ((), ba) \<in> fst (magnitudeCheck p' (snd (lookupAround2 p' (ksPSpace b))) (objBits aa) b); is_aligned p' 2; kheap a (p' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2))) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> pde_relation_aligned (p' >> 2) r aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba pd. \<lbrakk>p = p'; (a, b) \<in> state_relation; pde_at' p' b; ksPSpace b p' = Some (KOArch (KOPDE aa)); is_aligned p' (objBits aa); ((), ba) \<in> fst (magnitudeCheck p' (snd (lookupAround2 p' (ksPSpace b))) (objBits aa) b); is_aligned p' 2; kheap a (p' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (a, ba) \<in> state_relation \<and> pde_relation_aligned (p' >> 2) (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba pd. \<lbrakk>p = p'; (a, b) \<in> state_relation; ksPSpace b p' = Some (KOArch (KOPDE aa)); is_aligned p' (objBits aa); ((), ba) \<in> fst (magnitudeCheck p' (snd (lookupAround2 p' (ksPSpace b))) (objBits aa) b); is_aligned p' 2; kheap a (p' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); is_aligned p' (objBitsKO (KOArch (KOPDE aa))); ps_clear p' (objBitsKO (KOArch (KOPDE aa))) b\<rbrakk> \<Longrightarrow> (a, ba) \<in> state_relation \<and> pde_relation_aligned (p' >> 2) (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pd. \<lbrakk>p = p'; (a, b) \<in> state_relation; ksPSpace b p' = Some (KOArch (KOPDE aa)); ps_clear p' 2 b; is_aligned p' 2; kheap a (p' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> pde_relation_aligned (p' >> 2) (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pd. \<lbrakk>p = p'; ksPSpace b p' = Some (KOArch (KOPDE aa)); ps_clear p' 2 b; is_aligned p' 2; kheap a (p' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pspace_dom (kheap a) = dom (ksPSpace b); \<forall>x\<in>dom (kheap a). \<forall>xa\<in>obj_relation_cuts (the (kheap a x)) x. case xa of (y, P) \<Rightarrow> P (the (kheap a x)) (the (ksPSpace b y)); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b\<rbrakk> \<Longrightarrow> pde_relation_aligned (p' >> 2) (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pd. \<lbrakk>p = p'; ksPSpace b p' = Some (KOArch (KOPDE aa)); ps_clear p' 2 b; is_aligned p' 2; kheap a (p' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pspace_dom (kheap a) = dom (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x\<in>obj_relation_cuts (the (kheap a (p' && ~~ mask pd_bits))) (p' && ~~ mask pd_bits). case x of (y, P) \<Rightarrow> P (the (kheap a (p' && ~~ mask pd_bits))) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> pde_relation_aligned (p' >> 2) (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pd. \<lbrakk>p = p'; ksPSpace b p' = Some (KOArch (KOPDE aa)); ps_clear p' 2 b; is_aligned p' 2; kheap a (p' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pspace_dom (kheap a) = dom (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<forall>x. \<exists>pde. the (ksPSpace b ((p' && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) x << 2))) = KOArch (KOPDE pde) \<and> pde_relation_aligned x (pd x) pde\<rbrakk> \<Longrightarrow> pde_relation_aligned (p' >> 2) (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pd. \<lbrakk>p = p'; ksPSpace b p' = Some (KOArch (KOPDE aa)); ps_clear p' 2 b; is_aligned p' 2; kheap a (p' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pspace_dom (kheap a) = dom (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; \<exists>pde. the (ksPSpace b ((p' && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) << 2))) = KOArch (KOPDE pde) \<and> pde_relation_aligned (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (pd (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) pde\<rbrakk> \<Longrightarrow> pde_relation_aligned (p' >> 2) (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pd. \<lbrakk>p = p'; ksPSpace b p' = Some (KOArch (KOPDE aa)); ps_clear p' 2 b; is_aligned p' 2; kheap a (p' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); pspace_dom (kheap a) = dom (ksPSpace b); ekheap_relation (ekheap a) (ksPSpace b); sched_act_relation (scheduler_action a) (ksSchedulerAction b); ready_queues_relation (ready_queues a) (ksReadyQueues b); ghost_relation (kheap a) (gsUserPages b) (gsCNodes b); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) a) (cdt a) (ctes_of b); cdt_list_relation (cdt_list a) (cdt a) (ctes_of b); revokable_relation (is_original_cap a) (null_filter (caps_of_state a)) (ctes_of b); (arch_state a, ksArchState b) \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node a) (interrupt_states a) (ksInterruptState b); cur_thread a = ksCurThread b; idle_thread a = ksIdleThread b; machine_state a = ksMachineState b; work_units_completed a = ksWorkUnitsCompleted b; domain_index a = ksDomScheduleIdx b; domain_list a = ksDomSchedule b; cur_domain a = ksCurDomain b; domain_time a = ksDomainTime b; pde_relation_aligned (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2)) (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2))) aa\<rbrakk> \<Longrightarrow> pde_relation_aligned (p' >> 2) (pd (UCAST(32 \<rightarrow> 12) (p' && mask pd_bits >> 2))) aa proof (prove)
goal:
No subgoals!