theory VSpace_C

lemma invalidateHWASIDEntry_ccorres:
  "hwasid' = unat hwasid \<Longrightarrow>
   ccorres dc xfdc \<top> UNIV
   [] (invalidateHWASIDEntry hwasid)
      (Basic (\<lambda>s. globals_update (
          armKSHWASIDTable_'_update
            (\<lambda>_. Arrays.update (armKSHWASIDTable_' (globals s))
                hwasid' (scast asidInvalid))) s))" apply (clarsimp simp: invalidateHWASIDEntry_def) apply (rule ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: bind_def simpler_gets_def
                        simpler_modify_def) apply (clarsimp simp: rf_sr_def cstate_relation_def
                        Let_def) apply (clarsimp simp: carch_state_relation_def carch_globals_def
                        cmachine_state_relation_def) apply (simp add: array_relation_def split: if_split, erule allEI) apply (clarsimp simp: word_le_nat_alt) apply (simp add: option_to_0_def asidInvalid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hwasid' = unat hwasid \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) UNIV [] (invalidateHWASIDEntry hwasid) (\<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable hwasid' (SCAST(32 signed \<rightarrow> 32) asidInvalid)) proof (prove)
goal (1 subgoal):
 1. hwasid' = unat hwasid \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) UNIV [] (do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(hwasid := None)) (ksArchState s)\<rparr>)
od) (\<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable (unat hwasid) (SCAST(32 signed \<rightarrow> 32) asidInvalid)) proof (prove)
goal (1 subgoal):
 1. hwasid' = unat hwasid \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>armKSHWASIDTable :== Arrays.update \<acute>armKSHWASIDTable (unat hwasid) (SCAST(32 signed \<rightarrow> 32) asidInvalid) {s. \<exists>(rv, \<sigma>')\<in>fst ((do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(hwasid := None)) (ksArchState s)\<rparr>)
od) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. hwasid' = unat hwasid \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((do asidMap <- gets (\<lambda>x. armKSHWASIDTable (ksArchState x));
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(hwasid := None)) (ksArchState s)\<rparr>)
od) \<sigma>). (\<sigma>', globals_update (armKSHWASIDTable_'_update (\<lambda>_. Arrays.update (armKSHWASIDTable_' (globals s)) (unat hwasid) (SCAST(32 signed \<rightarrow> 32) asidInvalid))) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (armKSHWASIDTable_'_update (\<lambda>_. Arrays.update (armKSHWASIDTable_' (globals s)) (unat hwasid) (SCAST(32 signed \<rightarrow> 32) asidInvalid))) s))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>hwasid' = unat hwasid; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (\<sigma>\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. (armKSHWASIDTable (ksArchState \<sigma>))(hwasid := None)) (ksArchState \<sigma>)\<rparr>, globals_update (armKSHWASIDTable_'_update (\<lambda>_. Arrays.update (armKSHWASIDTable_' (globals x)) (unat hwasid) (SCAST(32 signed \<rightarrow> 32) asidInvalid))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>hwasid' = unat hwasid; 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)); carch_state_relation (ksArchState \<sigma>) (globals x); 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> carch_state_relation (armKSHWASIDTable_update (\<lambda>_. (armKSHWASIDTable (ksArchState \<sigma>))(hwasid := None)) (ksArchState \<sigma>)) (globals x\<lparr>armKSHWASIDTable_' := Arrays.update (armKSHWASIDTable_' (globals x)) (unat hwasid) (SCAST(32 signed \<rightarrow> 32) asidInvalid)\<rparr>) \<and> cmachine_state_relation (ksMachineState \<sigma>) (globals x\<lparr>armKSHWASIDTable_' := Arrays.update (armKSHWASIDTable_' (globals x)) (unat hwasid) (SCAST(32 signed \<rightarrow> 32) asidInvalid)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>hwasid' = unat hwasid; 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)); 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>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState \<sigma>)) (armKSHWASIDTable_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); array_relation ((=) \<circ> option_to_ptr) (2 ^ local.asid_high_bits - 1) (armKSASIDTable (ksArchState \<sigma>)) (armKSASIDTable_' (globals x)); exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (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); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']\<rbrakk> \<Longrightarrow> array_relation ((=) \<circ> option_to_0) 0xFF (\<lambda>a. if a = hwasid then None else armKSHWASIDTable (ksArchState \<sigma>) a) (Arrays.update (armKSHWASIDTable_' (globals x)) (unat hwasid) (SCAST(32 signed \<rightarrow> 32) asidInvalid)) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x i. \<lbrakk>hwasid' = unat hwasid; 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)); 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>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); \<forall>i\<le>2 ^ local.asid_high_bits - 1. option_to_ptr (armKSASIDTable (ksArchState \<sigma>) i) = armKSASIDTable_' (globals x).[unat i]; exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (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); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; i \<le> 0xFF \<longrightarrow> option_to_0 (armKSHWASIDTable (ksArchState \<sigma>) i) = armKSHWASIDTable_' (globals x).[unat i]\<rbrakk> \<Longrightarrow> (i = hwasid \<longrightarrow> hwasid \<le> 0xFF \<longrightarrow> Arrays.update (armKSHWASIDTable_' (globals x)) (unat hwasid) (SCAST(32 signed \<rightarrow> 32) asidInvalid).[unat hwasid] = 0) \<and> (i \<noteq> hwasid \<longrightarrow> i \<le> 0xFF \<longrightarrow> armKSHWASIDTable_' (globals x).[unat i] = Arrays.update (armKSHWASIDTable_' (globals x)) (unat hwasid) (SCAST(32 signed \<rightarrow> 32) asidInvalid).[unat i]) proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>hwasid' = unat hwasid; 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)); 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>; armKSNextASID_' (globals x) = armKSNextASID (ksArchState \<sigma>); irq_masks (ksMachineState \<sigma>) = irq_masks (phantom_machine_state_' (globals x)); armKSKernelVSpace_C = armKSKernelVSpace (ksArchState \<sigma>); irq_state (ksMachineState \<sigma>) = irq_state (phantom_machine_state_' (globals x)); device_state (ksMachineState \<sigma>) = device_state (phantom_machine_state_' (globals x)); \<forall>i. unat i \<le> unat (2 ^ local.asid_high_bits - 1) \<longrightarrow> option_to_ptr (armKSASIDTable (ksArchState \<sigma>) i) = armKSASIDTable_' (globals x).[unat i]; exclusive_state (ksMachineState \<sigma>) = exclusive_state (phantom_machine_state_' (globals x)); machine_state_rest (ksMachineState \<sigma>) = machine_state_rest (phantom_machine_state_' (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); armKSGlobalPD (ksArchState \<sigma>) = symbol_table ''armKSGlobalPD''; armKSGlobalPTs (ksArchState \<sigma>) = [symbol_table ''armKSGlobalPT'']; unat hwasid \<le> 255; option_to_0 (armKSHWASIDTable (ksArchState \<sigma>) hwasid) = armKSHWASIDTable_' (globals x).[unat hwasid]\<rbrakk> \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) asidInvalid = 0 proof (prove)
goal:
No subgoals!