theory ArchAcc_R

lemma getObject_PTE_corres [corres]:
  "p = p' \<Longrightarrow> corres (pte_relation_aligned (p >> 2)) (pte_at p) (pte_at' p')
     (get_pte p) (getObject p')" apply (simp add: getObject_def get_pte_def get_pt_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_all)[1] apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object, simp_all add: projectKOs)[1] 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: obj_at_def pte_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 pteBits_def) apply (clarsimp simp: state_relation_def pspace_relation_def) apply (drule bspec, blast) apply (clarsimp simp: other_obj_relation_def pte_relation_def) apply (erule_tac x="(ucast (p && mask pt_bits >> 2))" in allE) apply (clarsimp simp: mask_pt_bits_inner_beauty
                        pte_relation_aligned_simp obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p = p' \<Longrightarrow> corres (pte_relation_aligned (p >> 2)) (pte_at p) (pte_at' p') (get_pte p) (getObject p') proof (prove)
goal (1 subgoal):
 1. p = p' \<Longrightarrow> corres (pte_relation_aligned (p' >> 2)) (pte_at p') (pte_at' p') (do x <- gets kheap;
xa <- assert (\<exists>y. x (p' && ~~ mask pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_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 (pte_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. pte_at p' s \<and> pte_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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pte_relation_aligned (p' >> 2) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>p = p'; True; pte_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. pte_at p' s \<and> pte_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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pte_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 PTET; 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. pte_at p' s \<and> pte_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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pte_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 = PTET; 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. pte_at p' s \<and> pte_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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pte_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 = PTET; 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. pte_at p' s \<and> pte_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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pte_relation_aligned (p' >> 2) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s ko arch_kernel_object x2. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPTE x2)); is_aligned p' (objBitsKO (KOArch (KOPTE x2))); ps_clear p' (objBitsKO (KOArch (KOPTE x2))) s; ko = KOArch (KOPTE x2); arch_kernel_object = KOPTE x2\<rbrakk> \<Longrightarrow> is_aligned p' (objBits x2) \<and> (case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits x2 \<le> x - p')
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pte_at p' s \<and> pte_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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pte_relation_aligned (p' >> 2) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPTE x2)); is_aligned p' (objBitsKO (KOArch (KOPTE x2))); ps_clear p' (objBitsKO (KOArch (KOPTE x2))) s\<rbrakk> \<Longrightarrow> case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPTE x2)) \<le> x - p'
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pte_at p' s \<and> pte_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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pte_relation_aligned (p' >> 2) r r') proof (prove)
goal (4 subgoals):
 1. \<And>s x2. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPTE x2)); is_aligned p' (objBitsKO (KOArch (KOPTE x2)))\<rbrakk> \<Longrightarrow> p' \<le> p'
 2. \<And>s x2. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPTE x2)); is_aligned p' (objBitsKO (KOArch (KOPTE x2)))\<rbrakk> \<Longrightarrow> p' \<le> p' + 2 ^ objBitsKO (KOArch (KOPTE x2)) - 1
 3. \<And>s x2. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPTE x2)); is_aligned p' (objBitsKO (KOArch (KOPTE x2))); fst (lookupAround2 p' (ksPSpace s)) = Some (p', KOArch (KOPTE x2)); case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPTE x2)) \<le> x - p'\<rbrakk> \<Longrightarrow> case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPTE x2)) \<le> x - p'
 4. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pte_at p' s \<and> pte_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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pte_relation_aligned (p' >> 2) r r') proof (prove)
