theory CNodeInv_R

lemma cteMove_iflive'[wp]:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s
      \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s
      \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> NullCap) src s
      \<and> cte_wp_at' (\<lambda>c. cteCap c = NullCap) dest s\<rbrace>
     cteMove cap src dest
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" unfolding cteMove_def apply simp apply wp apply (simp only: if_live_then_nonz_cap'_def imp_conv_disj
                          ex_nonz_cap_to'_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift
                  hoare_vcg_ex_lift updateCap_cte_wp_at_cases
                  getCTE_wp hoare_weak_lift_imp)+ apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule(1) if_live_then_nonz_capE') apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (drule_tac x="(id (src := dest, dest := src)) cref" in spec) apply (clarsimp dest!: weak_derived_zobj split: if_split_asm) 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. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s\<rbrace> cteMove 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. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s\<rbrace> do oldCTE <- getCTE dest;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE src;
mdb <- return (cteMDBNode cte);
updateCap dest cap;
updateCap src capability.NullCap;
updateMDB dest (const mdb);
updateMDB src (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. dest))
od \<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. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s\<rbrace> do oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
cte <- getCTE src;
y <- updateCap dest cap;
y <- updateCap src capability.NullCap;
y <- updateMDB dest (const (cteMDBNode cte));
y <- updateMDB src (const nullMDBNode);
y <- updateMDB (mdbPrev (cteMDBNode cte)) (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode cte)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>oldCTE y ya cte yb. \<lbrace>?B5 oldCTE y ya cte yb\<rbrace> updateCap src capability.NullCap \<lbrace>\<lambda>yc. if_live_then_nonz_cap'\<rbrace>
 2. \<And>oldCTE y ya cte. \<lbrace>?B4 oldCTE y ya cte\<rbrace> updateCap dest cap \<lbrace>?B5 oldCTE y ya cte\<rbrace>
 3. \<And>oldCTE y ya. \<lbrace>?B3 oldCTE y ya\<rbrace> getCTE src \<lbrace>?B4 oldCTE y ya\<rbrace>
 4. \<And>oldCTE y. \<lbrace>?B2 oldCTE y\<rbrace> assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) \<lbrace>?B3 oldCTE y\<rbrace>
 5. \<And>oldCTE. \<lbrace>?B1 oldCTE\<rbrace> assert (cteCap oldCTE = capability.NullCap) \<lbrace>?B2 oldCTE\<rbrace>
 6. \<lbrace>?Q\<rbrace> getCTE dest \<lbrace>?B1\<rbrace>
 7. \<And>s. if_live_then_nonz_cap' s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>oldCTE y ya cte yb. \<lbrace>?B5 oldCTE y ya cte yb\<rbrace> updateCap src capability.NullCap \<lbrace>\<lambda>yc s. \<forall>ptr. \<not> ko_wp_at' live' ptr s \<or> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)\<rbrace>
 2. \<And>oldCTE y ya cte. \<lbrace>?B4 oldCTE y ya cte\<rbrace> updateCap dest cap \<lbrace>?B5 oldCTE y ya cte\<rbrace>
 3. \<And>oldCTE y ya. \<lbrace>?B3 oldCTE y ya\<rbrace> getCTE src \<lbrace>?B4 oldCTE y ya\<rbrace>
 4. \<And>oldCTE y. \<lbrace>?B2 oldCTE y\<rbrace> assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) \<lbrace>?B3 oldCTE y\<rbrace>
 5. \<And>oldCTE. \<lbrace>?B1 oldCTE\<rbrace> assert (cteCap oldCTE = capability.NullCap) \<lbrace>?B2 oldCTE\<rbrace>
 6. \<lbrace>?Q\<rbrace> getCTE dest \<lbrace>?B1\<rbrace>
 7. \<And>s. if_live_then_nonz_cap' s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) src 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. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s \<Longrightarrow> \<forall>x. (cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) dest s \<and> (mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> \<not> ko_wp_at' live' x s)))) \<or> (\<exists>xa. cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) dest s \<and> (mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (src = xa \<longrightarrow> (dest = xa \<longrightarrow> cte_wp_at' ((\<lambda>c. x \<in> zobj_refs' (cteCap c)) \<circ> cteCap_update (K capability.NullCap) \<circ> cteCap_update (K cap)) xa s) \<and> (dest \<noteq> xa \<longrightarrow> cte_wp_at' ((\<lambda>c. x \<in> zobj_refs' (cteCap c)) \<circ> cteCap_update (K capability.NullCap)) xa s)) \<and> (src \<noteq> xa \<longrightarrow> (dest = xa \<longrightarrow> cte_wp_at' ((\<lambda>c. x \<in> zobj_refs' (cteCap c)) \<circ> cteCap_update (K cap)) xa s) \<and> (dest \<noteq> xa \<longrightarrow> cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb x. \<lbrakk>if_live_then_nonz_cap' s; weak_derived' (cteCap cte) cap; ctes_of s src = Some cte; cteCap cte \<noteq> capability.NullCap; cteCap cteb = capability.NullCap; ctes_of s dest = Some cteb; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; \<forall>xa. src = xa \<or> src \<noteq> xa \<and> (dest = xa \<and> (ctes_of s xa = None \<or> x \<notin> zobj_refs' cap) \<or> dest \<noteq> xa \<and> (\<forall>cte. ctes_of s xa = Some cte \<longrightarrow> x \<notin> zobj_refs' (cteCap cte))); ko_wp_at' live' x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb x. \<lbrakk>weak_derived' (cteCap cte) cap; ctes_of s src = Some cte; cteCap cte \<noteq> capability.NullCap; cteCap cteb = capability.NullCap; ctes_of s dest = Some cteb; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; \<forall>xa. src = xa \<or> src \<noteq> xa \<and> (dest = xa \<and> (ctes_of s xa = None \<or> x \<notin> zobj_refs' cap) \<or> dest \<noteq> xa \<and> (\<forall>cte. ctes_of s xa = Some cte \<longrightarrow> x \<notin> zobj_refs' (cteCap cte))); ko_wp_at' live' x s; ex_nonz_cap_to' x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb x cref ctea. \<lbrakk>weak_derived' (cteCap cte) cap; ctes_of s src = Some cte; cteCap cte \<noteq> capability.NullCap; cteCap cteb = capability.NullCap; ctes_of s dest = Some cteb; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; \<forall>xa. src = xa \<or> src \<noteq> xa \<and> (dest = xa \<and> (ctes_of s xa = None \<or> x \<notin> zobj_refs' cap) \<or> dest \<noteq> xa \<and> (\<forall>cte. ctes_of s xa = Some cte \<longrightarrow> x \<notin> zobj_refs' (cteCap cte))); ko_wp_at' live' x s; ctes_of s cref = Some ctea; x \<in> zobj_refs' (cteCap ctea)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb x cref ctea. \<lbrakk>weak_derived' (cteCap cte) cap; ctes_of s src = Some cte; cteCap cte \<noteq> capability.NullCap; cteCap cteb = capability.NullCap; ctes_of s dest = Some cteb; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; ko_wp_at' live' x s; ctes_of s cref = Some ctea; x \<in> zobj_refs' (cteCap ctea); src = (id(src := dest, dest := src)) cref \<or> src \<noteq> (id(src := dest, dest := src)) cref \<and> (dest = (id(src := dest, dest := src)) cref \<and> (ctes_of s ((id(src := dest, dest := src)) cref) = None \<or> x \<notin> zobj_refs' cap) \<or> dest \<noteq> (id(src := dest, dest := src)) cref \<and> (\<forall>cte. ctes_of s ((id(src := dest, dest := src)) cref) = Some cte \<longrightarrow> x \<notin> zobj_refs' (cteCap cte)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!