theory KHeap_DR

lemma dcorres_lookup_slot:
  "\<lbrakk>w = of_bl ptr;length ptr = word_bits\<rbrakk> \<Longrightarrow>
  dcorres (dc \<oplus> (\<lambda>x y. x = transform_cslot_ptr (fst y))) \<top>
  (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs)
  (CSpace_D.lookup_slot thread w)
  (CSpace_A.lookup_slot_for_thread thread ptr)" apply (simp add: CSpace_D.lookup_slot_def lookup_slot_for_thread_def) apply (rule corres_guard_imp) apply (rule corres_splitEE) apply simp apply (rule get_cap_get_tcb_dcorres) apply (rule corres_dummy_returnOk_r) apply (rule corres_splitEE[OF resolve_address_bits_corres]) apply (clarsimp simp: word_bits_def)+ apply (rule corres_returnOk [where P=\<top> and P'=\<top>]) apply clarsimp apply wpsimp+ apply (erule (1) objs_valid_tcb_ctable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cslot_ptr (fst y))) (\<lambda>_. True) (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) (lookup_slot thread w) (lookup_slot_for_thread thread ptr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cslot_ptr (fst y))) (\<lambda>_. True) (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) (doE cspace_root <- liftE (KHeap_D.get_cap (thread, tcb_cspace_slot));
(slot, uu_) <- CSpace_D.resolve_address_bits cspace_root (of_bl ptr) word_bits;
returnOk slot
odE) (doE tcb <- liftE (gets_the (get_tcb thread));
CSpace_A.resolve_address_bits (tcb_ctable tcb, ptr)
odE) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cslot_ptr (fst y))) ?Q1 ?Q'1 (doE cspace_root <- liftE (KHeap_D.get_cap (thread, tcb_cspace_slot));
(slot, uu_) <- CSpace_D.resolve_address_bits cspace_root (of_bl ptr) word_bits;
returnOk slot
odE) (doE tcb <- liftE (gets_the (get_tcb thread));
CSpace_A.resolve_address_bits (tcb_ctable tcb, ptr)
odE)
 2. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'1 s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?r'5) ?P5 ?P'5 (liftE (KHeap_D.get_cap (thread, tcb_cspace_slot))) (liftE (gets_the (get_tcb thread)))
 2. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; ?r'5 cspace_root tcb\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cslot_ptr (fst y))) (?R5 cspace_root) (?R'5 tcb) (doE (slot, uu_) <- CSpace_D.resolve_address_bits cspace_root (of_bl ptr) word_bits;
returnOk slot
odE) (CSpace_A.resolve_address_bits (tcb_ctable tcb, ptr))
 3. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> liftE (KHeap_D.get_cap (thread, tcb_cspace_slot)) \<lbrace>?R5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> liftE (gets_the (get_tcb thread)) \<lbrace>?R'5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> (?P5 and ?Q5) s
 6. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'5 and ?Q'5) s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> dcorres ?r'5 ?P5 ?P'5 (KHeap_D.get_cap (thread, tcb_cspace_slot)) (gets_the (get_tcb thread))
 2. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; ?r'5 cspace_root tcb\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cslot_ptr (fst y))) (?R5 cspace_root) (?R'5 tcb) (doE (slot, uu_) <- CSpace_D.resolve_address_bits cspace_root (of_bl ptr) word_bits;
returnOk slot
odE) (CSpace_A.resolve_address_bits (tcb_ctable tcb, ptr))
 3. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> liftE (KHeap_D.get_cap (thread, tcb_cspace_slot)) \<lbrace>?R5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> liftE (gets_the (get_tcb thread)) \<lbrace>?R'5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> (?P5 and ?Q5) s
 6. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'5 and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cslot_ptr (fst y))) (?R5 cspace_root) (?R'5 tcb) (doE (slot, uu_) <- CSpace_D.resolve_address_bits cspace_root (of_bl ptr) word_bits;
returnOk slot
odE) (CSpace_A.resolve_address_bits (tcb_ctable tcb, ptr))
 2. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> liftE (KHeap_D.get_cap (thread, tcb_cspace_slot)) \<lbrace>?R5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> liftE (gets_the (get_tcb thread)) \<lbrace>?R'5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_etcbs and ?Q'5) s proof (prove)
goal (5 subgoals):
 1. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cslot_ptr (fst y))) (?R5 cspace_root) (?R'5 tcb) (doE (slot, uu_) <- CSpace_D.resolve_address_bits cspace_root (of_bl ptr) word_bits;
returnOk slot
odE) (CSpace_A.resolve_address_bits (tcb_ctable tcb, ptr) >>=E returnOk)
 2. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> liftE (KHeap_D.get_cap (thread, tcb_cspace_slot)) \<lbrace>?R5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> liftE (gets_the (get_tcb thread)) \<lbrace>?R'5\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_etcbs and ?Q'5) s proof (prove)
