theory KHeap_DR

lemma lookup_cap_corres:
  "\<lbrakk>w = of_bl blist;length blist = word_bits\<rbrakk> \<Longrightarrow>
  dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) \<top>
     (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs)
     (CSpace_D.lookup_cap thread w)
     (lookup_cap thread blist)" apply (simp add:CSpace_D.lookup_cap_def lookup_cap_def) apply (simp add:lookup_slot_def lookup_slot_for_thread_def bindE_assoc) apply (clarsimp simp: liftE_bindE) apply (rule dcorres_gets_the) apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb) apply (rule corres_guard_imp) apply (rule corres_splitEE[where r'="\<lambda>x y. fst x = transform_cslot_ptr (fst y)"]) apply (rule corres_rel_imp) apply (rule resolve_address_bits_corres) apply (simp add: word_bits_def) apply (clarsimp simp: obj_at_def opt_cap_tcb not_idle_thread_def transform_cap_def word_bits_def)+ apply (case_tac x, auto)[1] apply (simp add:liftE_bindE split_def) apply (rule get_cap_corres[unfolded split_def]) apply simp apply wp apply wp apply (rule validE_validE_R) apply (wp not_idle_thread_resolve_address_bits[where thread = thread]) apply simp+ apply (simp add:objs_valid_tcb_ctable)+ apply clarsimp apply (clarsimp simp:not_idle_thread_def opt_cap_tcb | drule(1) valid_etcbs_get_tcb_get_etcb)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w = of_bl blist; length blist = word_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (\<lambda>_. True) (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) (CSpace_D.lookup_cap thread w) (CSpace_A.lookup_cap thread blist) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w = of_bl blist; length blist = word_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (\<lambda>_. True) (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) (doE slot <- lookup_slot thread (of_bl blist);
