theory TcbAcc_R

lemma setObject_tcb_pspace_no_overlap':
  "\<lbrace>pspace_no_overlap' w s and tcb_at' t\<rbrace>
  setObject t (tcb::tcb)
  \<lbrace>\<lambda>rv. pspace_no_overlap' w s\<rbrace>" apply (clarsimp simp: setObject_def split_def valid_def in_monad) apply (clarsimp simp: obj_at'_def projectKOs) apply (erule (1) ps_clear_lookupAround2) apply (rule order_refl) apply (erule is_aligned_no_overflow) apply simp apply (clarsimp simp: updateObject_default_def in_monad projectKOs objBits_simps in_magnitude_check) apply (fastforce simp: pspace_no_overlap'_def objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_no_overlap' w s and tcb_at' t\<rbrace> setObject t tcb \<lbrace>\<lambda>rv. pspace_no_overlap' w s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa a ba s'' obj'. \<lbrakk>pspace_no_overlap' w s sa; tcb_at' t sa; fst (lookupAround2 t (ksPSpace sa)) = Some (a, ba); (obj', s'') \<in> fst (updateObject_default tcb ba t a (snd (lookupAround2 t (ksPSpace sa))) sa)\<rbrakk> \<Longrightarrow> pspace_no_overlap' w s (s''\<lparr>ksPSpace := (ksPSpace sa)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa a ba s'' obj' obj. \<lbrakk>pspace_no_overlap' w s sa; fst (lookupAround2 t (ksPSpace sa)) = Some (a, ba); (obj', s'') \<in> fst (updateObject_default tcb ba t a (snd (lookupAround2 t (ksPSpace sa))) sa); ksPSpace sa t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) sa\<rbrakk> \<Longrightarrow> pspace_no_overlap' w s (s''\<lparr>ksPSpace := (ksPSpace sa)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>sa a ba s'' obj' obj. \<lbrakk>pspace_no_overlap' w s sa; fst (lookupAround2 t (ksPSpace sa)) = Some (a, ba); (obj', s'') \<in> fst (updateObject_default tcb ba t a (snd (lookupAround2 t (ksPSpace sa))) sa); ksPSpace sa t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj))\<rbrakk> \<Longrightarrow> t \<le> ?p25 sa a ba s'' obj' obj
 2. \<And>sa a ba s'' obj' obj. \<lbrakk>pspace_no_overlap' w s sa; fst (lookupAround2 t (ksPSpace sa)) = Some (a, ba); (obj', s'') \<in> fst (updateObject_default tcb ba t a (snd (lookupAround2 t (ksPSpace sa))) sa); ksPSpace sa t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj))\<rbrakk> \<Longrightarrow> ?p25 sa a ba s'' obj' obj \<le> t + 2 ^ objBitsKO (KOTCB obj) - 1
 3. \<And>sa a ba s'' obj' obj. \<lbrakk>pspace_no_overlap' w s sa; fst (lookupAround2 t (ksPSpace sa)) = Some (a, ba); (obj', s'') \<in> fst (updateObject_default tcb ba t a (snd (lookupAround2 t (ksPSpace sa))) sa); ksPSpace sa t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); fst (lookupAround2 (?p25 sa a ba s'' obj' obj) (ksPSpace sa)) = Some (t, KOTCB obj); case snd (lookupAround2 (?p25 sa a ba s'' obj' obj) (ksPSpace sa)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> x - t\<rbrakk> \<Longrightarrow> pspace_no_overlap' w s (s''\<lparr>ksPSpace := (ksPSpace sa)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>sa a ba s'' obj' obj. \<lbrakk>pspace_no_overlap' w s sa; fst (lookupAround2 t (ksPSpace sa)) = Some (a, ba); (obj', s'') \<in> fst (updateObject_default tcb ba t a (snd (lookupAround2 t (ksPSpace sa))) sa); ksPSpace sa t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj))\<rbrakk> \<Longrightarrow> t \<le> t + 2 ^ objBitsKO (KOTCB obj) - 1
 2. \<And>sa a ba s'' obj' obj. \<lbrakk>pspace_no_overlap' w s sa; fst (lookupAround2 t (ksPSpace sa)) = Some (a, ba); (obj', s'') \<in> fst (updateObject_default tcb ba t a (snd (lookupAround2 t (ksPSpace sa))) sa); ksPSpace sa t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); fst (lookupAround2 t (ksPSpace sa)) = Some (t, KOTCB obj); case snd (lookupAround2 t (ksPSpace sa)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> x - t\<rbrakk> \<Longrightarrow> pspace_no_overlap' w s (s''\<lparr>ksPSpace := (ksPSpace sa)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa a ba s'' obj' obj. \<lbrakk>pspace_no_overlap' w s sa; fst (lookupAround2 t (ksPSpace sa)) = Some (a, ba); (obj', s'') \<in> fst (updateObject_default tcb ba t a (snd (lookupAround2 t (ksPSpace sa))) sa); ksPSpace sa t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); fst (lookupAround2 t (ksPSpace sa)) = Some (t, KOTCB obj); case snd (lookupAround2 t (ksPSpace sa)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> x - t\<rbrakk> \<Longrightarrow> pspace_no_overlap' w s (s''\<lparr>ksPSpace := (ksPSpace sa)(a \<mapsto> obj')\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa a s'' obj' obj. \<lbrakk>pspace_no_overlap' w s sa; t = a; (obj', s'') \<in> fst (updateObject_default tcb (KOTCB obj) a a (snd (lookupAround2 a (ksPSpace sa))) sa); ksPSpace sa a = Some (KOTCB obj); is_aligned a (objBitsKO (KOTCB obj)); case snd (lookupAround2 a (ksPSpace sa)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBitsKO (KOTCB obj) \<le> x - a\<rbrakk> \<Longrightarrow> pspace_no_overlap' w s (s''\<lparr>ksPSpace := \<lambda>b. if b = a then Some obj' else ksPSpace sa b\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>sa s'' obj. \<lbrakk>pspace_no_overlap' w s sa; ksPSpace sa t = Some (KOTCB obj); case snd (lookupAround2 t (ksPSpace sa)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - t; is_aligned t tcbBlockSizeBits; ((), s'') \<in> fst (magnitudeCheck t (snd (lookupAround2 t (ksPSpace sa))) tcbBlockSizeBits sa)\<rbrakk> \<Longrightarrow> pspace_no_overlap' w s (s''\<lparr>ksPSpace := \<lambda>a. if a = t then Some (KOTCB tcb) else ksPSpace sa a\<rparr>) proof (prove)
goal:
No subgoals!