goal (10 subgoals):
 1. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> length ptr \<le> 32
 2. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> cspace_root = transform_cap (tcb_ctable tcb)
 3. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> word_bits = length ptr
 4. \<And>cspace_root tcb rv rv'. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb); fst rv = transform_cslot_ptr (fst rv') \<and> snd rv = length (snd rv')\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cslot_ptr (fst y))) (?R13 cspace_root tcb rv) (?R'13 cspace_root tcb rv') (case rv of (slot, uu_) \<Rightarrow> returnOk slot) (returnOk rv')
 5. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cspace_root\<rbrace> CSpace_D.resolve_address_bits cspace_root (of_bl ptr) word_bits \<lbrace>?R13 cspace_root tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 tcb\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable tcb, ptr) \<lbrace>?R'13 cspace_root tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> liftE (KHeap_D.get_cap (thread, tcb_cspace_slot)) \<lbrace>\<lambda>cspace_root. (\<lambda>_. True) and ?Q15 cspace_root\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> liftE (gets_the (get_tcb thread)) \<lbrace>\<lambda>tcb. valid_objs and valid_cap (tcb_ctable tcb) and valid_global_refs and valid_idle and valid_etcbs and ?Q'17 tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 10. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_etcbs and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<And>tcb a b aa bb bc. \<lbrakk>w = of_bl ptr; length ptr = 32; (a, b) = transform_cslot_ptr (aa, bb)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. x = transform_cslot_ptr (fst y))) (?R13 (transform_cap (tcb_ctable tcb)) tcb (transform_cslot_ptr (aa, bb), length bc)) (?R'13 (transform_cap (tcb_ctable tcb)) tcb ((aa, bb), bc)) (returnOk (transform_cslot_ptr (aa, bb))) (returnOk ((aa, bb), bc))
 2. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cspace_root\<rbrace> CSpace_D.resolve_address_bits cspace_root (of_bl ptr) word_bits \<lbrace>?R13 cspace_root tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 tcb\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable tcb, ptr) \<lbrace>?R'13 cspace_root tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> liftE (KHeap_D.get_cap (thread, tcb_cspace_slot)) \<lbrace>\<lambda>cspace_root. (\<lambda>_. True) and ?Q15 cspace_root\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> liftE (gets_the (get_tcb thread)) \<lbrace>\<lambda>tcb. valid_objs and valid_cap (tcb_ctable tcb) and valid_global_refs and valid_idle and valid_etcbs and ?Q'17 tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 7. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_etcbs and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<And>tcb a b aa bb bc s s'. \<lbrakk>w = of_bl ptr; length ptr = 32; (a, b) = transform_cslot_ptr (aa, bb); (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; True; True\<rbrakk> \<Longrightarrow> transform_cslot_ptr (aa, bb) = transform_cslot_ptr (fst ((aa, bb), bc))
 2. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cspace_root\<rbrace> CSpace_D.resolve_address_bits cspace_root (of_bl ptr) word_bits \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 tcb\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable tcb, ptr) \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> liftE (KHeap_D.get_cap (thread, tcb_cspace_slot)) \<lbrace>\<lambda>cspace_root. (\<lambda>_. True) and ?Q15 cspace_root\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> liftE (gets_the (get_tcb thread)) \<lbrace>\<lambda>tcb. valid_objs and valid_cap (tcb_ctable tcb) and valid_global_refs and valid_idle and valid_etcbs and ?Q'17 tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 7. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_etcbs and ?Q'5) s proof (prove)
goal (6 subgoals):
 1. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 cspace_root\<rbrace> CSpace_D.resolve_address_bits cspace_root (of_bl ptr) word_bits \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>cspace_root tcb. \<lbrakk>w = of_bl ptr; length ptr = word_bits; cspace_root = transform_cap (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 tcb\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable tcb, ptr) \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> liftE (KHeap_D.get_cap (thread, tcb_cspace_slot)) \<lbrace>\<lambda>cspace_root. (\<lambda>_. True) and ?Q15 cspace_root\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> liftE (gets_the (get_tcb thread)) \<lbrace>\<lambda>tcb. valid_objs and valid_cap (tcb_ctable tcb) and valid_global_refs and valid_idle and valid_etcbs and ?Q'17 tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 6. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_etcbs and ?Q'5) s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>w = of_bl ptr; length ptr = word_bits; not_idle_thread thread s; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; get_tcb thread s = Some y\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_ctable y proof (prove)
goal:
No subgoals!