theory VSpace_R

lemma findFreeHWASID_corres:
  "corres (=)
          (valid_asid_map and valid_vspace_objs
              and pspace_aligned and pspace_distinct
              and (unique_table_refs o caps_of_state)
              and valid_vs_lookup and valid_arch_state
              and valid_global_objs)
          (pspace_aligned' and pspace_distinct' and no_0_obj')
          find_free_hw_asid findFreeHWASID" apply (simp add: find_free_hw_asid_def findFreeHWASID_def) apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF corres_trivial]) apply (clarsimp simp: arch_state_relation_def state_relation_def) apply (rule corres_split_eqr[OF corres_trivial]) apply (clarsimp simp: arch_state_relation_def state_relation_def) apply (subgoal_tac "take (length [minBound .e. maxBound :: hardware_asid])
                              ([next_asid .e. maxBound] @ [minBound .e. next_asid])
                              = [next_asid .e. maxBound] @ init [minBound .e. next_asid]") apply (cut_tac option="find (\<lambda>a. hw_asid_table a = None)
           ([next_asid .e. maxBound] @ init [minBound .e. next_asid])"
                   in option.nchotomy[rule_format]) apply (erule corres_disj_division) apply (clarsimp split del: if_split) apply (rule corres_split[OF invalidate_asid_ext_corres]) apply (rule corres_underlying_split [where r'=dc]) apply (rule corres_trivial, rule corres_machine_op) apply (rule corres_no_failI) apply (rule no_fail_invalidateLocalTLB_ASID) apply fastforce apply (rule corres_split) apply (rule invalidateHWASIDEntry_corres) apply (rule corres_split) apply (rule corres_trivial) apply (rule corres_modify) apply (simp add: minBound_word maxBound_word
                                    state_relation_def arch_state_relation_def) apply (rule corres_trivial) apply simp apply (wp | simp split del: if_split)+ apply (rule corres_trivial, clarsimp) apply (cut_tac x=next_asid in leq_maxBound) apply (simp only: word_le_nat_alt) apply (simp add: init_def upto_enum_word
                         minBound_word
                    del: upt.simps) apply wp+ apply (clarsimp dest!: findNoneD) apply (drule bspec, rule UnI1, simp, rule order_refl) apply (clarsimp simp: valid_arch_state_def) apply (frule(1) is_inv_SomeD) apply (clarsimp simp: valid_asid_map_def) apply (frule bspec, erule graph_ofI, clarsimp) apply (frule pd_at_asid_uniq, simp_all add: valid_asid_map_def valid_arch_state_def)[1] apply (drule subsetD, erule domI) apply simp apply (simp add: valid_vspace_objs_def) apply fastforce apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) (pspace_aligned' and pspace_distinct' and no_0_obj') find_free_hw_asid findFreeHWASID proof (prove)
goal (1 subgoal):
 1. corres (=) (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) (pspace_aligned' and pspace_distinct' and no_0_obj') (do hw_asid_table <- gets (arm_hwasid_table \<circ> arch_state);
next_asid <- gets (arm_next_asid \<circ> arch_state);
case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2
od) (do hwASIDTable <- gets (armKSHWASIDTable \<circ> ksArchState);
nextASID <- gets (armKSNextASID \<circ> ksArchState);
case find (\<lambda>a. hwASIDTable a = None) ([nextASID .e. maxBound] @ init [minBound .e. nextASID]) of None \<Rightarrow> do y <- invalidateASID (the (hwASIDTable nextASID));
y <- doMachineOp (invalidateLocalTLB_ASID nextASID);
y <- invalidateHWASIDEntry nextASID;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if nextASID = maxBound then minBound else nextASID + 1) (ksArchState s)\<rparr>);
return nextASID
od | Some x2 \<Rightarrow> return x2
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q7 ?Q'7 (do hw_asid_table <- gets (arm_hwasid_table \<circ> arch_state);
next_asid <- gets (arm_next_asid \<circ> arch_state);
case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2
od) (do hwASIDTable <- gets (armKSHWASIDTable \<circ> ksArchState);
nextASID <- gets (armKSNextASID \<circ> ksArchState);
case find (\<lambda>a. hwASIDTable a = None) ([nextASID .e. maxBound] @ init [minBound .e. nextASID]) of None \<Rightarrow> do y <- invalidateASID (the (hwASIDTable nextASID));
y <- doMachineOp (invalidateLocalTLB_ASID nextASID);
y <- invalidateHWASIDEntry nextASID;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if nextASID = maxBound then minBound else nextASID + 1) (ksArchState s)\<rparr>);
return nextASID
od | Some x2 \<Rightarrow> return x2
od)
 2. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ?Q7 s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ?Q'7 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_table. corres (=) (?R11 hw_asid_table) (?R'11 hw_asid_table) (do next_asid <- gets (arm_next_asid \<circ> arch_state);
case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2
od) (do nextASID <- gets (armKSNextASID \<circ> ksArchState);
case find (\<lambda>a. hw_asid_table a = None) ([nextASID .e. maxBound] @ init [minBound .e. nextASID]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table nextASID));
y <- doMachineOp (invalidateLocalTLB_ASID nextASID);
y <- invalidateHWASIDEntry nextASID;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if nextASID = maxBound then minBound else nextASID + 1) (ksArchState s)\<rparr>);
return nextASID
od | Some x2 \<Rightarrow> return x2
od)
 3. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>?R11\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>?R'11\<rbrace>
 5. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (5 subgoals):
 1. \<And>hw_asid_table. corres (=) (?R11 hw_asid_table) (?R'11 hw_asid_table) (do next_asid <- gets (arm_next_asid \<circ> arch_state);
case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2
od) (do nextASID <- gets (armKSNextASID \<circ> ksArchState);
case find (\<lambda>a. hw_asid_table a = None) ([nextASID .e. maxBound] @ init [minBound .e. nextASID]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table nextASID));
y <- doMachineOp (invalidateLocalTLB_ASID nextASID);
y <- invalidateHWASIDEntry nextASID;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if nextASID = maxBound then minBound else nextASID + 1) (ksArchState s)\<rparr>);
return nextASID
od | Some x2 \<Rightarrow> return x2
od)
 2. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>?R11\<rbrace>
 3. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>?R'11\<rbrace>
 4. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (8 subgoals):
 1. \<And>hw_asid_table. corres (=) (\<lambda>_. True) (\<lambda>_. True) (gets (arm_next_asid \<circ> arch_state)) (gets (armKSNextASID \<circ> ksArchState))
 2. \<And>hw_asid_table next_asid. corres (=) (?R17 hw_asid_table next_asid) (?R'17 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 3. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>?R17 hw_asid_table\<rbrace>
 4. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>?R'17 hw_asid_table\<rbrace>
 5. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
 6. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q'17 hw_asid_table\<rbrace>
 7. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (7 subgoals):
 1. \<And>hw_asid_table next_asid. corres (=) (?R17 hw_asid_table next_asid) (?R'17 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 2. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>?R17 hw_asid_table\<rbrace>
 3. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>?R'17 hw_asid_table\<rbrace>
 4. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
 5. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q'17 hw_asid_table\<rbrace>
 6. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (8 subgoals):
 1. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid] \<Longrightarrow> corres (=) (?R17 hw_asid_table next_asid) (?R'17 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 2. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 3. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>?R17 hw_asid_table\<rbrace>
 4. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>?R'17 hw_asid_table\<rbrace>
 5. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
 6. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q'17 hw_asid_table\<rbrace>
 7. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (8 subgoals):
 1. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<or> (\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2)\<rbrakk> \<Longrightarrow> corres (=) (?R17 hw_asid_table next_asid) (?R'17 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 2. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 3. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>?R17 hw_asid_table\<rbrace>
 4. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>?R'17 hw_asid_table\<rbrace>
 5. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
 6. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q'17 hw_asid_table\<rbrace>
 7. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (9 subgoals):
 1. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> corres (=) (?R26 hw_asid_table next_asid) (?S26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 2. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 3. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 4. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ?R26 hw_asid_table next_asid s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?T26 hw_asid_table next_asid s)\<rbrace>
 5. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ?S26 hw_asid_table next_asid s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?U26 hw_asid_table next_asid s)\<rbrace>
 6. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
 7. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q'17 hw_asid_table\<rbrace>
 8. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 9. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (9 subgoals):
 1. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> corres (=) (?R26 hw_asid_table next_asid) (?S26 hw_asid_table next_asid) (do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od) (do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od)
 2. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 3. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 4. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ?R26 hw_asid_table next_asid s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?T26 hw_asid_table next_asid s)\<rbrace>
 5. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ?S26 hw_asid_table next_asid s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?U26 hw_asid_table next_asid s)\<rbrace>
 6. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
 7. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q'17 hw_asid_table\<rbrace>
 8. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 9. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (11 subgoals):
 1. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> corres (=) (?R33 hw_asid_table next_asid rv) (?R'33 hw_asid_table next_asid rv') (do y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od) (do y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od)
 2. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>?R33 hw_asid_table next_asid\<rbrace>
 3. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>?R'33 hw_asid_table next_asid\<rbrace>
 4. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 5. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 6. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ((\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid (the (hw_asid_table next_asid)) pd s \<and> pd_at_uniq (the (hw_asid_table next_asid)) pd s \<and> the (hw_asid_table next_asid) \<noteq> 0 \<and> the (hw_asid_table next_asid) \<le> mask local.asid_bits) and ?Q33 hw_asid_table next_asid) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?T26 hw_asid_table next_asid s)\<rbrace>
 7. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'33 hw_asid_table next_asid) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?U26 hw_asid_table next_asid s)\<rbrace>
 8. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
 9. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q'17 hw_asid_table\<rbrace>
 10. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
