theory ArchVSpace_AI

lemma find_free_hw_asid_pd_at_asid [wp]:
  "\<lbrace>vspace_at_asid pd asid\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. vspace_at_asid pd asid\<rbrace>" apply (simp add: find_free_hw_asid_def invalidate_hw_asid_entry_def invalidate_asid_def
                   do_machine_op_def split_def
              cong: option.case_cong) apply (wp|wpc)+ apply (clarsimp simp: vspace_at_asid_def vs_lookup_arch_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>vspace_at_asid pd asid\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. vspace_at_asid pd asid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>vspace_at_asid pd asid\<rbrace> 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 <- do asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(the (hw_asid_table next_asid) := None)\<rparr>\<rparr>)
od;
y <- do ms <- gets machine_state;
p <- select_f (invalidateLocalTLB_ASID next_asid ms);
modify (machine_state_update (\<lambda>_. snd p))
od;
y <- do hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(next_asid := None)\<rparr>\<rparr>)
od;
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 \<lbrace>\<lambda>_. vspace_at_asid pd asid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. vspace_at_asid pd asid s \<Longrightarrow> (find (\<lambda>a. (arm_hwasid_table \<circ> arch_state) s a = None) (take (Suc (unat maxBound) - unat minBound) [(arm_next_asid \<circ> arch_state) s .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat ((arm_next_asid \<circ> arch_state) s)))) [minBound .e. (arm_next_asid \<circ> arch_state) s]) = None \<longrightarrow> (\<forall>x\<in>fst (invalidateLocalTLB_ASID ((arm_next_asid \<circ> arch_state) s) (machine_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>\<rparr>))). vspace_at_asid pd asid (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x\<rparr>)\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x\<rparr>))((arm_next_asid \<circ> arch_state) s := None)\<rparr>, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x\<rparr>)\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(the ((arm_hwasid_table \<circ> arch_state) s ((arm_next_asid \<circ> arch_state) s)) := None)\<rparr>, machine_state := snd x\<rparr>))((arm_next_asid \<circ> arch_state) s := None)\<rparr>\<rparr>)\<lparr>arm_next_asid := (arm_next_asid \<circ> arch_state) s + 1\<rparr>\<rparr>))) \<and> (\<forall>x. find (\<lambda>a. (arm_hwasid_table \<circ> arch_state) s a = None) (take (Suc (unat maxBound) - unat minBound) [(arm_next_asid \<circ> arch_state) s .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat ((arm_next_asid \<circ> arch_state) s)))) [minBound .e. (arm_next_asid \<circ> arch_state) s]) = Some x \<longrightarrow> vspace_at_asid pd asid s) proof (prove)
goal:
No subgoals!