theory VSpace_R

lemma invalidateHWASIDEntry_corres:
  "corres dc \<top> \<top> (invalidate_hw_asid_entry a) (invalidateHWASIDEntry a)" apply (simp add: invalidate_hw_asid_entry_def invalidateHWASIDEntry_def) apply (rule corres_guard_imp) apply (rule corres_split_eqr) apply (rule corres_trivial) apply (clarsimp simp: state_relation_def arch_state_relation_def) apply (rule corres_trivial, rule corres_modify) apply (clarsimp simp: state_relation_def arch_state_relation_def) apply (rule ext) apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (invalidate_hw_asid_entry a) (invalidateHWASIDEntry a) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (do hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(a := None)\<rparr>\<rparr>)
od) (do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(a := None)) (ksArchState s)\<rparr>)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(a := None)\<rparr>\<rparr>)
od) (do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(a := None)) (ksArchState s)\<rparr>)
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. True \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres (=) ?P4 ?P'4 (gets (arm_hwasid_table \<circ> arch_state)) (gets (armKSHWASIDTable \<circ> ksArchState))
 2. \<And>hw_asid_map. corres dc (?R4 hw_asid_map) (?R'4 hw_asid_map) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(a := None)\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hw_asid_map(a := None)) (ksArchState s)\<rparr>))
 3. \<lbrace>?Q4\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>?R'4\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. True \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. corres (=) (\<lambda>_. True) (\<lambda>_. True) (gets (arm_hwasid_table \<circ> arch_state)) (gets (armKSHWASIDTable \<circ> ksArchState))
 2. \<And>hw_asid_map. corres dc (?R4 hw_asid_map) (?R'4 hw_asid_map) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(a := None)\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hw_asid_map(a := None)) (ksArchState s)\<rparr>))
 3. \<lbrace>?Q4\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>?R'4\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>hw_asid_map. corres dc (?R4 hw_asid_map) (?R'4 hw_asid_map) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(a := None)\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hw_asid_map(a := None)) (ksArchState s)\<rparr>))
 2. \<lbrace>?Q4\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>hw_asid_map s s'. \<lbrakk>True; True; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(a := None)\<rparr>\<rparr>, s'\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hw_asid_map(a := None)) (ksArchState s')\<rparr>) \<in> state_relation
 2. \<lbrace>?Q4\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>hw_asid_map s s'. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); asid_table s = armKSASIDTable (ksArchState s') \<circ> UCAST(7 \<rightarrow> 32); arm_global_pd (arch_state s) = armKSGlobalPD (ksArchState s'); arm_hwasid_table (arch_state s) = armKSHWASIDTable (ksArchState s'); arm_global_pts (arch_state s) = armKSGlobalPTs (ksArchState s'); arm_next_asid (arch_state s) = armKSNextASID (ksArchState s'); arm_asid_map (arch_state s) = armKSASIDMap (ksArchState s'); arm_kernel_vspace (arch_state s) = armKSKernelVSpace (ksArchState s'); interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> hw_asid_map(a := None) = (\<lambda>b. if b = a then None else hw_asid_map b)
 2. \<lbrace>?Q4\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>hw_asid_map s s' x. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); asid_table s = armKSASIDTable (ksArchState s') \<circ> UCAST(7 \<rightarrow> 32); arm_global_pd (arch_state s) = armKSGlobalPD (ksArchState s'); arm_hwasid_table (arch_state s) = armKSHWASIDTable (ksArchState s'); arm_global_pts (arch_state s) = armKSGlobalPTs (ksArchState s'); arm_next_asid (arch_state s) = armKSNextASID (ksArchState s'); arm_asid_map (arch_state s) = armKSASIDMap (ksArchState s'); arm_kernel_vspace (arch_state s) = armKSKernelVSpace (ksArchState s'); interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> (hw_asid_map(a := None)) x = (if x = a then None else hw_asid_map x)
 2. \<lbrace>?Q4\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal:
No subgoals!