theory Ipc_R

lemma cteInsert_assume_Null:
  "\<lbrace>P\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace> \<Longrightarrow>
   \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) dest s \<longrightarrow> P s\<rbrace>
   cteInsert cap src dest
   \<lbrace>Q\<rbrace>" apply (rule hoare_name_pre_state) apply (erule impCE) apply (simp add: cteInsert_def) apply (rule hoare_seq_ext[OF _ getCTE_sp])+ apply (rule hoare_name_pre_state) apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule hoare_pre(1)) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest s \<longrightarrow> P s\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace>; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace>; \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<lbrace>P\<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 <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- updateCap dest cap;
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>Q\<rbrace>; \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<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 <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- updateCap dest cap;
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>Q\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s srcCTE x. \<lbrakk>\<lbrace>P\<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 <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- updateCap dest cap;
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>Q\<rbrace>; \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest s\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' (\<lambda>c. c = x) dest and (cte_wp_at' (\<lambda>c. c = srcCTE) src and (=) s)\<rbrace> do y <- assert (cteCap x = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer);
y <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- updateCap dest cap;
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>Q\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s srcCTE x sa. \<lbrakk>\<lbrace>P\<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 <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- updateCap dest cap;
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>Q\<rbrace>; \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) dest s; (cte_wp_at' (\<lambda>c. c = x) dest and (cte_wp_at' (\<lambda>c. c = srcCTE) src and (=) s)) sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> do y <- assert (cteCap x = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer);
y <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- updateCap dest cap;
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>Q\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>P\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> cteInsert cap src dest \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>P s; s = sa\<rbrakk> \<Longrightarrow> P sa proof (prove)
goal:
No subgoals!