kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchCSpace_AI

lemma setup_reply_master_cap_refs_in_kernel_window[wp, CSpace_AI_assms]:
  "\<lbrace>cap_refs_in_kernel_window and tcb_at t and pspace_in_kernel_window\<rbrace>
      setup_reply_master t
   \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp get_cap_wp) apply (clarsimp simp: pspace_in_kernel_window_def obj_at_def
                        cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window and tcb_at t and pspace_in_kernel_window\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window and tcb_at t and pspace_in_kernel_window\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cap_refs_in_kernel_window and tcb_at t and pspace_in_kernel_window) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (if cap = NullCap then \<lambda>s. (cap_refs_in_kernel_window and (\<lambda>s. \<forall>ref\<in>cap_range (ReplyCap t True {AllowGrant, AllowWrite}). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow)) (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) else cap_refs_in_kernel_window) s proof (prove)
goal:
No subgoals!
theory ArchCSpace_AI

lemma same_region_as_Untyped2 [CSpace_AI_assms]:
  "\<lbrakk> is_untyped_cap pcap; same_region_as pcap cap \<rbrakk> \<Longrightarrow>
  (is_physical cap \<and> cap_range cap \<noteq> {} \<and> cap_range cap \<subseteq> cap_range pcap)" by (fastforce simp: is_cap_simps cap_range_def is_physical_def arch_is_physical_def
               split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap pcap; same_region_as pcap cap\<rbrakk> \<Longrightarrow> is_physical cap \<and> cap_range cap \<noteq> {} \<and> cap_range cap \<subseteq> cap_range pcap
theory ArchCSpace_AI

lemma setup_reply_master_ioports[wp, CSpace_AI_assms]:
  "\<lbrace>valid_ioports\<rbrace> setup_reply_master c \<lbrace>\<lambda>rv. valid_ioports\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioports\<rbrace> setup_reply_master c \<lbrace>\<lambda>rv. valid_ioports\<rbrace>
theory ArchCSpace_AI

lemma cap_insert_derived_ioports[CSpace_AI_assms]:
  "\<lbrace>valid_ioports and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s)\<rbrace>
     cap_insert cap src dest
   \<lbrace>\<lambda>rv. valid_ioports\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioports and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s)\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. valid_ioports\<rbrace>
theory ArchCSpace_AI

lemma is_cap_simps':
  "is_cnode_cap cap = (\<exists>r bits g. cap = cap.CNodeCap r bits g)"
  "is_thread_cap cap = (\<exists>r. cap = cap.ThreadCap r)"
  "is_domain_cap cap = (cap = cap.DomainCap)"
  "is_untyped_cap cap = (\<exists>dev r bits f. cap = cap.UntypedCap dev r bits f)"
  "is_ep_cap cap = (\<exists>r b R. cap = cap.EndpointCap r b R)"
  "is_ntfn_cap cap = (\<exists>r b R. cap = cap.NotificationCap r b R)"
  "is_zombie cap = (\<exists>r b n. cap = cap.Zombie r b n)"
  "is_arch_cap cap = (\<exists>a. cap = cap.ArchObjectCap a)"
  "is_reply_cap cap = (\<exists>x R. cap = cap.ReplyCap x False R)"
  "is_master_reply_cap cap = (\<exists>x R. cap = cap.ReplyCap x True R)"
  "is_nondevice_page_cap cap = (\<exists> u v w x. cap = ArchObjectCap (PageCap False u v w x))" by (cases cap,  (auto simp: is_zombie_def is_arch_cap_def is_nondevice_page_cap_def
                              is_reply_cap_def is_master_reply_cap_def is_nondevice_page_cap_arch_def
                       split: cap.splits arch_cap.splits )+)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((is_cnode_cap cap = (\<exists>r bits g. cap = CNodeCap r bits g) &&& is_thread_cap cap = (\<exists>r. cap = ThreadCap r)) &&& is_domain_cap cap = (cap = DomainCap) &&& is_untyped_cap cap = (\<exists>dev r bits f. cap = UntypedCap dev r bits f) &&& is_ep_cap cap = (\<exists>r b R. cap = EndpointCap r b R)) &&& (is_ntfn_cap cap = (\<exists>r b R. cap = NotificationCap r b R) &&& is_zombie cap = (\<exists>r b n. cap = Zombie r b n) &&& is_arch_cap cap = (\<exists>a. cap = ArchObjectCap a)) &&& is_reply_cap cap = (\<exists>x R. cap = ReplyCap x False R) &&& is_master_reply_cap cap = (\<exists>x R. cap = ReplyCap x True R) &&& is_nondevice_page_cap cap = (\<exists>u v w x. cap = ArchObjectCap (PageCap False u v w x))
