theory Ctac_lemmas_C

lemma rf_sr_tcb_ctes_array_assertion':
  "\<lbrakk> (s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr tcb) s \<rbrakk>
    \<Longrightarrow> array_assertion (cte_Ptr (ptr_val tcb && ~~mask tcbBlockSizeBits))
        (unat tcbCNodeEntries) (hrs_htd (t_hrs_' (globals s')))" apply (rule h_t_array_valid_array_assertion, simp_all add: tcbCNodeEntries_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                        cvariable_array_map_relation_def
                        cpspace_relation_def) apply (drule obj_at_ko_at', clarsimp) apply (drule spec, drule mp, rule exI, erule ko_at_projectKO_opt) apply (frule ptr_val_tcb_ptr_mask) apply (simp add: mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr tcb) s\<rbrakk> \<Longrightarrow> array_assertion (cte_Ptr (ptr_val tcb && ~~ mask tcbBlockSizeBits)) (unat tcbCNodeEntries) (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' (ctcb_ptr_to_tcb_ptr tcb) s\<rbrakk> \<Longrightarrow> h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr (ptr_val tcb && ~~ mask tcbBlockSizeBits)) 5 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at' (ctcb_ptr_to_tcb_ptr tcb) s; cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); \<forall>p v. gsCNodes s p = Some v \<longrightarrow> h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr p) (2 ^ v); \<forall>p. (\<exists>v. map_to_tcbs (ksPSpace s) p = Some v) \<longrightarrow> h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr p) 5; apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s\<rbrakk> \<Longrightarrow> h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr (ptr_val tcb && ~~ mask tcbBlockSizeBits)) 5 proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); \<forall>p v. gsCNodes s p = Some v \<longrightarrow> h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr p) (2 ^ v); \<forall>p. (\<exists>v. map_to_tcbs (ksPSpace s) p = Some v) \<longrightarrow> h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr p) 5; apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; ko_at' ko (ctcb_ptr_to_tcb_ptr tcb) s\<rbrakk> \<Longrightarrow> h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr (ptr_val tcb && ~~ mask tcbBlockSizeBits)) 5 proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); \<forall>p v. gsCNodes s p = Some v \<longrightarrow> h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr p) (2 ^ v); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; ko_at' ko (ctcb_ptr_to_tcb_ptr tcb) s; h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr (ctcb_ptr_to_tcb_ptr tcb)) 5\<rbrakk> \<Longrightarrow> h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr (ptr_val tcb && ~~ mask tcbBlockSizeBits)) 5 proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>cmap_relation (ctes_of s) (cslift s') cte_Ptr ccte_relation; cmap_relation (map_to_tcbs (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation; cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); cmap_relation (map_to_pdes (ksPSpace s)) (cslift s') pde_Ptr cpde_relation; cmap_relation (map_to_ptes (ksPSpace s)) (cslift s') pte_Ptr cpte_relation; cmap_relation (map_to_asidpools (ksPSpace s)) (cslift s') ap_Ptr casid_pool_relation; cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_C) cuser_user_data_relation; cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') PTR(user_data_device_C) cuser_user_data_device_relation; carray_map_relation pdBits (map_to_pdes (ksPSpace s)) (c_h_t_valid s') pd_Ptr; carray_map_relation ptBits (map_to_ptes (ksPSpace s)) (c_h_t_valid s') pt_Ptr; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s')); carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); \<forall>p v. gsCNodes s p = Some v \<longrightarrow> h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr p) (2 ^ v); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; ko_at' ko (ctcb_ptr_to_tcb_ptr tcb) s; h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr (ctcb_ptr_to_tcb_ptr tcb)) 5; ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr tcb)) && ~~ mask tcbBlockSizeBits = ctcb_ptr_to_tcb_ptr tcb\<rbrakk> \<Longrightarrow> h_t_array_valid (hrs_htd (t_hrs_' (globals s'))) (cte_Ptr (ptr_val tcb && ~~ mask tcbBlockSizeBits)) 5 proof (prove)
goal:
No subgoals!