theory IpcCancel_C

lemma rf_sr_drop_bitmaps_dequeue_helper:
  "\<lbrakk> (\<sigma>,\<sigma>') \<in> rf_sr ;
     cbitmap_L1_relation ksqL1upd' ksqL1upd ; cbitmap_L2_relation ksqL2upd' ksqL2upd \<rbrakk>
   \<Longrightarrow>
((\<sigma>\<lparr>ksReadyQueues := ksqupd,
   ksReadyQueuesL2Bitmap := ksqL2upd,
   ksReadyQueuesL1Bitmap := ksqL1upd\<rparr>,
 \<sigma>'\<lparr>idx_' := i',
   queue_' := queue_upd',
   globals := globals \<sigma>'
     \<lparr>ksReadyQueuesL2Bitmap_' := ksqL2upd',
      ksReadyQueuesL1Bitmap_' := ksqL1upd',
      ksReadyQueues_' := ksqupd'\<rparr>\<rparr>)
         \<in> rf_sr)
 =
((\<sigma>\<lparr>ksReadyQueues := ksqupd\<rparr>,
 \<sigma>'\<lparr>idx_' := i',
   queue_' := queue_upd',
   globals := globals \<sigma>'
     \<lparr>ksReadyQueues_' := ksqupd'\<rparr>\<rparr>) \<in> rf_sr)
" unfolding rf_sr_def cstate_relation_def Let_def
             carch_state_relation_def cmachine_state_relation_def by (clarsimp simp: rf_sr_cbitmap_L1_relation rf_sr_cbitmap_L2_relation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, \<sigma>') \<in> rf_sr; cbitmap_L1_relation ksqL1upd' ksqL1upd; cbitmap_L2_relation ksqL2upd' ksqL2upd\<rbrakk> \<Longrightarrow> ((\<sigma>\<lparr>ksReadyQueues := ksqupd, ksReadyQueuesL2Bitmap := ksqL2upd, ksReadyQueuesL1Bitmap := ksqL1upd\<rparr>, \<sigma>'\<lparr>idx_' := i', queue_' := queue_upd', globals := globals \<sigma>'\<lparr>ksReadyQueuesL2Bitmap_' := ksqL2upd', ksReadyQueuesL1Bitmap_' := ksqL1upd', ksReadyQueues_' := ksqupd'\<rparr>\<rparr>) \<in> rf_sr) = ((\<sigma>\<lparr>ksReadyQueues := ksqupd\<rparr>, \<sigma>'\<lparr>idx_' := i', queue_' := queue_upd', globals := globals \<sigma>'\<lparr>ksReadyQueues_' := ksqupd'\<rparr>\<rparr>) \<in> rf_sr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, \<sigma>') \<in> {(s, s'). cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')) \<and> cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s) \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s) \<and> cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')) \<and> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')) \<and> (armKSNextASID_' (globals s') = armKSNextASID (ksArchState s) \<and> armKSKernelVSpace (ksArchState s) = armKSKernelVSpace_C \<and> array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')) \<and> array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')) \<and> asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) \<and> carch_globals (ksArchState s)) \<and> (irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')) \<and> irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')) \<and> device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')) \<and> exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')) \<and> machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s'))) \<and> cte_array_relation s (globals s') \<and> tcb_cte_array_relation s (globals s') \<and> apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s) \<and> ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s) \<and> ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s \<and> s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr \<and> ptr_span intStateIRQNode_array_Ptr \<subseteq> kernel_data_refs \<and> s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr \<and> ptr_span armKSGlobalPD_Ptr \<subseteq> kernel_data_refs \<and> htd_safe domain (hrs_htd (t_hrs_' (globals s'))) \<and> - domain \<subseteq> kernel_data_refs \<and> globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s) \<and> ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s) \<and> ksDomainTime_' (globals s') = ksDomainTime s}; cbitmap_L1_relation ksqL1upd' ksqL1upd; cbitmap_L2_relation ksqL2upd' ksqL2upd\<rbrakk> \<Longrightarrow> ((\<sigma>\<lparr>ksReadyQueues := ksqupd, ksReadyQueuesL2Bitmap := ksqL2upd, ksReadyQueuesL1Bitmap := ksqL1upd\<rparr>, \<sigma>'\<lparr>idx_' := i', queue_' := queue_upd', globals := globals \<sigma>'\<lparr>ksReadyQueuesL2Bitmap_' := ksqL2upd', ksReadyQueuesL1Bitmap_' := ksqL1upd', ksReadyQueues_' := ksqupd'\<rparr>\<rparr>) \<in> {(s, s'). cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')) \<and> cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s) \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s) \<and> cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')) \<and> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')) \<and> (armKSNextASID_' (globals s') = armKSNextASID (ksArchState s) \<and> armKSKernelVSpace (ksArchState s) = armKSKernelVSpace_C \<and> array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')) \<and> array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')) \<and> asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) \<and> carch_globals (ksArchState s)) \<and> (irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')) \<and> irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')) \<and> device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')) \<and> exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')) \<and> machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s'))) \<and> cte_array_relation s (globals s') \<and> tcb_cte_array_relation s (globals s') \<and> apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s) \<and> ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s) \<and> ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s \<and> s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr \<and> ptr_span intStateIRQNode_array_Ptr \<subseteq> kernel_data_refs \<and> s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr \<and> ptr_span armKSGlobalPD_Ptr \<subseteq> kernel_data_refs \<and> htd_safe domain (hrs_htd (t_hrs_' (globals s'))) \<and> - domain \<subseteq> kernel_data_refs \<and> globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s) \<and> ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s) \<and> ksDomainTime_' (globals s') = ksDomainTime s}) = ((\<sigma>\<lparr>ksReadyQueues := ksqupd\<rparr>, \<sigma>'\<lparr>idx_' := i', queue_' := queue_upd', globals := globals \<sigma>'\<lparr>ksReadyQueues_' := ksqupd'\<rparr>\<rparr>) \<in> {(s, s'). cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')) \<and> cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')) \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s) \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s) \<and> cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')) \<and> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')) \<and> (armKSNextASID_' (globals s') = armKSNextASID (ksArchState s) \<and> armKSKernelVSpace (ksArchState s) = armKSKernelVSpace_C \<and> array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) (armKSHWASIDTable_' (globals s')) \<and> array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState s)) (armKSASIDTable_' (globals s')) \<and> asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) \<and> carch_globals (ksArchState s)) \<and> (irq_masks (ksMachineState s) = irq_masks (phantom_machine_state_' (globals s')) \<and> irq_state (ksMachineState s) = irq_state (phantom_machine_state_' (globals s')) \<and> device_state (ksMachineState s) = device_state (phantom_machine_state_' (globals s')) \<and> exclusive_state (ksMachineState s) = exclusive_state (phantom_machine_state_' (globals s')) \<and> machine_state_rest (ksMachineState s) = machine_state_rest (phantom_machine_state_' (globals s'))) \<and> cte_array_relation s (globals s') \<and> tcb_cte_array_relation s (globals s') \<and> apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s) \<and> ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s) \<and> ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s \<and> s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr \<and> ptr_span intStateIRQNode_array_Ptr \<subseteq> kernel_data_refs \<and> s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr \<and> ptr_span armKSGlobalPD_Ptr \<subseteq> kernel_data_refs \<and> htd_safe domain (hrs_htd (t_hrs_' (globals s'))) \<and> - domain \<subseteq> kernel_data_refs \<and> globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s) \<and> ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s) \<and> ksDomainTime_' (globals s') = ksDomainTime s})