theory TcbAcc_AI

lemma sbn_invs_minor:
  "\<lbrace>bound_tcb_at (\<lambda>ntfn'. tcb_bound_refs ntfn' = tcb_bound_refs ntfn) t
    and (\<lambda>s. bound ntfn \<longrightarrow> ex_nonz_cap_to t s)
    and (\<lambda>s. t \<noteq> idle_thread s)
    and invs \<rbrace>
    set_bound_notification t ntfn
   \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: invs_def valid_state_def valid_pspace_def) apply (rule hoare_pre) apply (wp valid_irq_node_typ sbn_only_idle | simp)+ apply clarsimp apply (rule conjI) apply (simp add: pred_tcb_at_def, erule(1) obj_at_valid_objsE) subgoal by (clarsimp simp: valid_obj_def valid_tcb_def valid_bound_ntfn_def
                       split: Structures_A.thread_state.splits option.splits) apply (clarsimp elim!: rsubst[where P=sym_refs]
                 intro!: ext
                  dest!: bound_tcb_at_state_refs_ofD) apply (fastforce simp: tcb_ntfn_is_bound_def tcb_bound_refs_def tcb_st_refs_of_def
                   elim: obj_at_valid_objsE
                  split: option.splits thread_state.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at (\<lambda>ntfn'. tcb_bound_refs ntfn' = tcb_bound_refs ntfn) t and (\<lambda>s. ntfn \<noteq> None \<longrightarrow> ex_nonz_cap_to t s) and (\<lambda>s. t \<noteq> idle_thread s) and invs\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at (\<lambda>ntfn'. tcb_bound_refs ntfn' = tcb_bound_refs ntfn) t and (\<lambda>s. (\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s) and (\<lambda>s. t \<noteq> idle_thread s) and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb)\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace>
 2. \<And>s. (bound_tcb_at (\<lambda>ntfn'. tcb_bound_refs ntfn' = tcb_bound_refs ntfn) t and (\<lambda>s. (\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s) and (\<lambda>s. t \<noteq> idle_thread s) and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb)) s \<Longrightarrow> ?Q3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. bound_tcb_at (\<lambda>ntfn'. tcb_bound_refs ntfn' = tcb_bound_refs ntfn) t s \<and> ((\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s) \<and> t \<noteq> idle_thread s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<Longrightarrow> valid_bound_ntfn ntfn s \<and> sym_refs (\<lambda>a. if a = t then tcb_bound_refs ntfn \<union> {r \<in> state_refs_of s t. snd r \<noteq> TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>bound_tcb_at (\<lambda>ntfn'. tcb_bound_refs ntfn' = tcb_bound_refs ntfn) t s; (\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s; t \<noteq> idle_thread s; valid_objs 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\<rbrakk> \<Longrightarrow> valid_bound_ntfn ntfn s \<and> sym_refs (\<lambda>a. if a = t then tcb_bound_refs ntfn \<union> {r \<in> state_refs_of s t. snd r \<noteq> TCBBound} else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>bound_tcb_at (\<lambda>ntfn'. tcb_bound_refs ntfn' = tcb_bound_refs ntfn) t s; (\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s; t \<noteq> idle_thread s; valid_objs 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\<rbrakk> \<Longrightarrow> valid_bound_ntfn ntfn s
 2. \<And>s. \<lbrakk>bound_tcb_at (\<lambda>ntfn'. tcb_bound_refs ntfn' = tcb_bound_refs ntfn) t s; (\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s; t \<noteq> idle_thread s; valid_objs 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\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_bound_refs ntfn \<union> {r \<in> state_refs_of s t. snd r \<noteq> TCBBound} else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>(\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s; t \<noteq> idle_thread s; valid_objs 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 ko; \<exists>tcb. ko = TCB tcb \<and> tcb_bound_refs (tcb_bound_notification tcb) = tcb_bound_refs ntfn; valid_obj t ko s\<rbrakk> \<Longrightarrow> valid_bound_ntfn ntfn s
 2. \<And>s. \<lbrakk>bound_tcb_at (\<lambda>ntfn'. tcb_bound_refs ntfn' = tcb_bound_refs ntfn) t s; (\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s; t \<noteq> idle_thread s; valid_objs 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\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_bound_refs ntfn \<union> {r \<in> state_refs_of s t. snd r \<noteq> TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s_; t \<noteq> idle_thread s_; valid_objs 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 ko_; \<exists>tcb. ko_ = TCB tcb \<and> tcb_bound_refs (tcb_bound_notification tcb) = tcb_bound_refs ntfn; valid_obj t ko_ s_\<rbrakk> \<Longrightarrow> valid_bound_ntfn ntfn s_ proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>bound_tcb_at (\<lambda>ntfn'. tcb_bound_refs ntfn' = tcb_bound_refs ntfn) t s; (\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s; t \<noteq> idle_thread s; valid_objs 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\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_bound_refs ntfn \<union> {r \<in> state_refs_of s t. snd r \<noteq> TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>s ts ntfnptr. \<lbrakk>(\<exists>y. ntfn = Some y) \<longrightarrow> ex_nonz_cap_to t s; t \<noteq> idle_thread s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_bound_refs ntfnptr = tcb_bound_refs ntfn; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfn\<rbrakk> \<Longrightarrow> tcb_st_refs_of ts \<union> tcb_bound_refs ntfn = tcb_bound_refs ntfn \<union> {r. (r \<in> tcb_st_refs_of ts \<or> r \<in> tcb_bound_refs ntfn) \<and> snd r \<noteq> TCBBound} proof (prove)
goal:
No subgoals!