theory KHeap_DR

lemma not_idle_thread_resolve_address_bits:
  "\<lbrace>valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread and valid_etcbs\<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>_. \<top>\<rbrace>" apply (rule validE_R_validE) apply (rule_tac hoare_vcg_precond_impE_R) apply (rule validE_validE_R) apply (rule_tac Q="\<lambda>r. valid_etcbs and valid_global_refs and valid_objs and valid_idle and
                          valid_irq_node and ex_cte_cap_to (fst r)"
          in hoare_post_impErr[where E="\<lambda>x y. True"]) apply (wp rab_cte_cap_to) apply (auto intro: ex_cte_cap_wp_to_not_idle)[2] apply (clarsimp simp:ex_cte_cap_to_def) apply (rule_tac x = thread in exI,rule_tac x = "tcb_cnode_index 0" in exI) apply (clarsimp simp:cte_wp_at_cases obj_at_def is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread and valid_etcbs\<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> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread and valid_etcbs\<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>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'2\<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. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread and valid_etcbs) s \<Longrightarrow> ?P'2 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'2\<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. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread and valid_etcbs) s \<Longrightarrow> ?P'2 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'2\<rbrace> CSpace_A.resolve_address_bits (tcb_ctable obj, blist) \<lbrace>\<lambda>r. valid_etcbs and valid_global_refs and valid_objs and valid_idle and valid_irq_node and ex_cte_cap_wp_to (\<lambda>_. True) (fst r)\<rbrace>, \<lbrace>\<lambda>x y. True\<rbrace>
 2. \<And>rv s. (valid_etcbs and valid_global_refs and valid_objs and valid_idle and valid_irq_node and ex_cte_cap_wp_to (\<lambda>_. True) (fst rv)) s \<Longrightarrow> not_idle_thread (fst (fst rv)) s \<and> valid_etcbs s
 3. \<And>e s. True \<Longrightarrow> True
 4. \<And>s. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread and valid_etcbs) s \<Longrightarrow> ?P'2 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (valid_etcbs and valid_global_refs and valid_objs and valid_idle and valid_irq_node and ex_cte_cap_wp_to (\<lambda>_. True) (fst rv)) s \<Longrightarrow> not_idle_thread (fst (fst rv)) s \<and> valid_etcbs s
 2. \<And>e s. True \<Longrightarrow> True
 3. \<And>s. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread and valid_etcbs) s \<Longrightarrow> True \<and> (valid_etcbs and valid_global_refs and valid_objs and valid_idle and valid_irq_node) s \<and> (Structures_A.is_cnode_cap (fst (tcb_ctable obj, blist)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (tcb_ctable obj, blist)) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>cap. True) r s)) \<and> (\<forall>cap. Structures_A.is_cnode_cap cap \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread and valid_etcbs) s \<Longrightarrow> True \<and> (valid_etcbs and valid_global_refs and valid_objs and valid_idle and valid_irq_node) s \<and> (Structures_A.is_cnode_cap (fst (tcb_ctable obj, blist)) \<longrightarrow> (\<forall>r\<in>cte_refs (fst (tcb_ctable obj, blist)) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>cap. True) r s)) \<and> (\<forall>cap. Structures_A.is_cnode_cap cap \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>valid_global_refs s; valid_objs s; valid_idle s; valid_irq_node s; ko_at (TCB obj) thread s; valid_etcbs s; Structures_A.is_cnode_cap (tcb_ctable obj); (a, b) \<in> cte_refs (tcb_ctable obj) (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> \<exists>aa ba. cte_wp_at (\<lambda>c. (a, b) \<in> cte_refs c (interrupt_irq_node s)) (aa, ba) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>valid_global_refs s; valid_objs s; valid_idle s; valid_irq_node s; ko_at (TCB obj) thread s; valid_etcbs s; Structures_A.is_cnode_cap (tcb_ctable obj); (a, b) \<in> cte_refs (tcb_ctable obj) (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. (a, b) \<in> cte_refs c (interrupt_irq_node s)) (thread, tcb_cnode_index 0) s proof (prove)
goal:
No subgoals!