kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpaceInv_AI

lemma remove_rights_cap_valid[simp]:
  "s \<turnstile> c \<Longrightarrow> s \<turnstile> remove_rights S c" using valid_validate_vm_rights apply (cases c; simp add: remove_rights_def cap_rights_update_def
                            valid_cap_def cap_aligned_def
                     split: bool.splits) by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> c \<Longrightarrow> s \<turnstile> remove_rights S c proof (prove)
using this:
validate_vm_rights ?rs \<in> valid_vm_rights

goal (1 subgoal):
 1. s \<turnstile> c \<Longrightarrow> s \<turnstile> remove_rights S c proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>is_aligned (the (aobj_ref x12)) (arch_obj_size x12) \<and> arch_obj_size x12 < word_bits \<and> valid_arch_cap x12 s; c = ArchObjectCap x12\<rbrakk> \<Longrightarrow> valid_arch_cap (acap_rights_update (acap_rights x12 - S) x12) s
theory CSpaceInv_AI

lemma get_thread_state_inv [simp]:
  "\<lbrace> P \<rbrace> get_thread_state t \<lbrace> \<lambda>r. P \<rbrace>" apply (simp add: get_thread_state_def thread_get_def gets_the_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_thread_state t \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do tcb <- gets (get_tcb t) >>= assert_opt;
return (tcb_state tcb)
od \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> P s proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma get_bound_notification_inv[simp]:
  "\<lbrace>P\<rbrace> get_bound_notification t \<lbrace>\<lambda>r. P\<rbrace>" apply (simp add: get_bound_notification_def thread_get_def gets_the_def) apply (wp, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_bound_notification t \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do tcb <- gets (get_tcb t) >>= assert_opt;
return (tcb_bound_notification tcb)
od \<lbrace>\<lambda>r. P\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma gets_the_sp:
  "\<lbrace> Q \<rbrace> gets_the f \<lbrace>\<lambda>rv s. f s = Some rv \<and> Q s\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> gets_the f \<lbrace>\<lambda>rv s. f s = Some rv \<and> Q s\<rbrace>
theory CSpaceInv_AI

lemma gets_the_get_tcb_sp:
  "\<lbrace> Q \<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>t. Q and ko_at (TCB t) thread\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>t. Q and ko_at (TCB t) thread\<rbrace>
theory CSpaceInv_AI

lemma assert_get_tcb_sp:
  assumes "\<And>s. Q s \<Longrightarrow> valid_objs s"
  shows "\<lbrace> Q \<rbrace> gets_the (get_tcb thread)
         \<lbrace>\<lambda>t. Q and ko_at (TCB t) thread and valid_tcb thread t \<rbrace>" apply (rule hoare_strengthen_post[OF gets_the_get_tcb_sp]) apply (clarsimp simp: obj_at_def) apply (erule (1) valid_objsE[where x=thread, OF assms]) apply (clarsimp simp: valid_obj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>t. Q and ko_at (TCB t) thread and valid_tcb thread t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (Q and ko_at (TCB rv) thread) s \<Longrightarrow> (Q and ko_at (TCB rv) thread and valid_tcb thread rv) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>Q s; kheap s thread = Some (TCB rv)\<rbrakk> \<Longrightarrow> valid_tcb thread rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>kheap s thread = Some (TCB rv); valid_obj thread (TCB rv) s\<rbrakk> \<Longrightarrow> valid_tcb thread rv s proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma obj_at_tcb_update:
  "\<lbrakk> tcb_at t s; \<And>x y. P (TCB x) = P (TCB y)\<rbrakk> \<Longrightarrow>
  obj_at P t' (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = obj_at P t' s" apply (simp add: obj_at_def is_tcb_def) apply clarsimp apply (case_tac ko) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at t s; \<And>x y. P (TCB x) = P (TCB y)\<rbrakk> \<Longrightarrow> obj_at P t' (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = obj_at P t' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>ko. kheap s t = Some ko \<and> (case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False); \<And>x y. P (TCB x) = P (TCB y)\<rbrakk> \<Longrightarrow> t' = t \<longrightarrow> P (TCB tcb) = (\<exists>ko. kheap s t = Some ko \<and> P ko) proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>\<And>x y. P (TCB x) = P (TCB y); kheap s t = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; t' = t\<rbrakk> \<Longrightarrow> P (TCB tcb) = P ko proof (prove)
goal (5 subgoals):
 1. \<And>ko x11 x12. \<lbrakk>\<And>x y. P (TCB x) = P (TCB y); kheap s t = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; t' = t; ko = CNode x11 x12\<rbrakk> \<Longrightarrow> P (TCB tcb) = P ko
 2. \<And>ko x2. \<lbrakk>\<And>x y. P (TCB x) = P (TCB y); kheap s t = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; t' = t; ko = TCB x2\<rbrakk> \<Longrightarrow> P (TCB tcb) = P ko
 3. \<And>ko x3. \<lbrakk>\<And>x y. P (TCB x) = P (TCB y); kheap s t = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; t' = t; ko = Endpoint x3\<rbrakk> \<Longrightarrow> P (TCB tcb) = P ko
 4. \<And>ko x4. \<lbrakk>\<And>x y. P (TCB x) = P (TCB y); kheap s t = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; t' = t; ko = Notification x4\<rbrakk> \<Longrightarrow> P (TCB tcb) = P ko
 5. \<And>ko x5. \<lbrakk>\<And>x y. P (TCB x) = P (TCB y); kheap s t = Some ko; case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False; t' = t; ko = ArchObj x5\<rbrakk> \<Longrightarrow> P (TCB tcb) = P ko proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma obj_at_update:
  "obj_at P t' (s \<lparr>kheap := (kheap s)(t \<mapsto> v)\<rparr>) =
  (if t = t' then P v else obj_at P t' s)" by (simp add: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at P t' (s\<lparr>kheap := (kheap s)(t \<mapsto> v)\<rparr>) = (if t = t' then P v else obj_at P t' s)
theory CSpaceInv_AI

lemma iflive_tcb_update:
  "\<lbrakk> if_live_then_nonz_cap s; live (TCB tcb) \<longrightarrow> ex_nonz_cap_to t s;
           obj_at (same_caps (TCB tcb)) t s \<rbrakk>
  \<Longrightarrow> if_live_then_nonz_cap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>)" unfolding fun_upd_def apply (simp add: if_live_then_nonz_cap_def, erule allEI) apply safe apply (clarsimp simp add: obj_at_def elim!: ex_cap_to_after_update
                   split: if_split_asm | (erule notE, erule ex_cap_to_after_update))+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_live_then_nonz_cap s; live (TCB tcb) \<longrightarrow> ex_nonz_cap_to t s; obj_at (same_caps (TCB tcb)) t s\<rbrakk> \<Longrightarrow> if_live_then_nonz_cap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_live_then_nonz_cap s; live (TCB tcb) \<longrightarrow> ex_nonz_cap_to t s; obj_at (same_caps (TCB tcb)) t s\<rbrakk> \<Longrightarrow> if_live_then_nonz_cap (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB tcb) else kheap s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ptr. \<lbrakk>live (TCB tcb) \<longrightarrow> ex_nonz_cap_to t s; obj_at (same_caps (TCB tcb)) t s; obj_at live ptr s \<longrightarrow> ex_nonz_cap_to ptr s\<rbrakk> \<Longrightarrow> obj_at live ptr (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB tcb) else kheap s x\<rparr>) \<longrightarrow> ex_nonz_cap_to ptr (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB tcb) else kheap s x\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>ptr. \<lbrakk>obj_at (same_caps (TCB tcb)) t s; obj_at live ptr (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB tcb) else kheap s x\<rparr>); \<not> live (TCB tcb); \<not> obj_at live ptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to ptr (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB tcb) else kheap s x\<rparr>)
 2. \<And>ptr. \<lbrakk>obj_at (same_caps (TCB tcb)) t s; obj_at live ptr (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB tcb) else kheap s x\<rparr>); \<not> live (TCB tcb); ex_nonz_cap_to ptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to ptr (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB tcb) else kheap s x\<rparr>)
 3. \<And>ptr. \<lbrakk>obj_at (same_caps (TCB tcb)) t s; obj_at live ptr (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB tcb) else kheap s x\<rparr>); ex_nonz_cap_to t s; \<not> obj_at live ptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to ptr (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB tcb) else kheap s x\<rparr>)
 4. \<And>ptr. \<lbrakk>obj_at (same_caps (TCB tcb)) t s; obj_at live ptr (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB tcb) else kheap s x\<rparr>); ex_nonz_cap_to t s; ex_nonz_cap_to ptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to ptr (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB tcb) else kheap s x\<rparr>) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma ifunsafe_tcb_update:
  "\<lbrakk> if_unsafe_then_cap s; obj_at (same_caps (TCB tcb)) t s \<rbrakk>
  \<Longrightarrow> if_unsafe_then_cap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>)" apply (simp add: if_unsafe_then_cap_def, elim allEI) apply (clarsimp dest!: caps_of_state_cteD
                   simp: cte_wp_at_after_update fun_upd_def) apply (clarsimp simp: cte_wp_at_caps_of_state
                        ex_cte_cap_to_after_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_unsafe_then_cap s; obj_at (same_caps (TCB tcb)) t s\<rbrakk> \<Longrightarrow> if_unsafe_then_cap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>obj_at (same_caps (TCB tcb)) t s; caps_of_state s (a, b) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) s\<rbrakk> \<Longrightarrow> caps_of_state (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) (a, b) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>obj_at (same_caps (TCB tcb)) t s; caps_of_state s (a, b) = Some cap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) s; cte_wp_at ((=) cap) (a, b) s; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) (s\<lparr>kheap := \<lambda>x. if x = t then Some (TCB tcb) else kheap s x\<rparr>) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma zombies_tcb_update:
  "\<lbrakk> zombies_final s; obj_at (same_caps (TCB tcb)) t s \<rbrakk>
   \<Longrightarrow> zombies_final (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>)" apply (simp add: zombies_final_def is_final_cap'_def2, elim allEI) apply (clarsimp simp: cte_wp_at_after_update fun_upd_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>zombies_final s; obj_at (same_caps (TCB tcb)) t s\<rbrakk> \<Longrightarrow> zombies_final (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>obj_at (same_caps (TCB tcb)) t s; cte_wp_at is_zombie (a, b) s \<longrightarrow> cte_wp_at (\<lambda>cap. \<exists>a b. \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) s = (aa = a \<and> ba = b)) (a, b) s\<rbrakk> \<Longrightarrow> cte_wp_at is_zombie (a, b) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) \<longrightarrow> cte_wp_at (\<lambda>cap. \<exists>a b. \<forall>aa ba. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) (aa, ba) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = (aa = a \<and> ba = b)) (a, b) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma valid_reply_caps_tcb_update:
  "\<lbrakk>valid_reply_caps s; ko_at (TCB t) p s; tcb_state t = tcb_state t';
    same_caps (TCB t) (TCB t') \<rbrakk>
   \<Longrightarrow> valid_reply_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>)" apply (frule_tac P'="same_caps (TCB t')" in obj_at_weakenE, simp) apply (fastforce simp: valid_reply_caps_def has_reply_cap_def
                        pred_tcb_at_def obj_at_def fun_upd_def
                        cte_wp_at_after_update caps_of_state_after_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_reply_caps s; ko_at (TCB t) p s; tcb_state t = tcb_state t'; same_caps (TCB t) (TCB t')\<rbrakk> \<Longrightarrow> valid_reply_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_reply_caps s; ko_at (TCB t) p s; tcb_state t = tcb_state t'; same_caps (TCB t) (TCB t'); obj_at (same_caps (TCB t')) p s\<rbrakk> \<Longrightarrow> valid_reply_caps (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma valid_reply_masters_tcb_update:
  "\<lbrakk>valid_reply_masters s; ko_at (TCB t) p s; tcb_state t = tcb_state t';
    same_caps (TCB t) (TCB t') \<rbrakk>
   \<Longrightarrow> valid_reply_masters (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>)" by (clarsimp simp: valid_reply_masters_def fun_upd_def is_tcb
                     cte_wp_at_after_update obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_reply_masters s; ko_at (TCB t) p s; tcb_state t = tcb_state t'; same_caps (TCB t) (TCB t')\<rbrakk> \<Longrightarrow> valid_reply_masters (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>)
theory CSpaceInv_AI

lemma tcb_state_same_cte_wp_at:
  "\<lbrakk> ko_at (TCB t) p s; \<forall>(getF, v) \<in> ran tcb_cap_cases. getF t = getF t' \<rbrakk>
     \<Longrightarrow> \<forall>P p'. cte_wp_at P p' (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>)
             = cte_wp_at P p' s" apply (clarsimp simp add: cte_wp_at_cases obj_at_def) apply (case_tac "tcb_cap_cases b") apply simp apply (drule bspec, erule ranI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (TCB t) p s; \<forall>(getF, v)\<in>ran tcb_cap_cases. getF t = getF t'\<rbrakk> \<Longrightarrow> \<forall>P p'. cte_wp_at P p' (s\<lparr>kheap := (kheap s)(p \<mapsto> TCB t')\<rparr>) = cte_wp_at P p' s proof (prove)
goal (1 subgoal):
 1. \<And>P b. \<lbrakk>kheap s p = Some (TCB t); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, v) \<Rightarrow> getF t = getF t'\<rbrakk> \<Longrightarrow> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get t')) = (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get t)) proof (prove)
