theory CSpace_R

lemma cteInsert_iflive'[wp]:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s
      \<and> cte_wp_at' (\<lambda>c. cteCap c = NullCap) dest s\<rbrace>
     cteInsert cap src dest
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: cteInsert_def split del: if_split) apply (wp updateCap_iflive' hoare_drop_imps) apply (clarsimp simp:cte_wp_at_ctes_of) apply (wp hoare_vcg_conj_lift hoare_vcg_ex_lift hoare_vcg_ball_lift getCTE_wp
                 setUntypedCapAsFull_ctes_of setUntypedCapAsFull_if_live_then_nonz_cap')+ apply (clarsimp simp:cte_wp_at_ctes_of) apply (intro conjI) apply (rule_tac x = "case (ctes_of s dest) of Some a \<Rightarrow>a" in exI) apply (clarsimp) apply (case_tac cte,simp) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest 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>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>srcCTE x y ya. \<lbrace>?B4 srcCTE x y ya\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>yb s. cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' cap. ko_wp_at' (Not \<circ> live') p' s) dest s \<and> if_live_then_nonz_cap' s\<rbrace>
 2. \<And>srcCTE x y. \<lbrace>?B3 srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B4 srcCTE x y\<rbrace>
 3. \<And>srcCTE x. \<lbrace>?B2 srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B3 srcCTE x\<rbrace>
 4. \<And>srcCTE. \<lbrace>?B1 srcCTE\<rbrace> getCTE dest \<lbrace>?B2 srcCTE\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE src \<lbrace>?B1\<rbrace>
 6. \<And>s. if_live_then_nonz_cap' s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>srcCTE x. \<lbrace>?B4 srcCTE x () ()\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>yb s. (\<exists>cte. ctes_of s dest = Some cte \<and> (\<forall>p'\<in>zobj_refs' (cteCap cte) - zobj_refs' cap. ko_wp_at' (Not \<circ> live') p' s)) \<and> if_live_then_nonz_cap' s\<rbrace>
 2. \<And>srcCTE x y. \<lbrace>?B3 srcCTE x y\<rbrace> assert (mdbPrev (cteMDBNode x) = nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B4 srcCTE x y\<rbrace>
 3. \<And>srcCTE x. \<lbrace>?B2 srcCTE x\<rbrace> assert (cteCap x = capability.NullCap) \<lbrace>?B3 srcCTE x\<rbrace>
 4. \<And>srcCTE. \<lbrace>?B1 srcCTE\<rbrace> getCTE dest \<lbrace>?B2 srcCTE\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE src \<lbrace>?B1\<rbrace>
 6. \<And>s. if_live_then_nonz_cap' s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. if_live_then_nonz_cap' s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s \<Longrightarrow> (\<exists>x. (cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>ctea. cte_wp_at' ((=) ctea) dest s \<and> (cteCap ctea = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> src \<noteq> dest \<and> ctes_of s dest = Some x \<or> src = dest \<and> Some (CTE (maskedAsFull (cteCap cte) cap) (cteMDBNode cte)) = Some x \<and> cte_wp_at' ((=) cte) src s))))) \<and> (\<forall>x\<in>zobj_refs' (cteCap x) - zobj_refs' cap. cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) dest s \<and> (cteCap cte = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> ko_wp_at' (Not \<circ> live') x s)))))) \<and> (cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) dest s \<and> (cteCap cte = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> if_live_then_nonz_cap' s))))) \<and> (cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>ctea. cte_wp_at' ((=) ctea) dest s \<and> (cteCap ctea = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> cte_wp_at' ((=) cte) src s))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>if_live_then_nonz_cap' s; ctes_of s dest = Some cte; cteCap cte = capability.NullCap\<rbrakk> \<Longrightarrow> (\<exists>x. ((\<exists>cte. ctes_of s src = Some cte) \<longrightarrow> (\<exists>ctea. ctes_of s src = Some ctea \<and> (mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> src \<noteq> dest \<and> cte = x \<or> src = dest \<and> CTE (maskedAsFull (cteCap ctea) cap) (cteMDBNode ctea) = x \<and> ctes_of s src = Some ctea))) \<and> ((\<exists>cte. ctes_of s src = Some cte) \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<forall>x\<in>zobj_refs' (cteCap x) - zobj_refs' cap. ko_wp_at' (\<lambda>a. \<not> live' a) x s))) \<and> ((\<exists>cte. ctes_of s src = Some cte) \<longrightarrow> (\<exists>ctea. ctes_of s src = Some ctea \<and> (mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> ctes_of s src = Some ctea))) proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>if_live_then_nonz_cap' s; ctes_of s dest = Some cte; cteCap cte = capability.NullCap\<rbrakk> \<Longrightarrow> \<exists>x. ((\<exists>cte. ctes_of s src = Some cte) \<longrightarrow> (\<exists>ctea. ctes_of s src = Some ctea \<and> (mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> src \<noteq> dest \<and> cte = x \<or> src = dest \<and> CTE (maskedAsFull (cteCap ctea) cap) (cteMDBNode ctea) = x \<and> ctes_of s src = Some ctea))) \<and> ((\<exists>cte. ctes_of s src = Some cte) \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<forall>x\<in>zobj_refs' (cteCap x) - zobj_refs' cap. ko_wp_at' (\<lambda>a. \<not> live' a) x s))
 2. \<And>s cte. \<lbrakk>if_live_then_nonz_cap' s; ctes_of s dest = Some cte; cteCap cte = capability.NullCap\<rbrakk> \<Longrightarrow> (\<exists>cte. ctes_of s src = Some cte) \<longrightarrow> (\<exists>ctea. ctes_of s src = Some ctea \<and> (mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> ctes_of s src = Some ctea)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>if_live_then_nonz_cap' s; ctes_of s dest = Some cte; cteCap cte = capability.NullCap\<rbrakk> \<Longrightarrow> ((\<exists>cte. ctes_of s src = Some cte) \<longrightarrow> (\<exists>ctea. ctes_of s src = Some ctea \<and> (mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> src \<noteq> dest \<and> cte = (case ctes_of s dest of Some a \<Rightarrow> a) \<or> src = dest \<and> CTE (maskedAsFull (cteCap ctea) cap) (cteMDBNode ctea) = (case ctes_of s dest of Some a \<Rightarrow> a) \<and> ctes_of s src = Some ctea))) \<and> ((\<exists>cte. ctes_of s src = Some cte) \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<forall>x\<in>zobj_refs' (cteCap (case ctes_of s dest of Some a \<Rightarrow> a)) - zobj_refs' cap. ko_wp_at' (\<lambda>a. \<not> live' a) x s))
 2. \<And>s cte. \<lbrakk>if_live_then_nonz_cap' s; ctes_of s dest = Some cte; cteCap cte = capability.NullCap\<rbrakk> \<Longrightarrow> (\<exists>cte. ctes_of s src = Some cte) \<longrightarrow> (\<exists>ctea. ctes_of s src = Some ctea \<and> (mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> ctes_of s src = Some ctea)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>if_live_then_nonz_cap' s; cteCap cte = capability.NullCap; ctes_of s dest = Some cte; mdbPrev (cteMDBNode cte) = nullPointer; mdbNext (cteMDBNode cte) = nullPointer; src = dest\<rbrakk> \<Longrightarrow> CTE capability.NullCap (cteMDBNode cte) = cte
 2. \<And>s cte. \<lbrakk>if_live_then_nonz_cap' s; ctes_of s dest = Some cte; cteCap cte = capability.NullCap\<rbrakk> \<Longrightarrow> (\<exists>cte. ctes_of s src = Some cte) \<longrightarrow> (\<exists>ctea. ctes_of s src = Some ctea \<and> (mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> ctes_of s src = Some ctea)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>if_live_then_nonz_cap' s; ctes_of s dest = Some cte; cteCap cte = capability.NullCap\<rbrakk> \<Longrightarrow> (\<exists>cte. ctes_of s src = Some cte) \<longrightarrow> (\<exists>ctea. ctes_of s src = Some ctea \<and> (mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> ctes_of s src = Some ctea)) proof (prove)
goal:
No subgoals!