kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_AI

lemma sbn_st_tcb_at[wp]:
  "\<lbrace>st_tcb_at P t\<rbrace> set_bound_notification tcb ntfn \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace>" apply (simp add: set_bound_notification_def set_object_def get_object_def) apply wp apply (auto simp: pred_tcb_at_def obj_at_def get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> set_bound_notification tcb ntfn \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at P t\<rbrace> do tcba <- gets_the (get_tcb tcb);
kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh tcb = Some y);
return (the (kh tcb))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (tcba\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)
od \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at P t s \<Longrightarrow> get_tcb tcb s \<noteq> None \<longrightarrow> (\<exists>y. kheap s tcb = Some y) \<longrightarrow> a_type (the (kheap s tcb)) = ATCB \<longrightarrow> st_tcb_at P t (s\<lparr>kheap := (kheap s)(tcb \<mapsto> TCB (the (get_tcb tcb s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sbn_reply [wp]:
  "\<lbrace>valid_reply_caps\<rbrace>
   set_bound_notification p ntfn \<lbrace>\<lambda>_. valid_reply_caps\<rbrace>" apply (simp only: valid_reply_caps_def imp_conv_disj
                    cte_wp_at_caps_of_state has_reply_cap_def) apply (rule hoare_pre, wp hoare_vcg_all_lift
                            hoare_vcg_disj_lift) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps\<rbrace> set_bound_notification p ntfn \<lbrace>\<lambda>_. valid_reply_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>t. (\<nexists>p cap. caps_of_state s p = Some cap \<and> is_reply_cap_to t cap) \<or> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace> set_bound_notification p ntfn \<lbrace>\<lambda>_ s. (\<forall>t. (\<nexists>p cap. caps_of_state s p = Some cap \<and> is_reply_cap_to t cap) \<or> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>t. (\<nexists>p cap. caps_of_state s p = Some cap \<and> is_reply_cap_to t cap) \<or> st_tcb_at awaiting_reply t s) \<and> unique_reply_caps (caps_of_state s) \<Longrightarrow> (\<forall>x. (\<nexists>p cap. caps_of_state s p = Some cap \<and> is_reply_cap_to x cap) \<or> st_tcb_at awaiting_reply x s) \<and> unique_reply_caps (caps_of_state s) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sts_reply_masters [wp]:
  "\<lbrace>valid_reply_masters\<rbrace> set_thread_state p st \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>" apply (simp add: set_thread_state_thread_set) apply (wp thread_set_valid_reply_masters_trivial|simp)+ apply (fastforce simp: tcb_cap_cases_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters\<rbrace> set_thread_state p st \<lbrace>\<lambda>_. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters\<rbrace> do y <- thread_set (tcb_state_update (\<lambda>_. st)) p;
do_extended_op (set_thread_state_ext p)
od \<lbrace>\<lambda>_. valid_reply_masters\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, v) \<Rightarrow> getF (tcb\<lparr>tcb_state := st\<rparr>) = getF tcb
 2. \<And>s. valid_reply_masters s \<Longrightarrow> valid_reply_masters s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_reply_masters s \<Longrightarrow> valid_reply_masters s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sbn_reply_masters [wp]:
  "\<lbrace>valid_reply_masters\<rbrace> set_bound_notification p ntfn \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>" apply (simp add: set_bound_notification_thread_set) apply (wp thread_set_valid_reply_masters_trivial, simp) apply (fastforce simp: tcb_cap_cases_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters\<rbrace> set_bound_notification p ntfn \<lbrace>\<lambda>_. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters\<rbrace> thread_set (tcb_bound_notification_update (\<lambda>_. ntfn)) p \<lbrace>\<lambda>_. valid_reply_masters\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<forall>x\<in>ran tcb_cap_cases. case x of (getF, v) \<Rightarrow> getF (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>) = getF tcb
 2. \<And>s. valid_reply_masters s \<Longrightarrow> valid_reply_masters s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_reply_masters s \<Longrightarrow> valid_reply_masters s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_thread_state_mdb [wp]:
  "\<lbrace>valid_mdb\<rbrace> set_thread_state p st \<lbrace>\<lambda>_. valid_mdb\<rbrace>" apply (simp add: set_thread_state_thread_set) apply (wp thread_set_mdb|simp)+ apply (fastforce simp: tcb_cap_cases_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> set_thread_state p st \<lbrace>\<lambda>_. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> do y <- thread_set (tcb_state_update (\<lambda>_. st)) p;
do_extended_op (set_thread_state_ext p)
od \<lbrace>\<lambda>_. valid_mdb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (t\<lparr>tcb_state := st\<rparr>) = getF t
 2. \<And>s. valid_mdb s \<Longrightarrow> valid_mdb s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_mdb s \<Longrightarrow> valid_mdb s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_bound_notification_mdb [wp]:
  "\<lbrace>valid_mdb\<rbrace> set_bound_notification p ntfn \<lbrace>\<lambda>_. valid_mdb\<rbrace>" apply (simp add: set_bound_notification_thread_set) apply (wp thread_set_mdb) apply (fastforce simp: tcb_cap_cases_def) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> set_bound_notification p ntfn \<lbrace>\<lambda>_. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> thread_set (tcb_bound_notification_update (\<lambda>_. ntfn)) p \<lbrace>\<lambda>_. valid_mdb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (t\<lparr>tcb_bound_notification := ntfn\<rparr>) = getF t
 2. \<And>s. valid_mdb s \<Longrightarrow> valid_mdb s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_mdb s \<Longrightarrow> valid_mdb s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_thread_state_global_refs [wp]:
  "\<lbrace>valid_global_refs\<rbrace> set_thread_state p st \<lbrace>\<lambda>_. valid_global_refs\<rbrace>" apply (simp add: set_thread_state_thread_set) apply (wp thread_set_global_refs_triv|clarsimp simp: tcb_cap_cases_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> set_thread_state p st \<lbrace>\<lambda>_. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> do y <- thread_set (tcb_state_update (\<lambda>_. st)) p;
do_extended_op (set_thread_state_ext p)
od \<lbrace>\<lambda>_. valid_global_refs\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_bound_notification_global_refs [wp]:
  "\<lbrace>valid_global_refs\<rbrace> set_bound_notification p ntfn \<lbrace>\<lambda>_. valid_global_refs\<rbrace>" apply (simp add: set_bound_notification_thread_set) apply (wp thread_set_global_refs_triv|clarsimp simp: tcb_cap_cases_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> set_bound_notification p ntfn \<lbrace>\<lambda>_. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> thread_set (tcb_bound_notification_update (\<lambda>_. ntfn)) p \<lbrace>\<lambda>_. valid_global_refs\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma st_tcb_ex_cap:
  "\<lbrakk> st_tcb_at P t s; if_live_then_nonz_cap s;
      \<And>st. P st \<Longrightarrow> \<not> halted st\<rbrakk>
     \<Longrightarrow> ex_nonz_cap_to t s" unfolding pred_tcb_at_def by (erule (1) if_live_then_nonz_capD, fastforce simp: live_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at P t s; if_live_then_nonz_cap s; \<And>st. P st \<Longrightarrow> \<not> halted st\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (itcb_state (tcb_to_itcb tcb))) t s; if_live_then_nonz_cap s; \<And>st. P st \<Longrightarrow> \<not> halted st\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s
theory TcbAcc_AI

lemma bound_tcb_ex_cap:
  "\<lbrakk> bound_tcb_at P t s; if_live_then_nonz_cap s;
      \<And>ntfn. P ntfn \<Longrightarrow> bound ntfn \<rbrakk>
     \<Longrightarrow> ex_nonz_cap_to t s" unfolding pred_tcb_at_def by (erule (1) if_live_then_nonz_capD, fastforce simp: live_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bound_tcb_at P t s; if_live_then_nonz_cap s; \<And>ntfn. P ntfn \<Longrightarrow> ntfn \<noteq> None\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (itcb_bound_notification (tcb_to_itcb tcb))) t s; if_live_then_nonz_cap s; \<And>ntfn. P ntfn \<Longrightarrow> ntfn \<noteq> None\<rbrakk> \<Longrightarrow> ex_nonz_cap_to t s
theory TcbAcc_AI

lemma st_tcb_reply_cap_valid:
  "\<And>P t (s::'state_ext state).
    \<not> P (Structures_A.Inactive) \<and> \<not> P (Structures_A.IdleThreadState) \<Longrightarrow>
    \<forall>cap. (st_tcb_at P t s \<and> tcb_cap_valid cap (t, tcb_cnode_index 2) s) \<longrightarrow>
            is_master_reply_cap cap \<and> obj_ref_of cap = t" by (clarsimp simp: tcb_cap_valid_def st_tcb_at_tcb_at st_tcb_def2
                  split: Structures_A.thread_state.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P t s. \<not> P Inactive \<and> \<not> P IdleThreadState \<Longrightarrow> \<forall>cap. st_tcb_at P t s \<and> tcb_cap_valid cap (t, tcb_cnode_index 2) s \<longrightarrow> is_master_reply_cap cap \<and> obj_ref_of cap = t
theory TcbAcc_AI

lemma st_tcb_caller_cap_null:
  "\<And>ep data t (s::'state_ext state).
    \<forall>cap. (st_tcb_at (\<lambda>st. st = Structures_A.BlockedOnReceive ep data) t s \<and>
            tcb_cap_valid cap (t, tcb_cnode_index 3) s) \<longrightarrow>
            cap = cap.NullCap" by (clarsimp simp: tcb_cap_valid_def st_tcb_at_tcb_at st_tcb_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ep data t s. \<forall>cap. st_tcb_at (\<lambda>st. st = BlockedOnReceive ep data) t s \<and> tcb_cap_valid cap (t, tcb_cnode_index 3) s \<longrightarrow> cap = NullCap
theory TcbAcc_AI

lemma dom_tcb_cap_cases:
  "tcb_cnode_index 0 \<in> dom tcb_cap_cases"
  "tcb_cnode_index 1 \<in> dom tcb_cap_cases"
  "tcb_cnode_index 2 \<in> dom tcb_cap_cases"
  "tcb_cnode_index 3 \<in> dom tcb_cap_cases"
  "tcb_cnode_index 4 \<in> dom tcb_cap_cases" by clarsimp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (tcb_cnode_index 0 \<in> dom tcb_cap_cases &&& tcb_cnode_index 1 \<in> dom tcb_cap_cases) &&& tcb_cnode_index 2 \<in> dom tcb_cap_cases &&& tcb_cnode_index 3 \<in> dom tcb_cap_cases &&& tcb_cnode_index 4 \<in> dom tcb_cap_cases
theory TcbAcc_AI

lemma sts_obj_at_impossible:
  "(\<And>tcb. \<not> P (TCB tcb)) \<Longrightarrow> \<lbrace>obj_at P p\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. obj_at P p\<rbrace>" unfolding set_thread_state_thread_set by (wp, simp, wp thread_set_obj_at_impossible)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. \<not> P (TCB tcb)) \<Longrightarrow> \<lbrace>obj_at P p\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. obj_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. \<not> P (TCB tcb)) \<Longrightarrow> \<lbrace>obj_at P p\<rbrace> do thread_set (tcb_state_update (\<lambda>_. st)) t;
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>rv. obj_at P p\<rbrace>
theory TcbAcc_AI

lemma sbn_obj_at_impossible:
  "(\<And>tcb. \<not> P (TCB tcb)) \<Longrightarrow> \<lbrace>obj_at P p\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. obj_at P p\<rbrace>" unfolding set_bound_notification_thread_set by (wp thread_set_obj_at_impossible, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. \<not> P (TCB tcb)) \<Longrightarrow> \<lbrace>obj_at P p\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. obj_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. \<not> P (TCB tcb)) \<Longrightarrow> \<lbrace>obj_at P p\<rbrace> thread_set (tcb_bound_notification_update (\<lambda>_. ntfn)) t \<lbrace>\<lambda>rv. obj_at P p\<rbrace>
theory TcbAcc_AI

lemma sts_only_idle:
  "\<lbrace>only_idle and (\<lambda>s. idle st \<longrightarrow> t = idle_thread s)\<rbrace>
  set_thread_state t st \<lbrace>\<lambda>_. only_idle\<rbrace>" apply (simp add: set_thread_state_def set_object_def get_object_def) apply (wp|simp)+ apply (clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle and (\<lambda>s. idle st \<longrightarrow> t = idle_thread s)\<rbrace> set_thread_state t st \<lbrace>\<lambda>_. only_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle and (\<lambda>s. idle st \<longrightarrow> t = idle_thread 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>_. only_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. only_idle s \<and> (idle st \<longrightarrow> t = idle_thread s) \<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> only_idle (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sbn_only_idle[wp]:
  "\<lbrace>only_idle\<rbrace>
  set_bound_notification t ntfn \<lbrace>\<lambda>_. only_idle\<rbrace>" apply (simp add: set_bound_notification_def set_object_def get_object_def) apply (wp, simp) apply (clarsimp simp: only_idle_def pred_tcb_at_def obj_at_def get_tcb_def
                  split:option.splits kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. only_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle\<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 (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)
od \<lbrace>\<lambda>_. only_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. only_idle s \<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> only_idle (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_thread_state_pspace_in_kernel_window[wp]:
  "\<lbrace>pspace_in_kernel_window\<rbrace>
      set_thread_state p st \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>" by (simp add: set_thread_state_thread_set, wp, simp, wp)

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

lemma set_thread_state_cap_refs_in_kernel_window[wp]:
  "\<lbrace>cap_refs_in_kernel_window\<rbrace>
      set_thread_state p st \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" by (simp add: set_thread_state_thread_set
           | wp thread_set_cap_refs_in_kernel_window
                ball_tcb_cap_casesI)+

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

lemma set_thread_state_cap_refs_respects_device_regionw[wp]:
  "\<lbrace>cap_refs_respects_device_region\<rbrace>
      set_thread_state p st \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" by (simp add: set_thread_state_thread_set
           | wp thread_set_cap_refs_respects_device_region
                ball_tcb_cap_casesI)+

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

lemma set_bound_notification_pspace_in_kernel_window[wp]:
  "\<lbrace>pspace_in_kernel_window\<rbrace>
      set_bound_notification p ntfn \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>" by (simp add: set_bound_notification_thread_set, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> set_bound_notification p ntfn \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>
theory TcbAcc_AI

lemma set_bound_notification_cap_refs_in_kernel_window[wp]:
  "\<lbrace>cap_refs_in_kernel_window\<rbrace>
      set_bound_notification p ntfn \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" by (simp add: set_bound_notification_thread_set
           | wp thread_set_cap_refs_in_kernel_window
                ball_tcb_cap_casesI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window\<rbrace> set_bound_notification p ntfn \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>
theory TcbAcc_AI

lemma set_bound_notification_cap_refs_respects_device_region[wp]:
  "\<lbrace>cap_refs_respects_device_region\<rbrace>
      set_bound_notification p ntfn \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" by (simp add: set_bound_notification_thread_set
           | wp thread_set_cap_refs_respects_device_region
                ball_tcb_cap_casesI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region\<rbrace> set_bound_notification p ntfn \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>
theory TcbAcc_AI

lemma set_thread_state_valid_ioc[wp]:
  "\<lbrace>valid_ioc\<rbrace> set_thread_state t st \<lbrace>\<lambda>_. valid_ioc\<rbrace>" apply (simp add: set_thread_state_def) apply (wp, simp, (wp set_object_valid_ioc_caps)+) apply (intro impI conjI, clarsimp+) apply (clarsimp simp: valid_ioc_def) apply (drule spec, drule spec, erule impE, assumption) apply (clarsimp simp: get_tcb_def cap_of_def tcb_cnode_map_tcb_cap_cases
                        null_filter_def cte_wp_at_cases tcb_cap_cases_def
                 split: option.splits Structures_A.kernel_object.splits
                        if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> set_thread_state t st \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> do tcb <- gets_the (get_tcb t);
y <- set_object t (TCB (tcb\<lparr>tcb_state := st\<rparr>));
do_extended_op (set_thread_state_ext t)
od \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ioc s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> valid_ioc s \<and> typ_at (a_type (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>))) t s \<and> (\<forall>b. is_original_cap s (t, b) \<longrightarrow> null_filter (cap_of (TCB (the (get_tcb t s)\<lparr>tcb_state := st\<rparr>))) b \<noteq> None) proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>valid_ioc s; get_tcb t s = Some y; is_original_cap s (t, b)\<rbrakk> \<Longrightarrow> \<exists>ya. null_filter (cap_of (TCB (y\<lparr>tcb_state := st\<rparr>))) b = Some ya proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>\<forall>a b. is_original_cap s (a, b) \<longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s; get_tcb t s = Some y; is_original_cap s (t, b)\<rbrakk> \<Longrightarrow> \<exists>ya. null_filter (cap_of (TCB (y\<lparr>tcb_state := st\<rparr>))) b = Some ya proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>get_tcb t s = Some y; is_original_cap s (t, b); cte_wp_at (\<lambda>x. x \<noteq> NullCap) (t, b) s\<rbrakk> \<Longrightarrow> \<exists>ya. null_filter (cap_of (TCB (y\<lparr>tcb_state := st\<rparr>))) b = Some ya proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_bound_notification_valid_ioc[wp]:
  "\<lbrace>valid_ioc\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_ioc\<rbrace>" apply (simp add: set_bound_notification_def) apply (wp set_object_valid_ioc_caps, simp) apply (intro impI conjI, clarsimp+) apply (clarsimp simp: valid_ioc_def) apply (drule spec, drule spec, erule impE, assumption) apply (clarsimp simp: get_tcb_def cap_of_def tcb_cnode_map_tcb_cap_cases
                        null_filter_def cte_wp_at_cases tcb_cap_cases_def
                 split: option.splits Structures_A.kernel_object.splits
                        if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ioc s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> typ_at ATCB t s \<and> (\<forall>b. is_original_cap s (t, b) \<longrightarrow> (\<exists>y. null_filter (cap_of (TCB (the (get_tcb t s)\<lparr>tcb_bound_notification := ntfn\<rparr>))) b = Some y)) proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>valid_ioc s; get_tcb t s = Some y; is_original_cap s (t, b)\<rbrakk> \<Longrightarrow> \<exists>ya. null_filter (cap_of (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))) b = Some ya proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>\<forall>a b. is_original_cap s (a, b) \<longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s; get_tcb t s = Some y; is_original_cap s (t, b)\<rbrakk> \<Longrightarrow> \<exists>ya. null_filter (cap_of (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))) b = Some ya proof (prove)
goal (1 subgoal):
 1. \<And>s y b. \<lbrakk>get_tcb t s = Some y; is_original_cap s (t, b); cte_wp_at (\<lambda>x. x \<noteq> NullCap) (t, b) s\<rbrakk> \<Longrightarrow> \<exists>ya. null_filter (cap_of (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))) b = Some ya proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_set_valid_cap:
  shows "\<lbrace>valid_cap c\<rbrace> thread_set t p \<lbrace>\<lambda>rv. valid_cap c\<rbrace>" by (wp valid_cap_typ)

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

lemma thread_set_cte_at:
  shows "\<lbrace>cte_at c\<rbrace> thread_set t p \<lbrace>\<lambda>rv. cte_at c\<rbrace>" by (wp valid_cte_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) c\<rbrace> thread_set t p \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) c\<rbrace>