theory ArchAcc_R

lemma getObject_ASIDPool_corres [corres]:
  "p = p' \<Longrightarrow> corres (\<lambda>p p'. p = inv ASIDPool p' o ucast)
          (asid_pool_at p) (asid_pool_at' p')
          (get_asid_pool p) (getObject p')" apply (simp add: getObject_def get_asid_pool_def get_object_def split_def) apply (rule corres_no_failI) apply (rule no_fail_pre, wp) apply (clarsimp simp: typ_at'_def ko_wp_at'_def) apply (case_tac ko; simp) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object, simp_all)[1] apply (clarsimp simp: lookupAround2_known1
                         projectKOs) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps
                         archObjSize_def) apply (erule (1) ps_clear_lookupAround2) apply simp apply (erule is_aligned_no_overflow) apply simp apply (clarsimp simp add: objBits_simps archObjSize_def
                      split: option.split) apply (clarsimp simp: in_monad loadObject_default_def projectKOs) apply (simp add: bind_assoc exec_gets) apply (drule asid_pool_at_ko) apply (clarsimp simp: obj_at_def) apply (simp add: return_def) apply (simp add: in_magnitude_check objBits_simps
                   archObjSize_def pageBits_def) apply (clarsimp simp: state_relation_def pspace_relation_def) apply (drule bspec, blast) apply (clarsimp simp: other_obj_relation_def asid_pool_relation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p = p' \<Longrightarrow> corres (\<lambda>p p'. p = inv asidpool.ASIDPool p' \<circ> UCAST(10 \<rightarrow> 32)) (typ_at (AArch AASIDPool) p) (asid_pool_at' p') (get_asid_pool p) (getObject p') proof (prove)
goal (1 subgoal):
 1. p = p' \<Longrightarrow> corres (\<lambda>p p'. p = inv asidpool.ASIDPool p' \<circ> UCAST(10 \<rightarrow> 32)) (typ_at (AArch AASIDPool) p') (asid_pool_at' p') (do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
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 (asid_pool_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. typ_at (AArch AASIDPool) p' s \<and> asid_pool_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 kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) s). (t, t') \<in> state_relation \<and> r = inv asidpool.ASIDPool r' \<circ> UCAST(10 \<rightarrow> 32)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>p = p'; True; asid_pool_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. typ_at (AArch AASIDPool) p' s \<and> asid_pool_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 kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) s). (t, t') \<in> state_relation \<and> r = inv asidpool.ASIDPool r' \<circ> UCAST(10 \<rightarrow> 32)) 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 ASIDPoolT; ps_clear p' (objBitsKO ko) s\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p' (ksPSpace s)) = Some (a, b)) \<and> ((\<exists>a b. fst (lookupAround2 p' (ksPSpace s)) = Some (a, b)) \<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')))
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. typ_at (AArch AASIDPool) p' s \<and> asid_pool_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 kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) s). (t, t') \<in> state_relation \<and> r = inv asidpool.ASIDPool r' \<circ> UCAST(10 \<rightarrow> 32)) 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 = ASIDPoolT; ps_clear p' (objBitsKO (KOArch x8)) s; ko = KOArch x8\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p' (ksPSpace s)) = Some (a, b)) \<and> ((\<exists>a b. fst (lookupAround2 p' (ksPSpace s)) = Some (a, b)) \<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')))
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. typ_at (AArch AASIDPool) p' s \<and> asid_pool_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 kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) s). (t, t') \<in> state_relation \<and> r = inv asidpool.ASIDPool r' \<circ> UCAST(10 \<rightarrow> 32)) 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 = ASIDPoolT; ps_clear p' (objBitsKO (KOArch arch_kernel_object)) s; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p' (ksPSpace s)) = Some (a, b)) \<and> ((\<exists>a b. fst (lookupAround2 p' (ksPSpace s)) = Some (a, b)) \<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')))
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. typ_at (AArch AASIDPool) p' s \<and> asid_pool_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 kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) s). (t, t') \<in> state_relation \<and> r = inv asidpool.ASIDPool r' \<circ> UCAST(10 \<rightarrow> 32)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko arch_kernel_object x1. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOASIDPool x1)); is_aligned p' (objBitsKO (KOArch (KOASIDPool x1))); ps_clear p' (objBitsKO (KOArch (KOASIDPool x1))) s; ko = KOArch (KOASIDPool x1); arch_kernel_object = KOASIDPool x1\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 p' (ksPSpace s)) = Some (a, b)) \<and> ((\<exists>a b. fst (lookupAround2 p' (ksPSpace s)) = Some (a, b)) \<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')))
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. typ_at (AArch AASIDPool) p' s \<and> asid_pool_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 kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) s). (t, t') \<in> state_relation \<and> r = inv asidpool.ASIDPool r' \<circ> UCAST(10 \<rightarrow> 32)) proof (prove)
goal (2 subgoals):
 1. \<And>s x1. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOASIDPool x1)); is_aligned p' (objBitsKO (KOArch (KOASIDPool x1))); ps_clear p' (objBitsKO (KOArch (KOASIDPool x1))) s\<rbrakk> \<Longrightarrow> is_aligned p' (objBits x1) \<and> (case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits x1 \<le> x - p')
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. typ_at (AArch AASIDPool) p' s \<and> asid_pool_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 kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) s). (t, t') \<in> state_relation \<and> r = inv asidpool.ASIDPool r' \<circ> UCAST(10 \<rightarrow> 32)) proof (prove)
goal (2 subgoals):
 1. \<And>s x1. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOASIDPool x1)); is_aligned p' pageBits; ps_clear p' pageBits s\<rbrakk> \<Longrightarrow> case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ pageBits \<le> x - p'
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. typ_at (AArch AASIDPool) p' s \<and> asid_pool_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 kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) s). (t, t') \<in> state_relation \<and> r = inv asidpool.ASIDPool r' \<circ> UCAST(10 \<rightarrow> 32)) proof (prove)
goal (4 subgoals):
 1. \<And>s x1. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOASIDPool x1)); is_aligned p' pageBits\<rbrakk> \<Longrightarrow> p' \<le> p'
 2. \<And>s x1. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOASIDPool x1)); is_aligned p' pageBits\<rbrakk> \<Longrightarrow> p' \<le> p' + 2 ^ pageBits - 1
 3. \<And>s x1. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOASIDPool x1)); is_aligned p' pageBits; fst (lookupAround2 p' (ksPSpace s)) = Some (p', KOArch (KOASIDPool x1)); case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ pageBits \<le> x - p'\<rbrakk> \<Longrightarrow> case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ pageBits \<le> x - p'
 4. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. typ_at (AArch AASIDPool) p' s \<and> asid_pool_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 kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) s). (t, t') \<in> state_relation \<and> r = inv asidpool.ASIDPool r' \<circ> UCAST(10 \<rightarrow> 32)) proof (prove)
