theory IRQ_DP

lemma invoke_irq_handler_set_handler_wp:
       "\<lbrace>< irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap' \<and>* R> and
         K (\<not> ep_related_cap cap' \<and> \<not> is_untyped_cap cap)\<rbrace>
        invoke_irq_handler (SetIrqHandler irq cap slot)
       \<lbrace>\<lambda>_. < irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R> \<rbrace>" apply (clarsimp simp: invoke_irq_handler_def, wp) apply (wp sep_wp: insert_cap_child_wp insert_cap_sibling_wp)+ apply (sep_wp delete_cap_simple_format[where cap=cap'])+ apply (safe) apply (clarsimp) apply (frule sep_map_i_cdl_irq, clarsimp simp: get_irq_slot_def) apply (sep_solve) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap' \<and>* R) and K (\<not> ep_related_cap cap' \<and> cap_type cap \<noteq> Some UntypedType)\<rbrace> invoke_irq_handler (SetIrqHandler irq cap slot) \<lbrace>\<lambda>_. cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>irqslot y. \<lbrace>?P3 irqslot y\<rbrace> insert_cap_child cap slot irqslot \<lbrace>\<lambda>_. cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R)\<rbrace>
 2. \<And>irqslot y. \<lbrace>?P'3 irqslot y\<rbrace> insert_cap_sibling cap slot irqslot \<lbrace>\<lambda>_. cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R)\<rbrace>
 3. \<And>irqslot. \<lbrace>?B1 irqslot\<rbrace> delete_cap_simple irqslot \<lbrace>\<lambda>y. ?P3 irqslot y and ?P'3 irqslot y\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets (get_irq_slot irq) \<lbrace>?B1\<rbrace>
 5. \<And>s. (cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap' \<and>* R) and (\<lambda>y. \<not> ep_related_cap cap' \<and> cap_type cap \<noteq> Some UntypedType)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>irqslot. \<lbrace>?B1 irqslot\<rbrace> delete_cap_simple irqslot \<lbrace>\<lambda>y s. cdl.lift (irqslot \<mapsto>c - \<and>* (irqslot \<mapsto>c cap \<longrightarrow>* irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) and K (cap_type cap \<noteq> Some UntypedType)) s \<and> cdl.lift (irqslot \<mapsto>c - \<and>* (irqslot \<mapsto>c cap \<longrightarrow>* irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) and K (cap_type cap \<noteq> Some UntypedType)) s\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets (get_irq_slot irq) \<lbrace>?B1\<rbrace>
 3. \<And>s. (cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap' \<and>* R) and (\<lambda>y. \<not> ep_related_cap cap' \<and> cap_type cap \<noteq> Some UntypedType)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap' \<and>* R) and (\<lambda>y. \<not> ep_related_cap cap' \<and> cap_type cap \<noteq> Some UntypedType)) s \<Longrightarrow> cdl.lift (get_irq_slot irq s \<mapsto>c cap' \<and>* (get_irq_slot irq s \<mapsto>c NullCap \<longrightarrow>* (\<lambda>a. ((get_irq_slot irq s) \<mapsto>c - \<and>* (get_irq_slot irq s \<mapsto>c cap \<longrightarrow>* irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) and K (cap_type cap \<noteq> Some UntypedType)) a \<and> ((get_irq_slot irq s) \<mapsto>c - \<and>* (get_irq_slot irq s \<mapsto>c cap \<longrightarrow>* irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) and K (cap_type cap \<noteq> Some UntypedType)) a)) and K (\<not> ep_related_cap cap')) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap' \<and>* R) s; \<not> ep_related_cap cap'; cap_type cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> cdl.lift (get_irq_slot irq s \<mapsto>c cap' \<and>* (get_irq_slot irq s \<mapsto>c NullCap \<longrightarrow>* (\<lambda>a. ((get_irq_slot irq s) \<mapsto>c - \<and>* (get_irq_slot irq s \<mapsto>c cap \<longrightarrow>* irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) and K (cap_type cap \<noteq> Some UntypedType)) a \<and> ((get_irq_slot irq s) \<mapsto>c - \<and>* (get_irq_slot irq s \<mapsto>c cap \<longrightarrow>* irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) and K (cap_type cap \<noteq> Some UntypedType)) a))) s
 2. \<And>s. \<lbrakk>cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap' \<and>* R) s; \<not> ep_related_cap cap'; cap_type cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> cdl.lift (K (\<not> ep_related_cap cap')) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap' \<and>* R) s; \<not> ep_related_cap cap'; cap_type cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> cdl.lift (get_irq_slot irq s \<mapsto>c cap' \<and>* (get_irq_slot irq s \<mapsto>c NullCap \<longrightarrow>* (get_irq_slot irq s) \<mapsto>c - \<and>* (get_irq_slot irq s \<mapsto>c cap \<longrightarrow>* irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R))) s
 2. \<And>s. \<lbrakk>cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap' \<and>* R) s; \<not> ep_related_cap cap'; cap_type cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> cdl.lift (K (\<not> ep_related_cap cap')) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift (irq \<mapsto>irq cdl_irq_node s irq \<and>* (cdl_irq_node s irq, 0) \<mapsto>c cap' \<and>* R) s; \<not> ep_related_cap cap'; cap_type cap \<noteq> Some UntypedType; obj = cdl_irq_node s irq\<rbrakk> \<Longrightarrow> cdl.lift ((cdl_irq_node s irq, 0) \<mapsto>c cap' \<and>* ((cdl_irq_node s irq, 0) \<mapsto>c NullCap \<longrightarrow>* (cdl_irq_node s irq, 0) \<mapsto>c - \<and>* ((cdl_irq_node s irq, 0) \<mapsto>c cap \<longrightarrow>* irq \<mapsto>irq cdl_irq_node s irq \<and>* (cdl_irq_node s irq, 0) \<mapsto>c cap \<and>* R))) s
 2. \<And>s. \<lbrakk>cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap' \<and>* R) s; \<not> ep_related_cap cap'; cap_type cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> cdl.lift (K (\<not> ep_related_cap cap')) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap' \<and>* R) s; \<not> ep_related_cap cap'; cap_type cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> cdl.lift (K (\<not> ep_related_cap cap')) s proof (prove)
goal:
No subgoals!