kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_AI

lemma set_thread_state_ko:
  "\<lbrace>ko_at obj ptr and K (\<not>is_tcb obj)\<rbrace> set_thread_state x st \<lbrace>\<lambda>rv. ko_at obj ptr\<rbrace>" apply (simp add: set_thread_state_def) apply (wp set_object_ko|clarsimp)+ apply (drule get_tcb_SomeD) apply (clarsimp simp: obj_at_def is_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at obj ptr and K (\<not> is_tcb obj)\<rbrace> set_thread_state x st \<lbrace>\<lambda>rv. ko_at obj ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at obj ptr and (\<lambda>y. \<not> is_tcb obj)\<rbrace> do tcb <- gets_the (get_tcb x);
y <- set_object x (TCB (tcb\<lparr>tcb_state := st\<rparr>));
do_extended_op (set_thread_state_ext x)
od \<lbrace>\<lambda>rv. ko_at obj ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>ko_at obj ptr s; \<not> is_tcb obj; get_tcb ptr s = Some y; x = ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>ko_at obj ptr s; \<not> is_tcb obj; x = ptr; kheap s ptr = Some (TCB y)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_bound_notification_ko:
  "\<lbrace>ko_at obj ptr and K (\<not>is_tcb obj)\<rbrace> set_bound_notification x ntfn \<lbrace>\<lambda>rv. ko_at obj ptr\<rbrace>" apply (simp add: set_bound_notification_def) apply (wp set_object_ko, clarsimp) apply (drule get_tcb_SomeD) apply (clarsimp simp: obj_at_def is_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at obj ptr and K (\<not> is_tcb obj)\<rbrace> set_bound_notification x ntfn \<lbrace>\<lambda>rv. ko_at obj ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at obj ptr and (\<lambda>y. \<not> is_tcb obj)\<rbrace> do tcb <- gets_the (get_tcb x);
set_object x (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>rv. ko_at obj ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>ko_at obj ptr s; \<not> is_tcb obj; get_tcb ptr s = Some y; x = ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>ko_at obj ptr s; \<not> is_tcb obj; x = ptr; kheap s ptr = Some (TCB y)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_thread_state_valid_cap:
  "\<lbrace>valid_cap c\<rbrace> set_thread_state x st \<lbrace>\<lambda>rv. valid_cap c\<rbrace>" apply (simp add: set_thread_state_def) apply (wp set_object_valid_cap|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> set_thread_state x st \<lbrace>\<lambda>rv. valid_cap c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> do tcb <- gets_the (get_tcb x);
y <- set_object x (TCB (tcb\<lparr>tcb_state := st\<rparr>));
do_extended_op (set_thread_state_ext x)
od \<lbrace>\<lambda>rv. valid_cap c\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma dom_mapM:
  assumes "\<And>x. empty_fail (m x)"
  shows "do_machine_op (mapM m xs) = mapM (do_machine_op \<circ> m) xs" by (rule submonad_mapM [OF submonad_do_machine_op submonad_do_machine_op,
                             simplified]) fact+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do_machine_op (mapM m xs) = mapM (do_machine_op \<circ> m) xs
theory TcbAcc_AI

lemma sts_ex_nonz_cap_to[wp]:
  "\<lbrace>ex_nonz_cap_to p\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>" by (wp ex_nonz_cap_to_pres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to p\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>
theory TcbAcc_AI

lemma sts_ctis_neq:
  "\<lbrace>\<lambda>s. cur_thread s \<noteq> t \<and> ct_in_state P s\<rbrace> set_thread_state t st \<lbrace>\<lambda>_. ct_in_state P\<rbrace>" apply (simp add: ct_in_state_def set_thread_state_def set_object_def get_object_def) apply (wp|simp add: pred_tcb_at_def obj_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cur_thread s \<noteq> t \<and> ct_in_state P s\<rbrace> set_thread_state t st \<lbrace>\<lambda>_. ct_in_state P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cur_thread s \<noteq> t \<and> st_tcb_at P (cur_thread s) s\<rbrace> do tcb <- gets_the (get_tcb t);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
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. st_tcb_at P (cur_thread s) s\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma valid_running [simp]:
  "valid_tcb_state Structures_A.Running = \<top>" by (rule ext, simp add: valid_tcb_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb_state Running = (\<lambda>_. True)
theory TcbAcc_AI

lemma valid_inactive [simp]:
  "valid_tcb_state Structures_A.Inactive = \<top>" by (rule ext, simp add: valid_tcb_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb_state Inactive = (\<lambda>_. True)
theory TcbAcc_AI

lemma ntfn_queued_st_tcb_at:
  "\<And>P. \<lbrakk>ko_at (Notification ep) ptr s; (t, rt) \<in> ntfn_q_refs_of (ntfn_obj ep);
         valid_objs s; sym_refs (state_refs_of s);
         \<And>ref. P (Structures_A.BlockedOnNotification ref) \<rbrakk>
   \<Longrightarrow> st_tcb_at P t s" apply (case_tac "ntfn_obj ep", simp_all) apply (frule(1) sym_refs_ko_atD) apply (clarsimp) apply (erule_tac y="(t,NTFNSignal)" in my_BallE) apply (clarsimp simp: pred_tcb_at_def refs_of_rev elim!: obj_at_weakenE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>ko_at (Notification ep) ptr s; (t, rt) \<in> ntfn_q_refs_of (ntfn_obj ep); valid_objs s; sym_refs (state_refs_of s); \<And>ref. P (BlockedOnNotification ref)\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal (1 subgoal):
 1. \<And>P x2. \<lbrakk>ko_at (Notification ep) ptr s; t \<in> set x2 \<and> rt = NTFNSignal; valid_objs s; sym_refs (state_refs_of s); \<And>ref. P (BlockedOnNotification ref); ntfn_obj ep = WaitingNtfn x2\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal (1 subgoal):
 1. \<And>P x2. \<lbrakk>ko_at (Notification ep) ptr s; t \<in> set x2 \<and> rt = NTFNSignal; valid_objs s; sym_refs (state_refs_of s); \<And>ref. P (BlockedOnNotification ref); ntfn_obj ep = WaitingNtfn x2; state_refs_of s ptr = refs_of (Notification ep) \<and> (\<forall>(x, tp)\<in>refs_of (Notification ep). obj_at (\<lambda>ko. (ptr, symreftype tp) \<in> refs_of ko) x s)\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal (1 subgoal):
 1. \<And>P x2. \<lbrakk>ko_at (Notification ep) ptr s; valid_objs s; sym_refs (state_refs_of s); \<And>ref. P (BlockedOnNotification ref); ntfn_obj ep = WaitingNtfn x2; t \<in> set x2; rt = NTFNSignal; state_refs_of s ptr = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ep); \<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ep). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ptr, symreftype tp) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal (2 subgoals):
 1. \<And>P x2. \<lbrakk>ko_at (Notification ep) ptr s; valid_objs s; sym_refs (state_refs_of s); \<And>ref. P (BlockedOnNotification ref); ntfn_obj ep = WaitingNtfn x2; t \<in> set x2; rt = NTFNSignal; state_refs_of s ptr = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ep)\<rbrakk> \<Longrightarrow> (t, NTFNSignal) \<in> set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ep)
 2. \<And>P x2. \<lbrakk>ko_at (Notification ep) ptr s; valid_objs s; sym_refs (state_refs_of s); \<And>ref. P (BlockedOnNotification ref); ntfn_obj ep = WaitingNtfn x2; t \<in> set x2; rt = NTFNSignal; state_refs_of s ptr = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ep); case (t, NTFNSignal) of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ptr, symreftype tp) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma ep_queued_st_tcb_at:
  "\<And>P. \<lbrakk>ko_at (Endpoint ep) ptr s; (t, rt) \<in> ep_q_refs_of ep;
         valid_objs s; sym_refs (state_refs_of s);
         \<And>ref pl pl'. P (Structures_A.BlockedOnSend ref pl) \<and>
  P (Structures_A.BlockedOnReceive ref pl') \<rbrakk>
    \<Longrightarrow> st_tcb_at P t s" apply (case_tac ep, simp_all) apply (frule(1) sym_refs_ko_atD, clarsimp, erule (1) my_BallE,
         clarsimp simp: pred_tcb_at_def refs_of_rev elim!: obj_at_weakenE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>ko_at (Endpoint ep) ptr s; (t, rt) \<in> ep_q_refs_of ep; valid_objs s; sym_refs (state_refs_of s); \<And>ref pl pl'. P (BlockedOnSend ref pl) \<and> P (BlockedOnReceive ref pl')\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal (2 subgoals):
 1. \<And>P x2. \<lbrakk>ko_at (Endpoint (SendEP x2)) ptr s; t \<in> set x2 \<and> rt = EPSend; valid_objs s; sym_refs (state_refs_of s); \<And>ref pl pl'. P (BlockedOnSend ref pl) \<and> P (BlockedOnReceive ref pl'); ep = SendEP x2\<rbrakk> \<Longrightarrow> st_tcb_at P t s
 2. \<And>P x3. \<lbrakk>ko_at (Endpoint (RecvEP x3)) ptr s; t \<in> set x3 \<and> rt = EPRecv; valid_objs s; sym_refs (state_refs_of s); \<And>ref pl pl'. P (BlockedOnSend ref pl) \<and> P (BlockedOnReceive ref pl'); ep = RecvEP x3\<rbrakk> \<Longrightarrow> st_tcb_at P t s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_ct_running:
  "(\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow>
  \<lbrace>ct_running\<rbrace> thread_set f t \<lbrace>\<lambda>rv. ct_running\<rbrace>" apply (simp add: ct_in_state_def) apply (rule hoare_lift_Pf [where f=cur_thread]) apply (wp thread_set_no_change_tcb_state; simp) apply (simp add: thread_set_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>ct_running\<rbrace> thread_set f t \<lbrace>\<lambda>rv. ct_running\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at (\<lambda>st. st = Running) (cur_thread s) s\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. st_tcb_at (\<lambda>st. st = Running) (cur_thread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. st = Running) x\<rbrace> thread_set f t \<lbrace>\<lambda>_. st_tcb_at (\<lambda>st. st = Running) x\<rbrace>
 2. \<And>P. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P s. \<lbrakk>\<And>tcb. tcb_state (f tcb) = tcb_state tcb; P (cur_thread s)\<rbrakk> \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> P (cur_thread s) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sts_tcb_ko_at:
  "\<lbrace>\<lambda>s. \<forall>v'. v = (if t = t' then v' \<lparr>tcb_state := ts\<rparr> else v')
              \<longrightarrow> ko_at (TCB v') t' s \<longrightarrow> P v\<rbrace>
      set_thread_state t ts
   \<lbrace>\<lambda>rv s. ko_at (TCB v) t' s \<longrightarrow> P v\<rbrace>" apply (simp add: set_thread_state_def set_object_def get_object_def) apply (wp|simp)+ apply (clarsimp simp: obj_at_def dest!: get_tcb_SomeD) apply (simp add: get_tcb_def) done

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

lemma as_user_invs[wp]: "\<lbrace>invs:: 'state_ext state \<Rightarrow> bool\<rbrace> as_user t m \<lbrace>\<lambda>rv. invs\<rbrace>" apply (rule as_user_wp_thread_set_helper) apply (rule hoare_pre) apply (wp thread_set_invs_trivial ball_tcb_cap_casesI | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> as_user t m \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do tcb <- gets_the (get_tcb t);
p <- select_f (m (arch_tcb_context_get (tcb_arch tcb)));
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>) t
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> do tcb <- gets_the (get_tcb t);
p <- select_f (m (arch_tcb_context_get (tcb_arch tcb)));
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>) t
od \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>s. invs s \<Longrightarrow> ?Q2 s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_mrs_pred_tcb_at [wp]:
  "\<lbrace>pred_tcb_at proj P t\<rbrace> set_mrs r t' mrs \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>" apply (rule set_mrs_thread_set_dmo) apply (rule thread_set_no_change_tcb_pred) apply (simp add: tcb_to_itcb_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> set_mrs r t' mrs \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>c. \<lbrace>pred_tcb_at proj P t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (c tcb) (tcb_arch tcb)\<rparr>) r \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>
 2. \<And>x y. \<lbrace>pred_tcb_at proj P t\<rbrace> do_machine_op (storeWord x y) \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>c tcb. proj (tcb_to_itcb (tcb\<lparr>tcb_arch := arch_tcb_set_registers (c tcb) (tcb_arch tcb)\<rparr>)) = proj (tcb_to_itcb tcb)
 2. \<And>x y. \<lbrace>pred_tcb_at proj P t\<rbrace> do_machine_op (storeWord x y) \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrace>pred_tcb_at proj P t\<rbrace> do_machine_op (storeWord x y) \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma get_tcb_ko_atD:
  "get_tcb t s = Some tcb \<Longrightarrow> ko_at (TCB tcb) t s" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_tcb t s = Some tcb \<Longrightarrow> ko_at (TCB tcb) t s
theory TcbAcc_AI

lemma thread_set_ct_in_state:
  "(\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow>
  \<lbrace>ct_in_state st\<rbrace> thread_set f t \<lbrace>\<lambda>rv. ct_in_state st\<rbrace>" apply (simp add: ct_in_state_def) apply (rule hoare_lift_Pf [where f=cur_thread]) apply (wp thread_set_no_change_tcb_state; simp) apply (simp add: thread_set_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>ct_in_state st\<rbrace> thread_set f t \<lbrace>\<lambda>rv. ct_in_state st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at st (cur_thread s) s\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. st_tcb_at st (cur_thread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>st_tcb_at st x\<rbrace> thread_set f t \<lbrace>\<lambda>_. st_tcb_at st x\<rbrace>
 2. \<And>P. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. (\<And>tcb. tcb_state (f tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (f tcb))
od \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P s. \<lbrakk>\<And>tcb. tcb_state (f tcb) = tcb_state tcb; P (cur_thread s)\<rbrakk> \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> P (cur_thread s) proof (prove)
goal:
No subgoals!
theory ArchTcbAcc_AI

lemma cap_master_cap_arch_eqDs:
  "cap_master_cap cap = cap.ArchObjectCap (arch_cap.PageCap dev ref rghts sz mapdata)
     \<Longrightarrow> rghts = UNIV \<and> mapdata = None
          \<and> (\<exists>rghts mapdata. cap = cap.ArchObjectCap (arch_cap.PageCap dev ref rghts sz mapdata))"
  "cap_master_cap cap = cap.ArchObjectCap arch_cap.ASIDControlCap
     \<Longrightarrow> cap = cap.ArchObjectCap arch_cap.ASIDControlCap"
  "cap_master_cap cap = cap.ArchObjectCap (arch_cap.ASIDPoolCap pool asid)
     \<Longrightarrow> asid = 0 \<and> (\<exists>asid. cap = cap.ArchObjectCap (arch_cap.ASIDPoolCap pool asid))"
  "cap_master_cap cap = cap.ArchObjectCap (arch_cap.PageTableCap ptr data)
     \<Longrightarrow> data = None \<and> (\<exists>data. cap = cap.ArchObjectCap (arch_cap.PageTableCap ptr data))"
  "cap_master_cap cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap ptr data2)
     \<Longrightarrow> data2 = None \<and> (\<exists>data2. cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap ptr data2))" by (clarsimp simp: cap_master_cap_def
              split: cap.split_asm arch_cap.split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((cap_master_cap cap = ArchObjectCap (PageCap dev ref rghts sz mapdata) \<Longrightarrow> rghts = UNIV \<and> mapdata = None \<and> (\<exists>rghts mapdata. cap = ArchObjectCap (PageCap dev ref rghts sz mapdata))) &&& (cap_master_cap cap = ArchObjectCap ASIDControlCap \<Longrightarrow> cap = ArchObjectCap ASIDControlCap)) &&& (cap_master_cap cap = ArchObjectCap (ASIDPoolCap pool asid) \<Longrightarrow> asid = 0 \<and> (\<exists>asid. cap = ArchObjectCap (ASIDPoolCap pool asid))) &&& (cap_master_cap cap = ArchObjectCap (PageTableCap ptr data) \<Longrightarrow> data = None \<and> (\<exists>data. cap = ArchObjectCap (PageTableCap ptr data))) &&& (cap_master_cap cap = ArchObjectCap (PageDirectoryCap ptr data2) \<Longrightarrow> data2 = None \<and> (\<exists>data2. cap = ArchObjectCap (PageDirectoryCap ptr data2)))
theory ArchTcbAcc_AI

lemma vm_sets_diff[simp]:
  "vm_read_only \<noteq> vm_read_write" by (simp add: vm_read_write_def vm_read_only_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vm_read_only \<noteq> vm_read_write
theory ArchTcbAcc_AI

lemma valid_ipc_buffer_cap_0[simp, TcbAcc_AI_assms]:
  "valid_ipc_buffer_cap cap a \<Longrightarrow> valid_ipc_buffer_cap cap 0" by (auto simp add: valid_ipc_buffer_cap_def case_bool_If
    split: cap.split arch_cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_ipc_buffer_cap cap a \<Longrightarrow> valid_ipc_buffer_cap cap 0
theory ArchTcbAcc_AI

lemma thread_set_hyp_refs_trivial [TcbAcc_AI_assms]:
  assumes x: "\<And>tcb. tcb_state  (f tcb) = tcb_state  tcb"
  assumes y: "\<And>tcb. tcb_arch_ref (f tcb) = tcb_arch_ref tcb"
  shows      "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>" apply (simp add: thread_set_def set_object_def get_object_def) apply wp apply (clarsimp dest!: get_tcb_SomeD) apply (clarsimp elim!: rsubst[where P=P]) apply (rule all_ext;
         clarsimp simp: state_hyp_refs_of_def hyp_refs_of_def tcb_hyp_refs_def
                        get_tcb_def x y[simplified tcb_arch_ref_def]) done

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

lemma mab_wb [simp]:
  "msg_align_bits < word_bits" unfolding msg_align_bits word_bits_conv by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msg_align_bits < word_bits proof (prove)
goal (1 subgoal):
 1. 9 < 32