goal (3 subgoals):
 1. \<And>s x1. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOASIDPool x1)); is_aligned p' pageBits\<rbrakk> \<Longrightarrow> p' \<le> p' + 2 ^ pageBits - 1
 2. \<And>s x1. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOASIDPool x1)); is_aligned p' pageBits; fst (lookupAround2 p' (ksPSpace s)) = Some (p', KOArch (KOASIDPool x1)); case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ pageBits \<le> x - p'\<rbrakk> \<Longrightarrow> case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ pageBits \<le> x - p'
 3. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. typ_at (AArch AASIDPool) p' s \<and> asid_pool_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 kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) s). (t, t') \<in> state_relation \<and> r = inv asidpool.ASIDPool r' \<circ> UCAST(10 \<rightarrow> 32)) proof (prove)
goal (2 subgoals):
 1. \<And>s x1. \<lbrakk>p = p'; ksPSpace s p' = Some (KOArch (KOASIDPool x1)); is_aligned p' pageBits; fst (lookupAround2 p' (ksPSpace s)) = Some (p', KOArch (KOASIDPool x1)); case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ pageBits \<le> x - p'\<rbrakk> \<Longrightarrow> case snd (lookupAround2 p' (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ pageBits \<le> x - p'
 2. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. typ_at (AArch AASIDPool) p' s \<and> asid_pool_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 kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) s). (t, t') \<in> state_relation \<and> r = inv asidpool.ASIDPool r' \<circ> UCAST(10 \<rightarrow> 32)) proof (prove)
goal (1 subgoal):
 1. p = p' \<Longrightarrow> \<forall>(s, s')\<in>state_relation. typ_at (AArch AASIDPool) p' s \<and> asid_pool_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 kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