goal (2 subgoals):
 1. \<And>P b. \<lbrakk>kheap s p = Some (TCB t); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, v) \<Rightarrow> getF t = getF t'; tcb_cap_cases b = None\<rbrakk> \<Longrightarrow> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get t')) = (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get t))
 2. \<And>P b a. \<lbrakk>kheap s p = Some (TCB t); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, v) \<Rightarrow> getF t = getF t'; tcb_cap_cases b = Some a\<rbrakk> \<Longrightarrow> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get t')) = (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get t)) proof (prove)
goal (1 subgoal):
 1. \<And>P b a. \<lbrakk>kheap s p = Some (TCB t); \<forall>x\<in>ran tcb_cap_cases. case x of (getF, v) \<Rightarrow> getF t = getF t'; tcb_cap_cases b = Some a\<rbrakk> \<Longrightarrow> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get t')) = (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get t)) proof (prove)
goal (1 subgoal):
 1. \<And>P b a. \<lbrakk>kheap s p = Some (TCB t); tcb_cap_cases b = Some a; case a of (getF, v) \<Rightarrow> getF t = getF t'\<rbrakk> \<Longrightarrow> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get t')) = (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get t)) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma valid_tcb_state_update:
  "\<lbrakk> valid_tcb p t s; valid_tcb_state st s;
     case st of
                Structures_A.Inactive \<Rightarrow> True
              | Structures_A.BlockedOnReceive e data \<Rightarrow>
                     tcb_caller t = cap.NullCap
                   \<and> is_master_reply_cap (tcb_reply t)
                   \<and> obj_ref_of (tcb_reply t) = p
                   \<and> AllowGrant \<in> cap_rights (tcb_reply t)
              | _ \<Rightarrow> is_master_reply_cap (tcb_reply t)
                   \<and> obj_ref_of (tcb_reply t) = p
                   \<and> AllowGrant \<in> cap_rights (tcb_reply t) \<rbrakk> \<Longrightarrow>
   valid_tcb p (t\<lparr>tcb_state := st\<rparr>) s" by (simp add: valid_tcb_def valid_tcb_state_def ran_tcb_cap_cases
         split: Structures_A.thread_state.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_tcb p t s; valid_tcb_state st s; case st of Inactive \<Rightarrow> True | BlockedOnReceive e data \<Rightarrow> tcb_caller t = NullCap \<and> is_master_reply_cap (tcb_reply t) \<and> obj_ref_of (tcb_reply t) = p \<and> AllowGrant \<in> cap_rights (tcb_reply t) | _ \<Rightarrow> is_master_reply_cap (tcb_reply t) \<and> obj_ref_of (tcb_reply t) = p \<and> AllowGrant \<in> cap_rights (tcb_reply t)\<rbrakk> \<Longrightarrow> valid_tcb p (t\<lparr>tcb_state := st\<rparr>) s
