kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_AI

lemma gts_eq_ts:
  "\<lbrace> tcb_at thread \<rbrace> get_thread_state thread \<lbrace>\<lambda>rv. st_tcb_at ((=) rv) thread \<rbrace>" apply (rule hoare_strengthen_post) apply (rule gts_sp) apply (clarsimp simp add: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at thread\<rbrace> get_thread_state thread \<lbrace>\<lambda>rv. st_tcb_at ((=) rv) thread\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>tcb_at thread\<rbrace> get_thread_state thread \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> st_tcb_at ((=) rv) thread s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (st_tcb_at ((=) rv) thread and tcb_at thread) s \<Longrightarrow> st_tcb_at ((=) rv) thread s proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma si_tcb_at [wp]:
  "\<And>t' call bl w gr d t ep.
    \<lbrace>tcb_at t' :: 'state_ext state \<Rightarrow> bool\<rbrace>
      send_ipc call bl w gr d t ep
    \<lbrace>\<lambda>rv. tcb_at t'\<rbrace>" by (simp add: tcb_at_typ) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>t' call bl w gr d t ep. \<lbrace>tcb_at t'\<rbrace> send_ipc call bl w gr d t ep \<lbrace>\<lambda>rv. tcb_at t'\<rbrace>
theory Ipc_AI

lemma hf_tcb_at [wp]:
  "\<And>t' t x.
    \<lbrace>tcb_at t' :: 'state_ext state \<Rightarrow> bool\<rbrace>
      handle_fault t x
    \<lbrace>\<lambda>rv. tcb_at t'\<rbrace>" by (simp add: tcb_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>t' t x. \<lbrace>tcb_at t'\<rbrace> handle_fault t x \<lbrace>\<lambda>rv. tcb_at t'\<rbrace>
theory Ipc_AI

lemma sfi_tcb_at [wp]:
  "\<And>t t' f.
    \<lbrace>tcb_at t :: 'state_ext state \<Rightarrow> bool\<rbrace>
      send_fault_ipc t' f
    \<lbrace>\<lambda>_. tcb_at t\<rbrace>" by (simp add: tcb_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>t t' f. \<lbrace>tcb_at t\<rbrace> send_fault_ipc t' f \<lbrace>\<lambda>_. tcb_at t\<rbrace>
theory Ipc_AI

lemma pred_tcb_at_update1:
  "x \<noteq> t \<Longrightarrow> pred_tcb_at proj P x (s\<lparr>kheap := (kheap s)(t := v)\<rparr>) = pred_tcb_at proj P x s" by (simp add: pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> t \<Longrightarrow> pred_tcb_at proj P x (s\<lparr>kheap := (kheap s)(t := v)\<rparr>) = pred_tcb_at proj P x s
theory Ipc_AI

lemma pred_tcb_at_update2:
  "pred_tcb_at proj P t (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = P (proj (tcb_to_itcb tcb))" by (simp add: pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at proj P t (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB tcb)\<rparr>) = P (proj (tcb_to_itcb tcb))
theory Ipc_AI

lemma pred_tcb_clear:
  "pred_tcb_at proj P t (pspace_clear t' s) = (t \<noteq> t' \<and> pred_tcb_at proj P t s)" by (simp add: pred_tcb_at_def obj_at_def pspace_clear_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at proj P t (pspace_clear t' s) = (t \<noteq> t' \<and> pred_tcb_at proj P t s)
theory Ipc_AI

lemma pred_tcb_upd_apply:
  "pred_tcb_at proj P t (s\<lparr>kheap := (kheap s)(r \<mapsto> TCB v)\<rparr>) =
  (if t = r then P (proj (tcb_to_itcb v)) else pred_tcb_at proj P t s)" by (simp add: pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at proj P t (s\<lparr>kheap := (kheap s)(r \<mapsto> TCB v)\<rparr>) = (if t = r then P (proj (tcb_to_itcb v)) else pred_tcb_at proj P t s)
theory Ipc_AI

lemma setup_caller_cap_state_refs_of[wp]:
  "\<lbrace>\<lambda>s. P ((state_refs_of s) (sender := {r \<in> state_refs_of s sender. snd r = TCBBound}))\<rbrace>
     setup_caller_cap sender rcvr grant
   \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" apply (simp add: setup_caller_cap_def) apply (rule conjI) apply (clarify, wp, simp add: fun_upd_def cong: if_cong)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of s)(sender := {r \<in> state_refs_of s sender. snd r = TCBBound}))\<rbrace> setup_caller_cap sender rcvr grant \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (grant \<longrightarrow> \<lbrace>\<lambda>s. P ((state_refs_of s)(sender := {r \<in> state_refs_of s sender. snd r = TCBBound}))\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowGrant, AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>) \<and> (\<not> grant \<longrightarrow> \<lbrace>\<lambda>s. P ((state_refs_of s)(sender := {r \<in> state_refs_of s sender. snd r = TCBBound}))\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>) proof (prove)
goal (2 subgoals):
 1. grant \<longrightarrow> \<lbrace>\<lambda>s. P ((state_refs_of s)(sender := {r \<in> state_refs_of s sender. snd r = TCBBound}))\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowGrant, AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>
 2. \<not> grant \<longrightarrow> \<lbrace>\<lambda>s. P ((state_refs_of s)(sender := {r \<in> state_refs_of s sender. snd r = TCBBound}))\<rbrace> do y <- set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False {AllowWrite}) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma setup_caller_cap_iflive[wp]:
  "\<lbrace>if_live_then_nonz_cap and st_tcb_at (Not \<circ> halted) sender\<rbrace>
   setup_caller_cap sender rcvr grant
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>" unfolding setup_caller_cap_def apply (wp cap_insert_iflive) apply (clarsimp elim!: st_tcb_ex_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap and st_tcb_at (Not \<circ> halted) sender\<rbrace> setup_caller_cap sender rcvr grant \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap and st_tcb_at (Not \<circ> halted) sender\<rbrace> do set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (if_live_then_nonz_cap and st_tcb_at (Not \<circ> halted) sender) s \<Longrightarrow> (\<not> halted BlockedOnReply \<longrightarrow> ex_nonz_cap_to sender s) \<and> if_live_then_nonz_cap s proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma setup_caller_cap_globals[wp]:
  "\<lbrace>valid_objs and valid_global_refs and
    st_tcb_at (Not \<circ> halted) sender\<rbrace>
   setup_caller_cap sender rcvr grant
   \<lbrace>\<lambda>rv. valid_global_refs\<rbrace>" unfolding setup_caller_cap_def apply wpsimp apply (frule st_tcb_at_reply_cap_valid, clarsimp+) apply (clarsimp simp: cte_wp_at_caps_of_state cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_global_refs and st_tcb_at (Not \<circ> halted) sender\<rbrace> setup_caller_cap sender rcvr grant \<lbrace>\<lambda>rv. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_global_refs and st_tcb_at (Not \<circ> halted) sender\<rbrace> do set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs s; valid_global_refs s; st_tcb_at (Not \<circ> halted) sender s\<rbrakk> \<Longrightarrow> (grant \<longrightarrow> cte_wp_at (\<lambda>scap. cap_range (ReplyCap sender False {AllowGrant, AllowWrite}) \<subseteq> cap_range scap) (sender, tcb_cnode_index 2) s) \<and> (\<not> grant \<longrightarrow> cte_wp_at (\<lambda>scap. cap_range (ReplyCap sender False {AllowWrite}) \<subseteq> cap_range scap) (sender, tcb_cnode_index 2) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs s; valid_global_refs s; st_tcb_at (Not \<circ> halted) sender s; cte_wp_at (\<lambda>cap. is_master_reply_cap cap \<and> obj_ref_of cap = sender) (sender, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> (grant \<longrightarrow> cte_wp_at (\<lambda>scap. cap_range (ReplyCap sender False {AllowGrant, AllowWrite}) \<subseteq> cap_range scap) (sender, tcb_cnode_index 2) s) \<and> (\<not> grant \<longrightarrow> cte_wp_at (\<lambda>scap. cap_range (ReplyCap sender False {AllowWrite}) \<subseteq> cap_range scap) (sender, tcb_cnode_index 2) s) proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma setup_caller_cap_ifunsafe[wp]:
  "\<lbrace>if_unsafe_then_cap and valid_objs and tcb_at rcvr and ex_nonz_cap_to rcvr\<rbrace>
  setup_caller_cap sender rcvr grant
  \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>" unfolding setup_caller_cap_def by (wpsimp wp: cap_insert_ifunsafe ex_cte_cap_to_pres
           simp: ex_nonz_tcb_cte_caps dom_tcb_cap_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap and valid_objs and tcb_at rcvr and ex_nonz_cap_to rcvr\<rbrace> setup_caller_cap sender rcvr grant \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap and valid_objs and tcb_at rcvr and ex_nonz_cap_to rcvr\<rbrace> do set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>
theory Ipc_AI

lemma setup_caller_cap_idle[wp]:
  "\<lbrace>valid_idle and (\<lambda>s. st \<noteq> idle_thread s \<and> rt \<noteq> idle_thread s)\<rbrace>
   setup_caller_cap st rt grant
   \<lbrace>\<lambda>_. valid_idle\<rbrace>" unfolding setup_caller_cap_def apply (wp cap_insert_idle | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and (\<lambda>s. st \<noteq> idle_thread s \<and> rt \<noteq> idle_thread s)\<rbrace> setup_caller_cap st rt grant \<lbrace>\<lambda>_. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and (\<lambda>s. st \<noteq> idle_thread s \<and> rt \<noteq> idle_thread s)\<rbrace> do set_thread_state st BlockedOnReply;
cap_insert (ReplyCap st False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (st, tcb_cnode_index 2) (rt, tcb_cnode_index 3)
od \<lbrace>\<lambda>_. valid_idle\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma setup_caller_cap_reply_masters[wp]:
  "\<lbrace>valid_reply_masters and tcb_at rt\<rbrace>
   setup_caller_cap st rt grant
   \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace>" unfolding setup_caller_cap_def by (wpsimp simp: is_cap_simps tcb_at_cte_at dom_tcb_cap_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and tcb_at rt\<rbrace> setup_caller_cap st rt grant \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and tcb_at rt\<rbrace> do set_thread_state st BlockedOnReply;
cap_insert (ReplyCap st False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (st, tcb_cnode_index 2) (rt, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace>
theory Ipc_AI

lemma setup_caller_cap_irq_handlers[wp]:
  "\<lbrace>valid_irq_handlers and tcb_at st\<rbrace>
   setup_caller_cap st rt grant
   \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>" unfolding setup_caller_cap_def by (wpsimp simp: is_cap_simps tcb_at_cte_at dom_tcb_cap_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers and tcb_at st\<rbrace> setup_caller_cap st rt grant \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers and tcb_at st\<rbrace> do set_thread_state st BlockedOnReply;
cap_insert (ReplyCap st False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (st, tcb_cnode_index 2) (rt, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>
theory Ipc_AI

lemma setup_caller_cap_valid_arch_caps[wp]:
  "\<lbrace>valid_arch_caps and valid_objs and st_tcb_at (Not o halted) sender\<rbrace>
      setup_caller_cap sender recvr grant
    \<lbrace>\<lambda>rv. valid_arch_caps :: 'state_ext state \<Rightarrow> bool\<rbrace>" unfolding setup_caller_cap_def apply (wpsimp wp: cap_insert_valid_arch_caps) apply (auto elim: st_tcb_at_reply_cap_valid) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and valid_objs and st_tcb_at (Not \<circ> halted) sender\<rbrace> setup_caller_cap sender recvr grant \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_caps and valid_objs and st_tcb_at (Not \<circ> halted) sender\<rbrace> do set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (recvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_arch_caps s; valid_objs s; st_tcb_at (Not \<circ> halted) sender s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = sender) (sender, tcb_cnode_index 2) s proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma setup_caller_cap_cap_refs_in_window[wp]:
  "\<lbrace>valid_objs and cap_refs_in_kernel_window and
    st_tcb_at (Not \<circ> halted) sender\<rbrace>
   setup_caller_cap sender rcvr grant
   \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" unfolding setup_caller_cap_def apply (rule hoare_pre, wp) apply clarsimp apply (frule st_tcb_at_reply_cap_valid, clarsimp+) apply (clarsimp simp: cte_wp_at_caps_of_state cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cap_refs_in_kernel_window and st_tcb_at (Not \<circ> halted) sender\<rbrace> setup_caller_cap sender rcvr grant \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cap_refs_in_kernel_window and st_tcb_at (Not \<circ> halted) sender\<rbrace> do set_thread_state sender BlockedOnReply;
cap_insert (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (sender, tcb_cnode_index 2) (rcvr, tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and cap_refs_in_kernel_window and st_tcb_at (Not \<circ> halted) sender) s \<Longrightarrow> cap_refs_in_kernel_window s \<and> cte_wp_at (\<lambda>c. cap_range (ReplyCap sender False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) \<subseteq> cap_range c) (sender, tcb_cnode_index 2) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs s; cap_refs_in_kernel_window s; st_tcb_at (Not \<circ> halted) sender s\<rbrakk> \<Longrightarrow> (grant \<longrightarrow> cte_wp_at (\<lambda>c. cap_range (ReplyCap sender False {AllowGrant, AllowWrite}) \<subseteq> cap_range c) (sender, tcb_cnode_index 2) s) \<and> (\<not> grant \<longrightarrow> cte_wp_at (\<lambda>c. cap_range (ReplyCap sender False {AllowWrite}) \<subseteq> cap_range c) (sender, tcb_cnode_index 2) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs s; cap_refs_in_kernel_window s; st_tcb_at (Not \<circ> halted) sender s; cte_wp_at (\<lambda>cap. is_master_reply_cap cap \<and> obj_ref_of cap = sender) (sender, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> (grant \<longrightarrow> cte_wp_at (\<lambda>c. cap_range (ReplyCap sender False {AllowGrant, AllowWrite}) \<subseteq> cap_range c) (sender, tcb_cnode_index 2) s) \<and> (\<not> grant \<longrightarrow> cte_wp_at (\<lambda>c. cap_range (ReplyCap sender False {AllowWrite}) \<subseteq> cap_range c) (sender, tcb_cnode_index 2) s) proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma same_caps_tcb_upd_state[simp]:
 "same_caps (TCB (tcb \<lparr>tcb_state := BlockedOnReply\<rparr>)) = same_caps (TCB tcb)" apply (rule ext) apply (simp add:tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. same_caps (TCB (tcb\<lparr>tcb_state := BlockedOnReply\<rparr>)) = same_caps (TCB tcb) proof (prove)
goal (1 subgoal):
 1. \<And>x. same_caps (TCB (tcb\<lparr>tcb_state := BlockedOnReply\<rparr>)) x = same_caps (TCB tcb) x proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma same_caps_simps[simp]:
 "same_caps (CNode sz cs)  = (\<lambda>val. val = CNode sz cs)"
 "same_caps (TCB tcb)      = (\<lambda>val. (\<exists>tcb'. val = TCB tcb'
                                         \<and> (\<forall>(getF, t) \<in> ran tcb_cap_cases. getF tcb' = getF tcb)))"
 "same_caps (Endpoint ep)  = (\<lambda>val. is_ep val)"
 "same_caps (Notification ntfn) = (\<lambda>val. is_ntfn val)"
 "same_caps (ArchObj ao)   = (\<lambda>val. (\<exists>ao'. val = ArchObj ao'))" apply (rule ext) apply (case_tac val, (fastforce simp: is_obj_defs)+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (same_caps (CNode sz cs) = (\<lambda>val. val = CNode sz cs) &&& same_caps (TCB tcb) = (\<lambda>val. \<exists>tcb'. val = TCB tcb' \<and> (\<forall>(getF, t)\<in>ran tcb_cap_cases. getF tcb' = getF tcb))) &&& same_caps (Endpoint ep) = is_ep &&& same_caps (Notification ntfn) = is_ntfn &&& same_caps (ArchObj ao) = (\<lambda>val. \<exists>ao'. val = ArchObj ao') proof (prove)
goal (5 subgoals):
 1. \<And>val. same_caps (CNode sz cs) val = (val = CNode sz cs)
 2. same_caps (TCB tcb) = (\<lambda>val. \<exists>tcb'. val = TCB tcb' \<and> (\<forall>(getF, t)\<in>ran tcb_cap_cases. getF tcb' = getF tcb))
 3. same_caps (Endpoint ep) = is_ep
 4. same_caps (Notification ntfn) = is_ntfn
 5. same_caps (ArchObj ao) = (\<lambda>val. \<exists>ao'. val = ArchObj ao') proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma tcb_at_cte_at_3:
  "tcb_at tcb s \<Longrightarrow> cte_at (tcb, tcb_cnode_index 3) s" by (auto simp: obj_at_def cte_at_cases is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at tcb s \<Longrightarrow> cte_wp_at (\<lambda>_. True) (tcb, tcb_cnode_index 3) s
theory Ipc_AI

lemma invs_respects_device_region:
  "invs s \<Longrightarrow> cap_refs_respects_device_region s \<and> pspace_respects_device_region s" by (clarsimp simp: invs_def valid_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> cap_refs_respects_device_region s \<and> pspace_respects_device_region s
theory Ipc_AI

lemma set_message_info_valid_arch [wp]:
  "\<lbrace>valid_arch_state\<rbrace> set_message_info a b \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" apply (rule valid_arch_state_lift_aobj_at; wp?) unfolding set_message_info_def apply (wp as_user.aobj_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> set_message_info a b \<lbrace>\<lambda>_. valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> set_message_info a b \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> as_user a $ setRegister msg_info_register $ message_info_to_data b \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma set_message_info_global_refs [wp]:
  "\<lbrace>valid_global_refs\<rbrace> set_message_info a b \<lbrace>\<lambda>_. valid_global_refs\<rbrace>" by (rule valid_global_refs_cte_lift; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> set_message_info a b \<lbrace>\<lambda>_. valid_global_refs\<rbrace>
theory Ipc_AI

lemma tcb_cap_cases_tcb_context:
  "\<forall>(getF, v)\<in>ran tcb_cap_cases.
         getF (tcb_arch_update (arch_tcb_context_set F) tcb) = getF tcb" by (rule ball_tcb_cap_casesI, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (tcb_arch_update (arch_tcb_context_set F) tcb) = getF tcb
theory Ipc_AI

lemma valid_bound_tcb_exst[iff]:
 "valid_bound_tcb t (trans_state f s) = valid_bound_tcb t s" by (auto simp: valid_bound_tcb_def split:option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_bound_tcb t (trans_state f s) = valid_bound_tcb t s
theory Ipc_AI

lemma valid_bound_tcb_typ_at:
  "(\<And>p. \<lbrace>\<lambda>s. typ_at ATCB p s\<rbrace> f \<lbrace>\<lambda>_ s. typ_at ATCB p s\<rbrace>)
   \<Longrightarrow> \<lbrace>\<lambda>s. valid_bound_tcb tcb s\<rbrace> f \<lbrace>\<lambda>_ s. valid_bound_tcb tcb s\<rbrace>" apply (clarsimp simp: valid_bound_tcb_def split: option.splits) apply (wpsimp wp: hoare_vcg_all_lift tcb_at_typ_at hoare_weak_lift_imp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrace>typ_at ATCB p\<rbrace> f \<lbrace>\<lambda>_. typ_at ATCB p\<rbrace>) \<Longrightarrow> \<lbrace>valid_bound_tcb tcb\<rbrace> f \<lbrace>\<lambda>_. valid_bound_tcb tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrace>typ_at ATCB p\<rbrace> f \<lbrace>\<lambda>_. typ_at ATCB p\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x2. tcb = Some x2 \<longrightarrow> tcb_at x2 s\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>x2. tcb = Some x2 \<longrightarrow> tcb_at x2 s\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma pspace_clear_update1:
  "t \<noteq> t' \<Longrightarrow>
  pspace_clear t' (s\<lparr>kheap := (kheap s)(t := v)\<rparr>) =
  (pspace_clear t' s) \<lparr>kheap := (kheap (pspace_clear t' s))(t := v)\<rparr>" apply (simp add: pspace_clear_def) apply (cases s) apply simp apply (simp add: fun_upd_twist) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> pspace_clear t' (s\<lparr>kheap := (kheap s)(t := v)\<rparr>) = pspace_clear t' s\<lparr>kheap := (kheap (pspace_clear t' s))(t := v)\<rparr> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> s\<lparr>kheap := (kheap s)(t := v, t' := None)\<rparr> = s\<lparr>kheap := (kheap s)(t' := None, t := v)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>kheapa cdt is_original_cap cur_thread idle_thread machine_state interrupt_irq_node interrupt_states arch_state more. \<lbrakk>t \<noteq> t'; s = \<lparr>kheap = kheapa, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, \<dots> = more\<rparr>\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(t := v, t' := None)\<rparr> = s\<lparr>kheap := (kheap s)(t' := None, t := v)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>kheap cdt is_original_cap cur_thread idle_thread machine_state interrupt_irq_node interrupt_states arch_state more. \<lbrakk>t \<noteq> t'; s = \<lparr>kheap = kheap, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, \<dots> = more\<rparr>\<rbrakk> \<Longrightarrow> kheap(t := v, t' := None) = kheap(t' := None, t := v) proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma pspace_clear_update2:
  "pspace_clear t' (s\<lparr>kheap := (kheap s)(t' := v)\<rparr>) = pspace_clear t' s" by (simp add: pspace_clear_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_clear t' (s\<lparr>kheap := (kheap s)(t' := v)\<rparr>) = pspace_clear t' s