theory Untyped_R

lemma updateFreeIndex_cte_cap_wp_to'[wp]:
  "\<lbrace>\<lambda>s. cte_wp_at' (isUntypedCap o cteCap) p s
        \<and> ex_cte_cap_wp_to' P p' s\<rbrace>
     updateFreeIndex p idx
   \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P p'\<rbrace>" apply (simp add: updateFreeIndex_def updateTrackedFreeIndex_def getSlotCap_def) apply (wp updateCap_cte_cap_wp_to' getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of) apply (clarsimp simp: isCap_simps ex_cte_cap_wp_to'_def split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (isUntypedCap \<circ> cteCap) p s \<and> ex_cte_cap_wp_to' P p' s\<rbrace> updateFreeIndex p idx \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P p'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (isUntypedCap \<circ> cteCap) p s \<and> ex_cte_cap_wp_to' P p' s\<rbrace> do y <- do cte <- getCTE p;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cte <- getCTE p;
updateCap p (capFreeIndex_update (\<lambda>_. idx) (cteCap cte))
od \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P p'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (isUntypedCap \<circ> cteCap) p s \<and> ex_cte_cap_wp_to' P p' s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) p s \<longrightarrow> (\<forall>ctea. cte_wp_at' ((=) ctea) p (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>) \<longrightarrow> cte_wp_at' (\<lambda>cteb. p' \<in> cte_refs' (cteCap cteb) (irq_node' (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>)) \<and> P (cteCap cteb) \<longrightarrow> p' \<in> cte_refs' (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) (irq_node' (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>)) \<and> P (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea))) p (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>) \<and> ex_cte_cap_wp_to' P p' (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s ctea. \<lbrakk>ex_cte_cap_wp_to' P p' s; isUntypedCap (cteCap ctea); ctes_of s p = Some ctea\<rbrakk> \<Longrightarrow> (p' \<in> cte_refs' (cteCap ctea) (irq_node' s) \<and> P (cteCap ctea) \<longrightarrow> P (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea))) \<and> ex_cte_cap_wp_to' P p' (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) of None \<Rightarrow> case untypedZeroRange (cteCap ctea) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (cteCap ctea) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})\<rparr>) proof (prove)
goal:
No subgoals!