theory VSpace_R

lemma storeHWASID_corres:
  "corres dc
          (vspace_at_asid a pd and pd_at_uniq a pd
                  and valid_vspace_objs and pspace_distinct
                  and pspace_aligned and K (a \<noteq> 0 \<and> a \<le> mask asid_bits)
                  and valid_asid_map)
          (pspace_aligned' and pspace_distinct' and no_0_obj')
          (store_hw_asid a h) (storeHWASID a h)" apply (simp add: store_hw_asid_def storeHWASID_def) apply (rule corres_guard_imp) apply (rule corres_split[OF findPDForASIDAssert_corres[where pd=pd]]) apply (rule corres_split_eqr) apply (rule corres_trivial) apply (clarsimp simp: state_relation_def arch_state_relation_def) apply (rule corres_split) apply (rule corres_trivial, rule corres_modify) apply (clarsimp simp: state_relation_def) apply (simp add: arch_state_relation_def) apply (rule ext) apply simp 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 simp apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) (pspace_aligned' and pspace_distinct' and no_0_obj') (store_hw_asid a h) (storeHWASID a h) proof (prove)
goal (1 subgoal):
 1. corres dc (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) (pspace_aligned' and pspace_distinct' and no_0_obj') (do pd <- find_pd_for_asid_assert a;
asid_map <- gets (arm_asid_map \<circ> arch_state);
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pd))\<rparr>\<rparr>);
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(h \<mapsto> a)\<rparr>\<rparr>)
od) (do pd <- findPDForASIDAssert a;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(a \<mapsto> (h, pd))) (ksArchState s)\<rparr>);
hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(h \<mapsto> a)) (ksArchState s)\<rparr>)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do pd <- find_pd_for_asid_assert a;
asid_map <- gets (arm_asid_map \<circ> arch_state);
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pd))\<rparr>\<rparr>);
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(h \<mapsto> a)\<rparr>\<rparr>)
od) (do pd <- findPDForASIDAssert a;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(a \<mapsto> (h, pd))) (ksArchState s)\<rparr>);
hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(h \<mapsto> a)) (ksArchState s)\<rparr>)
od)
 2. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) 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>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> corres dc (?R4 pda) (?R'4 pdaa) (do asid_map <- gets (arm_asid_map \<circ> arch_state);
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>);
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(h \<mapsto> a)\<rparr>\<rparr>)
od) (do asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>);
hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(h \<mapsto> a)) (ksArchState s)\<rparr>)
od)
 2. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>?R'4\<rbrace>
 4. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd 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 (8 subgoals):
 1. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> corres (=) (?P10 pda) (?P'12 pdaa) (gets (arm_asid_map \<circ> arch_state)) (gets (armKSASIDMap \<circ> ksArchState))
 2. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> corres dc (?R9 pda pdaa asid_map) (?R'9 pda pdaa asid_map) (do y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>);
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(h \<mapsto> a)\<rparr>\<rparr>)
od) (do y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>);
hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(h \<mapsto> a)) (ksArchState s)\<rparr>)
od)
 3. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>?R9 pda pdaa\<rbrace>
 4. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>?R'9 pda pdaa\<rbrace>
 5. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. ?P10 pd and ?Q11 pd\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. ?P'12 pda and ?Q'13 pda\<rbrace>
 7. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
 8. \<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 (8 subgoals):
 1. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>_. True) (gets (arm_asid_map \<circ> arch_state)) (gets (armKSASIDMap \<circ> ksArchState))
 2. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> corres dc (?R9 pda pdaa asid_map) (?R'9 pda pdaa asid_map) (do y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>);
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(h \<mapsto> a)\<rparr>\<rparr>)
od) (do y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>);
hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(h \<mapsto> a)) (ksArchState s)\<rparr>)
od)
 3. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>?R9 pda pdaa\<rbrace>
 4. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>?R'9 pda pdaa\<rbrace>
 5. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 7. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
 8. \<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>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> corres dc (?R9 pda pdaa asid_map) (?R'9 pda pdaa asid_map) (do y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>);
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(h \<mapsto> a)\<rparr>\<rparr>)
od) (do y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>);
hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(h \<mapsto> a)) (ksArchState s)\<rparr>)
od)
 2. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>?R9 pda pdaa\<rbrace>
 3. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>?R'9 pda pdaa\<rbrace>
 4. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 6. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd 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 (10 subgoals):
 1. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> corres (?r'20 pda pdaa asid_map) (?P20 pda pdaa asid_map) (?P'20 pda pdaa asid_map) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>))
 2. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; ?r'20 pda pdaa asid_map rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R20 pda pdaa asid_map rv) (?R'20 pda pdaa asid_map rv') (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(h \<mapsto> a)\<rparr>\<rparr>)
