kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_AI

lemma det_query_twice:
  assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x. P\<rbrace>"
  assumes y: "det f"
  shows      "do x \<leftarrow> f; y :: tcb \<leftarrow> f; g x y od
               = do x \<leftarrow> f; g x x od" apply (subgoal_tac "\<exists>fn. f = (\<lambda>s. ({(fn s, s)}, False))") apply clarsimp apply (rule bind_cong [OF refl]) apply (simp add: bind_def) apply (rule_tac x="\<lambda>s. fst (THE x. x \<in> fst (f s))" in exI) apply (rule ext) apply (insert y, simp add: det_def) apply (erule_tac x=s in allE) apply clarsimp apply (rule sym) apply (rule state_unchanged [OF x]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- f;
f >>= g x
od = do x <- f;
g x x
od proof (prove)
goal (2 subgoals):
 1. \<exists>fn. f = (\<lambda>s. ({(fn s, s)}, False)) \<Longrightarrow> do x <- f;
f >>= g x
od = do x <- f;
g x x
od
 2. \<exists>fn. f = (\<lambda>s. ({(fn s, s)}, False)) proof (prove)
goal (2 subgoals):
 1. \<And>fn. f = (\<lambda>s. ({(fn s, s)}, False)) \<Longrightarrow> do x <- \<lambda>s. ({(fn s, s)}, False);
(\<lambda>s. ({(fn s, s)}, False)) >>= g x
od = do x <- \<lambda>s. ({(fn s, s)}, False);
g x x
od
 2. \<exists>fn. f = (\<lambda>s. ({(fn s, s)}, False)) proof (prove)
goal (2 subgoals):
 1. \<And>fn v s s'. \<lbrakk>f = (\<lambda>s. ({(fn s, s)}, False)); (v, s') \<in> fst ({(fn s, s)}, False)\<rbrakk> \<Longrightarrow> ((\<lambda>s. ({(fn s, s)}, False)) >>= g v) s' = g v v s'
 2. \<exists>fn. f = (\<lambda>s. ({(fn s, s)}, False)) proof (prove)
goal (1 subgoal):
 1. \<exists>fn. f = (\<lambda>s. ({(fn s, s)}, False)) proof (prove)
goal (1 subgoal):
 1. f = (\<lambda>s. ({(fst (THE x. x \<in> fst (f s)), s)}, False)) proof (prove)
