theory KHeap_DR

lemma dcorres_lookup_cap_and_slot:
  "\<lbrakk>w = of_bl ptr;length ptr = word_bits\<rbrakk> \<Longrightarrow>
   dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cap (fst y) \<and> snd x = transform_cslot_ptr (snd 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_cap_and_slot thread w)
  (cap_fault_on_failure w False $ CSpace_A.lookup_cap_and_slot thread ptr)" apply (simp add: CSpace_D.lookup_cap_and_slot_def cap_fault_injection
                   CSpace_A.lookup_cap_and_slot_def split_def) apply (rule dcorres_injection_handler_rhs) apply (rule corres_guard_imp) apply (rule corres_splitEE) apply (rule dcorres_lookup_slot; clarsimp) apply (rule corres_splitEE) apply simp apply (rule get_cap_corres, rule refl) apply (rule dcorres_returnOk, simp) apply ((wp|simp)+) apply (rule hoare_post_imp_R [where Q'="\<lambda>rv. valid_idle and valid_etcbs and real_cte_at (fst rv)"]) apply (wp lookup_slot_real_cte_at_wp) apply (clarsimp simp: valid_idle_def not_idle_thread_def
                          pred_tcb_at_def obj_at_def is_cap_table_def) apply simp apply simp 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. fst x = transform_cap (fst y) \<and> snd x = transform_cslot_ptr (snd y))) (\<lambda>_. True) (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) (CSpace_D.lookup_cap_and_slot thread w) (cap_fault_on_failure w False $ CSpace_A.lookup_cap_and_slot 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. fst x = transform_cap (fst y) \<and> snd x = transform_cslot_ptr (snd 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 slot <- lookup_slot thread (of_bl ptr);
cap <- liftE (KHeap_D.get_cap slot);
returnOk (cap, slot)
odE) (injection_handler (CapFault (of_bl ptr) False) (doE p <- lookup_slot_for_thread thread ptr;
cap <- liftE (CSpaceAcc_A.get_cap (fst p));
returnOk (cap, fst p)
odE)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cap (fst y) \<and> snd x = transform_cslot_ptr (snd 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 slot <- lookup_slot thread (of_bl ptr);
cap <- liftE (KHeap_D.get_cap slot);
returnOk (cap, slot)
odE) (doE p <- lookup_slot_for_thread thread ptr;
cap <- liftE (CSpaceAcc_A.get_cap (fst p));
returnOk (cap, fst p)
odE) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cap (fst y) \<and> snd x = transform_cslot_ptr (snd y))) ?Q3 ?Q'3 (doE slot <- lookup_slot thread (of_bl ptr);
cap <- liftE (KHeap_D.get_cap slot);
returnOk (cap, slot)
odE) (doE p <- lookup_slot_for_thread thread ptr;
cap <- liftE (CSpaceAcc_A.get_cap (fst p));
returnOk (cap, fst p)
odE)
 2. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ?Q3 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'3 s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?r'7) ?P7 ?P'7 (lookup_slot thread (of_bl ptr)) (lookup_slot_for_thread thread ptr)
 2. \<And>slot p. \<lbrakk>w = of_bl ptr; length ptr = word_bits; ?r'7 slot p\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cap (fst y) \<and> snd x = transform_cslot_ptr (snd y))) (?R7 slot) (?R'7 p) (doE cap <- liftE (KHeap_D.get_cap slot);
returnOk (cap, slot)
odE) (doE cap <- liftE (CSpaceAcc_A.get_cap (fst p));
returnOk (cap, fst p)
odE)
 3. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> lookup_slot thread (of_bl ptr) \<lbrace>?R7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> lookup_slot_for_thread thread ptr \<lbrace>?R'7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> (?P7 and ?Q7) 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'7 and ?Q'7) s proof (prove)
goal (5 subgoals):
 1. \<And>slot p. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cap (fst y) \<and> snd x = transform_cslot_ptr (snd y))) (?R7 slot) (?R'7 p) (doE cap <- liftE (KHeap_D.get_cap slot);
returnOk (cap, slot)
odE) (doE cap <- liftE (CSpaceAcc_A.get_cap (fst p));
returnOk (cap, fst p)
odE)
 2. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> lookup_slot thread (of_bl ptr) \<lbrace>?R7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> lookup_slot_for_thread thread ptr \<lbrace>?R'7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) 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_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and ?Q'7) s proof (prove)
goal (8 subgoals):
 1. \<And>slot p. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?r'21 slot p) (?P22 slot) (?P'24 p) (liftE (KHeap_D.get_cap slot)) (liftE (CSpaceAcc_A.get_cap (fst p)))
 2. \<And>slot p cap capa. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p); ?r'21 slot p cap capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cap (fst y) \<and> snd x = transform_cslot_ptr (snd y))) (?R21 slot p cap) (?R'21 slot p capa) (returnOk (cap, slot)) (returnOk (capa, fst p))
 3. \<And>slot p. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 slot\<rbrace> liftE (KHeap_D.get_cap slot) \<lbrace>?R21 slot p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>slot p. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 p\<rbrace> liftE (CSpaceAcc_A.get_cap (fst p)) \<lbrace>?R'21 slot p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> lookup_slot thread (of_bl ptr) \<lbrace>\<lambda>slot. ?P22 slot and ?Q23 slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> lookup_slot_for_thread thread ptr \<lbrace>\<lambda>p. ?P'24 p and ?Q'25 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 8. \<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_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and ?Q'7) s proof (prove)
