theory IRQ_DP

lemma seL4_IRQHandler_IRQControl_Get:
  "\<lbrace>\<guillemotleft>root_tcb_id \<mapsto>f root_tcb  \<and>*
    (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
    (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
     irq \<mapsto>irq irq_id \<and>*
     cnode_id  \<mapsto>f CNode (empty_cnode root_size) \<and>*
    (cnode_id, control_index) \<mapsto>c IrqControlCap \<and>*
    (cnode_id, root_index) \<mapsto>c cnode_cap \<and>*
    (cnode_id, target_index) \<mapsto>c target_cap \<and>* R\<guillemotright>
     and K (is_tcb root_tcb \<and>
            is_cnode_cap cnode_cap \<and>
            is_cnode_cap cnode_cap \<and>
            cnode_id      = cap_object cnode_cap \<and>
            target_index  = offset node_index root_size \<and>
            root_index    = offset croot root_size \<and>
            control_index = offset control_cap root_size \<and>
            one_lvl_lookup cnode_cap word_bits root_size \<and>
            one_lvl_lookup cnode_cap (unat node_depth) root_size \<and>
            guard_equal cnode_cap node_index (unat node_depth) \<and>
            guard_equal cnode_cap croot word_bits  \<and>
            guard_equal cnode_cap control_cap word_bits \<and>
            guard_equal cnode_cap node_index word_bits \<and>
            unat node_depth \<le> word_bits \<and> 0 < unat node_depth)\<rbrace>
     seL4_IRQControl_Get control_cap irq croot node_index node_depth
  \<lbrace>\<lambda>fail.
    \<guillemotleft>root_tcb_id \<mapsto>f root_tcb \<and>*
    (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>*
    \<comment> \<open>Cap to the root CNode.\<close>
    (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>*
     irq \<mapsto>irq irq_id \<and>*
    \<comment> \<open>Root CNode.\<close>
     cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
    (cnode_id, control_index) \<mapsto>c IrqControlCap \<and>*
    (cnode_id, root_index) \<mapsto>c cnode_cap \<and>*
    (cnode_id, target_index) \<mapsto>c IrqHandlerCap irq \<and>* R\<guillemotright>\<rbrace>" apply (rule hoare_gen_asm, elim conjE) apply (sep_wp seL4_IRQHandler_IRQControl_Get_helper [where t="obj_tcb root_tcb"]) apply (rule conjI, simp)+ apply simp apply simp apply (rule conjI) apply sep_solve apply (clarsimp simp: is_irqcontrol_cap_def ep_related_cap_def split: cdl_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Separation_SD.lift (root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (cnode_id, control_index) \<mapsto>c IrqControlCap \<and>* (cnode_id, root_index) \<mapsto>c cnode_cap \<and>* (cnode_id, target_index) \<mapsto>c target_cap \<and>* R) and K (is_tcb root_tcb \<and> is_cnode_cap cnode_cap \<and> is_cnode_cap cnode_cap \<and> cnode_id = cap_object cnode_cap \<and> target_index = offset node_index root_size \<and> root_index = offset croot root_size \<and> control_index = offset control_cap root_size \<and> one_lvl_lookup cnode_cap word_bits root_size \<and> one_lvl_lookup cnode_cap (unat node_depth) root_size \<and> guard_equal cnode_cap node_index (unat node_depth) \<and> guard_equal cnode_cap croot word_bits \<and> guard_equal cnode_cap control_cap word_bits \<and> guard_equal cnode_cap node_index word_bits \<and> unat node_depth \<le> word_bits \<and> 0 < unat node_depth)\<rbrace> seL4_IRQControl_Get control_cap irq croot node_index node_depth \<lbrace>\<lambda>fail. Separation_SD.lift (root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (cnode_id, control_index) \<mapsto>c IrqControlCap \<and>* (cnode_id, root_index) \<mapsto>c cnode_cap \<and>* (cnode_id, target_index) \<mapsto>c IrqHandlerCap irq \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_tcb root_tcb; is_cnode_cap cnode_cap; is_cnode_cap cnode_cap; cnode_id = cap_object cnode_cap; target_index = offset node_index root_size; root_index = offset croot root_size; control_index = offset control_cap root_size; one_lvl_lookup cnode_cap word_bits root_size; one_lvl_lookup cnode_cap (unat node_depth) root_size; guard_equal cnode_cap node_index (unat node_depth); guard_equal cnode_cap croot word_bits; guard_equal cnode_cap control_cap word_bits; guard_equal cnode_cap node_index word_bits; unat node_depth \<le> word_bits; 0 < unat node_depth\<rbrakk> \<Longrightarrow> \<lbrace>Separation_SD.lift (root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (cnode_id, control_index) \<mapsto>c IrqControlCap \<and>* (cnode_id, root_index) \<mapsto>c cnode_cap \<and>* (cnode_id, target_index) \<mapsto>c target_cap \<and>* R)\<rbrace> seL4_IRQControl_Get control_cap irq croot node_index node_depth \<lbrace>\<lambda>fail. Separation_SD.lift (root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (cnode_id, control_index) \<mapsto>c IrqControlCap \<and>* (cnode_id, root_index) \<mapsto>c cnode_cap \<and>* (cnode_id, target_index) \<mapsto>c IrqHandlerCap irq \<and>* R)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>R. \<lbrakk>is_tcb root_tcb; is_cnode_cap cnode_cap; is_cnode_cap cnode_cap; cnode_id = cap_object cnode_cap; target_index = offset node_index root_size; root_index = offset croot root_size; control_index = offset control_cap root_size; one_lvl_lookup cnode_cap word_bits root_size; one_lvl_lookup cnode_cap (unat node_depth) root_size; guard_equal cnode_cap node_index (unat node_depth); guard_equal cnode_cap croot word_bits; guard_equal cnode_cap control_cap word_bits; guard_equal cnode_cap node_index word_bits; unat node_depth \<le> word_bits; 0 < unat node_depth\<rbrakk> \<Longrightarrow> ?irq_cap17 = IrqHandlerCap irq \<and> ?target_index17 R = offset node_index ?root_size17 \<and> ?root_index17 R = offset croot ?root_size17 \<and> ?control_index17 R = offset control_cap ?root_size17 \<and> ?target_ptr17 = (cap_object ?root_cap17, ?target_index17 R) \<and> ?control_ptr17 = (cap_object ?root_cap17, ?control_index17 R) \<and> ?root_ptr17 = (cap_object ?root_cap17, ?root_index17 R) \<and> ?root_tcb17 = Tcb (obj_tcb root_tcb)
 2. \<And>s. \<lbrakk>is_tcb root_tcb; is_cnode_cap cnode_cap; is_cnode_cap cnode_cap; cnode_id = cap_object cnode_cap; target_index = offset node_index root_size; root_index = offset croot root_size; control_index = offset control_cap root_size; one_lvl_lookup cnode_cap word_bits root_size; one_lvl_lookup cnode_cap (unat node_depth) root_size; guard_equal cnode_cap node_index (unat node_depth); guard_equal cnode_cap croot word_bits; guard_equal cnode_cap control_cap word_bits; guard_equal cnode_cap node_index word_bits; unat node_depth \<le> word_bits; 0 < unat node_depth; Separation_SD.lift (root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (cnode_id, control_index) \<mapsto>c IrqControlCap \<and>* (cnode_id, root_index) \<mapsto>c cnode_cap \<and>* (cnode_id, target_index) \<mapsto>c target_cap \<and>* R) s\<rbrakk> \<Longrightarrow> Separation_SD.lift ((((((((root_tcb_id \<mapsto>f ?root_tcb17 \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap) \<and>* irq \<mapsto>irq ?obj17) \<and>* cap_object ?root_cap17 \<mapsto>f CNode (empty_cnode ?root_size17)) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c ?root_cap17) \<and>* ?control_ptr17 \<mapsto>c ?c_cap17) \<and>* ?target_ptr17 \<mapsto>c ?target_cap17) \<and>* ?root_ptr17 \<mapsto>c ?root_cap17) \<and>* (((((((root_tcb_id \<mapsto>f ?root_tcb17 \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap) \<and>* cap_object ?root_cap17 \<mapsto>f CNode (empty_cnode ?root_size17)) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c ?root_cap17) \<and>* irq \<mapsto>irq ?obj17) \<and>* ?control_ptr17 \<mapsto>c ?c_cap17) \<and>* ?target_ptr17 \<mapsto>c ?irq_cap17) \<and>* ?root_ptr17 \<mapsto>c ?root_cap17 \<longrightarrow>* root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (cnode_id, control_index) \<mapsto>c IrqControlCap \<and>* (cnode_id, root_index) \<mapsto>c cnode_cap \<and>* (cnode_id, target_index) \<mapsto>c IrqHandlerCap irq \<and>* R) and K (\<not> ep_related_cap ?c_cap17 \<and> one_lvl_lookup ?root_cap17 word_bits ?root_size17 \<and> one_lvl_lookup ?root_cap17 (unat node_depth) ?root_size17 \<and> guard_equal ?root_cap17 node_index (unat node_depth) \<and> guard_equal ?root_cap17 croot word_bits \<and> guard_equal ?root_cap17 control_cap word_bits \<and> guard_equal ?root_cap17 node_index word_bits \<and> unat node_depth \<le> word_bits \<and> 0 < unat node_depth \<and> is_irqcontrol_cap ?c_cap17 \<and> is_cnode_cap ?root_cap17 \<and> is_cnode_cap ?root_cap17)) s proof (prove)
goal (2 subgoals):
 1. \<And>R. \<lbrakk>is_tcb root_tcb; is_cnode_cap cnode_cap; is_cnode_cap cnode_cap; cnode_id = cap_object cnode_cap; target_index = offset node_index root_size; root_index = offset croot root_size; control_index = offset control_cap root_size; one_lvl_lookup cnode_cap word_bits root_size; one_lvl_lookup cnode_cap (unat node_depth) root_size; guard_equal cnode_cap node_index (unat node_depth); guard_equal cnode_cap croot word_bits; guard_equal cnode_cap control_cap word_bits; guard_equal cnode_cap node_index word_bits; unat node_depth \<le> word_bits; 0 < unat node_depth\<rbrakk> \<Longrightarrow> ?root_tcb17 = Tcb (obj_tcb root_tcb)
 2. \<And>s. \<lbrakk>is_tcb root_tcb; is_cnode_cap cnode_cap; is_cnode_cap cnode_cap; cnode_id = cap_object cnode_cap; target_index = offset node_index root_size; root_index = offset croot root_size; control_index = offset control_cap root_size; one_lvl_lookup cnode_cap word_bits root_size; one_lvl_lookup cnode_cap (unat node_depth) root_size; guard_equal cnode_cap node_index (unat node_depth); guard_equal cnode_cap croot word_bits; guard_equal cnode_cap control_cap word_bits; guard_equal cnode_cap node_index word_bits; unat node_depth \<le> word_bits; 0 < unat node_depth; Separation_SD.lift (root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (cnode_id, control_index) \<mapsto>c IrqControlCap \<and>* (cnode_id, root_index) \<mapsto>c cnode_cap \<and>* (cnode_id, target_index) \<mapsto>c target_cap \<and>* R) s\<rbrakk> \<Longrightarrow> Separation_SD.lift ((((((((root_tcb_id \<mapsto>f ?root_tcb17 \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap) \<and>* irq \<mapsto>irq ?obj17) \<and>* cap_object ?root_cap17 \<mapsto>f CNode (empty_cnode ?root_size17)) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c ?root_cap17) \<and>* (cap_object ?root_cap17, offset control_cap ?root_size17) \<mapsto>c ?c_cap17) \<and>* (cap_object ?root_cap17, offset node_index ?root_size17) \<mapsto>c ?target_cap17) \<and>* (cap_object ?root_cap17, offset croot ?root_size17) \<mapsto>c ?root_cap17) \<and>* (((((((root_tcb_id \<mapsto>f ?root_tcb17 \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap) \<and>* cap_object ?root_cap17 \<mapsto>f CNode (empty_cnode ?root_size17)) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c ?root_cap17) \<and>* irq \<mapsto>irq ?obj17) \<and>* (cap_object ?root_cap17, offset control_cap ?root_size17) \<mapsto>c ?c_cap17) \<and>* (cap_object ?root_cap17, offset node_index ?root_size17) \<mapsto>c IrqHandlerCap irq) \<and>* (cap_object ?root_cap17, offset croot ?root_size17) \<mapsto>c ?root_cap17 \<longrightarrow>* root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (cnode_id, control_index) \<mapsto>c IrqControlCap \<and>* (cnode_id, root_index) \<mapsto>c cnode_cap \<and>* (cnode_id, target_index) \<mapsto>c IrqHandlerCap irq \<and>* R) and K (\<not> ep_related_cap ?c_cap17 \<and> one_lvl_lookup ?root_cap17 word_bits ?root_size17 \<and> one_lvl_lookup ?root_cap17 (unat node_depth) ?root_size17 \<and> guard_equal ?root_cap17 node_index (unat node_depth) \<and> guard_equal ?root_cap17 croot word_bits \<and> guard_equal ?root_cap17 control_cap word_bits \<and> guard_equal ?root_cap17 node_index word_bits \<and> unat node_depth \<le> word_bits \<and> 0 < unat node_depth \<and> is_irqcontrol_cap ?c_cap17 \<and> is_cnode_cap ?root_cap17 \<and> is_cnode_cap ?root_cap17)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_tcb root_tcb; is_cnode_cap cnode_cap; is_cnode_cap cnode_cap; cnode_id = cap_object cnode_cap; target_index = offset node_index root_size; root_index = offset croot root_size; control_index = offset control_cap root_size; one_lvl_lookup cnode_cap word_bits root_size; one_lvl_lookup cnode_cap (unat node_depth) root_size; guard_equal cnode_cap node_index (unat node_depth); guard_equal cnode_cap croot word_bits; guard_equal cnode_cap control_cap word_bits; guard_equal cnode_cap node_index word_bits; unat node_depth \<le> word_bits; 0 < unat node_depth; Separation_SD.lift (root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (cnode_id, control_index) \<mapsto>c IrqControlCap \<and>* (cnode_id, root_index) \<mapsto>c cnode_cap \<and>* (cnode_id, target_index) \<mapsto>c target_cap \<and>* R) s\<rbrakk> \<Longrightarrow> Separation_SD.lift ((((((((root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap) \<and>* irq \<mapsto>irq ?obj17) \<and>* cap_object ?root_cap17 \<mapsto>f CNode (empty_cnode ?root_size17)) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c ?root_cap17) \<and>* (cap_object ?root_cap17, offset control_cap ?root_size17) \<mapsto>c ?c_cap17) \<and>* (cap_object ?root_cap17, offset node_index ?root_size17) \<mapsto>c ?target_cap17) \<and>* (cap_object ?root_cap17, offset croot ?root_size17) \<mapsto>c ?root_cap17) \<and>* (((((((root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap) \<and>* cap_object ?root_cap17 \<mapsto>f CNode (empty_cnode ?root_size17)) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c ?root_cap17) \<and>* irq \<mapsto>irq ?obj17) \<and>* (cap_object ?root_cap17, offset control_cap ?root_size17) \<mapsto>c ?c_cap17) \<and>* (cap_object ?root_cap17, offset node_index ?root_size17) \<mapsto>c IrqHandlerCap irq) \<and>* (cap_object ?root_cap17, offset croot ?root_size17) \<mapsto>c ?root_cap17 \<longrightarrow>* root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (cnode_id, control_index) \<mapsto>c IrqControlCap \<and>* (cnode_id, root_index) \<mapsto>c cnode_cap \<and>* (cnode_id, target_index) \<mapsto>c IrqHandlerCap irq \<and>* R) and K (\<not> ep_related_cap ?c_cap17 \<and> one_lvl_lookup ?root_cap17 word_bits ?root_size17 \<and> one_lvl_lookup ?root_cap17 (unat node_depth) ?root_size17 \<and> guard_equal ?root_cap17 node_index (unat node_depth) \<and> guard_equal ?root_cap17 croot word_bits \<and> guard_equal ?root_cap17 control_cap word_bits \<and> guard_equal ?root_cap17 node_index word_bits \<and> unat node_depth \<le> word_bits \<and> 0 < unat node_depth \<and> is_irqcontrol_cap ?c_cap17 \<and> is_cnode_cap ?root_cap17 \<and> is_cnode_cap ?root_cap17)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_tcb root_tcb; is_cnode_cap cnode_cap; cnode_id = cap_object cnode_cap; target_index = offset node_index root_size; root_index = offset croot root_size; control_index = offset control_cap root_size; one_lvl_lookup cnode_cap word_bits root_size; one_lvl_lookup cnode_cap (unat node_depth) root_size; guard_equal cnode_cap node_index (unat node_depth); guard_equal cnode_cap croot word_bits; guard_equal cnode_cap control_cap word_bits; guard_equal cnode_cap node_index word_bits; unat node_depth \<le> word_bits; 0 < unat node_depth; Separation_SD.lift (root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (cap_object cnode_cap, offset control_cap root_size) \<mapsto>c IrqControlCap \<and>* (cap_object cnode_cap, offset croot root_size) \<mapsto>c cnode_cap \<and>* (cap_object cnode_cap, offset node_index root_size) \<mapsto>c target_cap \<and>* R) s\<rbrakk> \<Longrightarrow> Separation_SD.lift ((((((((root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap) \<and>* irq \<mapsto>irq ?obj17) \<and>* cap_object ?root_cap17 \<mapsto>f CNode (empty_cnode ?root_size17)) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c ?root_cap17) \<and>* (cap_object ?root_cap17, offset control_cap ?root_size17) \<mapsto>c ?c_cap17) \<and>* (cap_object ?root_cap17, offset node_index ?root_size17) \<mapsto>c ?target_cap17) \<and>* (cap_object ?root_cap17, offset croot ?root_size17) \<mapsto>c ?root_cap17) \<and>* (((((((root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap) \<and>* cap_object ?root_cap17 \<mapsto>f CNode (empty_cnode ?root_size17)) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c ?root_cap17) \<and>* irq \<mapsto>irq ?obj17) \<and>* (cap_object ?root_cap17, offset control_cap ?root_size17) \<mapsto>c ?c_cap17) \<and>* (cap_object ?root_cap17, offset node_index ?root_size17) \<mapsto>c IrqHandlerCap irq) \<and>* (cap_object ?root_cap17, offset croot ?root_size17) \<mapsto>c ?root_cap17 \<longrightarrow>* root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (cap_object cnode_cap, offset control_cap root_size) \<mapsto>c IrqControlCap \<and>* (cap_object cnode_cap, offset croot root_size) \<mapsto>c cnode_cap \<and>* (cap_object cnode_cap, offset node_index root_size) \<mapsto>c IrqHandlerCap irq \<and>* R)) s \<and> \<not> ep_related_cap ?c_cap17 \<and> one_lvl_lookup ?root_cap17 word_bits ?root_size17 \<and> one_lvl_lookup ?root_cap17 (unat node_depth) ?root_size17 \<and> guard_equal ?root_cap17 node_index (unat node_depth) \<and> guard_equal ?root_cap17 croot word_bits \<and> guard_equal ?root_cap17 control_cap word_bits \<and> guard_equal ?root_cap17 node_index word_bits \<and> is_irqcontrol_cap ?c_cap17 \<and> is_cnode_cap ?root_cap17 proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_tcb root_tcb; is_cnode_cap cnode_cap; cnode_id = cap_object cnode_cap; target_index = offset node_index root_size; root_index = offset croot root_size; control_index = offset control_cap root_size; one_lvl_lookup cnode_cap word_bits root_size; one_lvl_lookup cnode_cap (unat node_depth) root_size; guard_equal cnode_cap node_index (unat node_depth); guard_equal cnode_cap croot word_bits; guard_equal cnode_cap control_cap word_bits; guard_equal cnode_cap node_index word_bits; unat node_depth \<le> word_bits; 0 < unat node_depth; Separation_SD.lift (root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (cap_object cnode_cap, offset control_cap root_size) \<mapsto>c IrqControlCap \<and>* (cap_object cnode_cap, offset croot root_size) \<mapsto>c cnode_cap \<and>* (cap_object cnode_cap, offset node_index root_size) \<mapsto>c target_cap \<and>* R) s\<rbrakk> \<Longrightarrow> Separation_SD.lift ((((((((root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap) \<and>* irq \<mapsto>irq ?obj17) \<and>* cap_object ?root_cap17 \<mapsto>f CNode (empty_cnode ?root_size17)) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c ?root_cap17) \<and>* (cap_object ?root_cap17, offset control_cap ?root_size17) \<mapsto>c ?c_cap17) \<and>* (cap_object ?root_cap17, offset node_index ?root_size17) \<mapsto>c ?target_cap17) \<and>* (cap_object ?root_cap17, offset croot ?root_size17) \<mapsto>c ?root_cap17) \<and>* (((((((root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap) \<and>* cap_object ?root_cap17 \<mapsto>f CNode (empty_cnode ?root_size17)) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c ?root_cap17) \<and>* irq \<mapsto>irq ?obj17) \<and>* (cap_object ?root_cap17, offset control_cap ?root_size17) \<mapsto>c ?c_cap17) \<and>* (cap_object ?root_cap17, offset node_index ?root_size17) \<mapsto>c IrqHandlerCap irq) \<and>* (cap_object ?root_cap17, offset croot ?root_size17) \<mapsto>c ?root_cap17 \<longrightarrow>* root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (cap_object cnode_cap, offset control_cap root_size) \<mapsto>c IrqControlCap \<and>* (cap_object cnode_cap, offset croot root_size) \<mapsto>c cnode_cap \<and>* (cap_object cnode_cap, offset node_index root_size) \<mapsto>c IrqHandlerCap irq \<and>* R)) s
 2. \<And>s. \<lbrakk>is_tcb root_tcb; is_cnode_cap cnode_cap; cnode_id = cap_object cnode_cap; target_index = offset node_index root_size; root_index = offset croot root_size; control_index = offset control_cap root_size; one_lvl_lookup cnode_cap word_bits root_size; one_lvl_lookup cnode_cap (unat node_depth) root_size; guard_equal cnode_cap node_index (unat node_depth); guard_equal cnode_cap croot word_bits; guard_equal cnode_cap control_cap word_bits; guard_equal cnode_cap node_index word_bits; unat node_depth \<le> word_bits; 0 < unat node_depth; Separation_SD.lift (root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (cap_object cnode_cap, offset control_cap root_size) \<mapsto>c IrqControlCap \<and>* (cap_object cnode_cap, offset croot root_size) \<mapsto>c cnode_cap \<and>* (cap_object cnode_cap, offset node_index root_size) \<mapsto>c target_cap \<and>* R) s\<rbrakk> \<Longrightarrow> \<not> ep_related_cap ?c_cap17 \<and> one_lvl_lookup ?root_cap17 word_bits ?root_size17 \<and> one_lvl_lookup ?root_cap17 (unat node_depth) ?root_size17 \<and> guard_equal ?root_cap17 node_index (unat node_depth) \<and> guard_equal ?root_cap17 croot word_bits \<and> guard_equal ?root_cap17 control_cap word_bits \<and> guard_equal ?root_cap17 node_index word_bits \<and> is_irqcontrol_cap ?c_cap17 \<and> is_cnode_cap ?root_cap17 proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_tcb root_tcb; is_cnode_cap cnode_cap; cnode_id = cap_object cnode_cap; target_index = offset node_index root_size; root_index = offset croot root_size; control_index = offset control_cap root_size; one_lvl_lookup cnode_cap word_bits root_size; one_lvl_lookup cnode_cap (unat node_depth) root_size; guard_equal cnode_cap node_index (unat node_depth); guard_equal cnode_cap croot word_bits; guard_equal cnode_cap control_cap word_bits; guard_equal cnode_cap node_index word_bits; unat node_depth \<le> word_bits; 0 < unat node_depth; Separation_SD.lift (root_tcb_id \<mapsto>f root_tcb \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* irq \<mapsto>irq irq_id \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (cap_object cnode_cap, offset control_cap root_size) \<mapsto>c IrqControlCap \<and>* (cap_object cnode_cap, offset croot root_size) \<mapsto>c cnode_cap \<and>* (cap_object cnode_cap, offset node_index root_size) \<mapsto>c target_cap \<and>* R) s\<rbrakk> \<Longrightarrow> \<not> ep_related_cap IrqControlCap \<and> one_lvl_lookup cnode_cap word_bits root_size \<and> one_lvl_lookup cnode_cap (unat node_depth) root_size \<and> guard_equal cnode_cap node_index (unat node_depth) \<and> guard_equal cnode_cap croot word_bits \<and> guard_equal cnode_cap control_cap word_bits \<and> guard_equal cnode_cap node_index word_bits \<and> is_irqcontrol_cap IrqControlCap \<and> is_cnode_cap cnode_cap proof (prove)
goal:
No subgoals!