theory Ipc_DR

lemma tcb_fault_handler_length:
  "\<lbrakk>valid_state s;ko_at (TCB tcb) thread s\<rbrakk>
           \<Longrightarrow> length (tcb_fault_handler tcb) = word_bits" apply (clarsimp simp:valid_state_def valid_pspace_def) apply (drule valid_tcb_objs) apply (simp add:obj_at_def,erule get_tcb_rev) apply (simp add:valid_tcb_def word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s; ko_at (TCB tcb) thread s\<rbrakk> \<Longrightarrow> length (tcb_fault_handler tcb) = word_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (TCB tcb) 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_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\<rbrakk> \<Longrightarrow> length (tcb_fault_handler tcb) = word_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko_at (TCB tcb) thread 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_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\<rbrakk> \<Longrightarrow> get_tcb ?thread30 s = Some ?y30
 2. \<lbrakk>ko_at (TCB tcb) thread 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_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; valid_tcb ?thread30 ?y30 s\<rbrakk> \<Longrightarrow> length (tcb_fault_handler tcb) = word_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (TCB tcb) thread 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_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; valid_tcb thread tcb s\<rbrakk> \<Longrightarrow> length (tcb_fault_handler tcb) = word_bits proof (prove)
goal:
No subgoals!