theory TcbAcc_AI

lemma set_thread_state_valid_objs[wp]:
 "\<lbrace>valid_objs and valid_tcb_state st and
   (\<lambda>s. (\<forall>a data. st = Structures_A.BlockedOnReceive a data \<longrightarrow>
              cte_wp_at ((=) cap.NullCap) (thread, tcb_cnode_index 3) s) \<and>
        (st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> halted st \<or>
              cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread)
                        (thread, tcb_cnode_index 2) s))\<rbrace>
  set_thread_state thread st
  \<lbrace>\<lambda>r. valid_objs\<rbrace>" apply (simp add: set_thread_state_def) apply (wp, simp, (wp set_object_valid_objs)+) apply (clarsimp simp: obj_at_def get_tcb_def is_tcb
                  split: Structures_A.kernel_object.splits option.splits) apply (simp add: valid_objs_def dom_def) apply (erule allE, erule impE, blast) apply (clarsimp simp: valid_obj_def valid_tcb_def
                        a_type_def tcb_cap_cases_def) 
  (* very slow *)
   by (erule cte_wp_atE disjE
       | clarsimp simp: st_tcb_def2 tcb_cap_cases_def
                 dest!: get_tcb_SomeD
                 split: Structures_A.thread_state.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_tcb_state st and (\<lambda>s. (\<forall>a data. st = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (thread, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s))\<rbrace> set_thread_state thread st \<lbrace>\<lambda>r. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_tcb_state st and (\<lambda>s. ((\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (thread, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s))\<rbrace> do tcb <- gets_the (get_tcb thread);
y <- set_object thread (TCB (tcb\<lparr>tcb_state := st\<rparr>));
do_extended_op (set_thread_state_ext thread)
od \<lbrace>\<lambda>r. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and valid_tcb_state st and (\<lambda>s. ((\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (thread, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s))) s \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> (valid_objs and valid_obj thread (TCB (the (get_tcb thread s)\<lparr>tcb_state := st\<rparr>))) s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_objs s; valid_tcb_state st s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (thread, tcb_cnode_index 3) s; st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s; kheap s thread = Some (TCB x2)\<rbrakk> \<Longrightarrow> valid_obj thread (TCB (x2\<lparr>tcb_state := st\<rparr>)) s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>\<forall>ptr. (\<exists>y. kheap s ptr = Some y) \<longrightarrow> (\<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s); valid_tcb_state st s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (thread, tcb_cnode_index 3) s; st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s; kheap s thread = Some (TCB x2)\<rbrakk> \<Longrightarrow> valid_obj thread (TCB (x2\<lparr>tcb_state := st\<rparr>)) s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_tcb_state st s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (thread, tcb_cnode_index 3) s; st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s; kheap s thread = Some (TCB x2); \<exists>obj. kheap s thread = Some obj \<and> valid_obj thread obj s\<rbrakk> \<Longrightarrow> valid_obj thread (TCB (x2\<lparr>tcb_state := st\<rparr>)) s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_tcb_state st s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (thread, tcb_cnode_index 3) s; st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s; kheap s thread = Some (TCB x2); s \<turnstile> tcb_ipcframe x2; is_nondevice_page_cap (tcb_ipcframe x2) \<or> NullCap = tcb_ipcframe x2; s \<turnstile> tcb_caller x2; (case tcb_state x2 of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller x2); s \<turnstile> tcb_reply x2; is_master_reply_cap (tcb_reply x2) \<and> obj_ref_of (tcb_reply x2) = thread \<and> AllowGrant \<in> cap_rights (tcb_reply x2) \<or> halted (tcb_state x2) \<and> tcb_reply x2 = NullCap; s \<turnstile> tcb_vtable x2; is_valid_vtable_root (tcb_vtable x2) \<or> NullCap = tcb_vtable x2; s \<turnstile> tcb_ctable x2; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> (case st of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller x2) \<and> (is_master_reply_cap (tcb_reply x2) \<and> obj_ref_of (tcb_reply x2) = thread \<and> AllowGrant \<in> cap_rights (tcb_reply x2) \<or> halted st \<and> tcb_reply x2 = NullCap) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>valid_tcb_state st s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (thread, tcb_cnode_index 3) s; st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s; kheap s thread = Some (TCB x2); s \<turnstile> tcb_ipcframe x2; is_nondevice_page_cap (tcb_ipcframe x2) \<or> NullCap = tcb_ipcframe x2; s \<turnstile> tcb_caller x2; (case tcb_state x2 of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller x2); s \<turnstile> tcb_reply x2; is_master_reply_cap (tcb_reply x2) \<and> obj_ref_of (tcb_reply x2) = thread \<and> AllowGrant \<in> cap_rights (tcb_reply x2) \<or> halted (tcb_state x2) \<and> tcb_reply x2 = NullCap; s \<turnstile> tcb_vtable x2; is_valid_vtable_root (tcb_vtable x2) \<or> NullCap = tcb_vtable x2; s \<turnstile> tcb_ctable x2; valid_ipc_buffer_cap (tcb_ipcframe x2) (tcb_ipc_buffer x2); valid_tcb_state (tcb_state x2) s; case tcb_fault x2 of None \<Rightarrow> True | Some x \<Rightarrow> valid_fault x; length (tcb_fault_handler x2) = word_bits; valid_bound_ntfn (tcb_bound_notification x2) s; valid_arch_tcb (tcb_arch x2) s\<rbrakk> \<Longrightarrow> (case st of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) (tcb_caller x2) \<and> (is_master_reply_cap (tcb_reply x2) \<and> obj_ref_of (tcb_reply x2) = thread \<and> AllowGrant \<in> cap_rights (tcb_reply x2) \<or> halted st \<and> tcb_reply x2 = NullCap)