theory CSpace_R

lemma setCTE_iflive':
  "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte')
                          - zobj_refs' (cteCap cte).
                                ko_wp_at' (Not \<circ> live') p' s) p s
      \<and> if_live_then_nonz_cap' s\<rbrace>
     setCTE p cte
   \<lbrace>\<lambda>rv s. if_live_then_nonz_cap' s\<rbrace>" unfolding if_live_then_nonz_cap'_def ex_nonz_cap_to'_def apply (rule hoare_pre) apply (simp only: imp_conv_disj) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift
             hoare_vcg_ex_lift setCTE_weak_cte_wp_at) apply clarsimp apply (drule spec, drule(1) mp) apply clarsimp apply (rule_tac x=cref in exI) apply (clarsimp simp: cte_wp_at'_def) apply (rule ccontr) apply (drule bspec, fastforce) apply (clarsimp simp: ko_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p' s) p s \<and> if_live_then_nonz_cap' s\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p' s) p s \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s))\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. \<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. \<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)\<rbrace>
 2. \<And>s. cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p' s) p s \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setCTE p cte \<lbrace>\<lambda>rv 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>s. cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p' s) p s \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p' s) p s \<and> (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<Longrightarrow> \<forall>x. \<not> ko_wp_at' live' x s \<or> (\<exists>xa. if xa = p then x \<in> zobj_refs' (cteCap cte) else cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p' s) p s; \<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s); ko_wp_at' live' x s\<rbrakk> \<Longrightarrow> \<exists>xa. (xa = p \<longrightarrow> x \<in> zobj_refs' (cteCap cte)) \<and> (xa \<noteq> p \<longrightarrow> cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p' s) p s; ko_wp_at' live' x s; \<exists>cref. cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) cref s\<rbrakk> \<Longrightarrow> \<exists>xa. (xa = p \<longrightarrow> x \<in> zobj_refs' (cteCap cte)) \<and> (xa \<noteq> p \<longrightarrow> cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s) proof (prove)
goal (1 subgoal):
 1. \<And>s x cref. \<lbrakk>cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p' s) p s; ko_wp_at' live' x s; cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) cref s\<rbrakk> \<Longrightarrow> \<exists>xa. (xa = p \<longrightarrow> x \<in> zobj_refs' (cteCap cte)) \<and> (xa \<noteq> p \<longrightarrow> cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s) proof (prove)
goal (1 subgoal):
 1. \<And>s x cref. \<lbrakk>cte_wp_at' (\<lambda>cte'. \<forall>p'\<in>zobj_refs' (cteCap cte') - zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p' s) p s; ko_wp_at' live' x s; cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) cref s\<rbrakk> \<Longrightarrow> (cref = p \<longrightarrow> x \<in> zobj_refs' (cteCap cte)) \<and> (cref \<noteq> p \<longrightarrow> cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) cref s) proof (prove)
goal (1 subgoal):
 1. \<And>s x ctea. \<lbrakk>ko_wp_at' live' x s; \<forall>p'\<in>zobj_refs' (cteCap ctea) - zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p' s; fst (getObject p s) = {(ctea, s)}; x \<in> zobj_refs' (cteCap ctea)\<rbrakk> \<Longrightarrow> x \<in> zobj_refs' (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>s x ctea. \<lbrakk>ko_wp_at' live' x s; \<forall>p'\<in>zobj_refs' (cteCap ctea) - zobj_refs' (cteCap cte). ko_wp_at' (Not \<circ> live') p' s; fst (getObject p s) = {(ctea, s)}; x \<in> zobj_refs' (cteCap ctea); x \<notin> zobj_refs' (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x ctea. \<lbrakk>ko_wp_at' live' x s; fst (getObject p s) = {(ctea, s)}; x \<in> zobj_refs' (cteCap ctea); x \<notin> zobj_refs' (cteCap cte); ko_wp_at' (Not \<circ> live') x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!