theory CSpaceInv_AI

lemma as_user_only_idle :
  "\<lbrace>only_idle\<rbrace> as_user t m \<lbrace>\<lambda>_. only_idle\<rbrace>" apply (simp add: as_user_def set_object_def get_object_def split_def) apply wp apply (clarsimp simp del: fun_upd_apply) apply (erule only_idle_tcb_update) apply (drule get_tcb_SomeD) apply (fastforce simp: obj_at_def) by (simp add: get_tcb_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle\<rbrace> as_user t m \<lbrace>\<lambda>_. only_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle\<rbrace> do tcb <- gets_the (get_tcb t);
p <- select_f (m (arch_tcb_context_get (tcb_arch tcb)));
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
return (fst p)
od \<lbrace>\<lambda>_. only_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. only_idle s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (m (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> only_idle (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb a b. \<lbrakk>only_idle s; get_tcb t s = Some y; kheap s t = Some (TCB tcb); (a, b) \<in> fst (m (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> only_idle (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb a b. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb); (a, b) \<in> fst (m (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> ko_at (TCB (?t27 s y tcb a b)) t s
 2. \<And>s y tcb a b. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb); (a, b) \<in> fst (m (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> tcb_state (?t27 s y tcb a b) = tcb_state (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>) \<or> tcb_state (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>) \<noteq> IdleThreadState proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb a b. \<lbrakk>kheap s t = Some (TCB tcb); (a, b) \<in> fst (m (arch_tcb_context_get (tcb_arch y))); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> ko_at (TCB (?t27 s y tcb a b)) t s
 2. \<And>s y tcb a b. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb); (a, b) \<in> fst (m (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> tcb_state (?t27 s y tcb a b) = tcb_state (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>) \<or> tcb_state (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>) \<noteq> IdleThreadState proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb a b. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb); (a, b) \<in> fst (m (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> tcb_state tcb = tcb_state (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>) \<or> tcb_state (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>) \<noteq> IdleThreadState