goal (8 subgoals):
 1. \<And>slot p. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p)\<rbrakk> \<Longrightarrow> dcorres (?r'21 (transform_cslot_ptr (fst p)) p) (?P22 (transform_cslot_ptr (fst p))) (?P'24 p) (KHeap_D.get_cap (transform_cslot_ptr (fst p))) (CSpaceAcc_A.get_cap (fst p))
 2. \<And>slot p cap capa. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p); ?r'21 slot p cap capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cap (fst y) \<and> snd x = transform_cslot_ptr (snd y))) (?R21 slot p cap) (?R'21 slot p capa) (returnOk (cap, slot)) (returnOk (capa, fst p))
 3. \<And>slot p. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 slot\<rbrace> liftE (KHeap_D.get_cap slot) \<lbrace>?R21 slot p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>slot p. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 p\<rbrace> liftE (CSpaceAcc_A.get_cap (fst p)) \<lbrace>?R'21 slot p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> lookup_slot thread (of_bl ptr) \<lbrace>\<lambda>slot. ?P22 slot and ?Q23 slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> lookup_slot_for_thread thread ptr \<lbrace>\<lambda>p. ?P'24 p and ?Q'25 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 8. \<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_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and ?Q'7) s proof (prove)
goal (7 subgoals):
 1. \<And>slot p cap capa. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p); cap = transform_cap capa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x y. fst x = transform_cap (fst y) \<and> snd x = transform_cslot_ptr (snd y))) (?R21 slot p cap) (?R'21 slot p capa) (returnOk (cap, slot)) (returnOk (capa, fst p))
 2. \<And>slot p. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 slot\<rbrace> liftE (KHeap_D.get_cap slot) \<lbrace>?R21 slot p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>slot p. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 p\<rbrace> liftE (CSpaceAcc_A.get_cap (fst p)) \<lbrace>?R'21 slot p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> lookup_slot thread (of_bl ptr) \<lbrace>\<lambda>slot. (\<lambda>a. True) and ?Q23 slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> lookup_slot_for_thread thread ptr \<lbrace>\<lambda>p. valid_idle and not_idle_thread (fst (fst p)) and valid_etcbs and ?Q'25 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) 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_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and ?Q'7) s proof (prove)
goal (6 subgoals):
 1. \<And>slot p. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 slot\<rbrace> liftE (KHeap_D.get_cap slot) \<lbrace>\<lambda>cap _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>slot p. \<lbrakk>w = of_bl ptr; length ptr = word_bits; slot = transform_cslot_ptr (fst p)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 p\<rbrace> liftE (CSpaceAcc_A.get_cap (fst p)) \<lbrace>\<lambda>capa _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> lookup_slot thread (of_bl ptr) \<lbrace>\<lambda>slot. (\<lambda>a. True) and ?Q23 slot\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> lookup_slot_for_thread thread ptr \<lbrace>\<lambda>p. valid_idle and not_idle_thread (fst (fst p)) and valid_etcbs and ?Q'25 p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) 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_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and ?Q'7) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?P'69\<rbrace> lookup_slot_for_thread thread ptr \<lbrace>\<lambda>rv s. not_idle_thread (fst (fst rv)) s \<and> valid_etcbs s\<rbrace>, -
 2. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> ?P'59 s)) 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> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>s. True \<and> valid_idle s \<and> ?P'69 s)) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>w = of_bl ptr; length ptr = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>?P'69\<rbrace> lookup_slot_for_thread thread ptr \<lbrace>\<lambda>rv. valid_idle and valid_etcbs and real_cte_at (fst rv)\<rbrace>, -
 2. \<And>rv s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; (valid_idle and valid_etcbs and real_cte_at (fst rv)) s\<rbrakk> \<Longrightarrow> not_idle_thread (fst (fst rv)) s \<and> valid_etcbs s
 3. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> ?P'59 s)) s
 4. \<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_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>s. True \<and> valid_idle s \<and> ?P'69 s)) s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; (valid_idle and valid_etcbs and real_cte_at (fst rv)) s\<rbrakk> \<Longrightarrow> not_idle_thread (fst (fst rv)) s \<and> valid_etcbs s
 2. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> ?P'59 s)) 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> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>s. True \<and> valid_idle s \<and> (valid_idle and valid_etcbs) s \<and> valid_objs s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>w = of_bl ptr; length ptr = word_bits; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True \<and> ?P'59 s)) s
 2. \<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_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>s. True \<and> valid_idle s \<and> (valid_idle and valid_etcbs) s \<and> valid_objs s)) s proof (prove)
goal (1 subgoal):
 1. \<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_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>s. True \<and> valid_idle s \<and> (valid_idle and valid_etcbs) s \<and> valid_objs s)) s proof (prove)
goal:
No subgoals!