theory IpcCancel_R

lemma rescheduleRequired_all_invs_but_ct_not_inQ:
  "\<lbrace>all_invs_but_ct_not_inQ'\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. invs'\<rbrace>" apply (simp add: invs'_def valid_state'_def) apply (rule hoare_pre) apply (wp rescheduleRequired_ct_not_inQ
             valid_irq_node_lift valid_irq_handlers_lift''
             irqs_masked_lift cur_tcb_lift
             untyped_ranges_zero_lift
             | simp add: cteCaps_of_def o_def)+ apply (auto simp: sch_act_wf_weak) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s) and cur_tcb'\<rbrace>
 2. \<And>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero' s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s) \<Longrightarrow> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> ksDomSchedule (newKernelState undefined) \<noteq> [] proof (prove)
goal:
No subgoals!