A total of 11 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> corres dc (?R33 hw_asid_table next_asid rv) (?R'33 hw_asid_table next_asid rv') (do_machine_op (invalidateLocalTLB_ASID next_asid)) (doMachineOp (invalidateLocalTLB_ASID next_asid))
 2. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?Q38 hw_asid_table next_asid rv rv' y) (?Q'38 hw_asid_table next_asid rv rv' ya) (do y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od) (do y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od)
 3. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R33 hw_asid_table next_asid rv\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>?Q38 hw_asid_table next_asid rv rv'\<rbrace>
 4. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'33 hw_asid_table next_asid rv'\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>?Q'38 hw_asid_table next_asid rv rv'\<rbrace>
 5. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>?R33 hw_asid_table next_asid\<rbrace>
 6. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>?R'33 hw_asid_table next_asid\<rbrace>
 7. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 8. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 9. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ((\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid (the (hw_asid_table next_asid)) pd s \<and> pd_at_uniq (the (hw_asid_table next_asid)) pd s \<and> the (hw_asid_table next_asid) \<noteq> 0 \<and> the (hw_asid_table next_asid) \<le> mask local.asid_bits) and ?Q33 hw_asid_table next_asid) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?T26 hw_asid_table next_asid s)\<rbrace>
 10. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'33 hw_asid_table next_asid) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?U26 hw_asid_table next_asid s)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (invalidateLocalTLB_ASID next_asid) (invalidateLocalTLB_ASID next_asid)
 2. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?Q38 hw_asid_table next_asid rv rv' y) (?Q'38 hw_asid_table next_asid rv rv' ya) (do y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od) (do y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od)
 3. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>?Q38 hw_asid_table next_asid rv rv'\<rbrace>
 4. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>?Q'38 hw_asid_table next_asid rv rv'\<rbrace>
 5. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv _. True\<rbrace>
 6. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv' _. True\<rbrace>
 7. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 8. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 9. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ((\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid (the (hw_asid_table next_asid)) pd s \<and> pd_at_uniq (the (hw_asid_table next_asid)) pd s \<and> the (hw_asid_table next_asid) \<noteq> 0 \<and> the (hw_asid_table next_asid) \<le> mask local.asid_bits) and ?Q33 hw_asid_table next_asid) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?T26 hw_asid_table next_asid s)\<rbrace>
 10. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'33 hw_asid_table next_asid) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?U26 hw_asid_table next_asid s)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (invalidateLocalTLB_ASID next_asid)
 2. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<forall>(s, s')\<in>Id. True \<and> True \<longrightarrow> (\<forall>(r', t')\<in>fst (invalidateLocalTLB_ASID next_asid s'). \<exists>(r, t)\<in>fst (invalidateLocalTLB_ASID next_asid s). (t, t') \<in> Id \<and> dc r r')
 3. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?Q38 hw_asid_table next_asid rv rv' y) (?Q'38 hw_asid_table next_asid rv rv' ya) (do y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od) (do y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od)
 4. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>?Q38 hw_asid_table next_asid rv rv'\<rbrace>
 5. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>?Q'38 hw_asid_table next_asid rv rv'\<rbrace>
 6. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv _. True\<rbrace>
 7. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv' _. True\<rbrace>
 8. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 9. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 10. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ((\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid (the (hw_asid_table next_asid)) pd s \<and> pd_at_uniq (the (hw_asid_table next_asid)) pd s \<and> the (hw_asid_table next_asid) \<noteq> 0 \<and> the (hw_asid_table next_asid) \<le> mask local.asid_bits) and ?Q33 hw_asid_table next_asid) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?T26 hw_asid_table next_asid s)\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<forall>(s, s')\<in>Id. True \<and> True \<longrightarrow> (\<forall>(r', t')\<in>fst (invalidateLocalTLB_ASID next_asid s'). \<exists>(r, t)\<in>fst (invalidateLocalTLB_ASID next_asid s). (t, t') \<in> Id \<and> dc r r')
 2. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?Q38 hw_asid_table next_asid rv rv' y) (?Q'38 hw_asid_table next_asid rv rv' ya) (do y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od) (do y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od)
 3. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>?Q38 hw_asid_table next_asid rv rv'\<rbrace>
 4. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>?Q'38 hw_asid_table next_asid rv rv'\<rbrace>
 5. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv _. True\<rbrace>
 6. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv' _. True\<rbrace>
 7. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 8. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 9. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ((\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid (the (hw_asid_table next_asid)) pd s \<and> pd_at_uniq (the (hw_asid_table next_asid)) pd s \<and> the (hw_asid_table next_asid) \<noteq> 0 \<and> the (hw_asid_table next_asid) \<le> mask local.asid_bits) and ?Q33 hw_asid_table next_asid) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?T26 hw_asid_table next_asid s)\<rbrace>
 10. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'33 hw_asid_table next_asid) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?U26 hw_asid_table next_asid s)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> corres (=) (?Q38 hw_asid_table next_asid rv rv' y) (?Q'38 hw_asid_table next_asid rv rv' ya) (do y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od) (do y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od)
 2. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>?Q38 hw_asid_table next_asid rv rv'\<rbrace>
 3. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>?Q'38 hw_asid_table next_asid rv rv'\<rbrace>
 4. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv _. True\<rbrace>
 5. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv' _. True\<rbrace>
 6. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 7. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 8. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ((\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid (the (hw_asid_table next_asid)) pd s \<and> pd_at_uniq (the (hw_asid_table next_asid)) pd s \<and> the (hw_asid_table next_asid) \<noteq> 0 \<and> the (hw_asid_table next_asid) \<le> mask local.asid_bits) and ?Q33 hw_asid_table next_asid) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?T26 hw_asid_table next_asid s)\<rbrace>
 9. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'33 hw_asid_table next_asid) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?U26 hw_asid_table next_asid s)\<rbrace>
 10. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
