theory VSpace_R

lemma invalidateASID_corres:
  "corres dc
          (valid_asid_map and valid_vspace_objs
               and pspace_aligned and pspace_distinct
               and vspace_at_asid a pd and pd_at_uniq a pd
               and K (a \<noteq> 0 \<and> a \<le> mask asid_bits))
          (pspace_aligned' and pspace_distinct' and no_0_obj')
     (invalidate_asid a) (invalidateASID a)"
  (is "corres dc ?P ?P' ?f ?f'") apply (simp add: invalidate_asid_def invalidateASID_def) apply (rule corres_guard_imp) apply (rule_tac pd=pd in findPDForASIDAssert_known_corres) apply (rule_tac P="?P" and P'="?P'" in corres_inst) apply (rule_tac r'="(=)" in corres_underlying_split [OF _ _ gets_sp gets_sp]) apply (clarsimp simp: state_relation_def arch_state_relation_def) apply (rule corres_modify) apply (simp add: state_relation_def arch_state_relation_def
                     fun_upd_def) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) (pspace_aligned' and pspace_distinct' and no_0_obj') (invalidate_asid a) (invalidateASID a) proof (prove)
goal (1 subgoal):
 1. corres dc (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) (pspace_aligned' and pspace_distinct' and no_0_obj') (do asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a := None)\<rparr>\<rparr>)
od) (do y <- findPDForASIDAssert a;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(a := None)) (ksArchState s)\<rparr>)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a := None)\<rparr>\<rparr>)
od) (do y <- findPDForASIDAssert a;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(a := None)) (ksArchState s)\<rparr>)
od)
 2. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres dc ?P4 ?P'4 (do asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a := None)\<rparr>\<rparr>)
od) (do asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(a := None)) (ksArchState s)\<rparr>)
od)
 2. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) s \<Longrightarrow> (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and ?P4) s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (?P'4 and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal (3 subgoals):
 1. corres dc (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) (pspace_aligned' and pspace_distinct' and no_0_obj') (do asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a := None)\<rparr>\<rparr>)
od) (do asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(a := None)) (ksArchState s)\<rparr>)
od)
 2. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) s \<Longrightarrow> (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits))) s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal (4 subgoals):
 1. corres (=) (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) (pspace_aligned' and pspace_distinct' and no_0_obj') (gets (arm_asid_map \<circ> arch_state)) (gets (armKSASIDMap \<circ> ksArchState))
 2. \<And>rv rv'. rv = rv' \<Longrightarrow> corres dc (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := rv(a := None)\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. rv'(a := None)) (ksArchState s)\<rparr>))
 3. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) s \<Longrightarrow> (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits))) s
 4. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. rv = rv' \<Longrightarrow> corres dc (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := rv(a := None)\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. rv'(a := None)) (ksArchState s)\<rparr>))
 2. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) s \<Longrightarrow> (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits))) s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' s s'. \<lbrakk>rv = rv'; (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) s; (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := rv(a := None)\<rparr>\<rparr>, s'\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. rv'(a := None)) (ksArchState s')\<rparr>) \<in> state_relation
 2. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) s \<Longrightarrow> (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits))) s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) s \<Longrightarrow> (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits))) s
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal:
No subgoals!