theory Finalise_R

lemma clearUntypedFreeIndex_noop_corres:
  "corres dc \<top> (cte_at' (cte_map slot))
    (return ()) (clearUntypedFreeIndex (cte_map slot))" apply (simp add: clearUntypedFreeIndex_def) apply (rule corres_guard_imp) apply (rule corres_bind_return2) apply (rule corres_symb_exec_r_conj[where P'="cte_at' (cte_map slot)"]) apply (rule corres_trivial, simp) apply (wp getCTE_wp' | wpc
        | simp add: updateTrackedFreeIndex_def getSlotCap_def)+ apply (clarsimp simp: state_relation_def) apply (rule no_fail_pre) apply (wp no_fail_getSlotCap getCTE_wp'
       | wpc | simp add: updateTrackedFreeIndex_def getSlotCap_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (cte_wp_at' (\<lambda>_. True) (cte_map slot)) (return ()) (clearUntypedFreeIndex (cte_map slot)) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (cte_wp_at' (\<lambda>_. True) (cte_map slot)) (return ()) (do cap <- getSlotCap (cte_map slot);
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex (cte_map slot) (maxFreeIndex (capBlockSize cap)) | _ \<Rightarrow> return ()
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (return ()) (do cap <- getSlotCap (cte_map slot);
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex (cte_map slot) (maxFreeIndex (capBlockSize cap)) | _ \<Rightarrow> return ()
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. cte_wp_at' (\<lambda>_. True) (cte_map slot) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (return ()) (do cap <- getSlotCap (cte_map slot);
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex (cte_map slot) (maxFreeIndex (capBlockSize cap)) | _ \<Rightarrow> return ()
od >>= return)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. cte_wp_at' (\<lambda>_. True) (cte_map slot) s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>rv. corres dc ?Q (?R'6 rv) (return ()) (return rv)
 2. \<lbrace>?Q'6\<rbrace> do cap <- getSlotCap (cte_map slot);
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex (cte_map slot) (maxFreeIndex (capBlockSize cap)) | _ \<Rightarrow> return ()
od \<lbrace>?R'6\<rbrace>
 3. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s'\<rbrace> do cap <- getSlotCap (cte_map slot);
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex (cte_map slot) (maxFreeIndex (capBlockSize cap)) | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 4. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (do cap <- getSlotCap (cte_map slot);
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex (cte_map slot) (maxFreeIndex (capBlockSize cap)) | _ \<Rightarrow> return ()
od)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. cte_wp_at' (\<lambda>_. True) (cte_map slot) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map slot) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q'6\<rbrace> do cap <- getSlotCap (cte_map slot);
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex (cte_map slot) (maxFreeIndex (capBlockSize cap)) | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s'\<rbrace> do cap <- getSlotCap (cte_map slot);
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex (cte_map slot) (maxFreeIndex (capBlockSize cap)) | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv s'. (s, s') \<in> state_relation\<rbrace>
 3. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (do cap <- getSlotCap (cte_map slot);
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex (cte_map slot) (maxFreeIndex (capBlockSize cap)) | _ \<Rightarrow> return ()
od)
 4. \<And>s. True \<Longrightarrow> True
 5. \<And>s. cte_wp_at' (\<lambda>_. True) (cte_map slot) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map slot) and ?Q'6) s proof (prove)
goal (4 subgoals):
 1. \<And>s sa. (s, sa) \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) sa \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (cte_map slot) sa \<longrightarrow> (\<forall>x xa xb. (\<exists>xc. cteCap cte = capability.UntypedCap x xa xb xc) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) (cte_map slot) sa \<longrightarrow> (s, sa\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. max_free_index xb) (cteCap cte)) of None \<Rightarrow> case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges sa | Some r \<Rightarrow> gsUntypedZeroRanges sa - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges sa | Some r \<Rightarrow> gsUntypedZeroRanges sa - {r})\<rparr>) \<in> state_relation))
 2. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (do cap <- getSlotCap (cte_map slot);
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex (cte_map slot) (maxFreeIndex (capBlockSize cap)) | _ \<Rightarrow> return ()
od)
 3. \<And>s. True \<Longrightarrow> True
 4. \<And>s. cte_wp_at' (\<lambda>_. True) (cte_map slot) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map slot) and (\<lambda>_. True)) s proof (prove)
goal (3 subgoals):
 1. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) s') (do cap <- getSlotCap (cte_map slot);
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex (cte_map slot) (maxFreeIndex (capBlockSize cap)) | _ \<Rightarrow> return ()
od)
 2. \<And>s. True \<Longrightarrow> True
 3. \<And>s. cte_wp_at' (\<lambda>_. True) (cte_map slot) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map slot) and (\<lambda>_. True)) s proof (prove)
goal (4 subgoals):
 1. \<And>s. True \<Longrightarrow> no_fail (?P133 s) (do cap <- getSlotCap (cte_map slot);
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex (cte_map slot) (maxFreeIndex (capBlockSize cap)) | _ \<Rightarrow> return ()
od)
 2. \<And>s sa. \<lbrakk>True; (s, sa) \<in> state_relation \<and> cte_wp_at' (\<lambda>_. True) (cte_map slot) sa\<rbrakk> \<Longrightarrow> ?P133 s sa
 3. \<And>s. True \<Longrightarrow> True
 4. \<And>s. cte_wp_at' (\<lambda>_. True) (cte_map slot) s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (cte_map slot) and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!