theory ADT_C

lemma (in kernel_m) cDomSchedule_to_H_correct:
  assumes valid: "valid_state' as"
  assumes cstate_rel: "cstate_relation as cs"
  assumes ms: "cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)"
  shows "cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as" using assms apply (clarsimp simp: cstate_relation_def Let_def valid_state'_def newKernelState_def cDomSchedule_to_H_def cdom_schedule_relation_def) apply (rule the_equality, simp) apply (rule nth_equalityI) apply simp apply (clarsimp simp: dom_schedule_entry_relation_def) apply (drule_tac x=i in spec)+ apply (rule prod_eqI) apply (subst up_ucast_inj_eq[where 'b=32, symmetric]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as proof (prove)
using this:
valid_state' as
cstate_relation as cs
cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)

goal (1 subgoal):
 1. cDomSchedule_to_H kernel_all_global_addresses.ksDomSchedule = kernel_state.ksDomSchedule as proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); valid_pspace' as; cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); sch_act_wf (ksSchedulerAction as) as; cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); Invariants_H.valid_queues as; zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); sym_refs (state_refs_of' as); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); if_live_then_nonz_cap' as; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); if_unsafe_then_cap' as; ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); valid_idle' as; ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); valid_global_refs' as; cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); valid_arch_state' as; cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); valid_irq_node' (irq_node' as) as; carch_state_relation (ksArchState as) cs; valid_irq_handlers' as; cmachine_state_relation (ksMachineState as) cs; valid_irq_states' as; cte_array_relation as cs; valid_machine_state' as; tcb_cte_array_relation as cs; irqs_masked' as; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); valid_queues' as; ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ct_not_inQ as; ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; ct_idle_or_in_cur_domain' as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; valid_pde_mappings' as; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; pspace_domain_valid as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; ksCurDomain as \<le> maxDomain; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; newKSDomSchedule \<noteq> []; htd_safe domain (hrs_htd (t_hrs_' cs)); \<forall>x\<in>set newKSDomSchedule. dschDomain x \<le> maxDomain \<and> 0 < dschLength x; - domain \<subseteq> kernel_data_refs; kernel_state.ksDomSchedule as = newKSDomSchedule; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; ksDomScheduleIdx as < 3; untyped_ranges_zero' as; length newKSDomSchedule = 3; \<forall>n\<le>3. dom_schedule_entry_relation (newKSDomSchedule ! n) (kernel_all_global_addresses.ksDomSchedule.[n]); ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as\<rbrakk> \<Longrightarrow> (THE as. length as = 3 \<and> (\<forall>n\<le>length as. dom_schedule_entry_relation (as ! n) (kernel_all_global_addresses.ksDomSchedule.[n]))) = newKSDomSchedule proof (prove)
goal (1 subgoal):
 1. \<And>asa. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); valid_pspace' as; cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); sch_act_wf (ksSchedulerAction as) as; cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); Invariants_H.valid_queues as; zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); sym_refs (state_refs_of' as); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); if_live_then_nonz_cap' as; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); if_unsafe_then_cap' as; ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); valid_idle' as; ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); valid_global_refs' as; cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); valid_arch_state' as; cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); valid_irq_node' (irq_node' as) as; carch_state_relation (ksArchState as) cs; valid_irq_handlers' as; cmachine_state_relation (ksMachineState as) cs; valid_irq_states' as; cte_array_relation as cs; valid_machine_state' as; tcb_cte_array_relation as cs; irqs_masked' as; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); valid_queues' as; ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ct_not_inQ as; ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; ct_idle_or_in_cur_domain' as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; valid_pde_mappings' as; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; pspace_domain_valid as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; ksCurDomain as \<le> maxDomain; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; newKSDomSchedule \<noteq> []; htd_safe domain (hrs_htd (t_hrs_' cs)); \<forall>x\<in>set newKSDomSchedule. dschDomain x \<le> maxDomain \<and> 0 < dschLength x; - domain \<subseteq> kernel_data_refs; kernel_state.ksDomSchedule as = newKSDomSchedule; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; ksDomScheduleIdx as < 3; untyped_ranges_zero' as; length newKSDomSchedule = 3; \<forall>n\<le>3. dom_schedule_entry_relation (newKSDomSchedule ! n) (kernel_all_global_addresses.ksDomSchedule.[n]); ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; length asa = 3 \<and> (\<forall>n\<le>length asa. dom_schedule_entry_relation (asa ! n) (kernel_all_global_addresses.ksDomSchedule.[n]))\<rbrakk> \<Longrightarrow> asa = newKSDomSchedule proof (prove)
goal (2 subgoals):
 1. \<And>asa. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); valid_pspace' as; cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); sch_act_wf (ksSchedulerAction as) as; cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); Invariants_H.valid_queues as; zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); sym_refs (state_refs_of' as); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); if_live_then_nonz_cap' as; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); if_unsafe_then_cap' as; ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); valid_idle' as; ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); valid_global_refs' as; cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); valid_arch_state' as; cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); valid_irq_node' (irq_node' as) as; carch_state_relation (ksArchState as) cs; valid_irq_handlers' as; cmachine_state_relation (ksMachineState as) cs; valid_irq_states' as; cte_array_relation as cs; valid_machine_state' as; tcb_cte_array_relation as cs; irqs_masked' as; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); valid_queues' as; ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ct_not_inQ as; ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; ct_idle_or_in_cur_domain' as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; valid_pde_mappings' as; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; pspace_domain_valid as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; ksCurDomain as \<le> maxDomain; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; newKSDomSchedule \<noteq> []; htd_safe domain (hrs_htd (t_hrs_' cs)); \<forall>x\<in>set newKSDomSchedule. dschDomain x \<le> maxDomain \<and> 0 < dschLength x; - domain \<subseteq> kernel_data_refs; kernel_state.ksDomSchedule as = newKSDomSchedule; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; ksDomScheduleIdx as < 3; untyped_ranges_zero' as; length newKSDomSchedule = 3; \<forall>n\<le>3. dom_schedule_entry_relation (newKSDomSchedule ! n) (kernel_all_global_addresses.ksDomSchedule.[n]); ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; length asa = 3 \<and> (\<forall>n\<le>length asa. dom_schedule_entry_relation (asa ! n) (kernel_all_global_addresses.ksDomSchedule.[n]))\<rbrakk> \<Longrightarrow> length asa = length newKSDomSchedule
 2. \<And>asa i. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); valid_pspace' as; cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); sch_act_wf (ksSchedulerAction as) as; cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); Invariants_H.valid_queues as; zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); sym_refs (state_refs_of' as); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); if_live_then_nonz_cap' as; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); if_unsafe_then_cap' as; ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); valid_idle' as; ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); valid_global_refs' as; cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); valid_arch_state' as; cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); valid_irq_node' (irq_node' as) as; carch_state_relation (ksArchState as) cs; valid_irq_handlers' as; cmachine_state_relation (ksMachineState as) cs; valid_irq_states' as; cte_array_relation as cs; valid_machine_state' as; tcb_cte_array_relation as cs; irqs_masked' as; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); valid_queues' as; ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ct_not_inQ as; ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; ct_idle_or_in_cur_domain' as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; valid_pde_mappings' as; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; pspace_domain_valid as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; ksCurDomain as \<le> maxDomain; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; newKSDomSchedule \<noteq> []; htd_safe domain (hrs_htd (t_hrs_' cs)); \<forall>x\<in>set newKSDomSchedule. dschDomain x \<le> maxDomain \<and> 0 < dschLength x; - domain \<subseteq> kernel_data_refs; kernel_state.ksDomSchedule as = newKSDomSchedule; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; ksDomScheduleIdx as < 3; untyped_ranges_zero' as; length newKSDomSchedule = 3; \<forall>n\<le>3. dom_schedule_entry_relation (newKSDomSchedule ! n) (kernel_all_global_addresses.ksDomSchedule.[n]); ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; length asa = 3 \<and> (\<forall>n\<le>length asa. dom_schedule_entry_relation (asa ! n) (kernel_all_global_addresses.ksDomSchedule.[n])); i < length asa\<rbrakk> \<Longrightarrow> asa ! i = newKSDomSchedule ! i proof (prove)
goal (1 subgoal):
 1. \<And>asa i. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); valid_pspace' as; cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); sch_act_wf (ksSchedulerAction as) as; cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); Invariants_H.valid_queues as; zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); sym_refs (state_refs_of' as); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); if_live_then_nonz_cap' as; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); if_unsafe_then_cap' as; ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); valid_idle' as; ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); valid_global_refs' as; cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); valid_arch_state' as; cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); valid_irq_node' (irq_node' as) as; carch_state_relation (ksArchState as) cs; valid_irq_handlers' as; cmachine_state_relation (ksMachineState as) cs; valid_irq_states' as; cte_array_relation as cs; valid_machine_state' as; tcb_cte_array_relation as cs; irqs_masked' as; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); valid_queues' as; ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ct_not_inQ as; ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; ct_idle_or_in_cur_domain' as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; valid_pde_mappings' as; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; pspace_domain_valid as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; ksCurDomain as \<le> maxDomain; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; newKSDomSchedule \<noteq> []; htd_safe domain (hrs_htd (t_hrs_' cs)); \<forall>x\<in>set newKSDomSchedule. dschDomain x \<le> maxDomain \<and> 0 < dschLength x; - domain \<subseteq> kernel_data_refs; kernel_state.ksDomSchedule as = newKSDomSchedule; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; ksDomScheduleIdx as < 3; untyped_ranges_zero' as; length newKSDomSchedule = 3; \<forall>n\<le>3. dom_schedule_entry_relation (newKSDomSchedule ! n) (kernel_all_global_addresses.ksDomSchedule.[n]); ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; length asa = 3 \<and> (\<forall>n\<le>length asa. dom_schedule_entry_relation (asa ! n) (kernel_all_global_addresses.ksDomSchedule.[n])); i < length asa\<rbrakk> \<Longrightarrow> asa ! i = newKSDomSchedule ! i proof (prove)
goal (1 subgoal):
 1. \<And>asa i. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); valid_pspace' as; cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); sch_act_wf (ksSchedulerAction as) as; cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); Invariants_H.valid_queues as; zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); sym_refs (state_refs_of' as); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); if_live_then_nonz_cap' as; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); if_unsafe_then_cap' as; ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); valid_idle' as; ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); valid_global_refs' as; cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); valid_arch_state' as; cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); valid_irq_node' (irq_node' as) as; carch_state_relation (ksArchState as) cs; valid_irq_handlers' as; cmachine_state_relation (ksMachineState as) cs; valid_irq_states' as; cte_array_relation as cs; valid_machine_state' as; tcb_cte_array_relation as cs; irqs_masked' as; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); valid_queues' as; ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ct_not_inQ as; ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; ct_idle_or_in_cur_domain' as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; valid_pde_mappings' as; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; pspace_domain_valid as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; ksCurDomain as \<le> maxDomain; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; newKSDomSchedule \<noteq> []; htd_safe domain (hrs_htd (t_hrs_' cs)); \<forall>x\<in>set newKSDomSchedule. dschDomain x \<le> maxDomain \<and> 0 < dschLength x; - domain \<subseteq> kernel_data_refs; kernel_state.ksDomSchedule as = newKSDomSchedule; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; ksDomScheduleIdx as < 3; untyped_ranges_zero' as; length newKSDomSchedule = 3; \<forall>n\<le>3. UCAST(8 \<rightarrow> 32) (fst (newKSDomSchedule ! n)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[n]) \<and> snd (newKSDomSchedule ! n) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[n]); ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; i < 3; length asa = 3; \<forall>n\<le>3. UCAST(8 \<rightarrow> 32) (fst (asa ! n)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[n]) \<and> snd (asa ! n) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[n])\<rbrakk> \<Longrightarrow> asa ! i = newKSDomSchedule ! i proof (prove)
goal (1 subgoal):
 1. \<And>asa i. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); valid_pspace' as; cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); sch_act_wf (ksSchedulerAction as) as; cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); Invariants_H.valid_queues as; zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); sym_refs (state_refs_of' as); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); if_live_then_nonz_cap' as; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); if_unsafe_then_cap' as; ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); valid_idle' as; ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); valid_global_refs' as; cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); valid_arch_state' as; cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); valid_irq_node' (irq_node' as) as; carch_state_relation (ksArchState as) cs; valid_irq_handlers' as; cmachine_state_relation (ksMachineState as) cs; valid_irq_states' as; cte_array_relation as cs; valid_machine_state' as; tcb_cte_array_relation as cs; irqs_masked' as; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); valid_queues' as; ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ct_not_inQ as; ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; ct_idle_or_in_cur_domain' as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; valid_pde_mappings' as; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; pspace_domain_valid as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; ksCurDomain as \<le> maxDomain; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; newKSDomSchedule \<noteq> []; htd_safe domain (hrs_htd (t_hrs_' cs)); \<forall>x\<in>set newKSDomSchedule. dschDomain x \<le> maxDomain \<and> 0 < dschLength x; - domain \<subseteq> kernel_data_refs; kernel_state.ksDomSchedule as = newKSDomSchedule; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; ksDomScheduleIdx as < 3; untyped_ranges_zero' as; length newKSDomSchedule = 3; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; i < 3; length asa = 3; i \<le> 3 \<longrightarrow> UCAST(8 \<rightarrow> 32) (fst (newKSDomSchedule ! i)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[i]) \<and> snd (newKSDomSchedule ! i) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[i]); i \<le> 3 \<longrightarrow> UCAST(8 \<rightarrow> 32) (fst (asa ! i)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[i]) \<and> snd (asa ! i) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[i])\<rbrakk> \<Longrightarrow> asa ! i = newKSDomSchedule ! i proof (prove)
goal (2 subgoals):
 1. \<And>asa i. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); valid_pspace' as; cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); sch_act_wf (ksSchedulerAction as) as; cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); Invariants_H.valid_queues as; zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); sym_refs (state_refs_of' as); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); if_live_then_nonz_cap' as; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); if_unsafe_then_cap' as; ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); valid_idle' as; ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); valid_global_refs' as; cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); valid_arch_state' as; cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); valid_irq_node' (irq_node' as) as; carch_state_relation (ksArchState as) cs; valid_irq_handlers' as; cmachine_state_relation (ksMachineState as) cs; valid_irq_states' as; cte_array_relation as cs; valid_machine_state' as; tcb_cte_array_relation as cs; irqs_masked' as; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); valid_queues' as; ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ct_not_inQ as; ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; ct_idle_or_in_cur_domain' as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; valid_pde_mappings' as; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; pspace_domain_valid as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; ksCurDomain as \<le> maxDomain; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; newKSDomSchedule \<noteq> []; htd_safe domain (hrs_htd (t_hrs_' cs)); \<forall>x\<in>set newKSDomSchedule. dschDomain x \<le> maxDomain \<and> 0 < dschLength x; - domain \<subseteq> kernel_data_refs; kernel_state.ksDomSchedule as = newKSDomSchedule; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; ksDomScheduleIdx as < 3; untyped_ranges_zero' as; length newKSDomSchedule = 3; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; i < 3; length asa = 3; i \<le> 3 \<longrightarrow> UCAST(8 \<rightarrow> 32) (fst (newKSDomSchedule ! i)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[i]) \<and> snd (newKSDomSchedule ! i) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[i]); i \<le> 3 \<longrightarrow> UCAST(8 \<rightarrow> 32) (fst (asa ! i)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[i]) \<and> snd (asa ! i) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[i])\<rbrakk> \<Longrightarrow> fst (asa ! i) = fst (newKSDomSchedule ! i)
 2. \<And>asa i. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); valid_pspace' as; cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); sch_act_wf (ksSchedulerAction as) as; cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); Invariants_H.valid_queues as; zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); sym_refs (state_refs_of' as); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); if_live_then_nonz_cap' as; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); if_unsafe_then_cap' as; ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); valid_idle' as; ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); valid_global_refs' as; cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); valid_arch_state' as; cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); valid_irq_node' (irq_node' as) as; carch_state_relation (ksArchState as) cs; valid_irq_handlers' as; cmachine_state_relation (ksMachineState as) cs; valid_irq_states' as; cte_array_relation as cs; valid_machine_state' as; tcb_cte_array_relation as cs; irqs_masked' as; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); valid_queues' as; ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ct_not_inQ as; ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; ct_idle_or_in_cur_domain' as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; valid_pde_mappings' as; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; pspace_domain_valid as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; ksCurDomain as \<le> maxDomain; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; newKSDomSchedule \<noteq> []; htd_safe domain (hrs_htd (t_hrs_' cs)); \<forall>x\<in>set newKSDomSchedule. dschDomain x \<le> maxDomain \<and> 0 < dschLength x; - domain \<subseteq> kernel_data_refs; kernel_state.ksDomSchedule as = newKSDomSchedule; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; ksDomScheduleIdx as < 3; untyped_ranges_zero' as; length newKSDomSchedule = 3; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; i < 3; length asa = 3; i \<le> 3 \<longrightarrow> UCAST(8 \<rightarrow> 32) (fst (newKSDomSchedule ! i)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[i]) \<and> snd (newKSDomSchedule ! i) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[i]); i \<le> 3 \<longrightarrow> UCAST(8 \<rightarrow> 32) (fst (asa ! i)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[i]) \<and> snd (asa ! i) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[i])\<rbrakk> \<Longrightarrow> snd (asa ! i) = snd (newKSDomSchedule ! i) proof (prove)
goal (3 subgoals):
 1. \<And>asa i. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); valid_pspace' as; cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); sch_act_wf (ksSchedulerAction as) as; cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); Invariants_H.valid_queues as; zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); sym_refs (state_refs_of' as); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); if_live_then_nonz_cap' as; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); if_unsafe_then_cap' as; ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); valid_idle' as; ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); valid_global_refs' as; cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); valid_arch_state' as; cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); valid_irq_node' (irq_node' as) as; carch_state_relation (ksArchState as) cs; valid_irq_handlers' as; cmachine_state_relation (ksMachineState as) cs; valid_irq_states' as; cte_array_relation as cs; valid_machine_state' as; tcb_cte_array_relation as cs; irqs_masked' as; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); valid_queues' as; ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ct_not_inQ as; ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; ct_idle_or_in_cur_domain' as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; valid_pde_mappings' as; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; pspace_domain_valid as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; ksCurDomain as \<le> maxDomain; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; newKSDomSchedule \<noteq> []; htd_safe domain (hrs_htd (t_hrs_' cs)); \<forall>x\<in>set newKSDomSchedule. dschDomain x \<le> maxDomain \<and> 0 < dschLength x; - domain \<subseteq> kernel_data_refs; kernel_state.ksDomSchedule as = newKSDomSchedule; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; ksDomScheduleIdx as < 3; untyped_ranges_zero' as; length newKSDomSchedule = 3; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; i < 3; length asa = 3; i \<le> 3 \<longrightarrow> UCAST(8 \<rightarrow> 32) (fst (newKSDomSchedule ! i)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[i]) \<and> snd (newKSDomSchedule ! i) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[i]); i \<le> 3 \<longrightarrow> UCAST(8 \<rightarrow> 32) (fst (asa ! i)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[i]) \<and> snd (asa ! i) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[i])\<rbrakk> \<Longrightarrow> LENGTH(8) \<le> LENGTH(32)
 2. \<And>asa i. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); valid_pspace' as; cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); sch_act_wf (ksSchedulerAction as) as; cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); Invariants_H.valid_queues as; zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); sym_refs (state_refs_of' as); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); if_live_then_nonz_cap' as; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); if_unsafe_then_cap' as; ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); valid_idle' as; ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); valid_global_refs' as; cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); valid_arch_state' as; cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); valid_irq_node' (irq_node' as) as; carch_state_relation (ksArchState as) cs; valid_irq_handlers' as; cmachine_state_relation (ksMachineState as) cs; valid_irq_states' as; cte_array_relation as cs; valid_machine_state' as; tcb_cte_array_relation as cs; irqs_masked' as; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); valid_queues' as; ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ct_not_inQ as; ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; ct_idle_or_in_cur_domain' as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; valid_pde_mappings' as; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; pspace_domain_valid as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; ksCurDomain as \<le> maxDomain; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; newKSDomSchedule \<noteq> []; htd_safe domain (hrs_htd (t_hrs_' cs)); \<forall>x\<in>set newKSDomSchedule. dschDomain x \<le> maxDomain \<and> 0 < dschLength x; - domain \<subseteq> kernel_data_refs; kernel_state.ksDomSchedule as = newKSDomSchedule; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; ksDomScheduleIdx as < 3; untyped_ranges_zero' as; length newKSDomSchedule = 3; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; i < 3; length asa = 3; i \<le> 3 \<longrightarrow> UCAST(8 \<rightarrow> 32) (fst (newKSDomSchedule ! i)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[i]) \<and> snd (newKSDomSchedule ! i) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[i]); i \<le> 3 \<longrightarrow> UCAST(8 \<rightarrow> 32) (fst (asa ! i)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[i]) \<and> snd (asa ! i) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[i])\<rbrakk> \<Longrightarrow> UCAST(8 \<rightarrow> 32) (fst (asa ! i)) = UCAST(8 \<rightarrow> 32) (fst (newKSDomSchedule ! i))
 3. \<And>asa i. \<lbrakk>cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as); valid_pspace' as; cpspace_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs); sch_act_wf (ksSchedulerAction as) as; cready_queues_relation (clift (t_hrs_' cs)) (ksReadyQueues_' cs) (ksReadyQueues as); Invariants_H.valid_queues as; zero_ranges_are_zero (gsUntypedZeroRanges as) (t_hrs_' cs); sym_refs (state_refs_of' as); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cs) (ksReadyQueuesL1Bitmap as); if_live_then_nonz_cap' as; cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cs) (ksReadyQueuesL2Bitmap as); if_unsafe_then_cap' as; ksCurThread_' cs = tcb_ptr_to_ctcb_ptr (ksCurThread as); valid_idle' as; ksIdleThread_' cs = tcb_ptr_to_ctcb_ptr (ksIdleThread as); valid_global_refs' as; cinterrupt_relation (ksInterruptState as) intStateIRQNode_array_Ptr (intStateIRQTable_' cs); valid_arch_state' as; cscheduler_action_relation (ksSchedulerAction as) (ksSchedulerAction_' cs); valid_irq_node' (irq_node' as) as; carch_state_relation (ksArchState as) cs; valid_irq_handlers' as; cmachine_state_relation (ksMachineState as) cs; valid_irq_states' as; cte_array_relation as cs; valid_machine_state' as; tcb_cte_array_relation as cs; irqs_masked' as; apsnd fst (ghost'state_' cs) = (gsUserPages as, gsCNodes as); valid_queues' as; ghost_size_rel (ghost'state_' cs) (gsMaxObjectSize as); ct_not_inQ as; ksWorkUnitsCompleted_' cs = ksWorkUnitsCompleted as; ct_idle_or_in_cur_domain' as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr; valid_pde_mappings' as; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; pspace_domain_valid as; hrs_htd (t_hrs_' cs) \<Turnstile>\<^sub>t armKSGlobalPD_Ptr; ksCurDomain as \<le> maxDomain; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; newKSDomSchedule \<noteq> []; htd_safe domain (hrs_htd (t_hrs_' cs)); \<forall>x\<in>set newKSDomSchedule. dschDomain x \<le> maxDomain \<and> 0 < dschLength x; - domain \<subseteq> kernel_data_refs; kernel_state.ksDomSchedule as = newKSDomSchedule; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; ksDomScheduleIdx as < 3; untyped_ranges_zero' as; length newKSDomSchedule = 3; ksDomScheduleIdx_' cs = word_of_nat (ksDomScheduleIdx as); ksCurDomain_' cs = UCAST(8 \<rightarrow> 32) (ksCurDomain as); ksDomainTime_' cs = ksDomainTime as; i < 3; length asa = 3; i \<le> 3 \<longrightarrow> UCAST(8 \<rightarrow> 32) (fst (newKSDomSchedule ! i)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[i]) \<and> snd (newKSDomSchedule ! i) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[i]); i \<le> 3 \<longrightarrow> UCAST(8 \<rightarrow> 32) (fst (asa ! i)) = domain_C (kernel_all_global_addresses.ksDomSchedule.[i]) \<and> snd (asa ! i) = dschedule_C.length_C (kernel_all_global_addresses.ksDomSchedule.[i])\<rbrakk> \<Longrightarrow> snd (asa ! i) = snd (newKSDomSchedule ! i) proof (prove)
goal:
No subgoals!