theory VSpace_C

lemma rf_sr_asidTable_None:
  "\<lbrakk> (\<sigma>, x) \<in> rf_sr; asid && mask asid_bits = asid; valid_arch_state' \<sigma>  \<rbrakk> \<Longrightarrow>
  (index (armKSASIDTable_' (globals x)) (unat (asid >> asid_low_bits)) = ap_Ptr 0) =
  (armKSASIDTable (ksArchState \<sigma>) (ucast (asid_high_bits_of asid)) = None)" apply (simp add: asid_high_bits_of_def ucast_ucast_mask) apply (subgoal_tac "(asid >> asid_low_bits) && mask 7 = asid >> asid_low_bits") (*asid_low_bits*)
    prefer 2 apply (rule word_eqI) apply (subst (asm) bang_eq) apply (simp add: word_size nth_shiftr asid_bits_def asid_low_bits_def) apply (case_tac "n < 7", simp)  (*asid_low_bits*)
    apply (clarsimp simp: linorder_not_less) apply (erule_tac x="n+10" in allE) apply (simp add: add.commute) apply simp apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def) apply (simp add: array_relation_def option_to_0_def) apply (erule_tac x="asid >> asid_low_bits" in allE) apply (erule impE) prefer 2 apply (drule sym [where t="index a b" for a b]) apply (simp add: option_to_0_def option_to_ptr_def split: option.splits) apply (clarsimp simp: valid_arch_state'_def valid_asid_table'_def ran_def) apply (simp add: and_mask_eq_iff_le_mask) apply (simp add: asid_high_bits_def mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) = None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) ((asid >> local.asid_low_bits) && mask 7) = None) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) ((asid >> local.asid_low_bits) && mask 7) = None)
 2. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>\<rbrakk> \<Longrightarrow> (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) ((asid >> local.asid_low_bits) && mask 7) = None)
 2. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>\<rbrakk> \<Longrightarrow> (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>\<rbrakk> \<Longrightarrow> (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits
 2. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) ((asid >> local.asid_low_bits) && mask 7) = None) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>\<rbrakk> \<Longrightarrow> n < size ((asid >> local.asid_low_bits) && mask 7) \<longrightarrow> ((asid >> local.asid_low_bits) && mask 7) !! n = (asid >> local.asid_low_bits) !! n
 2. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) ((asid >> local.asid_low_bits) && mask 7) = None) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>(\<sigma>, x) \<in> rf_sr; \<forall>n. (asid && mask local.asid_bits) !! n = asid !! n; valid_arch_state' \<sigma>\<rbrakk> \<Longrightarrow> n < size ((asid >> local.asid_low_bits) && mask 7) \<longrightarrow> ((asid >> local.asid_low_bits) && mask 7) !! n = (asid >> local.asid_low_bits) !! n
 2. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) ((asid >> local.asid_low_bits) && mask 7) = None) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>(\<sigma>, x) \<in> rf_sr; \<forall>n. (asid !! n \<and> n < 32 \<and> n < 17) = asid !! n; valid_arch_state' \<sigma>\<rbrakk> \<Longrightarrow> n < 32 \<longrightarrow> (asid !! (10 + n) \<and> n < 7) = asid !! (10 + n)
 2. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) ((asid >> local.asid_low_bits) && mask 7) = None) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>(\<sigma>, x) \<in> rf_sr; \<forall>n. (asid !! n \<and> n < 32 \<and> n < 17) = asid !! n; valid_arch_state' \<sigma>; \<not> n < 7\<rbrakk> \<Longrightarrow> n < 32 \<longrightarrow> (asid !! (10 + n) \<and> n < 7) = asid !! (10 + n)
 2. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) ((asid >> local.asid_low_bits) && mask 7) = None) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>(\<sigma>, x) \<in> rf_sr; \<forall>n. (asid !! n \<and> n < 32 \<and> n < 17) = asid !! n; valid_arch_state' \<sigma>; \<not> n < 7\<rbrakk> \<Longrightarrow> n < 32 \<longrightarrow> (asid !! (10 + n) \<and> n < 7) = asid !! (10 + n)
 2. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) ((asid >> local.asid_low_bits) && mask 7) = None) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>(\<sigma>, x) \<in> rf_sr; \<forall>n. (asid !! n \<and> n < 32 \<and> n < 17) = asid !! n; valid_arch_state' \<sigma>; 7 \<le> n; n < 32; asid !! (10 + n)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) ((asid >> local.asid_low_bits) && mask 7) = None) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>(\<sigma>, x) \<in> rf_sr; valid_arch_state' \<sigma>; 7 \<le> n; n < 32; asid !! (10 + n); (asid !! (n + 10) \<and> n + 10 < 32 \<and> n + 10 < 17) = asid !! (n + 10)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) ((asid >> local.asid_low_bits) && mask 7) = None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) ((asid >> local.asid_low_bits) && mask 7) = None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, x) \<in> rf_sr; asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) (asid >> local.asid_low_bits) = None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) (asid >> local.asid_low_bits) = None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); \<forall>i\<le>0xFF. (case armKSHWASIDTable (ksArchState \<sigma>) i of None \<Rightarrow> 0 | Some y \<Rightarrow> y) = armKSHWASIDTable_' (globals x).[unat i]; \<forall>i\<le>2 ^ local.asid_high_bits - 1. option_to_ptr (armKSASIDTable (ksArchState \<sigma>) i) = armKSASIDTable_' (globals x).[unat i]; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) (asid >> local.asid_low_bits) = None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); \<forall>i\<le>0xFF. (case armKSHWASIDTable (ksArchState \<sigma>) i of None \<Rightarrow> 0 | Some y \<Rightarrow> y) = armKSHWASIDTable_' (globals x).[unat i]; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1 \<longrightarrow> option_to_ptr (armKSASIDTable (ksArchState \<sigma>) (asid >> local.asid_low_bits)) = armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) (asid >> local.asid_low_bits) = None) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); \<forall>i\<le>0xFF. (case armKSHWASIDTable (ksArchState \<sigma>) i of None \<Rightarrow> 0 | Some y \<Rightarrow> y) = armKSHWASIDTable_' (globals x).[unat i]; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1
 2. \<lbrakk>asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); \<forall>i\<le>0xFF. (case armKSHWASIDTable (ksArchState \<sigma>) i of None \<Rightarrow> 0 | Some y \<Rightarrow> y) = armKSHWASIDTable_' (globals x).[unat i]; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; option_to_ptr (armKSASIDTable (ksArchState \<sigma>) (asid >> local.asid_low_bits)) = armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) (asid >> local.asid_low_bits) = None) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); \<forall>i\<le>0xFF. (case armKSHWASIDTable (ksArchState \<sigma>) i of None \<Rightarrow> 0 | Some y \<Rightarrow> y) = armKSHWASIDTable_' (globals x).[unat i]; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; option_to_ptr (armKSASIDTable (ksArchState \<sigma>) (asid >> local.asid_low_bits)) = armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)]\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) (asid >> local.asid_low_bits) = None)
 2. \<lbrakk>asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); \<forall>i\<le>0xFF. (case armKSHWASIDTable (ksArchState \<sigma>) i of None \<Rightarrow> 0 | Some y \<Rightarrow> y) = armKSHWASIDTable_' (globals x).[unat i]; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); \<forall>i\<le>0xFF. (case armKSHWASIDTable (ksArchState \<sigma>) i of None \<Rightarrow> 0 | Some y \<Rightarrow> y) = armKSHWASIDTable_' (globals x).[unat i]; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = option_to_ptr (armKSASIDTable (ksArchState \<sigma>) (asid >> local.asid_low_bits))\<rbrakk> \<Longrightarrow> (armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = NULL) = (armKSASIDTable (ksArchState \<sigma>) (asid >> local.asid_low_bits) = None)
 2. \<lbrakk>asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); \<forall>i\<le>0xFF. (case armKSHWASIDTable (ksArchState \<sigma>) i of None \<Rightarrow> 0 | Some y \<Rightarrow> y) = armKSHWASIDTable_' (globals x).[unat i]; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1 proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); \<forall>i. (i \<le> 0xFF \<longrightarrow> (\<exists>y. armKSHWASIDTable (ksArchState \<sigma>) i = Some y) \<or> armKSHWASIDTable_' (globals x).[unat i] = 0) \<and> (i \<le> 0xFF \<longrightarrow> (\<forall>x2. armKSHWASIDTable (ksArchState \<sigma>) i = Some x2 \<longrightarrow> x2 = armKSHWASIDTable_' (globals x).[unat i])); asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>; armKSASIDTable (ksArchState \<sigma>) (asid >> local.asid_low_bits) = Some x2; armKSASIDTable_' (globals x).[unat (asid >> local.asid_low_bits)] = ap_Ptr x2\<rbrakk> \<Longrightarrow> x2 \<noteq> 0
 2. \<lbrakk>asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); \<forall>i\<le>0xFF. (case armKSHWASIDTable (ksArchState \<sigma>) i of None \<Rightarrow> 0 | Some y \<Rightarrow> y) = armKSHWASIDTable_' (globals x).[unat i]; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid && mask local.asid_bits = asid; valid_arch_state' \<sigma>; (asid >> local.asid_low_bits) && mask 7 = asid >> local.asid_low_bits; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); \<forall>i\<le>0xFF. (case armKSHWASIDTable (ksArchState \<sigma>) i of None \<Rightarrow> 0 | Some y \<Rightarrow> y) = armKSHWASIDTable_' (globals x).[unat i]; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>asid \<le> mask local.asid_bits; valid_arch_state' \<sigma>; asid >> local.asid_low_bits \<le> mask 7; cpspace_relation (ksPSpace \<sigma>) (underlying_memory (ksMachineState \<sigma>)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues \<sigma>); zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap \<sigma>); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap \<sigma>); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread \<sigma>); cinterrupt_relation (ksInterruptState \<sigma>) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction \<sigma>) (ksSchedulerAction_' (globals x)); armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); \<forall>i\<le>0xFF. (case armKSHWASIDTable (ksArchState \<sigma>) i of None \<Rightarrow> 0 | Some y \<Rightarrow> y) = armKSHWASIDTable_' (globals x).[unat i]; asid_map_pd_to_hwasids (armKSASIDMap (ksArchState \<sigma>)) = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift x \<circ>\<^sub>m pd_pointer_to_asid_slot); carch_globals (ksArchState \<sigma>); cmachine_state_relation (ksMachineState \<sigma>) (globals x); cte_array_relation \<sigma> (globals x); tcb_cte_array_relation \<sigma> (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages \<sigma>, gsCNodes \<sigma>); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize \<sigma>); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted \<sigma>; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+4096} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - 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 \<sigma>) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx \<sigma>); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain \<sigma>); ksDomainTime_' (globals x) = ksDomainTime \<sigma>\<rbrakk> \<Longrightarrow> asid >> local.asid_low_bits \<le> 2 ^ local.asid_high_bits - 1 proof (prove)
goal:
No subgoals!