theory CSpaceInv_AI

lemma valid_tcb_if_valid_state:
  assumes vs: "valid_state s"
  assumes somet: "get_tcb thread s = Some y"
  shows "valid_tcb thread y s" proof - from somet have inran: "kheap s thread = Some (TCB y)" by (clarsimp simp: get_tcb_def
                split: option.splits Structures_A.kernel_object.splits) from vs have "(\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s)" by (simp add: valid_state_def valid_pspace_def valid_objs_def) with inran have "valid_obj thread (TCB y) s" by (fastforce simp: dom_def) thus ?thesis by (simp add: valid_tcb_def valid_obj_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb thread y s proof (state)
goal (1 subgoal):
 1. valid_tcb thread y s proof (chain)
picking this:
get_tcb thread s = Some y proof (prove)
using this:
get_tcb thread s = Some y

goal (1 subgoal):
 1. kheap s thread = Some (TCB y) proof (state)
this:
kheap s thread = Some (TCB y)

goal (1 subgoal):
 1. valid_tcb thread y s proof (chain)
picking this:
valid_state s proof (prove)
using this:
valid_state s

goal (1 subgoal):
 1. \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s proof (state)
this:
\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s

goal (1 subgoal):
 1. valid_tcb thread y s proof (chain)
picking this:
kheap s thread = Some (TCB y)
\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s proof (prove)
using this:
kheap s thread = Some (TCB y)
\<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s

goal (1 subgoal):
 1. valid_obj thread (TCB y) s proof (state)
this:
valid_obj thread (TCB y) s

goal (1 subgoal):
 1. valid_tcb thread y s proof (prove)
using this:
valid_obj thread (TCB y) s

goal (1 subgoal):
 1. valid_tcb thread y s proof (state)
this:
valid_tcb thread y s

goal:
No subgoals!
theory CSpaceInv_AI

lemma assert_get_tcb_ko:
  shows "\<lbrace> P \<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>t. ko_at (TCB t) thread \<rbrace>" by (clarsimp simp: valid_def in_monad gets_the_def get_tcb_def
                     obj_at_def
               split: option.splits Structures_A.kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> gets_the (get_tcb thread) \<lbrace>\<lambda>t. ko_at (TCB t) thread\<rbrace>
theory CSpaceInv_AI

lemma gts_st_tcb_at: "\<lbrace>st_tcb_at P t\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. P rv\<rbrace>" apply (simp add: get_thread_state_def thread_get_def) apply wp apply (clarsimp simp: pred_tcb_at_def obj_at_def get_tcb_def is_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> do tcb <- gets_the (get_tcb t);
return (tcb_state tcb)
od \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at P t s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> P (tcb_state (the (get_tcb t s))) proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma gts_st_tcb:
  "\<lbrace>\<top>\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. rv = st) t\<rbrace>" apply (simp add: get_thread_state_def thread_get_def) apply wp apply (clarsimp simp: pred_tcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. st_tcb_at ((=) rv) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do tcb <- gets_the (get_tcb t);
return (tcb_state tcb)
od \<lbrace>\<lambda>rv. st_tcb_at ((=) rv) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> st_tcb_at ((=) (tcb_state (the (get_tcb t s)))) t s proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma gbn_bound_tcb:
  "\<lbrace>\<top>\<rbrace> get_bound_notification t \<lbrace>\<lambda>rv. bound_tcb_at (\<lambda>ntfn. rv = ntfn) t\<rbrace>" apply (simp add: get_bound_notification_def thread_get_def) apply wp apply (clarsimp simp: pred_tcb_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_bound_notification t \<lbrace>\<lambda>rv. bound_tcb_at ((=) rv) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do tcb <- gets_the (get_tcb t);
return (tcb_bound_notification tcb)
od \<lbrace>\<lambda>rv. bound_tcb_at ((=) rv) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> bound_tcb_at ((=) (tcb_bound_notification (the (get_tcb t s)))) t s proof (prove)
goal:
No subgoals!
theory CSpaceInv_AI

lemma allActiveTCBs_valid_state:
  "\<lbrace>valid_state\<rbrace> allActiveTCBs \<lbrace>\<lambda>R s. valid_state s \<and> (\<forall>t \<in> R. st_tcb_at runnable t s) \<rbrace>" apply (simp add: allActiveTCBs_def, wp) apply (simp add: getActiveTCB_def pred_tcb_at_def obj_at_def get_tcb_def
              split: option.splits if_split_asm Structures_A.kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_state\<rbrace> allActiveTCBs \<lbrace>\<lambda>R s. valid_state s \<and> (\<forall>t\<in>R. st_tcb_at runnable t s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_state s \<Longrightarrow> valid_state s \<and> (\<forall>t\<in>{x. \<exists>y. getActiveTCB x s = Some y}. st_tcb_at runnable t s) proof (prove)
goal:
No subgoals!