theory Finalise_R

lemma updateFreeIndex_cte_wp_at:
  "\<lbrace>\<lambda>s. cte_at' p s \<and> P (cte_wp_at' (if p = p' then P'
      o (cteCap_update (capFreeIndex_update (K idx))) else P') p' s)\<rbrace>
    updateFreeIndex p idx
  \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p' s)\<rbrace>" apply (simp add: updateFreeIndex_def updateTrackedFreeIndex_def
        split del: if_split) apply (rule hoare_pre) apply (wp updateCap_cte_wp_at' getSlotCap_wp) apply (clarsimp simp: cte_wp_at_ctes_of) apply (cases "p' = p", simp_all) apply (case_tac cte, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>_. True) p s \<and> P (cte_wp_at' (if p = p' then P' \<circ> cteCap_update (capFreeIndex_update (K idx)) else P') p' s)\<rbrace> updateFreeIndex p idx \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>_. True) p s \<and> P (cte_wp_at' (if p = p' then P' \<circ> cteCap_update (capFreeIndex_update (\<lambda>y. idx)) else P') p' s)\<rbrace> do y <- do cap <- getSlotCap p;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cap <- getSlotCap p;
updateCap p (capFreeIndex_update (\<lambda>_. idx) cap)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p' s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> do y <- do cap <- getSlotCap p;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cap <- getSlotCap p;
updateCap p (capFreeIndex_update (\<lambda>_. idx) cap)
od \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p' s)\<rbrace>
 2. \<And>s. cte_wp_at' (\<lambda>_. True) p s \<and> P (cte_wp_at' (if p = p' then P' \<circ> cteCap_update (capFreeIndex_update (\<lambda>y. idx)) else P') p' s) \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>_. True) p s \<and> P (cte_wp_at' (if p = p' then P' \<circ> cteCap_update (capFreeIndex_update (\<lambda>y. idx)) else P') p' s) \<Longrightarrow> \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) p s \<and> (\<exists>capa. cte_wp_at' (\<lambda>c. cteCap c = capa) p (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>) \<and> (cte_wp_at' (\<lambda>_. True) p (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>) \<longrightarrow> P (cte_wp_at' (\<lambda>cte. if p' = p then P' (CTE (capFreeIndex_update (\<lambda>_. idx) capa) (cteMDBNode cte)) else P' cte) p' (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>P (\<exists>cte. ctes_of s p' = Some cte \<and> (if p = p' then P' \<circ> cteCap_update (capFreeIndex_update (\<lambda>y. idx)) else P') cte); ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> P (\<exists>ctea. (p' = p \<longrightarrow> cte = ctea \<and> P' (CTE (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) (cteMDBNode ctea))) \<and> (p' \<noteq> p \<longrightarrow> ctes_of s p' = Some ctea \<and> P' ctea)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>P (P' (cteCap_update (capFreeIndex_update (\<lambda>y. idx)) cte)); ctes_of s p = Some cte; p' = p\<rbrakk> \<Longrightarrow> P (P' (CTE (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) (cteMDBNode cte))) proof (prove)
goal:
No subgoals!