theory VSpace_R

lemma armv_contextSwitch_corres:
  "corres dc
          (vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask asid_bits)
           and unique_table_refs o caps_of_state
           and valid_global_objs and valid_vs_lookup
           and valid_asid_map and valid_vspace_objs
           and pspace_aligned and pspace_distinct
           and valid_arch_state)
          (pspace_aligned' and pspace_distinct' and no_0_obj')
          (arm_context_switch pd a) (armv_contextSwitch pd a)" apply (simp add: arm_context_switch_def armv_contextSwitch_def armv_contextSwitch_HWASID_def) apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF getHWASID_corres[where pd=pd]]) apply (rule corres_machine_op) apply (simp add: setCurrentPD_to_abs) apply (rule corres_rel_imp) apply (rule corres_underlying_trivial) apply (rule no_fail_pre) apply (wpsimp wp: no_fail_set_current_pd no_fail_setHardwareASID no_irq_set_current_pd
                      simp: setCurrentPD_to_abs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) (pspace_aligned' and pspace_distinct' and no_0_obj') (arm_context_switch pd a) (armv_contextSwitch pd a) proof (prove)
goal (1 subgoal):
 1. corres dc (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) (pspace_aligned' and pspace_distinct' and no_0_obj') (do hwasid <- get_hw_asid a;
do_machine_op (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od)
od) (do hwasid <- getHWASID a;
doMachineOp (do y <- setCurrentPD (addrFromPPtr pd);
setHardwareASID hwasid
od)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do hwasid <- get_hw_asid a;
do_machine_op (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od)
od) (do hwasid <- getHWASID a;
doMachineOp (do y <- setCurrentPD (addrFromPPtr pd);
setHardwareASID hwasid
od)
od)
 2. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> ?Q s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>hwasid. corres dc (?R4 hwasid) (?R'4 hwasid) (do_machine_op (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od)) (doMachineOp (do y <- setCurrentPD (addrFromPPtr pd);
setHardwareASID hwasid
od))
 2. \<lbrace>?Q4\<rbrace> get_hw_asid a \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getHWASID a \<lbrace>?R'4\<rbrace>
 4. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> (vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state and ?Q4) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>hwasid. corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od) (do y <- setCurrentPD (addrFromPPtr pd);
setHardwareASID hwasid
od)
 2. \<lbrace>?Q4\<rbrace> get_hw_asid a \<lbrace>\<lambda>hwasid _. True\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getHWASID a \<lbrace>\<lambda>hwasid _. True\<rbrace>
 4. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> (vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state and ?Q4) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>hwasid. corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od) (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od)
 2. \<lbrace>?Q4\<rbrace> get_hw_asid a \<lbrace>\<lambda>hwasid _. True\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getHWASID a \<lbrace>\<lambda>hwasid _. True\<rbrace>
 4. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> (vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state and ?Q4) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>hwasid. corres_underlying Id False True (?r'11 hwasid) (\<lambda>_. True) (\<lambda>_. True) (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od) (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od)
 2. \<And>hwasid x y. ?r'11 hwasid x y \<Longrightarrow> dc x y
 3. \<lbrace>?Q4\<rbrace> get_hw_asid a \<lbrace>\<lambda>hwasid _. True\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getHWASID a \<lbrace>\<lambda>hwasid _. True\<rbrace>
 5. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> (vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state and ?Q4) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>hwasid. True \<Longrightarrow> no_fail (\<lambda>_. True) (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od)
 2. \<And>hwasid x y. x = y \<Longrightarrow> dc x y
 3. \<lbrace>?Q4\<rbrace> get_hw_asid a \<lbrace>\<lambda>hwasid _. True\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getHWASID a \<lbrace>\<lambda>hwasid _. True\<rbrace>
 5. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> (vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state and ?Q4) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>hwasid. True \<Longrightarrow> no_fail (?P16 hwasid) (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od)
 2. \<And>hwasid s. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> ?P16 hwasid s
 3. \<And>hwasid x y. x = y \<Longrightarrow> dc x y
 4. \<lbrace>?Q4\<rbrace> get_hw_asid a \<lbrace>\<lambda>hwasid _. True\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getHWASID a \<lbrace>\<lambda>hwasid _. True\<rbrace>
 6. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> (vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state and ?Q4) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'4) s proof (prove)
goal:
No subgoals!