theory Interrupt_DR

lemma dcorres_invoke_irq_control_body:
"\<And>word p1 p2.
       dcorres dc (\<lambda>_. True)
        (invs and (cte_wp_at ((=) cap.NullCap) p1
              and cte_wp_at ((=) cap.IRQControlCap) p2
              and ex_cte_cap_wp_to Structures_A.is_cnode_cap p1
              and real_cte_at p1 and (\<lambda>y. word \<le> maxIRQ))
              and valid_etcbs)
        (insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr p2) (transform_cslot_ptr p1))
        (liftE (do y <- set_irq_state irq_state.IRQSignal word;
                   cap_insert (cap.IRQHandlerCap word) p2 p1
                od))" apply (clarsimp simp:liftE_def bind_assoc) apply (rule dcorres_symb_exec_r_strong) apply (rule corres_dummy_return_l) apply (rule corres_guard_imp) apply (rule corres_split) apply (subgoal_tac "IrqHandlerCap word = transform_cap (cap.IRQHandlerCap word)") apply (simp only:) apply (rule insert_cap_child_corres) apply (simp add:transform_cap_def) apply (rule corres_trivial) apply (rule corres_free_return) apply (wp|clarsimp)+ apply simp apply (simp add:valid_cap_def cap_aligned_def word_bits_def) apply (rule hoare_pre) apply (rule hoare_vcg_conj_lift) apply (rule_tac Q = "\<lambda>r s. cte_wp_at ((=) cap.IRQControlCap) (aa,ba) s
                                \<and> is_original_cap s (aa, ba)" in hoare_strengthen_post) apply (wp set_irq_state_cte_wp_at set_irq_state_original) apply (simp add:cte_wp_at_def should_be_parent_of_def) apply (simp add: not_idle_thread_def) apply wp apply (strengthen invs_valid_idle invs_mdb) apply (wp set_irq_state_invs) apply (clarsimp simp:invs_def valid_state_def valid_pspace_def) apply (rule conjI) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (erule irq_revocableD) apply (simp add:caps_of_state_cteD invs_def valid_state_def valid_pspace_def valid_mdb_def) apply (rule conjI) apply (drule ex_cte_cap_wp_to_not_idle, auto simp: not_idle_thread_def)[1] apply (drule_tac p = "(aa,ba)" in if_unsafe_then_capD) apply clarsimp apply simp apply (drule_tac r = "(aa,ba)" in ex_cte_cap_wp_to_not_idle) apply (clarsimp simp:not_idle_thread_def)+ apply (wp set_irq_state_dwp, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>word p1 p2. dcorres dc (\<lambda>_. True) (invs and (cte_wp_at ((=) cap.NullCap) p1 and cte_wp_at ((=) IRQControlCap) p2 and ex_cte_cap_wp_to Structures_A.is_cnode_cap p1 and real_cte_at p1 and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) (insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr p2) (transform_cslot_ptr p1)) (liftE (do y <- set_irq_state IRQSignal word;