od) (do hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(h \<mapsto> a)) (ksArchState s)\<rparr>)
od)
 3. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>?R20 pda pdaa asid_map\<rbrace>
 4. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>?R'20 pda pdaa asid_map\<rbrace>
 5. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. ?P20 pda pdaa asid_map and ?Q20 pda pdaa asid_map\<rbrace>
 6. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. ?P'20 pda pdaa asid_map and ?Q'20 pda pdaa asid_map\<rbrace>
 7. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 9. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
 10. \<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 (10 subgoals):
 1. \<And>pda pdaa asid_map s s'. \<lbrakk>pda = pd \<and> pdaa = pd; True; True; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>, s'\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s')\<rparr>) \<in> state_relation
 2. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R20 pda pdaa asid_map rv) (?R'20 pda pdaa asid_map rv') (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(h \<mapsto> a)\<rparr>\<rparr>)
od) (do hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(h \<mapsto> a)) (ksArchState s)\<rparr>)
od)
 3. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>?R20 pda pdaa asid_map\<rbrace>
 4. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>?R'20 pda pdaa asid_map\<rbrace>
 5. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q20 pda pdaa asid_map\<rbrace>
 6. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q'20 pda pdaa asid_map\<rbrace>
 7. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 9. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
 10. \<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 (10 subgoals):
 1. \<And>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'); (arch_state s, ksArchState s') \<in> arch_state_relation; 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> (arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pd))\<rparr>, armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pd))) (ksArchState s')) \<in> arch_state_relation
 2. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R20 pda pdaa asid_map rv) (?R'20 pda pdaa asid_map rv') (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(h \<mapsto> a)\<rparr>\<rparr>)
od) (do hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(h \<mapsto> a)) (ksArchState s)\<rparr>)
od)
 3. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>?R20 pda pdaa asid_map\<rbrace>
 4. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>?R'20 pda pdaa asid_map\<rbrace>
 5. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q20 pda pdaa asid_map\<rbrace>
 6. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q'20 pda pdaa asid_map\<rbrace>
 7. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 9. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
 10. \<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 (10 subgoals):
 1. \<And>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) \<and> arm_global_pd (arch_state s) = armKSGlobalPD (ksArchState s') \<and> arm_hwasid_table (arch_state s) = armKSHWASIDTable (ksArchState s') \<and> arm_global_pts (arch_state s) = armKSGlobalPTs (ksArchState s') \<and> arm_next_asid (arch_state s) = armKSNextASID (ksArchState s') \<and> arm_asid_map (arch_state s) = armKSASIDMap (ksArchState s') \<and> 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> asid_map(a \<mapsto> (h, pd)) = (\<lambda>b. if b = a then Some (h, pd) else asid_map b)
 2. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R20 pda pdaa asid_map rv) (?R'20 pda pdaa asid_map rv') (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(h \<mapsto> a)\<rparr>\<rparr>)