A total of 13 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> corres (?r'74 hw_asid_table next_asid rv rv' y ya) (?P75 hw_asid_table next_asid rv rv' y) (?P'77 hw_asid_table next_asid rv rv' ya) (invalidate_hw_asid_entry next_asid) (invalidateHWASIDEntry next_asid)
 2. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; ?r'74 hw_asid_table next_asid rv rv' y ya yb yc\<rbrakk> \<Longrightarrow> corres (=) (?R74 hw_asid_table next_asid rv rv' y ya yb) (?R'74 hw_asid_table next_asid rv rv' y ya yc) (do y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od) (do y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od)
 3. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q76 hw_asid_table next_asid rv rv' y\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>?R74 hw_asid_table next_asid rv rv' y ya\<rbrace>
 4. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace> invalidateHWASIDEntry next_asid \<lbrace>?R'74 hw_asid_table next_asid rv rv' y ya\<rbrace>
 5. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>y. ?P75 hw_asid_table next_asid rv rv' y and ?Q76 hw_asid_table next_asid rv rv' y\<rbrace>
 6. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>ya. ?P'77 hw_asid_table next_asid rv rv' ya and ?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace>
 7. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv _. True\<rbrace>
 8. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv' _. True\<rbrace>
 9. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 10. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres (=) (?R74 hw_asid_table next_asid rv rv' y ya yb) (?R'74 hw_asid_table next_asid rv rv' y ya yc) (do y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od) (do y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od)
 2. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q76 hw_asid_table next_asid rv rv' y\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>?R74 hw_asid_table next_asid rv rv' y ya\<rbrace>
 3. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace> invalidateHWASIDEntry next_asid \<lbrace>?R'74 hw_asid_table next_asid rv rv' y ya\<rbrace>
 4. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q76 hw_asid_table next_asid rv rv' y\<rbrace>
 5. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace>
 6. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv _. True\<rbrace>
 7. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv' _. True\<rbrace>
 8. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 9. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 10. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ((\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid (the (hw_asid_table next_asid)) pd s \<and> pd_at_uniq (the (hw_asid_table next_asid)) pd s \<and> the (hw_asid_table next_asid) \<noteq> 0 \<and> the (hw_asid_table next_asid) \<le> mask local.asid_bits) and ?Q33 hw_asid_table next_asid) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?T26 hw_asid_table next_asid s)\<rbrace>
A total of 15 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres (?r'84 hw_asid_table next_asid rv rv' y ya yb yc) (?P85 hw_asid_table next_asid rv rv' y ya yb) (?P'87 hw_asid_table next_asid rv rv' y ya yc) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>))
 2. \<And>hw_asid_table next_asid rv rv' y ya yb yc yd ye. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc; ?r'84 hw_asid_table next_asid rv rv' y ya yb yc yd ye\<rbrakk> \<Longrightarrow> corres (=) (?R84 hw_asid_table next_asid rv rv' y ya yb yc yd) (?R'84 hw_asid_table next_asid rv rv' y ya yb yc ye) (return next_asid) (return next_asid)
 3. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q86 hw_asid_table next_asid rv rv' y ya yb\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>) \<lbrace>?R84 hw_asid_table next_asid rv rv' y ya yb yc\<rbrace>
 4. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'88 hw_asid_table next_asid rv rv' y ya yc\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>) \<lbrace>?R'84 hw_asid_table next_asid rv rv' y ya yb yc\<rbrace>
 5. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q76 hw_asid_table next_asid rv rv' y\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>yb. ?P85 hw_asid_table next_asid rv rv' y ya yb and ?Q86 hw_asid_table next_asid rv rv' y ya yb\<rbrace>
 6. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace> invalidateHWASIDEntry next_asid \<lbrace>\<lambda>yc. ?P'87 hw_asid_table next_asid rv rv' y ya yc and ?Q'88 hw_asid_table next_asid rv rv' y ya yc\<rbrace>
 7. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q76 hw_asid_table next_asid rv rv' y\<rbrace>
 8. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace>
 9. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv _. True\<rbrace>
 10. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv' _. True\<rbrace>
A total of 18 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> corres (?r'84 hw_asid_table next_asid rv rv' y ya yb yc) (\<lambda>_. True) (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>)) (modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>))
 2. \<And>hw_asid_table next_asid rv rv' y ya yb yc yd ye. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc; ?r'84 hw_asid_table next_asid rv rv' y ya yb yc yd ye\<rbrakk> \<Longrightarrow> corres (=) (?R84 hw_asid_table next_asid rv rv' y ya yb yc yd) (?R'84 hw_asid_table next_asid rv rv' y ya yb yc ye) (return next_asid) (return next_asid)
 3. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q86 hw_asid_table next_asid rv rv' y ya yb\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>) \<lbrace>?R84 hw_asid_table next_asid rv rv' y ya yb yc\<rbrace>
 4. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'88 hw_asid_table next_asid rv rv' y ya yc\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>) \<lbrace>?R'84 hw_asid_table next_asid rv rv' y ya yb yc\<rbrace>
 5. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q76 hw_asid_table next_asid rv rv' y\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q86 hw_asid_table next_asid rv rv' y ya yb\<rbrace>
 6. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace> invalidateHWASIDEntry next_asid \<lbrace>\<lambda>yc. (\<lambda>_. True) and ?Q'88 hw_asid_table next_asid rv rv' y ya yc\<rbrace>
 7. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q76 hw_asid_table next_asid rv rv' y\<rbrace>
 8. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace>
 9. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv _. True\<rbrace>
 10. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv' _. True\<rbrace>
