theory IpcCancel_R

lemma tcbSchedDequeue_invs'_no_valid_queues:
   "\<lbrace>\<lambda>s. (\<forall>t' d p.
            (t' \<in> set(ksReadyQueues s (d, p)) \<longrightarrow>
             (obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s
              \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)))
            \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and>
         valid_bitmapQ s \<and>
         bitmapQ_no_L2_orphans s \<and>
         bitmapQ_no_L1_orphans s \<and>
         valid_pspace' s \<and>
         sch_act_wf (ksSchedulerAction s) 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>
         valid_dom_schedule' s \<and>
         untyped_ranges_zero' s \<and>
         cur_tcb' s \<and>
         tcb_at' t s\<rbrace>
    tcbSchedDequeue t
   \<lbrace>\<lambda>_. invs' \<rbrace>" apply (simp add: invs'_def valid_state'_def) apply (wp tcbSchedDequeue_valid_queues_weak valid_irq_handlers_lift
            valid_irq_node_lift valid_irq_handlers_lift'
            tcbSchedDequeue_irq_states irqs_masked_lift cur_tcb_lift
            untyped_ranges_zero_lift
         | clarsimp simp add: cteCaps_of_def valid_queues_def o_def)+ apply (rule conjI) apply (fastforce simp: obj_at'_def inQ_def st_tcb_at'_def valid_queues_no_bitmap_except_def) apply (rule conjI, clarsimp simp: correct_queue_def) apply (fastforce simp: valid_pspace'_def intro: obj_at'_conjI
                   elim: valid_objs'_maxDomain valid_objs'_maxPriority) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s \<and> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) 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> valid_dom_schedule' s \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> tcb_at' t s\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s \<and> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) 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' s \<and> tcb_at' t s\<rbrace> tcbSchedDequeue t \<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 (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb_at' t s\<rbrakk> \<Longrightarrow> valid_queues_no_bitmap_except t s \<and> correct_queue t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority) t s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb_at' t s\<rbrakk> \<Longrightarrow> valid_queues_no_bitmap_except t s
 2. \<And>s. \<lbrakk>\<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb_at' t s\<rbrakk> \<Longrightarrow> correct_queue t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority) t s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb_at' t s\<rbrakk> \<Longrightarrow> correct_queue t s \<and> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority) t s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>t' d p. (t' \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. tcbQueued tcb \<and> tcbDomain tcb = d \<and> tcbPriority tcb = p) t' s \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' runnable' t' s)) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); cur_tcb' s; tcb_at' t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain \<and> tcbPriority tcb \<le> maxPriority) t s proof (prove)
goal:
No subgoals!