theory Syscall_DR

lemma decode_invocation_irqhandlercap_corres:
  "\<lbrakk> Some intent = transform_intent (invocation_type label') args';
     invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
     invoked_cap = transform_cap invoked_cap';
     excaps = transform_cap_list excaps';
     invoked_cap' = cap.IRQHandlerCap x \<rbrakk> \<Longrightarrow>
    dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
        (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
        (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def) apply (clarsimp simp: throw_opt_def get_irq_handler_intent_def split: option.splits) apply (rule conjI) apply (auto simp: decode_irq_handler_invocation_def transform_intent_def
               simp flip: gen_invocation_type_eq
               split del: if_split
               split: invocation_label.splits gen_invocation_labels.splits cdl_intent.splits list.splits)[1] apply clarsimp apply (simp split: cdl_intent.splits) apply (rule corres_rel_imp) apply (erule decode_irq_handler_corres, simp+)[1] apply clarsimp apply (case_tac xa, simp) apply (simp add: cdl_invocation_relation_def
                   cdl_irq_handler_invocation_relation_def
                   translate_invocation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = transform_cap invoked_cap'; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqHandlerCap x; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQHandler)) (\<lambda>_. True) (\<lambda>_. True) (doE irq_handler_intent <- throw_opt undefined (get_irq_handler_intent intent);
liftME InvokeIrqHandler (Interrupt_D.decode_irq_handler_invocation (IrqHandlerCap x) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') irq_handler_intent)
odE) (Decode_A.decode_irq_handler_invocation label' x excaps') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqHandlerCap x; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x\<rbrakk> \<Longrightarrow> ((case intent of IrqHandlerIntent x \<Rightarrow> Some x | _ \<Rightarrow> None) = None \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQHandler)) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_irq_handler_invocation label' x excaps')) \<and> (\<forall>x2. (case intent of IrqHandlerIntent x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some x2 \<longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQHandler) \<circ> InvokeIrqHandler)) (\<lambda>_. True) (\<lambda>_. True) (Interrupt_D.decode_irq_handler_invocation (IrqHandlerCap x) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') x2) (Decode_A.decode_irq_handler_invocation label' x excaps')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqHandlerCap x; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x\<rbrakk> \<Longrightarrow> (case intent of IrqHandlerIntent x \<Rightarrow> Some x | _ \<Rightarrow> None) = None \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQHandler)) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_irq_handler_invocation label' x excaps')
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqHandlerCap x; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x\<rbrakk> \<Longrightarrow> \<forall>x2. (case intent of IrqHandlerIntent x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some x2 \<longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQHandler) \<circ> InvokeIrqHandler)) (\<lambda>_. True) (\<lambda>_. True) (Interrupt_D.decode_irq_handler_invocation (IrqHandlerCap x) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') x2) (Decode_A.decode_irq_handler_invocation label' x excaps') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqHandlerCap x; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x\<rbrakk> \<Longrightarrow> \<forall>x2. (case intent of IrqHandlerIntent x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some x2 \<longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQHandler) \<circ> InvokeIrqHandler)) (\<lambda>_. True) (\<lambda>_. True) (Interrupt_D.decode_irq_handler_invocation (IrqHandlerCap x) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') x2) (Decode_A.decode_irq_handler_invocation label' x excaps') proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqHandlerCap x; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x; (case intent of IrqHandlerIntent x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQHandler) \<circ> InvokeIrqHandler)) (\<lambda>_. True) (\<lambda>_. True) (Interrupt_D.decode_irq_handler_invocation (IrqHandlerCap x) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') x2) (Decode_A.decode_irq_handler_invocation label' x excaps') proof (prove)
goal (1 subgoal):
 1. \<And>x2 x4. \<lbrakk>Some (IrqHandlerIntent x2) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqHandlerCap x; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x; intent = IrqHandlerIntent x2; x4 = x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQHandler) \<circ> InvokeIrqHandler)) (\<lambda>_. True) (\<lambda>_. True) (Interrupt_D.decode_irq_handler_invocation (IrqHandlerCap x) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') x2) (Decode_A.decode_irq_handler_invocation label' x excaps') proof (prove)
goal (2 subgoals):
 1. \<And>x2 x4. \<lbrakk>Some (IrqHandlerIntent x2) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqHandlerCap x; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x; intent = IrqHandlerIntent x2; x4 = x2\<rbrakk> \<Longrightarrow> dcorres (?r'177 x2 x4) (\<lambda>_. True) (\<lambda>_. True) (Interrupt_D.decode_irq_handler_invocation (IrqHandlerCap x) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') x2) (Decode_A.decode_irq_handler_invocation label' x excaps')
 2. \<And>x2 x4 xa y. \<lbrakk>Some (IrqHandlerIntent x2) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqHandlerCap x; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x; intent = IrqHandlerIntent x2; x4 = x2; ?r'177 x2 x4 xa y\<rbrakk> \<Longrightarrow> (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQHandler) \<circ> InvokeIrqHandler)) xa y proof (prove)
goal (1 subgoal):
 1. \<And>x2 x4 xa y. \<lbrakk>Some (IrqHandlerIntent x2) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqHandlerCap x; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x; intent = IrqHandlerIntent x2; x4 = x2; (dc \<oplus> cdl_irq_handler_invocation_relation) xa y\<rbrakk> \<Longrightarrow> (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQHandler) \<circ> InvokeIrqHandler)) xa y proof (prove)
goal (1 subgoal):
 1. \<And>x2 xa y. \<lbrakk>Some (IrqHandlerIntent x2) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqHandlerCap x; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x; intent = IrqHandlerIntent x2; (dc \<oplus> cdl_irq_handler_invocation_relation) xa y\<rbrakk> \<Longrightarrow> (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQHandler) \<circ> InvokeIrqHandler)) xa y proof (prove)
goal (1 subgoal):
 1. \<And>x2 xa y b. \<lbrakk>Some (IrqHandlerIntent x2) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqHandlerCap x; excaps = transform_cap_list excaps'; invoked_cap' = IRQHandlerCap x; intent = IrqHandlerIntent x2; (dc \<oplus> cdl_irq_handler_invocation_relation) xa y; xa = Inr b\<rbrakk> \<Longrightarrow> (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQHandler) \<circ> InvokeIrqHandler)) xa y proof (prove)
goal:
No subgoals!