A total of 18 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>hw_asid_table next_asid rv rv' y ya yb yc s s'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc; True; True; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>, s'\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s')\<rparr>) \<in> state_relation
 2. \<And>hw_asid_table next_asid rv rv' y ya yb yc yd ye. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc; dc yd ye\<rbrakk> \<Longrightarrow> corres (=) (?R84 hw_asid_table next_asid rv rv' y ya yb yc yd) (?R'84 hw_asid_table next_asid rv rv' y ya yb yc ye) (return next_asid) (return next_asid)
 3. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q86 hw_asid_table next_asid rv rv' y ya yb\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>) \<lbrace>?R84 hw_asid_table next_asid rv rv' y ya yb yc\<rbrace>
 4. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'88 hw_asid_table next_asid rv rv' y ya yc\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>) \<lbrace>?R'84 hw_asid_table next_asid rv rv' y ya yb yc\<rbrace>
 5. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q76 hw_asid_table next_asid rv rv' y\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q86 hw_asid_table next_asid rv rv' y ya yb\<rbrace>
 6. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace> invalidateHWASIDEntry next_asid \<lbrace>\<lambda>yc. (\<lambda>_. True) and ?Q'88 hw_asid_table next_asid rv rv' y ya yc\<rbrace>
 7. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q76 hw_asid_table next_asid rv rv' y\<rbrace>
 8. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace>
 9. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv _. True\<rbrace>
 10. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv' _. True\<rbrace>
