theory ArchMove_C

lemma setCTE_asidpool':
  "\<lbrace> ko_at' (ASIDPool pool) p \<rbrace> setCTE c p' \<lbrace>\<lambda>_. ko_at' (ASIDPool pool) p\<rbrace>" apply (clarsimp simp: setCTE_def) apply (simp add: setObject_def split_def) apply (rule hoare_seq_ext [OF _ hoare_gets_sp]) apply (clarsimp simp: valid_def in_monad) apply (frule updateObject_type) apply (clarsimp simp: obj_at'_def projectKOs) apply (rule conjI) apply (clarsimp simp: lookupAround2_char1) apply (case_tac obj', auto)[1] apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object, auto)[1] apply (simp add: updateObject_cte) apply (clarsimp simp: updateObject_cte typeError_def magnitudeCheck_def in_monad
                   split: kernel_object.splits if_splits option.splits) apply (clarsimp simp: ps_clear_upd lookupAround2_char1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at' (asidpool.ASIDPool pool) p\<rbrace> setCTE c p' \<lbrace>\<lambda>_. ko_at' (asidpool.ASIDPool pool) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at' (asidpool.ASIDPool pool) p\<rbrace> setObject c p' \<lbrace>\<lambda>_. ko_at' (asidpool.ASIDPool pool) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at' (asidpool.ASIDPool pool) p\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 c ps));
obj' <- updateObject p' (snd p) c (fst p) (snd (lookupAround2 c ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>_. ko_at' (asidpool.ASIDPool pool) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ps. \<lbrace>\<lambda>s. ps = ksPSpace s \<and> ko_at' (asidpool.ASIDPool pool) p s\<rbrace> do p <- assert_opt (fst (lookupAround2 c ps));
obj' <- updateObject p' (snd p) c (fst p) (snd (lookupAround2 c ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>_. ko_at' (asidpool.ASIDPool pool) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>ko_at' (asidpool.ASIDPool pool) p s; fst (lookupAround2 c (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject p' ba c a (snd (lookupAround2 c (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> ko_at' (asidpool.ASIDPool pool) p (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>ko_at' (asidpool.ASIDPool pool) p s; fst (lookupAround2 c (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject p' ba c a (snd (lookupAround2 c (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba\<rbrakk> \<Longrightarrow> ko_at' (asidpool.ASIDPool pool) p (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>fst (lookupAround2 c (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject p' ba c a (snd (lookupAround2 c (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s\<rbrakk> \<Longrightarrow> (p = a \<longrightarrow> obj' = KOArch (KOASIDPool (asidpool.ASIDPool pool)) \<and> ps_clear a (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) \<and> (p \<noteq> a \<longrightarrow> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s a ba s'' obj'. \<lbrakk>fst (lookupAround2 c (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject p' ba c a (snd (lookupAround2 c (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s\<rbrakk> \<Longrightarrow> p = a \<longrightarrow> obj' = KOArch (KOASIDPool (asidpool.ASIDPool pool)) \<and> ps_clear a (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)
 2. \<And>s a ba s'' obj'. \<lbrakk>fst (lookupAround2 c (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject p' ba c a (snd (lookupAround2 c (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s\<rbrakk> \<Longrightarrow> p \<noteq> a \<longrightarrow> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s s'' obj'. \<lbrakk>(obj', s'') \<in> fst (updateObject p' (KOArch (KOASIDPool (asidpool.ASIDPool pool))) c p (snd (lookupAround2 c (ksPSpace s))) s); koTypeOf obj' = ArchT ASIDPoolT; is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s; p \<le> c; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); \<forall>z. p < z \<and> z \<le> c \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> obj' = KOArch (KOASIDPool (asidpool.ASIDPool pool)) \<and> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) (s''\<lparr>ksPSpace := (ksPSpace s)(p \<mapsto> obj')\<rparr>)
 2. \<And>s a ba s'' obj'. \<lbrakk>fst (lookupAround2 c (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject p' ba c a (snd (lookupAround2 c (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s\<rbrakk> \<Longrightarrow> p \<noteq> a \<longrightarrow> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s s'' x8. \<lbrakk>(KOArch x8, s'') \<in> fst (updateObject p' (KOArch (KOASIDPool (asidpool.ASIDPool pool))) c p (snd (lookupAround2 c (ksPSpace s))) s); archTypeOf x8 = ASIDPoolT; is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s; p \<le> c; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); \<forall>z. p < z \<and> z \<le> c \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> x8 = KOASIDPool (asidpool.ASIDPool pool)
 2. \<And>s a ba s'' obj'. \<lbrakk>fst (lookupAround2 c (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject p' ba c a (snd (lookupAround2 c (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s\<rbrakk> \<Longrightarrow> p \<noteq> a \<longrightarrow> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s s'' arch_kernel_object. \<lbrakk>(KOArch arch_kernel_object, s'') \<in> fst (updateObject p' (KOArch (KOASIDPool (asidpool.ASIDPool pool))) c p (snd (lookupAround2 c (ksPSpace s))) s); archTypeOf arch_kernel_object = ASIDPoolT; is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s; p \<le> c; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); \<forall>z. p < z \<and> z \<le> c \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> arch_kernel_object = KOASIDPool (asidpool.ASIDPool pool)
 2. \<And>s a ba s'' obj'. \<lbrakk>fst (lookupAround2 c (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject p' ba c a (snd (lookupAround2 c (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s\<rbrakk> \<Longrightarrow> p \<noteq> a \<longrightarrow> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s s'' x1. \<lbrakk>(KOArch (KOASIDPool x1), s'') \<in> fst (updateObject p' (KOArch (KOASIDPool (asidpool.ASIDPool pool))) c p (snd (lookupAround2 c (ksPSpace s))) s); is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s; p \<le> c; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); \<forall>z. p < z \<and> z \<le> c \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> x1 = asidpool.ASIDPool pool
 2. \<And>s a ba s'' obj'. \<lbrakk>fst (lookupAround2 c (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject p' ba c a (snd (lookupAround2 c (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s\<rbrakk> \<Longrightarrow> p \<noteq> a \<longrightarrow> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s s'' x1. \<lbrakk>(KOArch (KOASIDPool x1), s'') \<in> fst (typeError [] (KOArch (KOASIDPool (asidpool.ASIDPool pool))) s); is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s; p \<le> c; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); \<forall>z. p < z \<and> z \<le> c \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> x1 = asidpool.ASIDPool pool
 2. \<And>s a ba s'' obj'. \<lbrakk>fst (lookupAround2 c (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject p' ba c a (snd (lookupAround2 c (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s\<rbrakk> \<Longrightarrow> p \<noteq> a \<longrightarrow> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>fst (lookupAround2 c (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject p' ba c a (snd (lookupAround2 c (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba; ksPSpace s p = Some (KOArch (KOASIDPool (asidpool.ASIDPool pool))); is_aligned p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))); ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) s\<rbrakk> \<Longrightarrow> p \<noteq> a \<longrightarrow> ps_clear p (objBitsKO (KOArch (KOASIDPool (asidpool.ASIDPool pool)))) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>) proof (prove)
goal:
No subgoals!