theory TcbAcc_AI

lemma as_user_caps [wp]:
  "\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> as_user a f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" apply (simp add: as_user_def split_def set_object_def get_object_def) apply wp apply (clarsimp cong: if_cong) apply (clarsimp simp: get_tcb_def split: option.splits Structures_A.kernel_object.splits) apply (subst cte_wp_caps_of_lift) prefer 2 apply simp apply (clarsimp simp: cte_wp_at_cases tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> as_user a f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the (get_tcb a);
p <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh a = Some y);
return (the (kh a))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
return (fst p)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (caps_of_state s) \<Longrightarrow> get_tcb a s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb a s))))). (\<exists>y. kheap s a = Some y) \<longrightarrow> a_type (the (kheap s a)) = ATCB \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb a s)))\<rparr>))\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb aa b. \<lbrakk>P (caps_of_state s); get_tcb a s = Some y; kheap s a = Some (TCB tcb); (aa, b) \<in> fst (f (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> P (caps_of_state (s\<lparr>kheap := \<lambda>c. if c = a then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>)) else kheap s c\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y aa b. \<lbrakk>P (caps_of_state s); kheap s a = Some (TCB y); (aa, b) \<in> fst (f (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> P (caps_of_state (s\<lparr>kheap := \<lambda>c. if c = a then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>)) else kheap s c\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s y aa b p Pa. \<lbrakk>P (caps_of_state s); kheap s a = Some (TCB y); (aa, b) \<in> fst (f (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> cte_wp_at Pa p (s\<lparr>kheap := \<lambda>c. if c = a then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>)) else kheap s c\<rparr>) = cte_wp_at Pa p (?s'28 s y aa b)
 2. \<And>s y aa b. \<lbrakk>P (caps_of_state s); kheap s a = Some (TCB y); (aa, b) \<in> fst (f (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> P (caps_of_state (?s'28 s y aa b)) proof (prove)
goal (2 subgoals):
 1. \<And>s y aa b. \<lbrakk>P (caps_of_state s); kheap s a = Some (TCB y); (aa, b) \<in> fst (f (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> P (caps_of_state (?s'28 s y aa b))
 2. \<And>s y aa b p Pa. \<lbrakk>P (caps_of_state s); kheap s a = Some (TCB y); (aa, b) \<in> fst (f (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> cte_wp_at Pa p (s\<lparr>kheap := \<lambda>c. if c = a then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>)) else kheap s c\<rparr>) = cte_wp_at Pa p (?s'28 s y aa b) proof (prove)
goal (1 subgoal):
 1. \<And>s y aa b p Pa. \<lbrakk>P (caps_of_state s); kheap s a = Some (TCB y); (aa, b) \<in> fst (f (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> cte_wp_at Pa p (s\<lparr>kheap := \<lambda>c. if c = a then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>)) else kheap s c\<rparr>) = cte_wp_at Pa p s proof (prove)
goal:
No subgoals!