theory Ipc_R

lemma cteInsert_cap_to':
  "\<lbrace>ex_nonz_cap_to' p and cte_wp_at' (\<lambda>c. cteCap c = NullCap) dest\<rbrace>
     cteInsert cap src dest
   \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" apply (simp    add: cteInsert_def ex_nonz_cap_to'_def
                      updateCap_def setUntypedCapAsFull_def
           split del: if_split) apply (rule hoare_pre, rule hoare_vcg_ex_lift) apply (wp updateMDB_weak_cte_wp_at
             setCTE_weak_cte_wp_at
           | simp
           | rule hoare_drop_imps)+ apply (wp getCTE_wp) apply clarsimp apply (rule_tac x=cref in exI) apply (rule conjI) apply (clarsimp simp: cte_wp_at_ctes_of)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- if isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap then do cte <- getCTE src;
setCTE src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)) cte)
od else return ();
y <- do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>cref. \<lbrace>?P9 cref\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- if isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap then do cte <- getCTE src;
setCTE src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)) cte)
od else return ();
y <- do cte <- getCTE dest;
setCTE dest (cteCap_update (\<lambda>_. cap) cte)
od;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest) s \<Longrightarrow> \<exists>x. ?P9 x s proof (prove)
goal (2 subgoals):
 1. \<And>cref. \<lbrace>?P'81 cref\<rbrace> getCTE src \<lbrace>\<lambda>rv s. (isUntypedCap (cteCap rv) \<and> isUntypedCap cap \<and> capPtr (cteCap rv) = capPtr cap \<and> capBlockSize (cteCap rv) = capBlockSize cap \<longrightarrow> (cref = src \<longrightarrow> p \<in> zobj_refs' (cteCap rv)) \<and> (cref \<noteq> src \<longrightarrow> cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s)) \<and> ((capPtr (cteCap rv) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap rv) \<longrightarrow> capBlockSize (cteCap rv) \<noteq> capBlockSize cap) \<longrightarrow> cref \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s)\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest) s \<Longrightarrow> \<exists>x. (x = dest \<longrightarrow> p \<in> zobj_refs' cap) \<and> ?P'81 x s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s) and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest) s \<Longrightarrow> \<exists>x. (x = dest \<longrightarrow> p \<in> zobj_refs' cap) \<and> (cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (x = src \<longrightarrow> p \<in> zobj_refs' (cteCap cte)) \<and> (x \<noteq> src \<longrightarrow> cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) x s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> x \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) x s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s; cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrakk> \<Longrightarrow> \<exists>x. (x = dest \<longrightarrow> p \<in> zobj_refs' cap) \<and> (cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (x = src \<longrightarrow> p \<in> zobj_refs' (cteCap cte)) \<and> (x \<noteq> src \<longrightarrow> cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) x s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> x \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) x s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s; cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrakk> \<Longrightarrow> (cref = dest \<longrightarrow> p \<in> zobj_refs' cap) \<and> (cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (cref = src \<longrightarrow> p \<in> zobj_refs' (cteCap cte)) \<and> (cref \<noteq> src \<longrightarrow> cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> cref \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s))) proof (prove)
goal (2 subgoals):
 1. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s; cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrakk> \<Longrightarrow> cref = dest \<longrightarrow> p \<in> zobj_refs' cap
 2. \<And>s cref. \<lbrakk>cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s; cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> (cref = src \<longrightarrow> p \<in> zobj_refs' (cteCap cte)) \<and> (cref \<noteq> src \<longrightarrow> cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> cref \<noteq> dest \<longrightarrow> cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s)) proof (prove)
goal:
No subgoals!