theory Untyped_R

lemma updateNewFreeIndex_noop_psp_corres:
  "corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} False True
    dc \<top> (cte_at' slot)
    (return ()) (updateNewFreeIndex slot)" apply (simp add: updateNewFreeIndex_def) apply (rule corres_guard_imp) apply (rule corres_bind_return2) apply (rule corres_symb_exec_r_conj[where P'="cte_at' slot"]) apply (rule corres_trivial, simp) apply (wp getCTE_wp' | wpc
        | simp add: updateTrackedFreeIndex_def getSlotCap_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} False True dc (\<lambda>_. True) (cte_wp_at' (\<lambda>_. True) slot) (return ()) (updateNewFreeIndex slot) proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} False True dc (\<lambda>_. True) (cte_wp_at' (\<lambda>_. True) slot) (return ()) (do cap <- getSlotCap slot;
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex cap) | _ \<Rightarrow> return ()
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} False True dc ?Q ?Q' (return ()) (do cap <- getSlotCap slot;
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex cap) | _ \<Rightarrow> return ()
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. cte_wp_at' (\<lambda>_. True) slot s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} False True dc ?Q ?Q' (return ()) (do cap <- getSlotCap slot;
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex cap) | _ \<Rightarrow> return ()
od >>= return)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. cte_wp_at' (\<lambda>_. True) slot s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>rv. corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} False True dc ?Q (?R'6 rv) (return ()) (return rv)
 2. \<lbrace>?Q'6\<rbrace> do cap <- getSlotCap slot;
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex cap) | _ \<Rightarrow> return ()
od \<lbrace>?R'6\<rbrace>
 3. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} \<and> cte_wp_at' (\<lambda>_. True) slot s'\<rbrace> do cap <- getSlotCap slot;
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex cap) | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv s'. (s, s') \<in> {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')}\<rbrace>
 4. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} \<and> cte_wp_at' (\<lambda>_. True) slot s') (do cap <- getSlotCap slot;
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex cap) | _ \<Rightarrow> return ()
od)
 5. \<And>s. True \<Longrightarrow> ?Q s
 6. \<And>s. cte_wp_at' (\<lambda>_. True) slot s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q'6\<rbrace> do cap <- getSlotCap slot;
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex cap) | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>s. \<lbrace>\<lambda>s'. (s, s') \<in> {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} \<and> cte_wp_at' (\<lambda>_. True) slot s'\<rbrace> do cap <- getSlotCap slot;
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex cap) | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv s'. (s, s') \<in> {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')}\<rbrace>
 3. \<And>s. True \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} \<and> cte_wp_at' (\<lambda>_. True) slot s') (do cap <- getSlotCap slot;
case cap of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (capFreeIndex cap) | _ \<Rightarrow> return ()
od)
 4. \<And>s. True \<Longrightarrow> True
 5. \<And>s. cte_wp_at' (\<lambda>_. True) slot s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) slot and ?Q'6) s proof (prove)
goal:
No subgoals!