od) (do hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(h \<mapsto> a)) (ksArchState s)\<rparr>)
od)
 3. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>?R20 pda pdaa asid_map\<rbrace>
 4. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>?R'20 pda pdaa asid_map\<rbrace>
 5. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q20 pda pdaa asid_map\<rbrace>
 6. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q'20 pda pdaa asid_map\<rbrace>
 7. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 9. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
 10. \<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 (10 subgoals):
 1. \<And>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) \<and> arm_global_pd (arch_state s) = armKSGlobalPD (ksArchState s') \<and> arm_hwasid_table (arch_state s) = armKSHWASIDTable (ksArchState s') \<and> arm_global_pts (arch_state s) = armKSGlobalPTs (ksArchState s') \<and> arm_next_asid (arch_state s) = armKSNextASID (ksArchState s') \<and> arm_asid_map (arch_state s) = armKSASIDMap (ksArchState s') \<and> 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> (asid_map(a \<mapsto> (h, pd))) x = (if x = a then Some (h, pd) else asid_map x)
 2. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R20 pda pdaa asid_map rv) (?R'20 pda pdaa asid_map rv') (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(h \<mapsto> a)\<rparr>\<rparr>)
od) (do hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(h \<mapsto> a)) (ksArchState s)\<rparr>)
od)
 3. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>?R20 pda pdaa asid_map\<rbrace>
 4. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>?R'20 pda pdaa asid_map\<rbrace>
 5. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q20 pda pdaa asid_map\<rbrace>
 6. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q'20 pda pdaa asid_map\<rbrace>
 7. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 9. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
 10. \<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 (9 subgoals):
 1. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R20 pda pdaa asid_map rv) (?R'20 pda pdaa asid_map rv') (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(h \<mapsto> a)\<rparr>\<rparr>)