goal (3 subgoals):
 1. \<And>s x2. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPTE x2)); is_aligned p' (objBitsKO (KOArch (KOPTE x2)))\<rbrakk> \<Longrightarrow> p' \<le> p' + 2 ^ objBitsKO (KOArch (KOPTE x2)) - 1
 2. \<And>s x2. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPTE x2)); is_aligned p' (objBitsKO (KOArch (KOPTE x2))); fst (lookupAround2 p' (ksPSpace s)) = Some (p', KOArch (KOPTE x2)); case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPTE x2)) \<le> x - p'\<rbrakk> \<Longrightarrow> case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPTE x2)) \<le> x - p'
 3. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pte_at p' s \<and> pte_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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pte_relation_aligned (p' >> 2) r r') proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOPTE x2)); is_aligned p' (objBitsKO (KOArch (KOPTE x2))); fst (lookupAround2 p' (ksPSpace s)) = Some (p', KOArch (KOPTE x2)); case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPTE x2)) \<le> x - p'\<rbrakk> \<Longrightarrow> case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOArch (KOPTE x2)) \<le> x - p'
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pte_at p' s \<and> pte_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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pte_relation_aligned (p' >> 2) r r') proof (prove)
goal (1 subgoal):
 1. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. pte_at p' s \<and> pte_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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) s). (t, t') \<in> state_relation \<and> pte_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> pte_at p' s \<and> pte_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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) s). case x of (r, t) \<Rightarrow> (t, t') \<in> state_relation \<and> pte_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; pte_at p' a; pte_at' p' b; ksPSpace b p' = Some (KOArch (KOPTE 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 pt_bits) = Some y);
pt <- case the (x (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> pte_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; pte_at p' a; pte_at' p' b; ksPSpace b p' = Some (KOArch (KOPTE 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 pt_bits) = Some y);
pt <- case the (kheap a (p' && ~~ mask pt_bits)) of ArchObj (PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2)))
od) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> pte_relation_aligned (p' >> 2) r aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba pt. \<lbrakk>p = p'; (a, b) \<in> state_relation; pte_at' p' b; ksPSpace b p' = Some (KOArch (KOPTE 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 pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2))) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> pte_relation_aligned (p' >> 2) r aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba pt. \<lbrakk>p = p'; (a, b) \<in> state_relation; pte_at' p' b; ksPSpace b p' = Some (KOArch (KOPTE 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 pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (a, ba) \<in> state_relation \<and> pte_relation_aligned (p' >> 2) (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba pt. \<lbrakk>p = p'; (a, b) \<in> state_relation; ksPSpace b p' = Some (KOArch (KOPTE 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 pt_bits) = Some (ArchObj (PageTable pt)); is_aligned p' (objBitsKO (KOArch (KOPTE aa))); ps_clear p' (objBitsKO (KOArch (KOPTE aa))) b\<rbrakk> \<Longrightarrow> (a, ba) \<in> state_relation \<and> pte_relation_aligned (p' >> 2) (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pt. \<lbrakk>p = p'; (a, b) \<in> state_relation; ksPSpace b p' = Some (KOArch (KOPTE aa)); ps_clear p' 2 b; is_aligned p' 2; kheap a (p' && ~~ mask pt_bits) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> pte_relation_aligned (p' >> 2) (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pt. \<lbrakk>p = p'; ksPSpace b p' = Some (KOArch (KOPTE aa)); ps_clear p' 2 b; is_aligned p' 2; kheap a (p' && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); 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> pte_relation_aligned (p' >> 2) (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pt. \<lbrakk>p = p'; ksPSpace b p' = Some (KOArch (KOPTE aa)); ps_clear p' 2 b; is_aligned p' 2; kheap a (p' && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); 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 pt_bits))) (p' && ~~ mask pt_bits). case x of (y, P) \<Rightarrow> P (the (kheap a (p' && ~~ mask pt_bits))) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> pte_relation_aligned (p' >> 2) (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pt. \<lbrakk>p = p'; ksPSpace b p' = Some (KOArch (KOPTE aa)); ps_clear p' 2 b; is_aligned p' 2; kheap a (p' && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); 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>pte. the (ksPSpace b ((p' && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) x << 2))) = KOArch (KOPTE pte) \<and> pte_relation_aligned x (pt x) pte\<rbrakk> \<Longrightarrow> pte_relation_aligned (p' >> 2) (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2))) aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pt. \<lbrakk>p = p'; ksPSpace b p' = Some (KOArch (KOPTE aa)); ps_clear p' 2 b; is_aligned p' 2; kheap a (p' && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); 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>pte. the (ksPSpace b ((p' && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) << 2))) = KOArch (KOPTE pte) \<and> pte_relation_aligned (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (pt (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) pte\<rbrakk> \<Longrightarrow> pte_relation_aligned (p' >> 2) (pt (UCAST(32 \<rightarrow> 8) (p' && mask pt_bits >> 2))) aa proof (prove)
goal:
No subgoals!