liftE (KHeap_D.get_cap slot)
odE) (doE (ref', uu_) <- lookup_slot_for_thread thread blist;
liftE (CSpaceAcc_A.get_cap ref')
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w = of_bl blist; length blist = word_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (\<lambda>_. True) (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) (doE x <- liftE (KHeap_D.get_cap (thread, tcb_cspace_slot));
x <- CSpace_D.resolve_address_bits x (of_bl blist) word_bits;
slot <- case x of (slot, uu_) \<Rightarrow> returnOk slot;
liftE (KHeap_D.get_cap slot)
odE) (doE x <- liftE (gets_the (get_tcb thread));
(ref', uu_) <- CSpace_A.resolve_address_bits (tcb_ctable x, blist);
liftE (CSpaceAcc_A.get_cap ref')
odE) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w = of_bl blist; length blist = word_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (\<lambda>_. True) (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) (do x <- KHeap_D.get_cap (thread, tcb_cspace_slot);
doE x <- CSpace_D.resolve_address_bits x (of_bl blist) word_bits;
slot <- case x of (slot, uu_) \<Rightarrow> returnOk slot;
liftE (KHeap_D.get_cap slot)
odE
od) (do x <- gets_the (get_tcb thread);
doE (ref', uu_) <- CSpace_A.resolve_address_bits (tcb_ctable x, blist);
liftE (CSpaceAcc_A.get_cap ref')
odE
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) s = Some obj\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) ((=) s) ((=) s') (doE x <- CSpace_D.resolve_address_bits obj (of_bl blist) word_bits;
slot <- case x of (slot, uu_) \<Rightarrow> returnOk slot;
liftE (KHeap_D.get_cap slot)
odE) (doE (ref', uu_) <- CSpace_A.resolve_address_bits (tcb_ctable obj', blist);
liftE (CSpaceAcc_A.get_cap ref')
odE)
 2. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) ((=) (transform s')) ((=) s') (doE x <- CSpace_D.resolve_address_bits obj (of_bl blist) word_bits;
slot <- case x of (slot, uu_) \<Rightarrow> returnOk slot;
liftE (KHeap_D.get_cap slot)
odE) (doE (ref', uu_) <- CSpace_A.resolve_address_bits (tcb_ctable obj', blist);
liftE (CSpaceAcc_A.get_cap ref')
odE)
 2. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (?Q15 s' obj obj') (?Q'15 s' obj obj') (doE x <- CSpace_D.resolve_address_bits obj (of_bl blist) word_bits;
slot <- case x of (slot, uu_) \<Rightarrow> returnOk slot;
liftE (KHeap_D.get_cap slot)
odE) (doE (ref', uu_) <- CSpace_A.resolve_address_bits (tcb_ctable obj', blist);
liftE (CSpaceAcc_A.get_cap ref')
odE)
 2. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ?Q15 s' obj obj' s
 3. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> ?Q'15 s' obj obj' s
 4. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (7 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y))) (?P19 s' obj obj') (?P'19 s' obj obj') (CSpace_D.resolve_address_bits obj (of_bl blist) word_bits) (CSpace_A.resolve_address_bits (tcb_ctable obj', blist))
 2. \<And>s' obj obj' x rv'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; fst x = transform_cslot_ptr (fst rv')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (?R19 s' obj obj' x) (?R'19 s' obj obj' rv') (doE slot <- case x of (slot, uu_) \<Rightarrow> returnOk slot;
liftE (KHeap_D.get_cap slot)
odE) (case rv' of (ref', uu_) \<Rightarrow> liftE (CSpaceAcc_A.get_cap ref'))
 3. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 s' obj obj'\<rbrace> CSpace_D.resolve_address_bits obj (of_bl blist) word_bits \<lbrace>?R19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 s' obj obj'\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj', blist) \<lbrace>?R'19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> (?P19 s' obj obj' and ?Q19 s' obj obj') s
 6. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (?P'19 s' obj obj' and ?Q'19 s' obj obj') s
 7. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (8 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres (?r'25 s' obj obj') (?P19 s' obj obj') (?P'19 s' obj obj') (CSpace_D.resolve_address_bits obj (of_bl blist) word_bits) (CSpace_A.resolve_address_bits (tcb_ctable obj', blist))
 2. \<And>s' obj obj' x y. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; ?r'25 s' obj obj' x y\<rbrakk> \<Longrightarrow> (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y))) x y
 3. \<And>s' obj obj' x rv'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; fst x = transform_cslot_ptr (fst rv')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (?R19 s' obj obj' x) (?R'19 s' obj obj' rv') (doE slot <- case x of (slot, uu_) \<Rightarrow> returnOk slot;
liftE (KHeap_D.get_cap slot)
odE) (case rv' of (ref', uu_) \<Rightarrow> liftE (CSpaceAcc_A.get_cap ref'))
 4. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 s' obj obj'\<rbrace> CSpace_D.resolve_address_bits obj (of_bl blist) word_bits \<lbrace>?R19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 s' obj obj'\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj', blist) \<lbrace>?R'19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> (?P19 s' obj obj' and ?Q19 s' obj obj') s
 7. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (?P'19 s' obj obj' and ?Q'19 s' obj obj') s
 8. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (10 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> length blist \<le> 32
 2. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> obj = transform_cap (tcb_ctable obj')
 3. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> word_bits = length blist
 4. \<And>s' obj obj' x y. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) x y\<rbrakk> \<Longrightarrow> (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y))) x y
 5. \<And>s' obj obj' x rv'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; fst x = transform_cslot_ptr (fst rv')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (?R19 s' obj obj' x) (?R'19 s' obj obj' rv') (doE slot <- case x of (slot, uu_) \<Rightarrow> returnOk slot;
liftE (KHeap_D.get_cap slot)
odE) (case rv' of (ref', uu_) \<Rightarrow> liftE (CSpaceAcc_A.get_cap ref'))
 6. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 s' obj obj'\<rbrace> CSpace_D.resolve_address_bits obj (of_bl blist) word_bits \<lbrace>?R19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 s' obj obj'\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj', blist) \<lbrace>?R'19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q19 s' obj obj') s
 9. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (valid_objs and valid_cap (tcb_ctable obj') and valid_global_refs and valid_idle and valid_etcbs and ?Q'19 s' obj obj') s
 10. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (9 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> obj = transform_cap (tcb_ctable obj')
 2. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> word_bits = length blist
 3. \<And>s' obj obj' x y. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) x y\<rbrakk> \<Longrightarrow> (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y))) x y
 4. \<And>s' obj obj' x rv'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; fst x = transform_cslot_ptr (fst rv')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (?R19 s' obj obj' x) (?R'19 s' obj obj' rv') (doE slot <- case x of (slot, uu_) \<Rightarrow> returnOk slot;
liftE (KHeap_D.get_cap slot)
odE) (case rv' of (ref', uu_) \<Rightarrow> liftE (CSpaceAcc_A.get_cap ref'))
 5. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 s' obj obj'\<rbrace> CSpace_D.resolve_address_bits obj (of_bl blist) word_bits \<lbrace>?R19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 s' obj obj'\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj', blist) \<lbrace>?R'19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q19 s' obj obj') s
 8. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (valid_objs and valid_cap (tcb_ctable obj') and valid_global_refs and valid_idle and valid_etcbs and ?Q'19 s' obj obj') s
 9. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (7 subgoals):
 1. \<And>s' obj' x y etcb. \<lbrakk>w = of_bl blist; length blist = 32; get_tcb thread s' = Some obj'; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; thread \<noteq> idle_thread s'; valid_etcbs s'; (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y) \<and> snd x = length (snd y))) x y; get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> (dc \<oplus> (\<lambda>x y. fst x = transform_cslot_ptr (fst y))) x y
 2. \<And>s' obj obj' x rv'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; fst x = transform_cslot_ptr (fst rv')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (?R19 s' obj obj' x) (?R'19 s' obj obj' rv') (doE slot <- case x of (slot, uu_) \<Rightarrow> returnOk slot;
liftE (KHeap_D.get_cap slot)
odE) (case rv' of (ref', uu_) \<Rightarrow> liftE (CSpaceAcc_A.get_cap ref'))
 3. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 s' obj obj'\<rbrace> CSpace_D.resolve_address_bits obj (of_bl blist) word_bits \<lbrace>?R19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 s' obj obj'\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj', blist) \<lbrace>?R'19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q19 s' obj obj') s
 6. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (valid_objs and valid_cap (tcb_ctable obj') and valid_global_refs and valid_idle and valid_etcbs and ?Q'19 s' obj obj') s
 7. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (6 subgoals):
 1. \<And>s' obj obj' x rv'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; fst x = transform_cslot_ptr (fst rv')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cap y)) (?R19 s' obj obj' x) (?R'19 s' obj obj' rv') (doE slot <- case x of (slot, uu_) \<Rightarrow> returnOk slot;
liftE (KHeap_D.get_cap slot)
odE) (case rv' of (ref', uu_) \<Rightarrow> liftE (CSpaceAcc_A.get_cap ref'))
 2. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 s' obj obj'\<rbrace> CSpace_D.resolve_address_bits obj (of_bl blist) word_bits \<lbrace>?R19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 s' obj obj'\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj', blist) \<lbrace>?R'19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q19 s' obj obj') s
 5. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (valid_objs and valid_cap (tcb_ctable obj') and valid_global_refs and valid_idle and valid_etcbs and ?Q'19 s' obj obj') s
 6. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (6 subgoals):
 1. \<And>s' obj obj' x rv'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; fst x = transform_cslot_ptr (fst rv')\<rbrakk> \<Longrightarrow> dcorres (\<lambda>x y. x = transform_cap y) (?R19 s' obj obj' x) (?R'19 s' obj obj' rv') (KHeap_D.get_cap (transform_cslot_ptr (fst rv'))) (CSpaceAcc_A.get_cap (fst rv'))
 2. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 s' obj obj'\<rbrace> CSpace_D.resolve_address_bits obj (of_bl blist) word_bits \<lbrace>?R19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 s' obj obj'\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj', blist) \<lbrace>?R'19 s' obj obj'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q19 s' obj obj') s
 5. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (valid_objs and valid_cap (tcb_ctable obj') and valid_global_refs and valid_idle and valid_etcbs and ?Q'19 s' obj obj') s
 6. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (6 subgoals):
 1. \<And>s' obj obj' x rv'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; fst x = transform_cslot_ptr (fst rv')\<rbrakk> \<Longrightarrow> transform_cslot_ptr (fst rv') = transform_cslot_ptr (fst rv')
 2. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 s' obj obj'\<rbrace> CSpace_D.resolve_address_bits obj (of_bl blist) word_bits \<lbrace>\<lambda>x _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 s' obj obj'\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj', blist) \<lbrace>\<lambda>rv'. valid_idle and not_idle_thread (fst (fst rv')) and valid_etcbs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q19 s' obj obj') s
 5. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (valid_objs and valid_cap (tcb_ctable obj') and valid_global_refs and valid_idle and valid_etcbs and ?Q'19 s' obj obj') s
 6. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (5 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 s' obj obj'\<rbrace> CSpace_D.resolve_address_bits obj (of_bl blist) word_bits \<lbrace>\<lambda>x _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 s' obj obj'\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj', blist) \<lbrace>\<lambda>rv'. valid_idle and not_idle_thread (fst (fst rv')) and valid_etcbs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q19 s' obj obj') s
 4. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (valid_objs and valid_cap (tcb_ctable obj') and valid_global_refs and valid_idle and valid_etcbs and ?Q'19 s' obj obj') s
 5. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'19 s' obj obj'\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj', blist) \<lbrace>\<lambda>rv'. valid_idle and not_idle_thread (fst (fst rv')) and valid_etcbs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (valid_objs and valid_cap (tcb_ctable obj') and valid_global_refs and valid_idle and valid_etcbs and ?Q'19 s' obj obj') s
 4. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?P'96 s' obj obj'\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj', blist) \<lbrace>\<lambda>rv s. not_idle_thread (fst (fst rv)) s \<and> valid_etcbs s\<rbrace>, -
 2. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (valid_objs and valid_cap (tcb_ctable obj') and valid_global_refs and valid_idle and valid_etcbs and (\<lambda>s. True \<and> valid_idle s \<and> ?P'96 s' obj obj' s)) s
 4. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (4 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>?P'96 s' obj obj'\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj', blist) \<lbrace>\<lambda>rv s. not_idle_thread (fst (fst rv)) s \<and> valid_etcbs s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (valid_objs and valid_cap (tcb_ctable obj') and valid_global_refs and valid_idle and valid_etcbs and (\<lambda>s. True \<and> valid_idle s \<and> ?P'96 s' obj obj' s)) s
 4. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (3 subgoals):
 1. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 2. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s' = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s') = Some obj; valid_global_refs s'; valid_objs s'; valid_irq_node s'; valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; \<exists>etcb. get_etcb thread s' = Some etcb; s' = s\<rbrakk> \<Longrightarrow> (valid_objs and valid_cap (tcb_ctable obj') and valid_global_refs and valid_idle and valid_etcbs and (\<lambda>s. True \<and> valid_idle s \<and> (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj') thread and valid_etcbs) s)) s
 3. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s) = Some obj; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; not_idle_thread thread s; valid_etcbs s; \<exists>etcb. get_etcb thread s = Some etcb; s' = s\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ctable obj' \<and> ko_at (TCB obj') thread s
 2. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj' s. \<lbrakk>w = of_bl blist; length blist = word_bits; get_tcb thread s = Some obj'; opt_cap (thread, tcb_cspace_slot) (transform s) = Some obj; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; not_idle_thread thread s; valid_etcbs s; \<exists>etcb. get_etcb thread s = Some etcb; s' = s\<rbrakk> \<Longrightarrow> ko_at (TCB obj') thread s
 2. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>w = of_bl blist; length blist = word_bits; s = transform s'; True; (valid_global_refs and valid_objs and valid_irq_node and valid_idle and not_idle_thread thread and valid_etcbs) s'; get_tcb thread s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_cspace_slot) s \<noteq> None proof (prove)
goal:
No subgoals!