case kobj of ArchObj (arch_kernel_obj.ASIDPool pool) \<Rightarrow> return pool | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) s). (t, t') \<in> state_relation \<and> r = inv asidpool.ASIDPool r' \<circ> UCAST(10 \<rightarrow> 32)) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>p = p'; (a, b) \<in> state_relation; (aa, ba) \<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) b); typ_at (AArch AASIDPool) p' a; asid_pool_at' p' b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od >>= Structures_A.kernel_object.case_kernel_object (\<lambda>nat fun. fail) (\<lambda>tcb_ext. fail) (\<lambda>endpoint. fail) (\<lambda>notification_ext. fail) (case_arch_kernel_obj return (\<lambda>fun. fail) (\<lambda>fun. fail) (\<lambda>bool vmpage_size. fail))) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> r = inv asidpool.ASIDPool aa \<circ> UCAST(10 \<rightarrow> 32) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>p = p'; (a, b) \<in> state_relation; typ_at (AArch AASIDPool) p' a; asid_pool_at' p' b; ksPSpace b p' = Some (KOArch (KOASIDPool 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 kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od >>= Structures_A.kernel_object.case_kernel_object (\<lambda>nat fun. fail) (\<lambda>tcb_ext. fail) (\<lambda>endpoint. fail) (\<lambda>notification_ext. fail) (case_arch_kernel_obj return (\<lambda>fun. fail) (\<lambda>fun. fail) (\<lambda>bool vmpage_size. fail))) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> r = inv asidpool.ASIDPool aa \<circ> UCAST(10 \<rightarrow> 32) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>p = p'; (a, b) \<in> state_relation; typ_at (AArch AASIDPool) p' a; asid_pool_at' p' b; ksPSpace b p' = Some (KOArch (KOASIDPool 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 y <- assert (\<exists>y. kheap a p' = Some y);
case the (kheap a p') of ArchObj (arch_kernel_obj.ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> r = inv asidpool.ASIDPool aa \<circ> UCAST(10 \<rightarrow> 32) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>p = p'; (a, b) \<in> state_relation; asid_pool_at' p' b; ksPSpace b p' = Some (KOArch (KOASIDPool aa)); is_aligned p' (objBits aa); ((), ba) \<in> fst (magnitudeCheck p' (snd (lookupAround2 p' (ksPSpace b))) (objBits aa) b); \<exists>pool. ako_at (arch_kernel_obj.ASIDPool pool) p' a\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do y <- assert (\<exists>y. kheap a p' = Some y);
case the (kheap a p') of ArchObj (arch_kernel_obj.ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail
od) a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> r = inv asidpool.ASIDPool aa \<circ> UCAST(10 \<rightarrow> 32) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba pool. \<lbrakk>p = p'; (a, b) \<in> state_relation; asid_pool_at' p' b; ksPSpace b p' = Some (KOArch (KOASIDPool aa)); is_aligned p' (objBits aa); ((), ba) \<in> fst (magnitudeCheck p' (snd (lookupAround2 p' (ksPSpace b))) (objBits aa) b); kheap a p' = Some (ArchObj (arch_kernel_obj.ASIDPool pool))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (return pool a). case x of (r, t) \<Rightarrow> (t, ba) \<in> state_relation \<and> r = inv asidpool.ASIDPool aa \<circ> UCAST(10 \<rightarrow> 32) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba pool. \<lbrakk>p = p'; (a, b) \<in> state_relation; asid_pool_at' p' b; ksPSpace b p' = Some (KOArch (KOASIDPool aa)); is_aligned p' (objBits aa); ((), ba) \<in> fst (magnitudeCheck p' (snd (lookupAround2 p' (ksPSpace b))) (objBits aa) b); kheap a p' = Some (ArchObj (arch_kernel_obj.ASIDPool pool))\<rbrakk> \<Longrightarrow> (a, ba) \<in> state_relation \<and> pool = inv asidpool.ASIDPool aa \<circ> UCAST(10 \<rightarrow> 32) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pool. \<lbrakk>p = p'; (a, b) \<in> state_relation; asid_pool_at' p' b; ksPSpace b p' = Some (KOArch (KOASIDPool aa)); is_aligned p' 12; ps_clear p' 12 b; kheap a p' = Some (ArchObj (arch_kernel_obj.ASIDPool pool))\<rbrakk> \<Longrightarrow> pool = inv asidpool.ASIDPool aa \<circ> UCAST(10 \<rightarrow> 32) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pool. \<lbrakk>p = p'; asid_pool_at' p' b; ksPSpace b p' = Some (KOArch (KOASIDPool aa)); is_aligned p' 12; ps_clear p' 12 b; kheap a p' = Some (ArchObj (arch_kernel_obj.ASIDPool pool)); 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> pool = inv asidpool.ASIDPool aa \<circ> UCAST(10 \<rightarrow> 32) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa pool. \<lbrakk>p = p'; asid_pool_at' p' b; ksPSpace b p' = Some (KOArch (KOASIDPool aa)); is_aligned p' 12; ps_clear p' 12 b; kheap a p' = Some (ArchObj (arch_kernel_obj.ASIDPool pool)); 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')) p'. case x of (y, P) \<Rightarrow> P (the (kheap a p')) (the (ksPSpace b y))\<rbrakk> \<Longrightarrow> pool = inv asidpool.ASIDPool aa \<circ> UCAST(10 \<rightarrow> 32) proof (prove)
goal:
No subgoals!