theory KHeap_R

lemma setEndpoint_iflive'[wp]:
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s
      \<and> (v \<noteq> IdleEP \<longrightarrow> ex_nonz_cap_to' p s)\<rbrace>
     setEndpoint p v
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" unfolding setEndpoint_def apply (wp setObject_iflive'[where P="\<top>"]) apply simp apply (simp add: objBits_simps') apply simp apply (clarsimp simp: updateObject_default_def in_monad projectKOs) apply (clarsimp simp: updateObject_default_def in_monad
                         projectKOs bind_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> (v \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' p s)\<rbrace> setEndpoint p v \<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> (v \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' p s)\<rbrace> setObject p v \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ko s x y n. updateObject v ko p y n s = updateObject_default v ko p y n s
 2. \<And>x. objBits x = ?n1
 3. 1 < 2 ^ ?n1
 4. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (KOTCB tcb) p x n s); True; lookupAround2 p (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)
 5. \<And>x n cte s. fst (updateObject v (KOCTE cte) p x n s) = {}
 6. \<And>s. if_live_then_nonz_cap' s \<and> (v \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' p s) \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal (5 subgoals):
 1. \<And>x. objBits x = ?n1
 2. 1 < 2 ^ ?n1
 3. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (KOTCB tcb) p x n s); True; lookupAround2 p (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)
 4. \<And>x n cte s. fst (updateObject v (KOCTE cte) p x n s) = {}
 5. \<And>s. if_live_then_nonz_cap' s \<and> (v \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' p s) \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal (4 subgoals):
 1. 1 < 2 ^ 4
 2. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (KOTCB tcb) p x n s); True; lookupAround2 p (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)
 3. \<And>x n cte s. fst (updateObject v (KOCTE cte) p x n s) = {}
 4. \<And>s. if_live_then_nonz_cap' s \<and> (v \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' p s) \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal (3 subgoals):
 1. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (KOTCB tcb) p x n s); True; lookupAround2 p (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)
 2. \<And>x n cte s. fst (updateObject v (KOCTE cte) p x n s) = {}
 3. \<And>s. if_live_then_nonz_cap' s \<and> (v \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' p s) \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>x n cte s. fst (updateObject v (KOCTE cte) p x n s) = {}
 2. \<And>s. if_live_then_nonz_cap' s \<and> (v \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' p s) \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. if_live_then_nonz_cap' s \<and> (v \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' p s) \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO v) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal:
No subgoals!