theory Syscall_DR

lemma decode_invocation_irqcontrolcap_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.IRQControlCap \<rbrakk> \<Longrightarrow>
    dcorres (dc \<oplus> cdl_invocation_relation)
        \<top>
        (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. valid_cap (fst e) s) and valid_global_refs and valid_idle and valid_etcbs)
        (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(case_tac "\<exists> ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'") apply(erule exE, rotate_tac -1, drule sym) apply(clarsimp simp: throw_opt_def get_irq_control_intent_def) apply (rule dcorres_liftME_liftME) apply (rule decode_irq_control_corres, auto simp: transform_cap_def)[1] apply (clarsimp simp: cdl_irq_control_invocation_relation_def) apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def) apply (rule corres_guard_imp) apply (clarsimp simp: throw_opt_def split: cdl_intent.split option.splits) apply (auto simp: get_irq_control_intent_def split: cdl_intent.split intro!: decode_irq_control_error_corres) 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' = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (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 = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl)) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (doE irq_control_intent <- throw_opt undefined (get_irq_control_intent intent);
liftME InvokeIrqControl (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') irq_control_intent)
odE) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst 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 = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<exists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl)) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (doE irq_control_intent <- throw_opt undefined (get_irq_control_intent intent);
liftME InvokeIrqControl (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') irq_control_intent)
odE) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps'))
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<nexists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl)) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (doE irq_control_intent <- throw_opt undefined (get_irq_control_intent intent);
liftME InvokeIrqControl (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') irq_control_intent)
odE) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps')) proof (prove)
goal (2 subgoals):
 1. \<And>ici. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; transform_intent (invocation_type label') args' = Some (IrqControlIntent ici)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl)) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (doE irq_control_intent <- throw_opt undefined (get_irq_control_intent intent);
liftME InvokeIrqControl (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') irq_control_intent)
odE) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps'))
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<nexists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl)) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (doE irq_control_intent <- throw_opt undefined (get_irq_control_intent intent);
liftME InvokeIrqControl (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') irq_control_intent)
odE) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps')) proof (prove)
goal (2 subgoals):
 1. \<And>ici. \<lbrakk>intent = IrqControlIntent ici; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; transform_intent (invocation_type label') args' = Some (IrqControlIntent ici)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl) \<circ> InvokeIrqControl)) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') ici) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps'))
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<nexists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl)) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (doE irq_control_intent <- throw_opt undefined (get_irq_control_intent intent);
liftME InvokeIrqControl (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') irq_control_intent)
odE) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps')) proof (prove)
goal (3 subgoals):
 1. \<And>ici. \<lbrakk>intent = IrqControlIntent ici; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; transform_intent (invocation_type label') args' = Some (IrqControlIntent ici)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?rvrel8 ici) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') ici) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps'))
 2. \<And>ici r r'. \<lbrakk>intent = IrqControlIntent ici; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; transform_intent (invocation_type label') args' = Some (IrqControlIntent ici); ?rvrel8 ici r r'\<rbrakk> \<Longrightarrow> cdl_invocation_relation (InvokeIrqControl r) (InvokeIRQControl r')
 3. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<nexists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl)) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (doE irq_control_intent <- throw_opt undefined (get_irq_control_intent intent);
liftME InvokeIrqControl (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') irq_control_intent)
odE) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps')) proof (prove)
goal (2 subgoals):
 1. \<And>ici r r'. \<lbrakk>intent = IrqControlIntent ici; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; transform_intent (invocation_type label') args' = Some (IrqControlIntent ici); cdl_irq_control_invocation_relation r r'\<rbrakk> \<Longrightarrow> cdl_invocation_relation (InvokeIrqControl r) (InvokeIRQControl r')
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<nexists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl)) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (doE irq_control_intent <- throw_opt undefined (get_irq_control_intent intent);
liftME InvokeIrqControl (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') irq_control_intent)
odE) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps')) proof (prove)
goal (2 subgoals):
 1. \<And>ici r'. \<lbrakk>intent = IrqControlIntent ici; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; transform_intent (invocation_type label') args' = Some (IrqControlIntent ici)\<rbrakk> \<Longrightarrow> cdl_invocation_relation (InvokeIrqControl (translate_irq_control_invocation r')) (InvokeIRQControl r')
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<nexists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl)) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (doE irq_control_intent <- throw_opt undefined (get_irq_control_intent intent);
liftME InvokeIrqControl (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') irq_control_intent)
odE) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst 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 = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<nexists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl)) (\<lambda>_. True) (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) (doE irq_control_intent <- throw_opt undefined (get_irq_control_intent intent);
liftME InvokeIrqControl (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') irq_control_intent)
odE) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps')) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<nexists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl)) ?Q23 ?Q'23 (doE irq_control_intent <- throw_opt undefined (get_irq_control_intent intent);
liftME InvokeIrqControl (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') irq_control_intent)
odE) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps'))
 2. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<nexists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'; True\<rbrakk> \<Longrightarrow> ?Q23 s
 3. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<nexists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'; (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'23 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<forall>ici. Some (IrqControlIntent ici) \<noteq> transform_intent (invocation_type label') args'\<rbrakk> \<Longrightarrow> (get_irq_control_intent intent = None \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl)) ?Q23 ?Q'23 throw (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps'))) \<and> (\<forall>x2. get_irq_control_intent intent = Some x2 \<longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> InvokeIRQControl) \<circ> InvokeIrqControl)) ?Q23 ?Q'23 (Interrupt_D.decode_irq_control_invocation IrqControlCap (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') x2) (Decode_A.decode_irq_control_invocation label' args' invoked_cap_ref' (map fst excaps')))
 2. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<nexists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'; True\<rbrakk> \<Longrightarrow> ?Q23 s
 3. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = IrqControlCap; excaps = transform_cap_list excaps'; invoked_cap' = IRQControlCap; \<nexists>ici. Some (IrqControlIntent ici) = transform_intent (invocation_type label') args'; (valid_objs and (\<lambda>s. \<forall>e\<in>set excaps'. s \<turnstile> fst e) and valid_global_refs and valid_idle and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'23 s proof (prove)
goal:
No subgoals!