theory ArchCSpace_AI

lemma arch_post_cap_deletion_invs:
  "\<lbrace>invs and (\<lambda>s. arch_post_cap_delete_pre (ArchObjectCap c) (caps_of_state s))\<rbrace> arch_post_cap_deletion c \<lbrace>\<lambda>rv. invs\<rbrace>" by (wpsimp simp: arch_post_cap_delete_pre_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. arch_post_cap_delete_pre (ArchObjectCap c) (caps_of_state s))\<rbrace> arch_post_cap_deletion c \<lbrace>\<lambda>rv. invs\<rbrace>
theory ArchCSpace_AI

lemma set_cap_kernel_window_simple:
  "\<lbrace>\<lambda>s. cap_refs_in_kernel_window s
      \<and> cte_wp_at (\<lambda>cap'. cap_range cap' = cap_range cap) ptr s\<rbrace>
     set_cap cap ptr
   \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" apply (wp ARM.set_cap_cap_refs_in_kernel_window) apply (clarsimp simp: cte_wp_at_caps_of_state
                        ARM.cap_refs_in_kernel_windowD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cap_refs_in_kernel_window s \<and> cte_wp_at (\<lambda>cap'. cap_range cap' = cap_range cap) ptr s\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cap_refs_in_kernel_window s \<and> cte_wp_at (\<lambda>cap'. cap_range cap' = cap_range cap) ptr s \<Longrightarrow> (cap_refs_in_kernel_window and (\<lambda>s. \<forall>ref\<in>cap_range cap. ARM_A.arm_kernel_vspace (arch_state s) ref = ARM_H.ArmVSpaceKernelWindow)) s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma gts_sp:
  "\<lbrace>P\<rbrace> get_thread_state t \<lbrace>\<lambda>st. st_tcb_at (\<lambda>x. st = x) t and P\<rbrace>" apply (simp add: pred_conj_def) apply (rule hoare_weaken_pre) apply (rule hoare_vcg_conj_lift) apply (rule gts_st_tcb) apply (rule gts_inv) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_thread_state t \<lbrace>\<lambda>st. st_tcb_at ((=) st) t and P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_thread_state t \<lbrace>\<lambda>st x. st_tcb_at ((=) st) t x \<and> P x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_thread_state t \<lbrace>\<lambda>st x. st_tcb_at ((=) st) t x \<and> P x\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P3\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. st_tcb_at ((=) rv) t\<rbrace>
 2. \<lbrace>?P'3\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?P3 s \<and> ?P'3 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'3\<rbrace> get_thread_state t \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> True \<and> ?P'3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> True \<and> P s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma gbn_sp:
  "\<lbrace>P\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfn. bound_tcb_at (\<lambda>x. ntfn = x) t and P\<rbrace>" apply (simp add: pred_conj_def) apply (rule hoare_weaken_pre) apply (rule hoare_vcg_conj_lift) apply (rule gbn_bound_tcb) apply (rule gbn_inv) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfn. bound_tcb_at ((=) ntfn) t and P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfn x. bound_tcb_at ((=) ntfn) t x \<and> P x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get_bound_notification t \<lbrace>\<lambda>ntfn x. bound_tcb_at ((=) ntfn) t x \<and> P x\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P3\<rbrace> get_bound_notification t \<lbrace>\<lambda>rv. bound_tcb_at ((=) rv) t\<rbrace>
 2. \<lbrace>?P'3\<rbrace> get_bound_notification t \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>s. P s \<Longrightarrow> ?P3 s \<and> ?P'3 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'3\<rbrace> get_bound_notification t \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> True \<and> ?P'3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> True \<and> P s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma red_univ_get_wp[simp]:
  "(\<forall>(rv, s') \<in> fst (f s). s = s' \<longrightarrow> (rv, s') \<in> fst (f s'))" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>(rv, s')\<in>fst (f s). s = s' \<longrightarrow> (rv, s') \<in> fst (f s')
theory TcbAcc_AI

lemma thread_get_inv [wp]: "\<lbrace>P\<rbrace> thread_get f t \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: thread_get_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> thread_get f t \<lbrace>\<lambda>rv. P\<rbrace>
theory TcbAcc_AI

lemma (in TcbAcc_AI_arch_tcb_context_set_eq) thread_get_as_user:
  "thread_get (arch_tcb_context_get o tcb_arch) t = as_user t get" apply (simp add: thread_get_def as_user_def) apply (rule bind_cong [OF refl]) apply (clarsimp simp: gets_the_member set_object_def get_object_def in_monad bind_assoc
                        gets_def put_def bind_def get_def return_def select_f_def
                 dest!: get_tcb_SomeD) apply (subgoal_tac "(kheap s)(t \<mapsto> TCB v) = kheap s", simp) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_get (arch_tcb_context_get \<circ> tcb_arch) t = as_user t get proof (prove)
goal (1 subgoal):
 1. do tcb <- gets_the (get_tcb t);
return (arch_tcb_context_get (tcb_arch tcb))
od = do tcb <- gets_the (get_tcb t);
(a, uc') <- select_f (get (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>));
return a
od proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. (v, s') \<in> fst (gets_the (get_tcb t) s) \<Longrightarrow> return (arch_tcb_context_get (tcb_arch v)) s' = (do (a, uc') <- select_f (get (arch_tcb_context_get (tcb_arch v)));
y <- set_object t (TCB (v\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch v)\<rparr>));
return a
od) s' proof (prove)
goal (1 subgoal):
 1. \<And>v s. kheap s t = Some (TCB v) \<Longrightarrow> s = s\<lparr>kheap := (kheap s)(t \<mapsto> TCB v)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>v s. kheap s t = Some (TCB v) \<Longrightarrow> (kheap s)(t \<mapsto> TCB v) = kheap s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_as_user:
  "thread_set (\<lambda>tcb. tcb \<lparr> tcb_arch := arch_tcb_context_set (f $ arch_tcb_context_get (tcb_arch tcb)) (tcb_arch tcb) \<rparr>) t
    = as_user t (modify f)" proof - have P: "\<And>f. det (modify f)" by (simp add: modify_def) thus ?thesis apply (simp add: as_user_def P thread_set_def) apply (clarsimp simp add: select_f_def simpler_modify_def bind_def image_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set (f $ arch_tcb_context_get (tcb_arch tcb)) (tcb_arch tcb)\<rparr>) t = as_user t (modify f) proof (state)
goal (1 subgoal):
 1. thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set (f $ arch_tcb_context_get (tcb_arch tcb)) (tcb_arch tcb)\<rparr>) t = as_user t (modify f) proof (prove)
goal (1 subgoal):
 1. \<And>f. det (modify f) proof (state)
this:
det (modify ?f)

goal (1 subgoal):
 1. thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set (f $ arch_tcb_context_get (tcb_arch tcb)) (tcb_arch tcb)\<rparr>) t = as_user t (modify f) proof (prove)
using this:
det (modify ?f)

goal (1 subgoal):
 1. thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set (f $ arch_tcb_context_get (tcb_arch tcb)) (tcb_arch tcb)\<rparr>) t = as_user t (modify f) proof (prove)
