kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_AI

lemma set_thread_state_cte_wp_at [wp]:
  "\<lbrace>cte_wp_at P c\<rbrace> set_thread_state st p' \<lbrace>\<lambda>rv. cte_wp_at P c\<rbrace>" apply (simp add: set_thread_state_def set_object_def get_object_def) apply (wp|simp)+ apply (clarsimp cong: if_cong) apply (drule get_tcb_SomeD) apply (auto simp: cte_wp_at_cases tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P c\<rbrace> set_thread_state st p' \<lbrace>\<lambda>rv. cte_wp_at P c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at P c\<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. cte_wp_at P c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at P c s \<Longrightarrow> (\<exists>y. get_tcb st s = Some y) \<longrightarrow> (\<exists>y. kheap s st = Some y) \<longrightarrow> a_type (the (kheap s st)) = ATCB \<longrightarrow> cte_wp_at P c (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 (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>cte_wp_at P c s; get_tcb st s = Some y; kheap s st = Some (TCB tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P c (s\<lparr>kheap := \<lambda>a. if a = st then Some (TCB (y\<lparr>tcb_state := p'\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>cte_wp_at P c s; kheap s st = Some (TCB tcb); kheap s st = Some (TCB y)\<rbrakk> \<Longrightarrow> cte_wp_at P c (s\<lparr>kheap := \<lambda>a. if a = st then Some (TCB (y\<lparr>tcb_state := p'\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma set_object_tcb_at [wp]:
  "\<lbrace> tcb_at t' \<rbrace> set_object t (TCB x) \<lbrace>\<lambda>_. tcb_at t'\<rbrace>" by (rule set_object_at_obj1) (simp add: is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t'\<rbrace> set_object t (TCB x) \<lbrace>\<lambda>_. tcb_at t'\<rbrace>
theory TcbAcc_AI

lemma as_user_tcb [wp]: "\<lbrace>tcb_at t'\<rbrace> as_user t m \<lbrace>\<lambda>rv. tcb_at t'\<rbrace>" apply (simp add: as_user_def split_def) apply wp apply simp done

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

lemma load_word_offs_P[wp]:
  "\<lbrace>P\<rbrace> load_word_offs a x \<lbrace>\<lambda>_. P\<rbrace>" unfolding load_word_offs_def by (wp dmo_inv loadWord_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> load_word_offs a x \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do_machine_op $ loadWord (a + word_of_nat (x * word_size)) \<lbrace>\<lambda>_. P\<rbrace>
theory TcbAcc_AI

lemma valid_tcb_objs:
  assumes vs: "valid_objs s"
  assumes somet: "get_tcb thread s = Some y"
  shows "valid_tcb thread y s" proof - from somet have inran: "kheap s thread = Some (TCB y)" by (clarsimp simp: get_tcb_def
                split: option.splits Structures_A.kernel_object.splits) with vs have "valid_obj thread (TCB y) s" by (fastforce simp: valid_objs_def dom_def) thus ?thesis by (simp add: valid_tcb_def valid_obj_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb thread y s proof (state)
goal (1 subgoal):
 1. valid_tcb thread y s proof (chain)
picking this:
get_tcb thread s = Some y proof (prove)
using this:
get_tcb thread s = Some y

goal (1 subgoal):
 1. kheap s thread = Some (TCB y) proof (state)
this:
kheap s thread = Some (TCB y)

goal (1 subgoal):
 1. valid_tcb thread y s proof (chain)
picking this:
valid_objs s
kheap s thread = Some (TCB y) proof (prove)
using this:
valid_objs s
kheap s thread = Some (TCB y)

goal (1 subgoal):
 1. valid_obj thread (TCB y) s proof (state)
this:
valid_obj thread (TCB y) s

goal (1 subgoal):
 1. valid_tcb thread y s proof (prove)
using this:
valid_obj thread (TCB y) s

goal (1 subgoal):
 1. valid_tcb thread y s proof (state)
this:
valid_tcb thread y s

goal:
No subgoals!
theory TcbAcc_AI

lemma get_cap_aligned:
  "\<lbrace>valid_objs\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. cap_aligned rv\<rbrace>" apply (rule hoare_strengthen_post, rule get_cap_valid) apply (clarsimp simp: valid_cap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. cap_aligned rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. s \<turnstile> rv \<Longrightarrow> cap_aligned rv proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_get_wp:
  "\<lbrace>\<lambda>s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (f tcb) s) ptr s\<rbrace>
    thread_get f ptr
   \<lbrace>P\<rbrace>" apply (clarsimp simp: valid_def obj_at_def) apply (frule in_inv_by_hoareD [OF thread_get_inv]) apply (clarsimp simp: thread_get_def bind_def gets_the_def
                        assert_opt_def split_def return_def fail_def
                        gets_def get_def
                 split: option.splits
                 dest!: get_tcb_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (f tcb) s) ptr s\<rbrace> thread_get f ptr \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb. \<lbrakk>(a, b) \<in> fst (thread_get f ptr s); kheap s ptr = Some (TCB tcb); P (f tcb) s\<rbrakk> \<Longrightarrow> P a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b tcb. \<lbrakk>(a, b) \<in> fst (thread_get f ptr s); kheap s ptr = Some (TCB tcb); P (f tcb) s; b = s\<rbrakk> \<Longrightarrow> P a b proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma thread_get_sp:
  "\<lbrace>P\<rbrace> thread_get f ptr
   \<lbrace>\<lambda>rv. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> f tcb = rv) ptr and P\<rbrace>" apply (clarsimp simp: valid_def obj_at_def) apply (frule in_inv_by_hoareD [OF thread_get_inv]) apply (clarsimp simp: thread_get_def bind_def gets_the_def
                        assert_opt_def split_def return_def fail_def
                        gets_def get_def
                 split: option.splits
                 dest!: get_tcb_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> thread_get f ptr \<lbrace>\<lambda>rv. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> f tcb = rv) ptr and P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (thread_get f ptr s)\<rbrakk> \<Longrightarrow> (\<exists>ko. kheap b ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> f tcb = a)) \<and> P b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (thread_get f ptr s); b = s\<rbrakk> \<Longrightarrow> (\<exists>ko. kheap b ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> f tcb = a)) \<and> P b proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma gbn_wp:
  "\<lbrace>\<lambda>s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (tcb_bound_notification tcb) s) ptr s \<rbrace>
     get_bound_notification ptr
   \<lbrace>P\<rbrace>" apply (simp add: get_bound_notification_def) apply (wp thread_get_wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (tcb_bound_notification tcb) s) ptr s\<rbrace> get_bound_notification ptr \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> P (tcb_bound_notification tcb) s) ptr s\<rbrace> thread_get tcb_bound_notification ptr \<lbrace>P\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma wf_cs_0:
  "well_formed_cnode_n sz cn \<Longrightarrow> \<exists>n. n \<in> dom cn \<and> bl_to_bin n = 0" unfolding well_formed_cnode_n_def apply clarsimp apply (rule_tac x = "replicate sz False" in exI) apply (simp add: bl_to_bin_rep_False) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n sz cn \<Longrightarrow> \<exists>n. n \<in> dom cn \<and> bl_to_bin n = 0 proof (prove)
goal (1 subgoal):
 1. dom cn = {x. length x = sz} \<Longrightarrow> \<exists>n. n \<in> dom cn \<and> bl_to_bin n = 0 proof (prove)
goal (1 subgoal):
 1. dom cn = {x. length x = sz} \<Longrightarrow> \<exists>n. length n = sz \<and> bl_to_bin n = 0 proof (prove)
goal (1 subgoal):
 1. dom cn = {x. length x = sz} \<Longrightarrow> length (replicate sz False) = sz \<and> bl_to_bin (replicate sz False) = 0 proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma ct_active_st_tcb_at_weaken:
  "\<lbrakk> st_tcb_at P (cur_thread s) s;
     \<And>st. P st \<Longrightarrow> active st\<rbrakk>
  \<Longrightarrow> ct_active s" apply (unfold ct_in_state_def) apply (erule pred_tcb_weakenE) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at P (cur_thread s) s; \<And>st. P st \<Longrightarrow> active st\<rbrakk> \<Longrightarrow> ct_active s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at P (cur_thread s) s; \<And>st. P st \<Longrightarrow> active st\<rbrakk> \<Longrightarrow> st_tcb_at active (cur_thread s) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>\<And>st. P st \<Longrightarrow> active st; P (itcb_state tcb)\<rbrakk> \<Longrightarrow> active (itcb_state tcb) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma ct_in_state_decomp:
  assumes x: "\<lbrace>\<lambda>s. t = (cur_thread s)\<rbrace> f \<lbrace>\<lambda>rv s. t = (cur_thread s)\<rbrace>"
  assumes y: "\<lbrace>Pre\<rbrace> f \<lbrace>\<lambda>rv. st_tcb_at Prop t\<rbrace>"
  shows      "\<lbrace>\<lambda>s. Pre s \<and> t = (cur_thread s)\<rbrace> f \<lbrace>\<lambda>rv. ct_in_state Prop\<rbrace>" apply (rule hoare_post_imp [where Q="\<lambda>rv s. t = cur_thread s \<and> st_tcb_at Prop t s"]) apply (clarsimp simp add: ct_in_state_def) apply (rule hoare_vcg_precond_imp) apply (wp x y) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Pre s \<and> t = cur_thread s\<rbrace> f \<lbrace>\<lambda>rv. ct_in_state Prop\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. t = cur_thread s \<and> st_tcb_at Prop t s \<Longrightarrow> ct_in_state Prop s
 2. \<lbrace>\<lambda>s. Pre s \<and> t = cur_thread s\<rbrace> f \<lbrace>\<lambda>rv s. t = cur_thread s \<and> st_tcb_at Prop t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Pre s \<and> t = cur_thread s\<rbrace> f \<lbrace>\<lambda>rv s. t = cur_thread s \<and> st_tcb_at Prop t s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q9\<rbrace> f \<lbrace>\<lambda>rv s. t = cur_thread s \<and> st_tcb_at Prop t s\<rbrace>
 2. \<And>s. Pre s \<and> t = cur_thread s \<Longrightarrow> ?Q9 s proof (prove)
goal (1 subgoal):
 1. \<And>s. Pre s \<and> t = cur_thread s \<Longrightarrow> t = cur_thread s \<and> Pre s proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sts_st_tcb_at:
  "\<lbrace>\<top>\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>r. r = ts) t\<rbrace>" by (simp add: set_thread_state_def pred_tcb_at_def | wp set_object_at_obj3)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>r. r = ts) t\<rbrace>
theory TcbAcc_AI

lemma sbn_bound_tcb_at:
  "\<lbrace>\<top>\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. bound_tcb_at (\<lambda>r. r = ntfn) t\<rbrace>" by (simp add: set_bound_notification_def pred_tcb_at_def | wp set_object_at_obj3)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. bound_tcb_at (\<lambda>r. r = ntfn) t\<rbrace>
theory TcbAcc_AI

lemma sts_st_tcb_at':
  "\<lbrace>K (P ts)\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" apply (rule hoare_assume_pre) apply (rule hoare_chain) apply (rule sts_st_tcb_at) apply simp apply (clarsimp elim!: pred_tcb_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (P ts)\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. K (P ts) s \<Longrightarrow> \<lbrace>K (P ts)\<rbrace> set_thread_state t ts \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. K (P ts) s \<Longrightarrow> \<lbrace>?P2 s\<rbrace> set_thread_state t ts \<lbrace>?Q2 s\<rbrace>
 2. \<And>s sa. \<lbrakk>K (P ts) s; K (P ts) sa\<rbrakk> \<Longrightarrow> ?P2 s sa
 3. \<And>s rv sa. \<lbrakk>K (P ts) s; ?Q2 s rv sa\<rbrakk> \<Longrightarrow> st_tcb_at P t sa proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>K (P ts) s; K (P ts) sa\<rbrakk> \<Longrightarrow> True
 2. \<And>s rv sa. \<lbrakk>K (P ts) s; st_tcb_at (\<lambda>r. r = ts) t sa\<rbrakk> \<Longrightarrow> st_tcb_at P t sa proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>K (P ts) s; st_tcb_at (\<lambda>r. r = ts) t sa\<rbrakk> \<Longrightarrow> st_tcb_at P t sa proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sbn_bound_tcb_at':
  "\<lbrace>K (P ntfn)\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. bound_tcb_at P t\<rbrace>" apply (rule hoare_assume_pre) apply (rule hoare_chain) apply (rule sbn_bound_tcb_at) apply simp apply (clarsimp elim!: pred_tcb_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (P ntfn)\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. bound_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. K (P ntfn) s \<Longrightarrow> \<lbrace>K (P ntfn)\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>rv. bound_tcb_at P t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. K (P ntfn) s \<Longrightarrow> \<lbrace>?P2 s\<rbrace> set_bound_notification t ntfn \<lbrace>?Q2 s\<rbrace>
 2. \<And>s sa. \<lbrakk>K (P ntfn) s; K (P ntfn) sa\<rbrakk> \<Longrightarrow> ?P2 s sa
 3. \<And>s rv sa. \<lbrakk>K (P ntfn) s; ?Q2 s rv sa\<rbrakk> \<Longrightarrow> bound_tcb_at P t sa proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>K (P ntfn) s; K (P ntfn) sa\<rbrakk> \<Longrightarrow> True
 2. \<And>s rv sa. \<lbrakk>K (P ntfn) s; bound_tcb_at (\<lambda>r. r = ntfn) t sa\<rbrakk> \<Longrightarrow> bound_tcb_at P t sa proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>K (P ntfn) s; bound_tcb_at (\<lambda>r. r = ntfn) t sa\<rbrakk> \<Longrightarrow> bound_tcb_at P t sa proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sts_valid_idle [wp]:
  "\<lbrace>valid_idle and
     (\<lambda>s. t = idle_thread s \<longrightarrow> idle ts)\<rbrace>
   set_thread_state t ts
   \<lbrace>\<lambda>_. valid_idle\<rbrace>" apply (simp add: set_thread_state_def set_object_def get_object_def) apply (wp|simp)+ apply (clarsimp cong: if_cong) apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def get_tcb_def) done

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

lemma sbn_valid_idle [wp]:
  "\<lbrace>valid_idle and
     (\<lambda>s. t = idle_thread s \<longrightarrow> \<not> bound ntfn)\<rbrace>
   set_bound_notification t ntfn
   \<lbrace>\<lambda>_. valid_idle\<rbrace>" apply (simp add: set_bound_notification_def set_object_def get_object_def) apply (wp, simp) apply (clarsimp cong: if_cong) apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and (\<lambda>s. t = idle_thread s \<longrightarrow> \<not> ntfn \<noteq> None)\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and (\<lambda>s. t = idle_thread s \<longrightarrow> ntfn = None)\<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>_. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_idle s \<and> (t = idle_thread s \<longrightarrow> ntfn = None) \<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> valid_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 (1 subgoal):
 1. \<And>s y tcb. \<lbrakk>valid_idle s; t = idle_thread s \<longrightarrow> ntfn = None; get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> valid_idle (s\<lparr>kheap := \<lambda>a. if a = t then Some (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sts_distinct [wp]:
  "set_thread_state t st \<lbrace>pspace_distinct\<rbrace>" apply (simp add: set_thread_state_def) apply (wp set_object_distinct|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct\<rbrace> set_thread_state t st \<lbrace>\<lambda>_. pspace_distinct\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct\<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>_. pspace_distinct\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sbn_distinct [wp]:
  "set_bound_notification t ntfn \<lbrace>pspace_distinct\<rbrace>" apply (simp add: set_bound_notification_def) apply (wp set_object_distinct, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. pspace_distinct\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_distinct\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>_. pspace_distinct\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sts_cur_tcb [wp]:
  "set_thread_state t st \<lbrace>\<lambda>s. cur_tcb s\<rbrace>" apply (clarsimp simp: set_thread_state_def set_object_def get_object_def
                        gets_the_def valid_def in_monad) apply (drule get_tcb_SomeD) apply (frule in_dxo_pspaceD) apply (drule in_dxo_cur_threadD) apply (clarsimp simp: cur_tcb_def obj_at_def is_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb\<rbrace> set_thread_state t st \<lbrace>\<lambda>_. cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b tcb tcba. \<lbrakk>cur_tcb s; get_tcb t s = Some tcb; kheap s t = Some (TCB tcba); ((), b) \<in> fst (do_extended_op (set_thread_state_ext t) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := st\<rparr>))\<rparr>))\<rbrakk> \<Longrightarrow> cur_tcb b proof (prove)
goal (1 subgoal):
 1. \<And>s b tcb tcba. \<lbrakk>cur_tcb s; kheap s t = Some (TCB tcba); ((), b) \<in> fst (do_extended_op (set_thread_state_ext t) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := st\<rparr>))\<rparr>)); kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> cur_tcb b proof (prove)
goal (1 subgoal):
 1. \<And>s b tcb tcba. \<lbrakk>cur_tcb s; kheap s t = Some (TCB tcba); ((), b) \<in> fst (do_extended_op (set_thread_state_ext t) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := st\<rparr>))\<rparr>)); kheap s t = Some (TCB tcb); kheap b = kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := st\<rparr>))\<rparr>)\<rbrakk> \<Longrightarrow> cur_tcb b proof (prove)
goal (1 subgoal):
 1. \<And>s b tcb tcba. \<lbrakk>cur_tcb s; kheap s t = Some (TCB tcba); kheap s t = Some (TCB tcb); kheap b = kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := st\<rparr>))\<rparr>); cur_thread b = cur_thread (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := st\<rparr>))\<rparr>)\<rbrakk> \<Longrightarrow> cur_tcb b proof (prove)
goal:
No subgoals!
theory TcbAcc_AI

lemma sbn_cur_tcb [wp]:
  "set_bound_notification t ntfn \<lbrace>\<lambda>s. cur_tcb s\<rbrace>" apply (clarsimp simp: set_bound_notification_def set_object_def get_object_def
                        gets_the_def valid_def in_monad) apply (drule get_tcb_SomeD) apply (clarsimp simp: cur_tcb_def obj_at_def is_tcb_def) done

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