theory Untyped_R

lemma updateFreeIndex_cte_wp_at:
  "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. P (cteCap_update (if p = slot
      then capFreeIndex_update (\<lambda>_. idx) else id) c)) p s\<rbrace>
    updateFreeIndex slot idx
  \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>" apply (simp add: updateFreeIndex_def updateTrackedFreeIndex_def getSlotCap_def split del: if_split) apply (rule hoare_pre, wp updateCap_cte_wp_at' getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac "the (ctes_of s p)") apply (auto split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>c. P (cteCap_update (if p = slot then capFreeIndex_update (\<lambda>_. idx) else id) c)) p\<rbrace> updateFreeIndex slot idx \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>c. P (cteCap_update (if p = slot then capFreeIndex_update (\<lambda>_. idx) else id) c)) p\<rbrace> do y <- do cte <- getCTE slot;
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 slot;
updateCap slot (capFreeIndex_update (\<lambda>_. idx) (cteCap cte))
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>c. P (cteCap_update (if p = slot then capFreeIndex_update (\<lambda>_. idx) else id) c)) p s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) slot s \<longrightarrow> (\<forall>ctea. cte_wp_at' ((=) ctea) slot (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>_. True) slot (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>cte. if p = slot then P (CTE (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) (cteMDBNode cte)) else P cte) 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 cte ctea. \<lbrakk>ctes_of s p = Some cte; P (cteCap_update (if p = slot then capFreeIndex_update (\<lambda>_. idx) else id) cte); ctes_of s slot = Some ctea\<rbrakk> \<Longrightarrow> \<exists>cteb. (p = slot \<longrightarrow> ctea = cteb \<and> P (CTE (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) (cteMDBNode cteb))) \<and> (p \<noteq> slot \<longrightarrow> cte = cteb \<and> P cteb) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea x1 x2. \<lbrakk>ctes_of s p = Some cte; P (cteCap_update (if p = slot then capFreeIndex_update (\<lambda>_. idx) else id) cte); ctes_of s slot = Some ctea; the (ctes_of s p) = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>cteb. (p = slot \<longrightarrow> ctea = cteb \<and> P (CTE (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) (cteMDBNode cteb))) \<and> (p \<noteq> slot \<longrightarrow> cte = cteb \<and> P cteb) proof (prove)
goal:
No subgoals!