A total of 18 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>hw_asid_table next_asid rv rv' y ya yb yc yd ye. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc; dc yd ye\<rbrakk> \<Longrightarrow> corres (=) (?R84 hw_asid_table next_asid rv rv' y ya yb yc yd) (?R'84 hw_asid_table next_asid rv rv' y ya yb yc ye) (return next_asid) (return next_asid)
 2. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q86 hw_asid_table next_asid rv rv' y ya yb\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>) \<lbrace>?R84 hw_asid_table next_asid rv rv' y ya yb yc\<rbrace>
 3. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'88 hw_asid_table next_asid rv rv' y ya yc\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>) \<lbrace>?R'84 hw_asid_table next_asid rv rv' y ya yb yc\<rbrace>
 4. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q76 hw_asid_table next_asid rv rv' y\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q86 hw_asid_table next_asid rv rv' y ya yb\<rbrace>
 5. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace> invalidateHWASIDEntry next_asid \<lbrace>\<lambda>yc. (\<lambda>_. True) and ?Q'88 hw_asid_table next_asid rv rv' y ya yc\<rbrace>
 6. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q76 hw_asid_table next_asid rv rv' y\<rbrace>
 7. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace>
 8. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv _. True\<rbrace>
 9. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv' _. True\<rbrace>
 10. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
