theory Move_C

lemma getObject_tcb_det:
  "(r::tcb,s') \<in> fst (getObject p s) \<Longrightarrow> fst (getObject p s) = {(r,s)} \<and> s' = s" apply (clarsimp simp add: getObject_def bind_def get_def gets_def
                            return_def loadObject_default_def split_def) apply (clarsimp split: kernel_object.split_asm if_split_asm option.split_asm
                   simp: in_monad typeError_def alignError_def magnitudeCheck_def
                         objBits_def objBitsKO_def projectKOs
                         lookupAround2_def Let_def o_def) apply (simp_all add: bind_def return_def assert_opt_def split_def projectKOs
                        alignCheck_def is_aligned_mask[symmetric]
                        unless_def when_def magnitudeCheck_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, s') \<in> fst (getObject p s) \<Longrightarrow> fst (getObject p s) = {(r, s)} \<and> s' = s proof (prove)
goal (1 subgoal):
 1. \<And>a b ba bb bc. \<lbrakk>((a, b), ba) \<in> fst (assert_opt (fst (lookupAround2 (fromPPtr p) (ksPSpace s))) s); ((), bb) \<in> fst (assert (fromPPtr p = a) ba); (r, bc) \<in> fst (projectKO b bb); is_aligned (fromPPtr p) (objBits r); ((), s') \<in> fst (magnitudeCheck (fromPPtr p) (snd (lookupAround2 (fromPPtr p) (ksPSpace s))) (objBits r) bc)\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (assert_opt (fst (lookupAround2 (fromPPtr p) (ksPSpace s))) s). \<Union>xa\<in>fst (assert (fromPPtr p = fst (fst x)) (snd x)). \<Union>x\<in>fst (projectKO (snd (fst x)) (snd xa)). \<Union>xa\<in>fst (alignCheck (fromPPtr p) (objBits (fst x)) (snd x)). \<Union>xa\<in>fst (magnitudeCheck (fromPPtr p) (snd (lookupAround2 (fromPPtr p) (ksPSpace s))) (objBits (fst x)) (snd xa)). {(fst x, snd xa)}) = {(r, s)} \<and> s' = s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fst (case lookupAround (fromPPtr p) (ksPSpace s) of (before, None, after) \<Rightarrow> (before, case after of None \<Rightarrow> None | Some x \<Rightarrow> Some (fst x)) | (before, Some v, after) \<Rightarrow> (Some (fromPPtr p, v), case after of None \<Rightarrow> None | Some x \<Rightarrow> Some (fst x))) = Some (fromPPtr p, KOTCB r); is_aligned (fromPPtr p) tcbBlockSizeBits; snd (case lookupAround (fromPPtr p) (ksPSpace s) of (before, None, after) \<Rightarrow> (before, case after of None \<Rightarrow> None | Some x \<Rightarrow> Some (fst x)) | (before, Some v, after) \<Rightarrow> (Some (fromPPtr p, v), case after of None \<Rightarrow> None | Some x \<Rightarrow> Some (fst x))) = None; s' = s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return (fromPPtr p, KOTCB r) s). \<Union>xa\<in>fst (assert (fromPPtr p = fst (fst x)) (snd x)). \<Union>x\<in>fst (projectKO (snd (fst x)) (snd xa)). \<Union>xa\<in>fst (alignCheck (fromPPtr p) tcbBlockSizeBits (snd x)). \<Union>xa\<in>fst (return () (snd xa)). {(fst x, snd xa)}) = {(r, s)}
 2. \<And>x2. \<lbrakk>fst (case lookupAround (fromPPtr p) (ksPSpace s) of (before, None, after) \<Rightarrow> (before, case after of None \<Rightarrow> None | Some x \<Rightarrow> Some (fst x)) | (before, Some v, after) \<Rightarrow> (Some (fromPPtr p, v), case after of None \<Rightarrow> None | Some x \<Rightarrow> Some (fst x))) = Some (fromPPtr p, KOTCB r); is_aligned (fromPPtr p) tcbBlockSizeBits; snd (case lookupAround (fromPPtr p) (ksPSpace s) of (before, None, after) \<Rightarrow> (before, case after of None \<Rightarrow> None | Some x \<Rightarrow> Some (fst x)) | (before, Some v, after) \<Rightarrow> (Some (fromPPtr p, v), case after of None \<Rightarrow> None | Some x \<Rightarrow> Some (fst x))) = Some x2; \<not> x2 - fromPPtr p < 2 ^ tcbBlockSizeBits; s' = s\<rbrakk> \<Longrightarrow> (\<Union>x\<in>fst (return (fromPPtr p, KOTCB r) s). \<Union>xa\<in>fst (assert (fromPPtr p = fst (fst x)) (snd x)). \<Union>x\<in>fst (projectKO (snd (fst x)) (snd xa)). \<Union>xa\<in>fst (alignCheck (fromPPtr p) tcbBlockSizeBits (snd x)). \<Union>xa\<in>fst (return () (snd xa)). {(fst x, snd xa)}) = {(r, s)} proof (prove)
goal:
No subgoals!