goal (1 subgoal):
 1. do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (f (arch_tcb_context_get (tcb_arch tcb))) (tcb_arch tcb)\<rparr>))
od = do tcb <- gets_the (get_tcb t);
(a, uc') <- select_f (modify f (arch_tcb_context_get (tcb_arch tcb)));
set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od proof (prove)
goal:
No subgoals! proof (state)
this:
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set (f $ arch_tcb_context_get (tcb_arch tcb)) (tcb_arch tcb)\<rparr>) t = as_user t (modify f)

goal:
No subgoals!
theory TcbAcc_AI

lemma ball_tcb_cap_casesI:
  "\<lbrakk> P (tcb_ctable, tcb_ctable_update, (\<lambda>_ _. \<top>));
     P (tcb_vtable, tcb_vtable_update, (\<lambda>_ _. is_valid_vtable_root or ((=) cap.NullCap)));
     P (tcb_reply, tcb_reply_update, (\<lambda>t st c. (is_master_reply_cap c
                                                \<and> obj_ref_of c = t
                                                \<and> AllowGrant \<in> cap_rights c)
                                             \<or> (halted st \<and> (c = cap.NullCap))));
     P (tcb_caller, tcb_caller_update, (\<lambda>_ st. case st of
                                       Structures_A.BlockedOnReceive e data \<Rightarrow>
                                         ((=) cap.NullCap)
                                     | _ \<Rightarrow> is_reply_cap or ((=) cap.NullCap)));
     P (tcb_ipcframe, tcb_ipcframe_update, (\<lambda>_ _. is_nondevice_page_cap or ((=) cap.NullCap))) \<rbrakk>
    \<Longrightarrow> \<forall>x \<in> ran tcb_cap_cases. P x" by (simp add: tcb_cap_cases_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (tcb_ctable, tcb_ctable_update, \<lambda>_ _ _. True); P (tcb_vtable, tcb_vtable_update, \<lambda>_ _. is_valid_vtable_root or (=) NullCap); P (tcb_reply, tcb_reply_update, \<lambda>t st c. is_master_reply_cap c \<and> obj_ref_of c = t \<and> AllowGrant \<in> cap_rights c \<or> halted st \<and> c = NullCap); P (tcb_caller, tcb_caller_update, \<lambda>_ st. case st of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap); P (tcb_ipcframe, tcb_ipcframe_update, \<lambda>_ _. is_nondevice_page_cap or (=) NullCap)\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cap_cases. P x
