theory ArchVSpace_AI

lemma find_free_hw_asid_pd_at_uniq [wp]:
  "\<lbrace>pd_at_uniq pd asid\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. pd_at_uniq 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: pd_at_uniq_def ran_option_map
                 dest!: ran_restrictD split: if_split_asm) apply (rule ccontr, erule notE, rule image_eqI[rotated],
         rule ranI) apply (fastforce simp add: restrict_map_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pd_at_uniq pd asid\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. pd_at_uniq pd asid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pd_at_uniq 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>_. pd_at_uniq pd asid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pd_at_uniq 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>))). pd_at_uniq 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> pd_at_uniq pd asid s) proof (prove)
goal (1 subgoal):
 1. \<And>s b a x. \<lbrakk>asid \<notin> snd ` ran (arm_asid_map (arch_state s) |` (- {pd})); find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); x \<noteq> the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))); arm_asid_map (arch_state s) x = Some (a, asid)\<rbrakk> \<Longrightarrow> x = pd proof (prove)
goal (2 subgoals):
 1. \<And>s b a x. \<lbrakk>find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); x \<noteq> the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))); arm_asid_map (arch_state s) x = Some (a, asid); x \<noteq> pd\<rbrakk> \<Longrightarrow> (arm_asid_map (arch_state s) |` (- {pd})) (?a83 s b a x) = Some (?x80 s b a x)
 2. \<And>s b a x. \<lbrakk>find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); x \<noteq> the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))); arm_asid_map (arch_state s) x = Some (a, asid); x \<noteq> pd\<rbrakk> \<Longrightarrow> asid = snd (?x80 s b a x) proof (prove)
goal (1 subgoal):
 1. \<And>s b a x. \<lbrakk>find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = None; ((), b) \<in> fst (invalidateLocalTLB_ASID (arm_next_asid (arch_state s)) (machine_state s)); x \<noteq> the (arm_hwasid_table (arch_state s) (arm_next_asid (arch_state s))); arm_asid_map (arch_state s) x = Some (a, asid); x \<noteq> pd\<rbrakk> \<Longrightarrow> asid = snd (a, asid) proof (prove)
goal:
No subgoals!