goal (1 subgoal):
 1. \<And>s. f s = ({(fst (THE x. x \<in> fst (f s)), s)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>s. \<exists>a b. f s = ({(a, b)}, False) \<Longrightarrow> f s = ({(fst (THE x. x \<in> fst (f s)), s)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>a b. f s = ({(a, b)}, False) \<Longrightarrow> f s = ({(fst (THE x. x \<in> fst (f s)), s)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. f s = ({(a, b)}, False) \<Longrightarrow> b = s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. f s = ({(a, b)}, False) \<Longrightarrow> s = b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. f s = ({(a, b)}, False) \<Longrightarrow> (?x22 s a b, b) \<in> fst (f s) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma as_user_psp_distinct[wp]:
  "\<lbrace>pspace_distinct\<rbrace> as_user t m \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>" by (wp as_user_wp_thread_set_helper) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct\<rbrace> as_user t m \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>
theory TcbAcc_AI

lemma as_user_psp_aligned[wp]:
  "\<lbrace>pspace_aligned\<rbrace> as_user t m \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>" by (wp as_user_wp_thread_set_helper) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> as_user t m \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>
theory TcbAcc_AI

lemma as_user_objs [wp]:
  "\<lbrace>valid_objs\<rbrace> as_user a f \<lbrace>\<lambda>rv. valid_objs\<rbrace>" apply (wp as_user_wp_thread_set_helper
            thread_set_valid_objs_triv) apply (wpsimp simp: ran_tcb_cap_cases valid_arch_arch_tcb_context_set)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> as_user a f \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>tcb p tcba. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (tcba\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcba)\<rparr>) = getF tcba
 2. \<And>tcb p tcba. tcb_state (tcba\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcba)\<rparr>) = tcb_state tcba
 3. \<And>tcb p tcba. tcb_ipc_buffer (tcba\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcba)\<rparr>) = tcb_ipc_buffer tcba \<or> tcb_ipc_buffer (tcba\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcba)\<rparr>) = 0
 4. \<And>tcb p tcba. tcb_fault_handler (tcba\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcba)\<rparr>) \<noteq> tcb_fault_handler tcba \<longrightarrow> length (tcb_fault_handler (tcba\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcba)\<rparr>)) = word_bits
 5. \<And>tcb p tcba. tcb_fault (tcba\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcba)\<rparr>) \<noteq> tcb_fault tcba \<longrightarrow> (case tcb_fault (tcba\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcba)\<rparr>) of None \<Rightarrow> True | Some f \<Rightarrow> valid_fault f)
 6. \<And>tcb p tcba. tcb_bound_notification (tcba\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcba)\<rparr>) \<noteq> tcb_bound_notification tcba \<longrightarrow> tcb_bound_notification (tcba\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcba)\<rparr>) = None
 7. \<And>tcb p tcba s. valid_arch_tcb (tcb_arch (tcba\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcba)\<rparr>)) s = valid_arch_tcb (tcb_arch tcba) s
 8. \<And>tcb. \<lbrace>?B2 tcb\<rbrace> select_f (f (arch_tcb_context_get (tcb_arch tcb))) \<lbrace>\<lambda>p. valid_objs\<rbrace>
 9. \<lbrace>?Q\<rbrace> gets_the (get_tcb a) \<lbrace>?B2\<rbrace>
 10. \<And>s. valid_objs s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma as_user_reply[wp]:
  "\<lbrace>valid_reply_caps\<rbrace> as_user t f \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>" by (wp as_user_wp_thread_set_helper thread_set_valid_reply_caps_trivial
         ball_tcb_cap_casesI | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps\<rbrace> as_user t f \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>
theory TcbAcc_AI

lemma as_user_reply_masters[wp]:
  "\<lbrace>valid_reply_masters\<rbrace> as_user t f \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>" by (wp as_user_wp_thread_set_helper thread_set_valid_reply_masters_trivial
         ball_tcb_cap_casesI | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters\<rbrace> as_user t f \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>
theory TcbAcc_AI

lemma as_user_arch[wp]:
  "\<lbrace>\<lambda>s. P (arch_state s)\<rbrace> as_user t f \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>" apply (simp add: as_user_def split_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> as_user t f \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> do tcb <- gets_the (get_tcb t);
p <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (arch_state s) \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). P (arch_state s)) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma as_user_irq_handlers[wp]:
  "\<lbrace>valid_irq_handlers\<rbrace> as_user t f \<lbrace>\<lambda>_. valid_irq_handlers\<rbrace>" apply (rule as_user_wp_thread_set_helper) apply (wp valid_irq_handlers_lift thread_set_caps_of_state_trivial
                ball_tcb_cap_casesI | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers\<rbrace> as_user t f \<lbrace>\<lambda>_. valid_irq_handlers\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers\<rbrace> do tcb <- gets_the (get_tcb t);
p <- select_f (f (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>_. valid_irq_handlers\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma as_user_iflive[wp]:
  "\<lbrace>if_live_then_nonz_cap\<rbrace> as_user t f \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace>" by (wp as_user_wp_thread_set_helper thread_set_iflive_trivial
         ball_tcb_cap_casesI | simp add:)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap\<rbrace> as_user t f \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace>
theory TcbAcc_AI

lemma as_user_ifunsafe[wp]:
  "\<lbrace>if_unsafe_then_cap\<rbrace> as_user t f \<lbrace>\<lambda>_. if_unsafe_then_cap\<rbrace>" by (wp as_user_wp_thread_set_helper thread_set_ifunsafe_trivial
         ball_tcb_cap_casesI | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> as_user t f \<lbrace>\<lambda>_. if_unsafe_then_cap\<rbrace>
theory TcbAcc_AI

lemma as_user_zombies[wp]:
  "\<lbrace>zombies_final\<rbrace> as_user t f \<lbrace>\<lambda>_. zombies_final\<rbrace>" by (wp as_user_wp_thread_set_helper thread_set_zombies_trivial
         ball_tcb_cap_casesI | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final\<rbrace> as_user t f \<lbrace>\<lambda>_. zombies_final\<rbrace>
theory TcbAcc_AI

lemma as_user_refs_of[wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>
     as_user t m
   \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" apply (wp as_user_wp_thread_set_helper
            thread_set_refs_trivial | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> as_user t m \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma as_user_global_refs [wp]:
  "\<lbrace>valid_global_refs\<rbrace> as_user t f \<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> as_user t f \<lbrace>\<lambda>_. valid_global_refs\<rbrace>
theory TcbAcc_AI

lemma as_user_ct: "\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> as_user t m \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>" apply (simp add: as_user_def split_def set_object_def get_object_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> as_user t m \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> do tcb <- gets_the (get_tcb t);
p <- select_f (m (arch_tcb_context_get (tcb_arch tcb)));
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_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
return (fst p)
od \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cur_thread s) \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (m (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> P (cur_thread (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>))) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma as_user_cur [wp]:
  "\<lbrace>cur_tcb\<rbrace> as_user t f \<lbrace>\<lambda>_. cur_tcb\<rbrace>" by (wp as_user_wp_thread_set_helper) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb\<rbrace> as_user t f \<lbrace>\<lambda>_. cur_tcb\<rbrace>
theory TcbAcc_AI

lemma as_user_ex_nonz_cap_to[wp]:
  "\<lbrace>ex_nonz_cap_to p\<rbrace> as_user t m \<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> as_user t m \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>
theory TcbAcc_AI

lemma as_user_pred_tcb_at [wp]:
  "\<lbrace>pred_tcb_at proj P t\<rbrace> as_user t' m \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>" by (wp as_user_wp_thread_set_helper thread_set_no_change_tcb_pred
      | simp add: tcb_to_itcb_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> as_user t' m \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>
theory TcbAcc_AI

lemma ct_in_state_thread_state_lift:
  assumes ct: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>"
  assumes st: "\<And>t. \<lbrace>st_tcb_at P t\<rbrace> f \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace>"
  shows "\<lbrace>ct_in_state P\<rbrace> f \<lbrace>\<lambda>_. ct_in_state P\<rbrace>" apply (clarsimp simp: ct_in_state_def) apply (clarsimp simp: valid_def) apply (frule (1) use_valid [OF _ ct]) apply (drule (1) use_valid [OF _ st], assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state P\<rbrace> f \<lbrace>\<lambda>_. ct_in_state P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. st_tcb_at P (cur_thread s) s\<rbrace> f \<lbrace>\<lambda>_ s. st_tcb_at P (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>st_tcb_at P (cur_thread s) s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> st_tcb_at P (cur_thread b) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>st_tcb_at P (cur_thread s) s; (a, b) \<in> fst (f s); st_tcb_at P (cur_thread b) s\<rbrakk> \<Longrightarrow> st_tcb_at P (cur_thread b) b proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma as_user_ct_in_state:
  "\<lbrace>ct_in_state x\<rbrace> as_user t f \<lbrace>\<lambda>_. ct_in_state x\<rbrace>" by (rule ct_in_state_thread_state_lift) (wpsimp wp: as_user_ct)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state x\<rbrace> as_user t f \<lbrace>\<lambda>_. ct_in_state x\<rbrace>
theory TcbAcc_AI

lemma set_object_ntfn_at:
  "\<lbrace> ntfn_at p and tcb_at r \<rbrace> set_object r obj \<lbrace> \<lambda>rv. ntfn_at p \<rbrace>" apply (rule set_object_at_obj2) apply (clarsimp simp: is_obj_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ntfn_at p and tcb_at r\<rbrace> set_object r obj \<lbrace>\<lambda>rv. ntfn_at p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko. is_tcb ko \<Longrightarrow> \<not> is_ntfn ko proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma gts_wf[wp]: "\<lbrace>tcb_at t and invs\<rbrace> get_thread_state t \<lbrace>valid_tcb_state\<rbrace>" apply (simp add: get_thread_state_def thread_get_def) apply wp apply (clarsimp simp: invs_def valid_state_def valid_pspace_def
                        valid_objs_def get_tcb_def dom_def
                  split: option.splits Structures_A.kernel_object.splits) apply (erule allE, erule impE, blast) apply (clarsimp simp: valid_obj_def valid_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t and invs\<rbrace> get_thread_state t \<lbrace>valid_tcb_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t and invs\<rbrace> do tcb <- gets_the (get_tcb t);
return (tcb_state tcb)
od \<lbrace>valid_tcb_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at t and invs) s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> valid_tcb_state (tcb_state (the (get_tcb t s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>tcb_at t s; \<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; kheap s t = Some (TCB x2)\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state x2) s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>tcb_at t s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; kheap s t = Some (TCB x2); \<exists>obj. kheap s t = Some obj \<and> valid_obj t obj s\<rbrakk> \<Longrightarrow> valid_tcb_state (tcb_state x2) s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma idle_thread_idle[wp]:
  "\<lbrace>\<lambda>s. valid_idle s \<and> t = idle_thread s\<rbrace> get_thread_state t \<lbrace>\<lambda>r s. idle r\<rbrace>" apply (clarsimp simp: valid_def get_thread_state_def thread_get_def bind_def return_def
                        gets_the_def gets_def get_def assert_opt_def get_tcb_def
                        fail_def valid_idle_def obj_at_def pred_tcb_at_def
                 split: option.splits Structures_A.kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_idle s \<and> t = idle_thread s\<rbrace> get_thread_state t \<lbrace>\<lambda>r s. idle r\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_bound_notification_valid_objs[wp]:
  "\<lbrace>valid_objs and valid_bound_ntfn ntfn\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_objs\<rbrace>" apply (simp add: set_bound_notification_def) apply (wp set_object_valid_objs, simp) apply (clarsimp simp: obj_at_def get_tcb_def is_tcb
                  split: option.splits kernel_object.splits) apply (erule (1) valid_objsE) apply (auto simp: valid_obj_def valid_tcb_def tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_bound_ntfn ntfn\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_bound_ntfn ntfn\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<and> valid_bound_ntfn ntfn s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> valid_obj t (TCB (the (get_tcb t s)\<lparr>tcb_bound_notification := ntfn\<rparr>)) s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_objs s; valid_bound_ntfn ntfn s; kheap s t = Some (TCB x2)\<rbrakk> \<Longrightarrow> valid_obj t (TCB (x2\<lparr>tcb_bound_notification := ntfn\<rparr>)) s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_bound_ntfn ntfn s; kheap s t = Some (TCB x2); valid_obj t (TCB x2) s\<rbrakk> \<Longrightarrow> valid_obj t (TCB (x2\<lparr>tcb_bound_notification := ntfn\<rparr>)) s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_bound_notification_aligned[wp]:
 "\<lbrace>pspace_aligned\<rbrace>
  set_bound_notification thread ntfn
  \<lbrace>\<lambda>r. pspace_aligned\<rbrace>" apply (simp add: set_bound_notification_def) apply (wp set_object_aligned) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> set_bound_notification thread ntfn \<lbrace>\<lambda>r. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> do tcb <- gets_the (get_tcb thread);
set_object thread (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>r. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned s \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> pspace_aligned s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_thread_state_typ_at [wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_thread_state st p' \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" apply (simp add: set_thread_state_def set_object_def get_object_def) apply (wp|clarsimp)+ apply (clarsimp simp: obj_at_def a_type_def dest!: get_tcb_SomeD) done

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

lemma set_bound_notification_tcb[wp]:
  "\<lbrace>tcb_at t\<rbrace> set_bound_notification t' ntfn \<lbrace>\<lambda>rv. tcb_at t\<rbrace>" by (simp add: tcb_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> set_bound_notification t' ntfn \<lbrace>\<lambda>rv. tcb_at t\<rbrace>