theory KHeap_R

lemma setObject_iflive':
  fixes v :: "'a :: pspace_storable"
  assumes R: "\<And>ko s x y n. (updateObject v ko ptr y n s)
                   = (updateObject_default v ko ptr y n s)"
  assumes n: "\<And>x :: 'a. objBits x = n"
  assumes m: "(1 :: word32) < 2 ^ n"
  assumes x: "\<And>x n tcb s t. \<lbrakk> t \<in> fst (updateObject v (KOTCB tcb) ptr x n s); P s;
                               lookupAround2 ptr (ksPSpace s) = (Some (x, KOTCB tcb), n) \<rbrakk>
                  \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>(getF, setF) \<in> ran tcb_cte_cases. getF tcb' = getF tcb)"
  assumes y: "\<And>x n cte s. fst (updateObject v (KOCTE cte) ptr x n s) = {}"
  shows      "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' ptr s) \<and> P s\<rbrace>
                setObject ptr v
              \<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) apply (rule setObject_ko_wp_at [OF R n m]) apply (rule hoare_vcg_ex_lift) apply (rule setObject_cte_wp_at'[where Q = P, OF x y]) apply assumption+ apply clarsimp apply (clarsimp simp: ko_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' ptr s) \<and> P s\<rbrace> setObject ptr v \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>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)) \<and> (live' (injectKO v) \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<and> P s\<rbrace> setObject ptr v \<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> setObject ptr v \<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. (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<and> (live' (injectKO v) \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<and> P s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject ptr v \<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. (\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<and> (live' (injectKO v) \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<and> P s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>ptra. \<lbrace>?P5 ptra\<rbrace> setObject ptr v \<lbrace>\<lambda>rv s. \<not> ko_wp_at' live' ptra s\<rbrace>
 2. \<And>ptra. \<lbrace>?P'5 ptra\<rbrace> setObject ptr v \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. ptra \<in> zobj_refs' (cteCap c)) cref s\<rbrace>
 3. \<And>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)) \<and> (live' (injectKO v) \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<and> P s \<Longrightarrow> \<forall>x. ?P5 x s \<or> ?P'5 x s proof (prove)
goal (2 subgoals):
 1. \<And>ptra. \<lbrace>?P'5 ptra\<rbrace> setObject ptr v \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. ptra \<in> zobj_refs' (cteCap c)) cref s\<rbrace>
 2. \<And>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)) \<and> (live' (injectKO v) \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<and> P s \<Longrightarrow> \<forall>x. (obj_at' (\<lambda>x. True) ptr s \<longrightarrow> \<not> ko_wp_at' (if ptr = x then K (live' (injectKO v)) else live') x s) \<or> ?P'5 x s proof (prove)
goal (2 subgoals):
 1. \<And>ptra cref. \<lbrace>?P10 ptra cref\<rbrace> setObject ptr v \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. ptra \<in> zobj_refs' (cteCap c)) cref\<rbrace>
 2. \<And>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)) \<and> (live' (injectKO v) \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<and> P s \<Longrightarrow> \<forall>x. (obj_at' (\<lambda>x. True) ptr s \<longrightarrow> \<not> ko_wp_at' (if ptr = x then K (live' (injectKO v)) else live') x s) \<or> (\<exists>xa. ?P10 x xa s) proof (prove)
goal (4 subgoals):
 1. \<And>ptra cref x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (KOTCB tcb) ptr x n s); P s; lookupAround2 ptr (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> t \<in> fst (updateObject v (KOTCB tcb) ptr (?x14 ptra cref x n tcb s t) (?n14 ptra cref x n tcb s t) s)
 2. \<And>ptra cref x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (KOTCB tcb) ptr x n s); P s; lookupAround2 ptr (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> P s
 3. \<And>ptra cref x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (KOTCB tcb) ptr x n s); P s; lookupAround2 ptr (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> lookupAround2 ptr (ksPSpace s) = (Some (?x14 ptra cref x n tcb s t, KOTCB tcb), ?n14 ptra cref x n tcb s t)
 4. \<And>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)) \<and> (live' (injectKO v) \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<and> P s \<Longrightarrow> \<forall>x. (obj_at' (\<lambda>x. True) ptr s \<longrightarrow> \<not> ko_wp_at' (if ptr = x then K (live' (injectKO v)) else live') x s) \<or> (\<exists>xa. (cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa and P) s) proof (prove)
goal (1 subgoal):
 1. \<And>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)) \<and> (live' (injectKO v) \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)) \<and> P s \<Longrightarrow> \<forall>x. (obj_at' (\<lambda>x. True) ptr s \<longrightarrow> \<not> ko_wp_at' (if ptr = x then K (live' (injectKO v)) else live') x s) \<or> (\<exists>xa. (cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa and P) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s); P s; obj_at' (\<lambda>x. True) ptr s; ko_wp_at' (\<lambda>y. False) ptr s; \<not> live' (injectKO v)\<rbrakk> \<Longrightarrow> \<exists>x. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) x s proof (prove)
goal:
No subgoals!