theory CSpace_R

lemma setCTE_ko_wp_at_live[wp]:
  "\<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace>
    setCTE p v
   \<lbrace>\<lambda>rv s. P (ko_wp_at' live' p' s)\<rbrace>" apply (clarsimp simp: setCTE_def setObject_def split_def
                        valid_def in_monad ko_wp_at'_def
             split del: if_split
                 elim!: rsubst[where P=P]) apply (drule(1) updateObject_cte_is_tcb_or_cte [OF _ refl, rotated]) apply (elim exE conjE disjE) apply (clarsimp simp: ps_clear_upd objBits_simps
                         lookupAround2_char1) apply (simp add: tcb_cte_cases_def split: if_split_asm) apply (clarsimp simp: ps_clear_upd objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (ko_wp_at' live' p' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); (obj', s'') \<in> fst (updateObject v ba p a (snd (lookupAround2 p (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> (\<exists>ko. ksPSpace s p' = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> live' ko \<and> ps_clear p' (objBitsKO ko) s) = (\<exists>ko. (if p' = a then Some obj' else ksPSpace s p') = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> live' ko \<and> ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); (\<exists>tcb getF setF. ba = KOTCB tcb \<and> s'' = s \<and> tcb_cte_cases (p - a) = Some (getF, setF) \<and> obj' = KOTCB (setF (\<lambda>x. v) tcb) \<and> is_aligned a tcbBlockSizeBits \<and> ps_clear a tcbBlockSizeBits s) \<or> (\<exists>cte'. ba = KOCTE cte' \<and> obj' = KOCTE v \<and> s'' = s \<and> p = a \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits s)\<rbrakk> \<Longrightarrow> (\<exists>ko. ksPSpace s p' = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> live' ko \<and> ps_clear p' (objBitsKO ko) s) = (\<exists>ko. (if p' = a then Some obj' else ksPSpace s p') = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> live' ko \<and> ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s a ba s'' obj' tcb getF setF. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOTCB tcb; s'' = s; tcb_cte_cases (p - a) = Some (getF, setF); obj' = KOTCB (setF (\<lambda>x. v) tcb); is_aligned a tcbBlockSizeBits; ps_clear a tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> (\<exists>ko. ksPSpace s p' = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> live' ko \<and> ps_clear p' (objBitsKO ko) s) = (\<exists>ko. (if p' = a then Some obj' else ksPSpace s p') = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> live' ko \<and> ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>))
 2. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE v; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (\<exists>ko. ksPSpace s p' = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> live' ko \<and> ps_clear p' (objBitsKO ko) s) = (\<exists>ko. (if p' = a then Some obj' else ksPSpace s p') = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> live' ko \<and> ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s tcb getF setF. \<lbrakk>tcb_cte_cases (p - p') = Some (getF, setF); is_aligned p' tcbBlockSizeBits; ps_clear p' tcbBlockSizeBits s; p' \<le> p; ksPSpace s p' = Some (KOTCB tcb); \<forall>z. p' < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None\<rbrakk> \<Longrightarrow> ((\<exists>y. tcbBoundNotification tcb = Some y) \<or> tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> tcbState tcb \<noteq> Structures_H.thread_state.IdleThreadState \<or> tcbQueued tcb) = ((\<exists>y. tcbBoundNotification (setF (\<lambda>x. v) tcb) = Some y) \<or> tcbState (setF (\<lambda>x. v) tcb) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (setF (\<lambda>x. v) tcb) \<noteq> Structures_H.thread_state.IdleThreadState \<or> tcbQueued (setF (\<lambda>x. v) tcb))
 2. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE v; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (\<exists>ko. ksPSpace s p' = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> live' ko \<and> ps_clear p' (objBitsKO ko) s) = (\<exists>ko. (if p' = a then Some obj' else ksPSpace s p') = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> live' ko \<and> ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s'' obj' cte'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, ba); ba = KOCTE cte'; obj' = KOCTE v; s'' = s; p = a; is_aligned p cte_level_bits; ps_clear p cte_level_bits s\<rbrakk> \<Longrightarrow> (\<exists>ko. ksPSpace s p' = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> live' ko \<and> ps_clear p' (objBitsKO ko) s) = (\<exists>ko. (if p' = a then Some obj' else ksPSpace s p') = Some ko \<and> is_aligned p' (objBitsKO ko) \<and> live' ko \<and> ps_clear p' (objBitsKO ko) (s''\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>)) proof (prove)
goal:
No subgoals!