od) (do hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(h \<mapsto> a)) (ksArchState s)\<rparr>)
od)
 2. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>?R20 pda pdaa asid_map\<rbrace>
 3. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>?R'20 pda pdaa asid_map\<rbrace>
 4. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q20 pda pdaa asid_map\<rbrace>
 5. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q'20 pda pdaa asid_map\<rbrace>
 6. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 8. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
 9. \<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 (12 subgoals):
 1. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> corres (=) (?P52 pda pdaa asid_map rv) (?P'54 pda pdaa asid_map rv') (gets (arm_hwasid_table \<circ> arch_state)) (gets (armKSHWASIDTable \<circ> ksArchState))
 2. \<And>pda pdaa asid_map rv rv' hw_asid_map. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R51 pda pdaa asid_map rv rv' hw_asid_map) (?R'51 pda pdaa asid_map rv rv' hw_asid_map) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(h \<mapsto> a)\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hw_asid_map(h \<mapsto> a)) (ksArchState s)\<rparr>))
 3. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 pda pdaa asid_map rv\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>?R51 pda pdaa asid_map rv rv'\<rbrace>
 4. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'55 pda pdaa asid_map rv'\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>?R'51 pda pdaa asid_map rv rv'\<rbrace>
 5. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>\<lambda>rv. ?P52 pda pdaa asid_map rv and ?Q53 pda pdaa asid_map rv\<rbrace>
 6. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>\<lambda>rv'. ?P'54 pda pdaa asid_map rv' and ?Q'55 pda pdaa asid_map rv'\<rbrace>
 7. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q20 pda pdaa asid_map\<rbrace>
 8. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q'20 pda pdaa asid_map\<rbrace>
 9. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>_. True) (gets (arm_hwasid_table \<circ> arch_state)) (gets (armKSHWASIDTable \<circ> ksArchState))
 2. \<And>pda pdaa asid_map rv rv' hw_asid_map. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R51 pda pdaa asid_map rv rv' hw_asid_map) (?R'51 pda pdaa asid_map rv rv' hw_asid_map) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(h \<mapsto> a)\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hw_asid_map(h \<mapsto> a)) (ksArchState s)\<rparr>))
 3. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 pda pdaa asid_map rv\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>?R51 pda pdaa asid_map rv rv'\<rbrace>
 4. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'55 pda pdaa asid_map rv'\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>?R'51 pda pdaa asid_map rv rv'\<rbrace>
 5. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q53 pda pdaa asid_map rv\<rbrace>
 6. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'55 pda pdaa asid_map rv'\<rbrace>
 7. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q20 pda pdaa asid_map\<rbrace>
 8. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q'20 pda pdaa asid_map\<rbrace>
 9. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>pda pdaa asid_map rv rv' hw_asid_map. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R51 pda pdaa asid_map rv rv' hw_asid_map) (?R'51 pda pdaa asid_map rv rv' hw_asid_map) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(h \<mapsto> a)\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hw_asid_map(h \<mapsto> a)) (ksArchState s)\<rparr>))
 2. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 pda pdaa asid_map rv\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>?R51 pda pdaa asid_map rv rv'\<rbrace>
 3. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'55 pda pdaa asid_map rv'\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>?R'51 pda pdaa asid_map rv rv'\<rbrace>
 4. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q53 pda pdaa asid_map rv\<rbrace>
 5. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'55 pda pdaa asid_map rv'\<rbrace>
 6. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q20 pda pdaa asid_map\<rbrace>
 7. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q'20 pda pdaa asid_map\<rbrace>
 8. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 10. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>pda pdaa asid_map rv rv' hw_asid_map s s'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'; True; True; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(h \<mapsto> a)\<rparr>\<rparr>, s'\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hw_asid_map(h \<mapsto> a)) (ksArchState s')\<rparr>) \<in> state_relation
 2. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 pda pdaa asid_map rv\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 3. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'55 pda pdaa asid_map rv'\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 4. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q53 pda pdaa asid_map rv\<rbrace>
 5. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'55 pda pdaa asid_map rv'\<rbrace>
 6. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q20 pda pdaa asid_map\<rbrace>
 7. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q'20 pda pdaa asid_map\<rbrace>
 8. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 10. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 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(h \<mapsto> a) = (\<lambda>b. if b = h then Some a else hw_asid_map b)
 2. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 pda pdaa asid_map rv\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 3. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'55 pda pdaa asid_map rv'\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 4. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q53 pda pdaa asid_map rv\<rbrace>
 5. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'55 pda pdaa asid_map rv'\<rbrace>
 6. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q20 pda pdaa asid_map\<rbrace>
 7. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q'20 pda pdaa asid_map\<rbrace>
 8. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 10. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (11 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(h \<mapsto> a)) x = (if x = h then Some a else hw_asid_map x)
 2. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 pda pdaa asid_map rv\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 3. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'55 pda pdaa asid_map rv'\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 4. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q53 pda pdaa asid_map rv\<rbrace>
 5. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'55 pda pdaa asid_map rv'\<rbrace>
 6. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q20 pda pdaa asid_map\<rbrace>
 7. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q'20 pda pdaa asid_map\<rbrace>
 8. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 10. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 pda pdaa asid_map rv\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 2. \<And>pda pdaa asid_map rv rv'. \<lbrakk>pda = pd \<and> pdaa = pd; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'55 pda pdaa asid_map rv'\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_map _. True\<rbrace>
 3. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(a \<mapsto> (h, pda))\<rparr>\<rparr>) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q53 pda pdaa asid_map rv\<rbrace>
 4. \<And>pda pdaa asid_map. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'20 pda pdaa asid_map\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asid_map(a \<mapsto> (h, pdaa))) (ksArchState s)\<rparr>) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'55 pda pdaa asid_map rv'\<rbrace>
 5. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q11 pda\<rbrace> gets (arm_asid_map \<circ> arch_state) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q20 pda pdaa asid_map\<rbrace>
 6. \<And>pda pdaa. pda = pd \<and> pdaa = pd \<Longrightarrow> \<lbrace>?Q'13 pdaa\<rbrace> gets (armKSASIDMap \<circ> ksArchState) \<lbrace>\<lambda>asid_map. (\<lambda>_. True) and ?Q'20 pda pdaa asid_map\<rbrace>
 7. \<lbrace>?Q4\<rbrace> find_pd_for_asid_assert a \<lbrace>\<lambda>pd. (\<lambda>_. True) and ?Q11 pd\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> findPDForASIDAssert a \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q'13 pda\<rbrace>
 9. \<And>s. (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map) s \<Longrightarrow> (K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid a pd and pd_at_uniq a pd and ?Q4) s
 10. \<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!