theory TcbAcc_AI

lemma thread_set_typ_at[wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> thread_set f p' \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def) apply wp apply clarsimp apply (drule get_tcb_SomeD) apply (clarsimp simp: obj_at_def a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> thread_set f p' \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> do tcb <- gets_the (get_tcb p');
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p' = Some y);
return (the (kh p'))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(p' \<mapsto> TCB (f tcb))\<rparr>)
od \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (typ_at T p s) \<Longrightarrow> get_tcb p' s \<noteq> None \<longrightarrow> (\<exists>y. kheap s p' = Some y) \<longrightarrow> a_type (the (kheap s p')) = ATCB \<longrightarrow> P (typ_at T p (s\<lparr>kheap := (kheap s)(p' \<mapsto> TCB (f (the (get_tcb p' s))))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>P (typ_at T p s); get_tcb p' s = Some y; kheap s p' = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P (typ_at T p (s\<lparr>kheap := \<lambda>a. if a = p' then Some (TCB (f (the (get_tcb p' s)))) else kheap s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>P (typ_at T p s); kheap s p' = Some (TCB tcb); kheap s p' = Some (TCB y)\<rbrakk> \<Longrightarrow> P (typ_at T p (s\<lparr>kheap := \<lambda>a. if a = p' then Some (TCB (f (the (get_tcb p' s)))) else kheap s a\<rparr>)) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_tcb[wp]:
  "\<lbrace>tcb_at t\<rbrace> thread_set t' f \<lbrace>\<lambda>rv. tcb_at t\<rbrace>" by (simp add: thread_set_typ_at [where P="\<lambda>s. s"] tcb_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> thread_set t' f \<lbrace>\<lambda>rv. tcb_at t\<rbrace>
theory TcbAcc_AI

lemma thread_set_no_change_tcb_pred:
  assumes x: "\<And>tcb. proj (tcb_to_itcb (f tcb))    = proj (tcb_to_itcb tcb)"
  shows      "\<lbrace>pred_tcb_at proj P t\<rbrace> thread_set f t' \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>" apply (simp add: thread_set_def pred_tcb_at_def) apply wp apply (rule set_object_at_obj) apply wp apply (clarsimp simp: obj_at_def) apply (drule get_tcb_SomeD) apply (clarsimp simp: x) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> thread_set f t' \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (proj (tcb_to_itcb tcb))) t\<rbrace> do tcb <- gets_the (get_tcb t');
set_object t' (TCB (f tcb))
od \<lbrace>\<lambda>rv. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (proj (tcb_to_itcb tcb))) t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> set_object t' (TCB (f tcb)) \<lbrace>\<lambda>rv. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (proj (tcb_to_itcb tcb))) t\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets_the (get_tcb t') \<lbrace>?B1\<rbrace>
 3. \<And>s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (proj (tcb_to_itcb tcb))) t s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> gets_the (get_tcb t') \<lbrace>\<lambda>tcb s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (proj (tcb_to_itcb tcb))) t s \<and> (t = t' \<longrightarrow> (\<exists>tcba. TCB (f tcb) = TCB tcba \<and> P (proj (tcb_to_itcb tcba))))\<rbrace>
 2. \<And>s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (proj (tcb_to_itcb tcb))) t s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (proj (tcb_to_itcb tcb))) t s \<Longrightarrow> get_tcb t' s \<noteq> None \<longrightarrow> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (proj (tcb_to_itcb tcb))) t s \<and> (t = t' \<longrightarrow> (\<exists>tcb. TCB (f (the (get_tcb t' s))) = TCB tcb \<and> P (proj (tcb_to_itcb tcb)))) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb y. \<lbrakk>kheap s t' = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); get_tcb t' s = Some y; t = t'\<rbrakk> \<Longrightarrow> P (proj (tcb_to_itcb (f y))) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb y. \<lbrakk>kheap s t' = Some (TCB tcb); P (proj (tcb_to_itcb tcb)); t = t'; kheap s t' = Some (TCB y)\<rbrakk> \<Longrightarrow> P (proj (tcb_to_itcb (f y))) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma pspace_valid_objsE:
  assumes p: "kheap s p = Some ko"
  assumes v: "valid_objs s"
  assumes Q: "\<lbrakk>kheap s p = Some ko; valid_obj p ko s\<rbrakk> \<Longrightarrow> Q"
  shows "Q" proof - from p have "ko_at ko p s" by (simp add: obj_at_def) with v show Q by (auto elim: obj_at_valid_objsE simp: Q) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q proof (state)
goal (1 subgoal):
 1. Q proof (chain)
picking this:
kheap s p = Some ko proof (prove)
using this:
kheap s p = Some ko

goal (1 subgoal):
 1. ko_at ko p s proof (state)
this:
ko_at ko p s

goal (1 subgoal):
 1. Q proof (chain)
picking this:
valid_objs s
ko_at ko p s proof (prove)
using this:
valid_objs s
ko_at ko p s

goal (1 subgoal):
 1. Q proof (state)
this:
Q

goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_aligned [wp]:
  "\<lbrace>pspace_aligned\<rbrace> thread_set f t \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>" apply (simp add: thread_set_def) apply (wp set_object_aligned) apply (clarsimp simp: a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> thread_set f t \<lbrace>\<lambda>rv. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>rv. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> pspace_aligned s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_distinct [wp]:
  "\<lbrace>pspace_distinct\<rbrace> thread_set f t \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>" apply (simp add: thread_set_def) apply (wp set_object_distinct) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct\<rbrace> thread_set f t \<lbrace>\<lambda>rv. pspace_distinct\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>rv. pspace_distinct\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_distinct s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> pspace_distinct s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_cur_tcb:
  shows "\<lbrace>\<lambda>s. cur_tcb s\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. cur_tcb s\<rbrace>" apply (simp add: cur_tcb_def) apply (clarsimp simp: thread_set_def pred_tcb_at_def set_object_def get_object_def
                        in_monad gets_the_def valid_def) apply (clarsimp dest!: get_tcb_SomeD simp: obj_at_def is_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb\<rbrace> thread_set f t \<lbrace>\<lambda>rv. cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at (cur_thread s) s\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. tcb_at (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s tcb tcba. \<lbrakk>tcb_at (cur_thread s) s; get_tcb t s = Some tcb; kheap s t = Some (TCB tcba)\<rbrakk> \<Longrightarrow> tcb_at (cur_thread s) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (f tcb))\<rparr>) proof (prove)
goal:
No subgoals!