cap_insert (IRQHandlerCap word) p2 p1
od)) proof (prove)
goal (1 subgoal):
 1. \<And>word a b aa ba. dcorres dc (\<lambda>_. True) (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) (insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b))) (do x <- set_irq_state IRQSignal word;
r <- cap_insert (IRQHandlerCap word) (aa, ba) (a, b);
return (Inr ())
od) proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba rv. dcorres dc (\<lambda>_. True) (?Q' word a b aa ba rv) (insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b))) (do r <- cap_insert (IRQHandlerCap word) (aa, ba) (a, b);
return (Inr ())
od)
 2. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>?Q' word a b aa ba\<rbrace>
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba rv. dcorres dc (\<lambda>_. True) (?Q' word a b aa ba rv) (insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b)) >>= return) (do r <- cap_insert (IRQHandlerCap word) (aa, ba) (a, b);
return (Inr ())
od)
 2. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>?Q' word a b aa ba\<rbrace>
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>word a b aa ba rv. dcorres dc (?Q6 word a b aa ba rv) (?Q'6 word a b aa ba rv) (insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b)) >>= return) (do r <- cap_insert (IRQHandlerCap word) (aa, ba) (a, b);
return (Inr ())
od)
 2. \<And>word a b aa ba rv s. True \<Longrightarrow> ?Q6 word a b aa ba rv s
 3. \<And>word a b aa ba rv s. ?Q' word a b aa ba rv s \<Longrightarrow> ?Q'6 word a b aa ba rv s
 4. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>?Q' word a b aa ba\<rbrace>
 5. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>word a b aa ba rv. dcorres (?r'10 word a b aa ba rv) (?P10 word a b aa ba rv) (?P'10 word a b aa ba rv) (insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b))) (cap_insert (IRQHandlerCap word) (aa, ba) (a, b))
 2. \<And>word a b aa ba rv x r. ?r'10 word a b aa ba rv x r \<Longrightarrow> dcorres dc (?R10 word a b aa ba rv x) (?R'10 word a b aa ba rv r) (return x) (return (Inr ()))
 3. \<And>word a b aa ba rv. \<lbrace>?Q10 word a b aa ba rv\<rbrace> insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b)) \<lbrace>?R10 word a b aa ba rv\<rbrace>
 4. \<And>word a b aa ba rv. \<lbrace>?Q'10 word a b aa ba rv\<rbrace> cap_insert (IRQHandlerCap word) (aa, ba) (a, b) \<lbrace>?R'10 word a b aa ba rv\<rbrace>
 5. \<And>word a b aa ba rv s. True \<Longrightarrow> (?P10 word a b aa ba rv and ?Q10 word a b aa ba rv) s
 6. \<And>word a b aa ba rv s. ?Q' word a b aa ba rv s \<Longrightarrow> (?P'10 word a b aa ba rv and ?Q'10 word a b aa ba rv) s
 7. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>?Q' word a b aa ba\<rbrace>
 8. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>word a b aa ba rv. IrqHandlerCap word = transform_cap (IRQHandlerCap word) \<Longrightarrow> dcorres (?r'10 word a b aa ba rv) (?P10 word a b aa ba rv) (?P'10 word a b aa ba rv) (insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b))) (cap_insert (IRQHandlerCap word) (aa, ba) (a, b))
 2. \<And>word a b aa ba rv. IrqHandlerCap word = transform_cap (IRQHandlerCap word)
 3. \<And>word a b aa ba rv x r. ?r'10 word a b aa ba rv x r \<Longrightarrow> dcorres dc (?R10 word a b aa ba rv x) (?R'10 word a b aa ba rv r) (return x) (return (Inr ()))
 4. \<And>word a b aa ba rv. \<lbrace>?Q10 word a b aa ba rv\<rbrace> insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b)) \<lbrace>?R10 word a b aa ba rv\<rbrace>
 5. \<And>word a b aa ba rv. \<lbrace>?Q'10 word a b aa ba rv\<rbrace> cap_insert (IRQHandlerCap word) (aa, ba) (a, b) \<lbrace>?R'10 word a b aa ba rv\<rbrace>
 6. \<And>word a b aa ba rv s. True \<Longrightarrow> (?P10 word a b aa ba rv and ?Q10 word a b aa ba rv) s
 7. \<And>word a b aa ba rv s. ?Q' word a b aa ba rv s \<Longrightarrow> (?P'10 word a b aa ba rv and ?Q'10 word a b aa ba rv) s
 8. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>?Q' word a b aa ba\<rbrace>
 9. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>word a b aa ba rv. IrqHandlerCap word = transform_cap (IRQHandlerCap word) \<Longrightarrow> dcorres (?r'10 word a b aa ba rv) (?P10 word a b aa ba rv) (?P'10 word a b aa ba rv) (insert_cap_child (transform_cap (IRQHandlerCap word)) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b))) (cap_insert (IRQHandlerCap word) (aa, ba) (a, b))
 2. \<And>word a b aa ba rv. IrqHandlerCap word = transform_cap (IRQHandlerCap word)
 3. \<And>word a b aa ba rv x r. ?r'10 word a b aa ba rv x r \<Longrightarrow> dcorres dc (?R10 word a b aa ba rv x) (?R'10 word a b aa ba rv r) (return x) (return (Inr ()))
 4. \<And>word a b aa ba rv. \<lbrace>?Q10 word a b aa ba rv\<rbrace> insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b)) \<lbrace>?R10 word a b aa ba rv\<rbrace>
 5. \<And>word a b aa ba rv. \<lbrace>?Q'10 word a b aa ba rv\<rbrace> cap_insert (IRQHandlerCap word) (aa, ba) (a, b) \<lbrace>?R'10 word a b aa ba rv\<rbrace>
 6. \<And>word a b aa ba rv s. True \<Longrightarrow> (?P10 word a b aa ba rv and ?Q10 word a b aa ba rv) s
 7. \<And>word a b aa ba rv s. ?Q' word a b aa ba rv s \<Longrightarrow> (?P'10 word a b aa ba rv and ?Q'10 word a b aa ba rv) s
 8. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>?Q' word a b aa ba\<rbrace>
 9. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>word a b aa ba rv. IrqHandlerCap word = transform_cap (IRQHandlerCap word)
 2. \<And>word a b aa ba rv x r. dc x r \<Longrightarrow> dcorres dc (?R10 word a b aa ba rv x) (?R'10 word a b aa ba rv r) (return x) (return (Inr ()))
 3. \<And>word a b aa ba rv. \<lbrace>?Q10 word a b aa ba rv\<rbrace> insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b)) \<lbrace>?R10 word a b aa ba rv\<rbrace>
 4. \<And>word a b aa ba rv. \<lbrace>?Q'10 word a b aa ba rv\<rbrace> cap_insert (IRQHandlerCap word) (aa, ba) (a, b) \<lbrace>?R'10 word a b aa ba rv\<rbrace>
 5. \<And>word a b aa ba rv s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q10 word a b aa ba rv) s
 6. \<And>word a b aa ba rv s. ?Q' word a b aa ba rv s \<Longrightarrow> ((\<lambda>s. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (aa, ba)) (IRQHandlerCap word) (cap_insert_dest_original (IRQHandlerCap word) cap')) (aa, ba) s \<and> not_idle_thread (fst (a, b)) s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread (fst (aa, ba)) s \<and> valid_objs s \<and> cap_aligned (IRQHandlerCap word)) and ?Q'10 word a b aa ba rv) s
 7. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>?Q' word a b aa ba\<rbrace>
 8. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>word a b aa ba rv x r. dc x r \<Longrightarrow> dcorres dc (?R10 word a b aa ba rv x) (?R'10 word a b aa ba rv r) (return x) (return (Inr ()))
 2. \<And>word a b aa ba rv. \<lbrace>?Q10 word a b aa ba rv\<rbrace> insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b)) \<lbrace>?R10 word a b aa ba rv\<rbrace>
 3. \<And>word a b aa ba rv. \<lbrace>?Q'10 word a b aa ba rv\<rbrace> cap_insert (IRQHandlerCap word) (aa, ba) (a, b) \<lbrace>?R'10 word a b aa ba rv\<rbrace>
 4. \<And>word a b aa ba rv s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q10 word a b aa ba rv) s
 5. \<And>word a b aa ba rv s. ?Q' word a b aa ba rv s \<Longrightarrow> ((\<lambda>s. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (aa, ba)) (IRQHandlerCap word) (cap_insert_dest_original (IRQHandlerCap word) cap')) (aa, ba) s \<and> not_idle_thread (fst (a, b)) s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread (fst (aa, ba)) s \<and> valid_objs s \<and> cap_aligned (IRQHandlerCap word)) and ?Q'10 word a b aa ba rv) s
 6. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>?Q' word a b aa ba\<rbrace>
 7. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>word a b aa ba rv x r. dc x r \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (return (Inr ()))
 2. \<And>word a b aa ba rv. \<lbrace>?Q10 word a b aa ba rv\<rbrace> insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b)) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>word a b aa ba rv. \<lbrace>?Q'10 word a b aa ba rv\<rbrace> cap_insert (IRQHandlerCap word) (aa, ba) (a, b) \<lbrace>\<lambda>r _. True\<rbrace>
 4. \<And>word a b aa ba rv s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q10 word a b aa ba rv) s
 5. \<And>word a b aa ba rv s. ?Q' word a b aa ba rv s \<Longrightarrow> ((\<lambda>s. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (aa, ba)) (IRQHandlerCap word) (cap_insert_dest_original (IRQHandlerCap word) cap')) (aa, ba) s \<and> not_idle_thread (fst (a, b)) s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread (fst (aa, ba)) s \<and> valid_objs s \<and> cap_aligned (IRQHandlerCap word)) and ?Q'10 word a b aa ba rv) s
 6. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>?Q' word a b aa ba\<rbrace>
 7. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>word a b aa ba rv. \<lbrace>?Q10 word a b aa ba rv\<rbrace> insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b)) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>word a b aa ba rv. \<lbrace>?Q'10 word a b aa ba rv\<rbrace> cap_insert (IRQHandlerCap word) (aa, ba) (a, b) \<lbrace>\<lambda>r _. True\<rbrace>
 3. \<And>word a b aa ba rv s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q10 word a b aa ba rv) s
 4. \<And>word a b aa ba rv s. ?Q' word a b aa ba rv s \<Longrightarrow> ((\<lambda>s. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (aa, ba)) (IRQHandlerCap word) (cap_insert_dest_original (IRQHandlerCap word) cap')) (aa, ba) s \<and> not_idle_thread (fst (a, b)) s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread (fst (aa, ba)) s \<and> valid_objs s \<and> cap_aligned (IRQHandlerCap word)) and ?Q'10 word a b aa ba rv) s
 5. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>?Q' word a b aa ba\<rbrace>
 6. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba s. ?Q' word a b aa ba () s \<Longrightarrow> cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (aa, ba)) (IRQHandlerCap word) (cap_insert_dest_original (IRQHandlerCap word) cap')) (aa, ba) s \<and> not_idle_thread a s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread aa s \<and> valid_objs s \<and> cap_aligned (IRQHandlerCap word)
 2. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>?Q' word a b aa ba\<rbrace>
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r b. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap b (aa, ba)) (IRQHandlerCap word) (cap_insert_dest_original (IRQHandlerCap word) cap')) (aa, ba) b \<and> not_idle_thread a b \<and> valid_idle b \<and> valid_etcbs b \<and> valid_mdb b \<and> not_idle_thread aa b \<and> valid_objs b \<and> cap_aligned (IRQHandlerCap word)\<rbrace>
 2. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>word a b aa ba. \<lbrace>invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r b. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap b (aa, ba)) (IRQHandlerCap word) (cap_insert_dest_original (IRQHandlerCap word) cap')) (aa, ba) b \<and> not_idle_thread a b \<and> valid_idle b \<and> valid_etcbs b \<and> valid_mdb b \<and> not_idle_thread aa b \<and> valid_objs b\<rbrace>
 2. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba. \<lbrace>?Q28 word a b aa ba\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r b. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap b (aa, ba)) (IRQHandlerCap word) (cap_insert_dest_original (IRQHandlerCap word) cap')) (aa, ba) b \<and> not_idle_thread a b \<and> valid_idle b \<and> valid_etcbs b \<and> valid_mdb b \<and> not_idle_thread aa b \<and> valid_objs b\<rbrace>
 2. \<And>word a b aa ba s. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) s \<Longrightarrow> ?Q28 word a b aa ba s
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>word a b aa ba. \<lbrace>?P31 word a b aa ba\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (aa, ba)) (IRQHandlerCap word) (cap_insert_dest_original (IRQHandlerCap word) cap')) (aa, ba) s\<rbrace>
 2. \<And>word a b aa ba. \<lbrace>?P'31 word a b aa ba\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>rv s. not_idle_thread a s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread aa s \<and> valid_objs s\<rbrace>
 3. \<And>word a b aa ba s. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) s \<Longrightarrow> ?P31 word a b aa ba s \<and> ?P'31 word a b aa ba s
 4. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>word a b aa ba. \<lbrace>?P31 word a b aa ba\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. cte_wp_at ((=) IRQControlCap) (aa, ba) s \<and> is_original_cap s (aa, ba)\<rbrace>
 2. \<And>word a b aa ba rv s. cte_wp_at ((=) IRQControlCap) (aa, ba) s \<and> is_original_cap s (aa, ba) \<Longrightarrow> cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (aa, ba)) (IRQHandlerCap word) (cap_insert_dest_original (IRQHandlerCap word) cap')) (aa, ba) s
 3. \<And>word a b aa ba. \<lbrace>?P'31 word a b aa ba\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>rv s. not_idle_thread a s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread aa s \<and> valid_objs s\<rbrace>
 4. \<And>word a b aa ba s. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) s \<Longrightarrow> ?P31 word a b aa ba s \<and> ?P'31 word a b aa ba s
 5. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>word a b aa ba rv s. cte_wp_at ((=) IRQControlCap) (aa, ba) s \<and> is_original_cap s (aa, ba) \<Longrightarrow> cte_wp_at (\<lambda>cap'. should_be_parent_of cap' (is_original_cap s (aa, ba)) (IRQHandlerCap word) (cap_insert_dest_original (IRQHandlerCap word) cap')) (aa, ba) s
 2. \<And>word a b aa ba. \<lbrace>?P'31 word a b aa ba\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>rv s. not_idle_thread a s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread aa s \<and> valid_objs s\<rbrace>
 3. \<And>word a b aa ba s. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) s \<Longrightarrow> (cte_wp_at ((=) IRQControlCap) (aa, ba) s \<and> is_original_cap s (aa, ba)) \<and> ?P'31 word a b aa ba s
 4. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba. \<lbrace>?P'31 word a b aa ba\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>rv s. not_idle_thread a s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> not_idle_thread aa s \<and> valid_objs s\<rbrace>
 2. \<And>word a b aa ba s. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) s \<Longrightarrow> (cte_wp_at ((=) IRQControlCap) (aa, ba) s \<and> is_original_cap s (aa, ba)) \<and> ?P'31 word a b aa ba s
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba. \<lbrace>?P'31 word a b aa ba\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>rv s. a \<noteq> idle_thread s \<and> valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> aa \<noteq> idle_thread s \<and> valid_objs s\<rbrace>
 2. \<And>word a b aa ba s. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) s \<Longrightarrow> (cte_wp_at ((=) IRQControlCap) (aa, ba) s \<and> is_original_cap s (aa, ba)) \<and> ?P'31 word a b aa ba s
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba. \<lbrace>?P'42 word a b aa ba\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>rv s. valid_idle s \<and> valid_etcbs s \<and> valid_mdb s \<and> aa \<noteq> idle_thread s \<and> valid_objs s\<rbrace>
 2. \<And>word a b aa ba s. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) s \<Longrightarrow> (cte_wp_at ((=) IRQControlCap) (aa, ba) s \<and> is_original_cap s (aa, ba)) \<and> a \<noteq> idle_thread s \<and> ?P'42 word a b aa ba s
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba. \<lbrace>?P'42 word a b aa ba\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. invs s \<and> valid_etcbs s \<and> invs s \<and> aa \<noteq> idle_thread s \<and> valid_objs s\<rbrace>
 2. \<And>word a b aa ba s. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) s \<Longrightarrow> (cte_wp_at ((=) IRQControlCap) (aa, ba) s \<and> is_original_cap s (aa, ba)) \<and> a \<noteq> idle_thread s \<and> ?P'42 word a b aa ba s
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>word a b aa ba s. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) s \<Longrightarrow> (cte_wp_at ((=) IRQControlCap) (aa, ba) s \<and> is_original_cap s (aa, ba)) \<and> a \<noteq> idle_thread s \<and> (invs s \<and> (IRQSignal \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap word \<notin> ran (caps_of_state s))) \<and> valid_etcbs s \<and> (invs s \<and> (IRQSignal \<noteq> IRQSignal \<longrightarrow> IRQHandlerCap word \<notin> ran (caps_of_state s))) \<and> aa \<noteq> idle_thread s \<and> valid_objs s
 2. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; cte_wp_at ((=) IRQControlCap) (aa, ba) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> is_original_cap s (aa, ba) \<and> a \<noteq> idle_thread s \<and> aa \<noteq> idle_thread s
 2. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; cte_wp_at ((=) IRQControlCap) (aa, ba) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> is_original_cap s (aa, ba)
 2. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; cte_wp_at ((=) IRQControlCap) (aa, ba) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s \<and> aa \<noteq> idle_thread s
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (a, b) = Some cap.NullCap; caps_of_state s (aa, ba) = Some IRQControlCap; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> is_original_cap s (aa, ba)
 2. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; cte_wp_at ((=) IRQControlCap) (aa, ba) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s \<and> aa \<noteq> idle_thread s
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (a, b) = Some cap.NullCap; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> irq_revocable (is_original_cap s) (caps_of_state s)
 2. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; cte_wp_at ((=) IRQControlCap) (aa, ba) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s \<and> aa \<noteq> idle_thread s
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; cte_wp_at ((=) IRQControlCap) (aa, ba) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s \<and> aa \<noteq> idle_thread s
 2. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; cte_wp_at ((=) IRQControlCap) (aa, ba) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s
 2. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; cte_wp_at ((=) IRQControlCap) (aa, ba) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> aa \<noteq> idle_thread s
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; cte_wp_at ((=) IRQControlCap) (aa, ba) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> aa \<noteq> idle_thread s
 2. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> if_unsafe_then_cap s
 2. \<And>word a b aa ba s cap. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s; IRQControlCap = cap\<rbrakk> \<Longrightarrow> cap \<noteq> cap.NullCap
 3. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. IRQControlCap = cap' \<and> appropriate_cte_cap cap' cap) (aa, ba) s\<rbrakk> \<Longrightarrow> aa \<noteq> idle_thread s
 4. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>word a b aa ba s cap. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s; IRQControlCap = cap\<rbrakk> \<Longrightarrow> cap \<noteq> cap.NullCap
 2. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. IRQControlCap = cap' \<and> appropriate_cte_cap cap' cap) (aa, ba) s\<rbrakk> \<Longrightarrow> aa \<noteq> idle_thread s
 3. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. IRQControlCap = cap' \<and> appropriate_cte_cap cap' cap) (aa, ba) s\<rbrakk> \<Longrightarrow> aa \<noteq> idle_thread s
 2. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> valid_global_refs s
 2. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> valid_idle s
 4. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s\<rbrakk> \<Longrightarrow> valid_irq_node s
 5. \<And>word a b aa ba s. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at ((=) cap.NullCap) (a, b) s; ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) s; cap_table_at (length b) a s; word \<le> maxIRQ; valid_etcbs s; not_idle_thread (fst (aa, ba)) s\<rbrakk> \<Longrightarrow> aa \<noteq> idle_thread s
 6. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. (invs and (cte_wp_at ((=) cap.NullCap) (a, b) and cte_wp_at ((=) IRQControlCap) (aa, ba) and ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) and cap_table_at (length b) a and (\<lambda>y. word \<le> maxIRQ)) and valid_etcbs) ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>word a b aa ba cs. \<lbrace>\<lambda>ps. invs ps \<and> cte_wp_at ((=) cap.NullCap) (a, b) ps \<and> cte_wp_at ((=) IRQControlCap) (aa, ba) ps \<and> ex_cte_cap_wp_to Structures_A.is_cnode_cap (a, b) ps \<and> cap_table_at (length b) a ps \<and> word \<le> maxIRQ \<and> valid_etcbs ps \<and> transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!