theory VSpace_R

lemma findFreeHWASID_None_map [wp]:
  "\<lbrace>\<lambda>s. armKSASIDMap (ksArchState s) asid = None\<rbrace>
  findFreeHWASID
  \<lbrace>\<lambda>rv s. armKSASIDMap (ksArchState s) asid = None\<rbrace>" apply (simp add: findFreeHWASID_def invalidateHWASIDEntry_def invalidateASID_def
                   doMachineOp_def split_def
              cong: option.case_cong) apply (rule hoare_pre) apply (wp|wpc|simp split del: if_split)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. armKSASIDMap (ksArchState s) asid = None\<rbrace> findFreeHWASID \<lbrace>\<lambda>rv s. armKSASIDMap (ksArchState s) asid = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. armKSASIDMap (ksArchState s) asid = None\<rbrace> 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 <- do y <- findPDForASIDAssert (the (hwASIDTable nextASID));
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(the (hwASIDTable nextASID) := None)) (ksArchState s)\<rparr>)
od;
y <- do ms <- gets ksMachineState;
p <- select_f (invalidateLocalTLB_ASID nextASID ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od;
y <- do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(nextASID := None)) (ksArchState s)\<rparr>)
od;
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 \<lbrace>\<lambda>rv s. armKSASIDMap (ksArchState s) asid = None\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q7\<rbrace> 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 <- do y <- findPDForASIDAssert (the (hwASIDTable nextASID));
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(the (hwASIDTable nextASID) := None)) (ksArchState s)\<rparr>)
od;
y <- do ms <- gets ksMachineState;
p <- select_f (invalidateLocalTLB_ASID nextASID ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od;
y <- do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(nextASID := None)) (ksArchState s)\<rparr>)
od;
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 \<lbrace>\<lambda>rv s. armKSASIDMap (ksArchState s) asid = None\<rbrace>
 2. \<And>s. armKSASIDMap (ksArchState s) asid = None \<Longrightarrow> ?Q7 s proof (prove)
goal (1 subgoal):
 1. \<And>s. armKSASIDMap (ksArchState s) asid = None \<Longrightarrow> find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = None \<longrightarrow> (\<exists>b. ((), b) \<in> fst (invalidateLocalTLB_ASID (armKSNextASID (ksArchState s)) (ksMachineState s))) \<longrightarrow> (if asid = the (armKSHWASIDTable (ksArchState s) (armKSNextASID (ksArchState s))) then None else armKSASIDMap (ksArchState s) asid) = None proof (prove)
goal:
No subgoals!