theory KHeap_AI

lemma shows
  sts_caps_of_state[wp]:
    "set_thread_state t st \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace>" and
  set_bound_caps_of_state[wp]:
    "set_bound_notification t e \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace>" and
  as_user_caps_of_state[wp]:
    "as_user p f \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace>" unfolding set_thread_state_def set_bound_notification_def as_user_def set_object_def get_object_def
            set_mrs_def apply (all \<open>(wp | wpc | simp)+ ; clarsimp, erule rsubst[where P=P], rule cte_wp_caps_of_lift\<close>) by (auto simp: cte_wp_at_cases2 tcb_cnode_map_def dest!: get_tcb_SomeD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_thread_state t st \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> &&& \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_bound_notification t e \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> &&& \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> as_user p 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 t;
do kobj <- do kh <- gets kheap;
assert (kh t \<noteq> None);
return $ the $ kh t
od;
assert (a_type kobj = a_type (TCB (tcb\<lparr>tcb_state := st\<rparr>)));
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := st\<rparr>))\<rparr>)
od;
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> &&& \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the $ get_tcb t;
kobj <- do kh <- gets kheap;
assert (kh t \<noteq> None);
return $ the $ kh t
od;
assert (a_type kobj = a_type (TCB (tcb\<lparr>tcb_bound_notification := e\<rparr>)));
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_bound_notification := e\<rparr>))\<rparr>)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> &&& \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the $ get_tcb p;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
do kobj <- do kh <- gets kheap;
assert (kh p \<noteq> None);
return $ the $ kh p
od;
assert (a_type kobj = a_type (TCB new_tcb));
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB new_tcb)\<rparr>)
od;
return a
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s y tcb p P. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P p s = cte_wp_at P p (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>)) else kheap s a\<rparr>)
 2. \<And>s y tcb p P. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P p s = cte_wp_at P p (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_bound_notification := e\<rparr>)) else kheap s a\<rparr>)
 3. \<And>s y x xa tcb pa P. \<lbrakk>(x, xa) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); get_tcb p s = Some y; kheap s p = Some (TCB tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P pa s = cte_wp_at P pa (s\<lparr>kheap := \<lambda>a. if a = p then Some (TCB (the (get_tcb p s)\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch (the (get_tcb p s)))\<rparr>)) else kheap s a\<rparr>)