theory Interrupt_DR

lemma dcorres_arch_invoke_irq_control:
  "dcorres dc \<top> (invs and arch_irq_control_inv_valid arch_irq_control_invocation and valid_etcbs)
    (Interrupt_D.invoke_irq_control (
       translate_irq_control_invocation (
          irq_control_invocation.ArchIRQControl arch_irq_control_invocation)))
    (arch_invoke_irq_control arch_irq_control_invocation)" apply (case_tac arch_irq_control_invocation) apply (simp add:Interrupt_D.invoke_irq_control_def arch_irq_control_inv_valid_def) apply (rename_tac word p1 p2 t) apply (subst liftE_distrib) apply (simp add: liftE_bindE) apply (rule corres_dummy_return_pl) apply (rule corres_guard_imp) apply (rule corres_split[OF dmo_setIRQTrigger_dcorres]) apply clarsimp apply (rule dcorres_invoke_irq_control_body) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and arch_irq_control_inv_valid arch_irq_control_invocation and valid_etcbs) (Interrupt_D.invoke_irq_control (translate_irq_control_invocation (ArchIRQControl arch_irq_control_invocation))) (local.arch_invoke_irq_control arch_irq_control_invocation) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. arch_irq_control_invocation = ArchIRQControlIssue x1 x2 x3 x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and arch_irq_control_inv_valid arch_irq_control_invocation and valid_etcbs) (Interrupt_D.invoke_irq_control (translate_irq_control_invocation (ArchIRQControl arch_irq_control_invocation))) (local.arch_invoke_irq_control arch_irq_control_invocation) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. arch_irq_control_invocation = ArchIRQControlIssue x1 x2 x3 x4 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and (cte_wp_at ((=) cap.NullCap) x2 and cte_wp_at ((=) IRQControlCap) x3 and ex_cte_cap_wp_to Structures_A.is_cnode_cap x2 and real_cte_at x2 and (\<lambda>y. x1 \<le> maxIRQ)) and valid_etcbs) (insert_cap_child (IrqHandlerCap x1) (transform_cslot_ptr x3) (transform_cslot_ptr x2)) (liftE (do y <- do_machine_op (setIRQTrigger x1 x4);
y <- set_irq_state IRQSignal x1;
cap_insert (IRQHandlerCap x1) x3 x2
od)) proof (prove)
goal (1 subgoal):
 1. \<And>word p1 p2 t. arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t \<Longrightarrow> 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 <- do_machine_op (setIRQTrigger word t);
y <- set_irq_state IRQSignal word;
cap_insert (IRQHandlerCap word) p2 p1
od)) proof (prove)
goal (1 subgoal):
 1. \<And>word p1 p2 t. arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t \<Longrightarrow> 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)) (doE x <- liftE (do_machine_op (setIRQTrigger word t));
liftE (do y <- set_irq_state IRQSignal word;
cap_insert (IRQHandlerCap word) p2 p1
od)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>word p1 p2 t. arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t \<Longrightarrow> 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)) (do x <- do_machine_op (setIRQTrigger word t);
liftE (do y <- set_irq_state IRQSignal word;
cap_insert (IRQHandlerCap word) p2 p1
od)
od) proof (prove)
goal (1 subgoal):
 1. \<And>word p1 p2 t. arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t \<Longrightarrow> 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) (do return (?b2 word p1 p2 t);
insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr p2) (transform_cslot_ptr p1)
od) (do x <- do_machine_op (setIRQTrigger word t);
liftE (do y <- set_irq_state IRQSignal word;
cap_insert (IRQHandlerCap word) p2 p1
od)
od) proof (prove)
goal (3 subgoals):
 1. \<And>word p1 p2 t. arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t \<Longrightarrow> dcorres dc (?Q4 word p1 p2 t) (?Q'4 word p1 p2 t) (do return (?b2 word p1 p2 t);
insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr p2) (transform_cslot_ptr p1)
od) (do x <- do_machine_op (setIRQTrigger word t);
liftE (do y <- set_irq_state IRQSignal word;
cap_insert (IRQHandlerCap word) p2 p1
od)
od)
 2. \<And>word p1 p2 t s. \<lbrakk>arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t; True\<rbrakk> \<Longrightarrow> ?Q4 word p1 p2 t s
 3. \<And>word p1 p2 t s. \<lbrakk>arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t; (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) s\<rbrakk> \<Longrightarrow> ?Q'4 word p1 p2 t s proof (prove)
goal (5 subgoals):
 1. \<And>word p1 p2 t rv x. \<lbrakk>arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t; dc rv x\<rbrakk> \<Longrightarrow> dcorres dc (?R8 word p1 p2 t rv) (?R'8 word p1 p2 t x) (K_bind (insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr p2) (transform_cslot_ptr p1)) rv) (liftE (do y <- set_irq_state IRQSignal word;
cap_insert (IRQHandlerCap word) p2 p1
od))
 2. \<And>word p1 p2 t. arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t \<Longrightarrow> \<lbrace>?Q8 word p1 p2 t\<rbrace> return () \<lbrace>?R8 word p1 p2 t\<rbrace>
 3. \<And>word p1 p2 t. arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t \<Longrightarrow> \<lbrace>?Q'8 word p1 p2 t\<rbrace> do_machine_op (setIRQTrigger word t) \<lbrace>?R'8 word p1 p2 t\<rbrace>
 4. \<And>word p1 p2 t s. \<lbrakk>arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 word p1 p2 t) s
 5. \<And>word p1 p2 t s. \<lbrakk>arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t; (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) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8 word p1 p2 t) s proof (prove)
goal (5 subgoals):
 1. \<And>word a b aa ba t. arch_irq_control_invocation = ArchIRQControlIssue word (a, b) (aa, ba) t \<Longrightarrow> dcorres dc (?R8 word (a, b) (aa, ba) t ()) (?R'8 word (a, b) (aa, ba) t ()) (insert_cap_child (IrqHandlerCap word) (transform_cslot_ptr (aa, ba)) (transform_cslot_ptr (a, b))) (liftE (do y <- set_irq_state IRQSignal word;
cap_insert (IRQHandlerCap word) (aa, ba) (a, b)
od))
 2. \<And>word p1 p2 t. arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t \<Longrightarrow> \<lbrace>?Q8 word p1 p2 t\<rbrace> return () \<lbrace>?R8 word p1 p2 t\<rbrace>
 3. \<And>word p1 p2 t. arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t \<Longrightarrow> \<lbrace>?Q'8 word p1 p2 t\<rbrace> do_machine_op (setIRQTrigger word t) \<lbrace>?R'8 word p1 p2 t\<rbrace>
 4. \<And>word p1 p2 t s. \<lbrakk>arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 word p1 p2 t) s
 5. \<And>word p1 p2 t s. \<lbrakk>arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t; (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) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8 word p1 p2 t) s proof (prove)
goal (4 subgoals):
 1. \<And>word p1 p2 t. arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t \<Longrightarrow> \<lbrace>?Q8 word p1 p2 t\<rbrace> return () \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>word p1 p2 t. arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t \<Longrightarrow> \<lbrace>?Q'8 word p1 p2 t\<rbrace> do_machine_op (setIRQTrigger word t) \<lbrace>\<lambda>a. 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\<rbrace>
 3. \<And>word p1 p2 t s. \<lbrakk>arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 word p1 p2 t) s
 4. \<And>word p1 p2 t s. \<lbrakk>arch_irq_control_invocation = ArchIRQControlIssue word p1 p2 t; (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) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'8 word p1 p2 t) s proof (prove)
goal:
No subgoals!