theory TcbAcc_R

lemma threadSet_valid_pspace'T_P:
  assumes x: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases. getF (F tcb) = getF tcb"
  assumes z: "\<forall>tcb. (P \<longrightarrow> Q (tcbState tcb)) \<longrightarrow>
                     (\<forall>s. valid_tcb_state' (tcbState tcb) s
                              \<longrightarrow> valid_tcb_state' (tcbState (F tcb)) s)"
  assumes v: "\<forall>tcb. (P \<longrightarrow> Q' (tcbBoundNotification tcb)) \<longrightarrow>
                     (\<forall>s. valid_bound_ntfn' (tcbBoundNotification tcb) s
                              \<longrightarrow> valid_bound_ntfn' (tcbBoundNotification (F tcb)) s)"

  assumes y: "\<forall>tcb. is_aligned (tcbIPCBuffer tcb) msg_align_bits
                      \<longrightarrow> is_aligned (tcbIPCBuffer (F tcb)) msg_align_bits"
  assumes u: "\<forall>tcb. tcbDomain tcb \<le> maxDomain \<longrightarrow> tcbDomain (F tcb) \<le> maxDomain"
  assumes w: "\<forall>tcb. tcbPriority tcb \<le> maxPriority \<longrightarrow> tcbPriority (F tcb) \<le> maxPriority"
  assumes w': "\<forall>tcb. tcbMCP tcb \<le> maxPriority \<longrightarrow> tcbMCP (F tcb) \<le> maxPriority"
  shows
  "\<lbrace>valid_pspace' and (\<lambda>s. P \<longrightarrow> st_tcb_at' Q t s \<and> bound_tcb_at' Q' t s)\<rbrace>
     threadSet F t
   \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>" apply (simp add: valid_pspace'_def threadSet_def) apply (rule hoare_pre,
         wp setObject_tcb_valid_objs getObject_tcb_wp) apply (clarsimp simp: obj_at'_def projectKOs pred_tcb_at'_def) apply (erule(1) valid_objsE') apply (clarsimp simp add: valid_obj'_def valid_tcb'_def
                            bspec_split [OF spec [OF x]] z
                            split_paired_Ball y u w v w') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace' and (\<lambda>s. P \<longrightarrow> st_tcb_at' Q t s \<and> bound_tcb_at' Q' t s)\<rbrace> threadSet F t \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. P \<longrightarrow> st_tcb_at' Q t s \<and> bound_tcb_at' Q' t s)\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and (\<lambda>s. P \<longrightarrow> st_tcb_at' Q t s \<and> bound_tcb_at' Q' t s)) s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (valid_objs' and (tcb_at' t and valid_obj' (injectKO (F ta)))) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> (valid_mdb' and obj_at' (\<lambda>t. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF t = getF (F ta)) t) s) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; P \<longrightarrow> Q (tcbState obj) \<and> Q' (tcbBoundNotification obj); ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s\<rbrakk> \<Longrightarrow> valid_obj' (KOTCB (F obj)) s \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF obj = getF (F obj)) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; P \<longrightarrow> Q (tcbState obj) \<and> Q' (tcbBoundNotification obj); ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s; valid_obj' (KOTCB obj) s\<rbrakk> \<Longrightarrow> valid_obj' (KOTCB (F obj)) s \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF obj = getF (F obj)) proof (prove)
goal:
No subgoals!