A total of 17 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>hw_asid_table next_asid rv rv' y ya yb yc yd ye. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc; dc yd ye\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>_. True) (return next_asid) (return next_asid)
 2. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q86 hw_asid_table next_asid rv rv' y ya yb\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>) \<lbrace>\<lambda>yd _. True\<rbrace>
 3. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'88 hw_asid_table next_asid rv rv' y ya yc\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>) \<lbrace>\<lambda>ye _. True\<rbrace>
 4. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q76 hw_asid_table next_asid rv rv' y\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q86 hw_asid_table next_asid rv rv' y ya yb\<rbrace>
 5. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace> invalidateHWASIDEntry next_asid \<lbrace>\<lambda>yc. (\<lambda>_. True) and ?Q'88 hw_asid_table next_asid rv rv' y ya yc\<rbrace>
 6. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q76 hw_asid_table next_asid rv rv' y\<rbrace>
 7. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace>
 8. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv _. True\<rbrace>
 9. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv' _. True\<rbrace>
 10. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
A total of 17 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q86 hw_asid_table next_asid rv rv' y ya yb\<rbrace> modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>) \<lbrace>\<lambda>yd _. True\<rbrace>
 2. \<And>hw_asid_table next_asid rv rv' y ya yb yc. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya; dc yb yc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'88 hw_asid_table next_asid rv rv' y ya yc\<rbrace> modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>) \<lbrace>\<lambda>ye _. True\<rbrace>
 3. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q76 hw_asid_table next_asid rv rv' y\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>yb. (\<lambda>_. True) and ?Q86 hw_asid_table next_asid rv rv' y ya yb\<rbrace>
 4. \<And>hw_asid_table next_asid rv rv' y ya. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace> invalidateHWASIDEntry next_asid \<lbrace>\<lambda>yc. (\<lambda>_. True) and ?Q'88 hw_asid_table next_asid rv rv' y ya yc\<rbrace>
 5. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do_machine_op (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q76 hw_asid_table next_asid rv rv' y\<rbrace>
 6. \<And>hw_asid_table next_asid rv rv'. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doMachineOp (invalidateLocalTLB_ASID next_asid) \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'78 hw_asid_table next_asid rv rv' ya\<rbrace>
 7. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 hw_asid_table next_asid\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv _. True\<rbrace>
 8. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'33 hw_asid_table next_asid\<rbrace> invalidateASID (the (hw_asid_table next_asid)) \<lbrace>\<lambda>rv' _. True\<rbrace>
 9. \<And>hw_asid_table next_asid. \<lbrakk>take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 10. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
A total of 16 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>hw_asid_table next_asid. \<lbrakk>take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid] = [next_asid .e. maxBound] @ init [minBound .e. next_asid]; \<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?T26 hw_asid_table next_asid) (?U26 hw_asid_table next_asid) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2) (case find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidateASID (the (hw_asid_table next_asid));
y <- doMachineOp (invalidateLocalTLB_ASID next_asid);
y <- invalidateHWASIDEntry next_asid;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if next_asid = maxBound then minBound else next_asid + 1) (ksArchState s)\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2)
 2. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 3. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ((\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid (the (hw_asid_table next_asid)) pd s \<and> pd_at_uniq (the (hw_asid_table next_asid)) pd s \<and> the (hw_asid_table next_asid) \<noteq> 0 \<and> the (hw_asid_table next_asid) \<le> mask local.asid_bits) and (\<lambda>s. True)) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?T26 hw_asid_table next_asid s)\<rbrace>
 4. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> ?U26 hw_asid_table next_asid s)\<rbrace>
 5. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
 6. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q'17 hw_asid_table\<rbrace>
 7. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (7 subgoals):
 1. \<And>hw_asid_table next_asid. take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 2. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ((\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid (the (hw_asid_table next_asid)) pd s \<and> pd_at_uniq (the (hw_asid_table next_asid)) pd s \<and> the (hw_asid_table next_asid) \<noteq> 0 \<and> the (hw_asid_table next_asid) \<le> mask local.asid_bits) and (\<lambda>s. True)) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> True)\<rbrace>
 3. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> True)\<rbrace>
 4. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
 5. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q'17 hw_asid_table\<rbrace>
 6. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (7 subgoals):
 1. \<And>hw_asid_table next_asid. next_asid \<le> maxBound \<Longrightarrow> take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 2. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ((\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid (the (hw_asid_table next_asid)) pd s \<and> pd_at_uniq (the (hw_asid_table next_asid)) pd s \<and> the (hw_asid_table next_asid) \<noteq> 0 \<and> the (hw_asid_table next_asid) \<le> mask local.asid_bits) and (\<lambda>s. True)) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> True)\<rbrace>
 3. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> True)\<rbrace>
 4. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
 5. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q'17 hw_asid_table\<rbrace>
 6. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (7 subgoals):
 1. \<And>hw_asid_table next_asid. unat next_asid \<le> unat maxBound \<Longrightarrow> take (length [minBound .e. maxBound]) ([next_asid .e. maxBound] @ [minBound .e. next_asid]) = [next_asid .e. maxBound] @ init [minBound .e. next_asid]
 2. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ((\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid (the (hw_asid_table next_asid)) pd s \<and> pd_at_uniq (the (hw_asid_table next_asid)) pd s \<and> the (hw_asid_table next_asid) \<noteq> 0 \<and> the (hw_asid_table next_asid) \<le> mask local.asid_bits) and (\<lambda>s. True)) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> True)\<rbrace>
 3. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> True)\<rbrace>
 4. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
 5. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q'17 hw_asid_table\<rbrace>
 6. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (6 subgoals):
 1. \<And>hw_asid_table. \<lbrace>?Q17 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> ((\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid (the (hw_asid_table next_asid)) pd s \<and> pd_at_uniq (the (hw_asid_table next_asid)) pd s \<and> the (hw_asid_table next_asid) \<noteq> 0 \<and> the (hw_asid_table next_asid) \<le> mask local.asid_bits) and (\<lambda>s. True)) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> True)\<rbrace>
 2. \<And>hw_asid_table. \<lbrace>?Q'17 hw_asid_table\<rbrace> gets (armKSNextASID \<circ> ksArchState) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) s) \<and> ((\<exists>x2. find (\<lambda>a. hw_asid_table a = None) ([next_asid .e. maxBound] @ init [minBound .e. next_asid]) = Some x2) \<longrightarrow> True)\<rbrace>
 3. \<lbrace>?Q11\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q17 hw_asid_table\<rbrace>
 4. \<lbrace>?Q'11\<rbrace> gets (armKSHWASIDTable \<circ> ksArchState) \<lbrace>\<lambda>hw_asid_table. (\<lambda>_. True) and ?Q'17 hw_asid_table\<rbrace>
 5. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and ?Q11) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'11) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (arm_hwasid_table \<circ> arch_state) s a = None) ([(arm_next_asid \<circ> arch_state) sa .e. maxBound] @ init [minBound .e. (arm_next_asid \<circ> arch_state) sa]) = None \<longrightarrow> ((\<lambda>sb. \<exists>pd. valid_asid_map sb \<and> valid_vspace_objs sb \<and> pspace_aligned sb \<and> pspace_distinct sb \<and> vspace_at_asid (the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) sa))) pd sb \<and> pd_at_uniq (the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) sa))) pd sb \<and> the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) sa)) \<noteq> 0 \<and> the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) sa)) \<le> mask local.asid_bits) and (\<lambda>s. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (arm_hwasid_table \<circ> arch_state) s a = None) ([(arm_next_asid \<circ> arch_state) sa .e. maxBound] @ init [minBound .e. (arm_next_asid \<circ> arch_state) sa]) = Some x2) \<longrightarrow> True))) s)) s
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = Some x2) \<longrightarrow> True))) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_asid_map s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_arch_state s; valid_global_objs s; \<forall>x\<in>{x. arm_next_asid (arch_state s) \<le> x} \<union> set (init [minBound .e. arm_next_asid (arch_state s)]). \<exists>y. arm_hwasid_table (arch_state s) x = Some y\<rbrakk> \<Longrightarrow> \<exists>pd. vspace_at_asid (the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)))) pd s \<and> pd_at_uniq (the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)))) pd s \<and> the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) \<noteq> 0 \<and> the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) \<le> mask local.asid_bits
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = Some x2) \<longrightarrow> True))) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_asid_map s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_arch_state s; valid_global_objs s; \<exists>y. arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y\<rbrakk> \<Longrightarrow> \<exists>pd. vspace_at_asid (the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)))) pd s \<and> pd_at_uniq (the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)))) pd s \<and> the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) \<noteq> 0 \<and> the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))) \<le> mask local.asid_bits
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = Some x2) \<longrightarrow> True))) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>valid_asid_map s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_global_objs s; arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> \<exists>pd. vspace_at_asid y pd s \<and> pd_at_uniq y pd s \<and> y \<noteq> 0 \<and> y \<le> mask local.asid_bits
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = Some x2) \<longrightarrow> True))) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>valid_asid_map s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_global_objs s; arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); (map_option fst \<circ> arm_asid_map (arch_state s)) y = Some (arm_next_asid (arch_state s))\<rbrakk> \<Longrightarrow> \<exists>pd. vspace_at_asid y pd s \<and> pd_at_uniq y pd s \<and> y \<noteq> 0 \<and> y \<le> mask local.asid_bits
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = Some x2) \<longrightarrow> True))) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s y b. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_global_objs s; arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) y = Some (arm_next_asid (arch_state s), b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>pd. vspace_at_asid y pd s \<and> pd_at_uniq y pd s \<and> y \<noteq> 0 \<and> y \<le> mask local.asid_bits
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = Some x2) \<longrightarrow> True))) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s y b. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_global_objs s; arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) y = Some (arm_next_asid (arch_state s), b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0; vspace_at_asid y b s; y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>pd. vspace_at_asid y pd s \<and> pd_at_uniq y pd s \<and> y \<le> mask local.asid_bits
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = Some x2) \<longrightarrow> True))) s)) s proof (prove)
goal (3 subgoals):
 1. \<And>s y b. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_global_objs s; arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) y = Some (arm_next_asid (arch_state s), b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0; vspace_at_asid y b s; y \<noteq> 0\<rbrakk> \<Longrightarrow> y \<le> mask local.asid_bits
 2. \<And>s y b. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_global_objs s; arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) y = Some (arm_next_asid (arch_state s), b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0; vspace_at_asid y b s; y \<noteq> 0; pd_at_uniq y b s\<rbrakk> \<Longrightarrow> \<exists>pd. vspace_at_asid y pd s \<and> pd_at_uniq y pd s \<and> y \<le> mask local.asid_bits
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = Some x2) \<longrightarrow> True))) s)) s proof (prove)
goal (3 subgoals):
 1. \<And>s y b. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_global_objs s; arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) y = Some (arm_next_asid (arch_state s), b); \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0; vspace_at_asid y b s; y \<noteq> 0; y \<in> {0..mask local.asid_bits}\<rbrakk> \<Longrightarrow> y \<le> mask local.asid_bits
 2. \<And>s y b. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_global_objs s; arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) y = Some (arm_next_asid (arch_state s), b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0; vspace_at_asid y b s; y \<noteq> 0; pd_at_uniq y b s\<rbrakk> \<Longrightarrow> \<exists>pd. vspace_at_asid y pd s \<and> pd_at_uniq y pd s \<and> y \<le> mask local.asid_bits
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = Some x2) \<longrightarrow> True))) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s y b. \<lbrakk>valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_global_objs s; arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) y = Some (arm_next_asid (arch_state s), b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0; vspace_at_asid y b s; y \<noteq> 0; pd_at_uniq y b s\<rbrakk> \<Longrightarrow> \<exists>pd. vspace_at_asid y pd s \<and> pd_at_uniq y pd s \<and> y \<le> mask local.asid_bits
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = Some x2) \<longrightarrow> True))) s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s y b. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_vs_lookup s; valid_global_objs s; arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s)) = Some y; valid_asid_table (asid_table s) s; typ_at (AArch APageDirectory) (arm_global_pd (arch_state s)) s; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s)); arm_asid_map (arch_state s) y = Some (arm_next_asid (arch_state s), b); dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0; vspace_at_asid y b s; y \<noteq> 0; pd_at_uniq y b s\<rbrakk> \<Longrightarrow> \<exists>pd. vspace_at_asid y pd s \<and> pd_at_uniq y pd s \<and> y \<le> mask local.asid_bits
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = Some x2) \<longrightarrow> True))) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>_. True)) sa) \<and> ((\<exists>x2. find (\<lambda>a. (armKSHWASIDTable \<circ> ksArchState) s a = None) ([(armKSNextASID \<circ> ksArchState) sa .e. maxBound] @ init [minBound .e. (armKSNextASID \<circ> ksArchState) sa]) = Some x2) \<longrightarrow> True))) s)) s proof (prove)
goal:
No subgoals!