theory Syscall_DR

lemma decode_invocation_untypedcap_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.UntypedCap dev a b idx \<rbrakk> \<Longrightarrow>
    dcorres (dc \<oplus> cdl_invocation_relation) \<top>
        (invs and cte_wp_at ((=) invoked_cap') invoked_cap_ref'
                 and (\<lambda>s. \<forall>x \<in> set (map fst excaps'). s \<turnstile> x)
                 and (\<lambda>s. \<forall>x \<in> set excaps'. cte_wp_at ((=) (fst x)) (snd x) s)
                 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> ui. intent = UntypedIntent ui") apply (clarsimp simp: throw_opt_def get_untyped_intent_def split: cdl_intent.splits option.splits) apply (rule dcorres_liftME_liftME) apply (rule corres_guard_imp, rule decode_untyped_corres, auto simp: transform_cap_def)[1] apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def) apply (clarsimp simp: throw_opt_def get_untyped_intent_def split: cdl_intent.split) apply (rule absorb_imp,clarsimp)+ apply (rule dcorres_free_throw) apply (subst decode_untyped_label_not_match) apply simp+ 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' = cap.UntypedCap dev a b idx\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (invs and cte_wp_at ((=) invoked_cap') invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set (map fst excaps'). s \<turnstile> x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) 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 = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (doE untyped_intent <- throw_opt undefined (get_untyped_intent intent);
liftME cdl_invocation.InvokeUntyped (Untyped_D.decode_untyped_invocation (cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a)) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') untyped_intent)
odE) (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (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 = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; \<exists>ui. intent = UntypedIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (doE untyped_intent <- throw_opt undefined (get_untyped_intent intent);
liftME cdl_invocation.InvokeUntyped (Untyped_D.decode_untyped_invocation (cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a)) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') untyped_intent)
odE) (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; \<nexists>ui. intent = UntypedIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (doE untyped_intent <- throw_opt undefined (get_untyped_intent intent);
liftME cdl_invocation.InvokeUntyped (Untyped_D.decode_untyped_invocation (cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a)) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') untyped_intent)
odE) (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps')) proof (prove)
goal (2 subgoals):
 1. \<And>ui. \<lbrakk>Some (UntypedIntent ui) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; intent = UntypedIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped) \<circ> cdl_invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Untyped_D.decode_untyped_invocation (cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a)) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') ui) (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; \<nexists>ui. intent = UntypedIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (doE untyped_intent <- throw_opt undefined (get_untyped_intent intent);
liftME cdl_invocation.InvokeUntyped (Untyped_D.decode_untyped_invocation (cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a)) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') untyped_intent)
odE) (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps')) proof (prove)
goal (3 subgoals):
 1. \<And>ui. \<lbrakk>Some (UntypedIntent ui) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; intent = UntypedIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?rvrel21 ui) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (Untyped_D.decode_untyped_invocation (cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a)) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') ui) (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))
 2. \<And>ui r r'. \<lbrakk>Some (UntypedIntent ui) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; intent = UntypedIntent ui; ?rvrel21 ui r r'\<rbrakk> \<Longrightarrow> cdl_invocation_relation (cdl_invocation.InvokeUntyped r) (invocation.InvokeUntyped r')
 3. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; \<nexists>ui. intent = UntypedIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (doE untyped_intent <- throw_opt undefined (get_untyped_intent intent);
liftME cdl_invocation.InvokeUntyped (Untyped_D.decode_untyped_invocation (cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a)) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') untyped_intent)
odE) (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps')) proof (prove)
goal (2 subgoals):
 1. \<And>ui r r'. \<lbrakk>Some (UntypedIntent ui) = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; intent = UntypedIntent ui; r = translate_untyped_invocation r'\<rbrakk> \<Longrightarrow> cdl_invocation_relation (cdl_invocation.InvokeUntyped r) (invocation.InvokeUntyped r')
 2. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; \<nexists>ui. intent = UntypedIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (doE untyped_intent <- throw_opt undefined (get_untyped_intent intent);
liftME cdl_invocation.InvokeUntyped (Untyped_D.decode_untyped_invocation (cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a)) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') untyped_intent)
odE) (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (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 = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; \<nexists>ui. intent = UntypedIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) (doE untyped_intent <- throw_opt undefined (get_untyped_intent intent);
liftME cdl_invocation.InvokeUntyped (Untyped_D.decode_untyped_invocation (cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a)) (transform_cslot_ptr invoked_cap_ref') (transform_cap_list excaps') untyped_intent)
odE) (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (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 = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; \<forall>ui. intent \<noteq> UntypedIntent ui\<rbrakk> \<Longrightarrow> ((\<exists>x1. intent = CNodeIntent x1) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))) \<and> ((\<exists>x2. intent = TcbIntent x2) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))) \<and> ((\<exists>x4. intent = IrqHandlerIntent x4) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))) \<and> ((\<exists>x5. intent = IrqControlIntent x5) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))) \<and> ((\<exists>x6. intent = PageTableIntent x6) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))) \<and> ((\<exists>x7. intent = PageIntent x7) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))) \<and> ((\<exists>x8. intent = PageDirectoryIntent x8) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))) \<and> ((\<exists>x9. intent = AsidControlIntent x9) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))) \<and> ((\<exists>x10. intent = AsidPoolIntent x10) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))) \<and> ((\<exists>x11. intent = NotificationIntent x11) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))) \<and> ((\<exists>x12. intent = EndpointIntent x12) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps'))) \<and> ((\<exists>x13. intent = DomainIntent x13) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (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 = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; \<forall>ui. intent \<noteq> UntypedIntent ui\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> invocation.InvokeUntyped)) (\<lambda>_. True) (invs and cte_wp_at ((=) (cap.UntypedCap dev a b idx)) invoked_cap_ref' and (\<lambda>s. \<forall>x\<in>set excaps'. s \<turnstile> fst x) and (\<lambda>s. \<forall>x\<in>set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) throw (Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps')) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; \<forall>ui. intent \<noteq> UntypedIntent ui\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label' args' invoked_cap_ref' (cap.UntypedCap dev a b idx) (map fst excaps') \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; \<forall>ui. intent \<noteq> UntypedIntent ui\<rbrakk> \<Longrightarrow> Some (?intent73 s) = transform_intent (invocation_type label') args'
 2. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; \<forall>ui. intent \<noteq> UntypedIntent ui\<rbrakk> \<Longrightarrow> \<forall>ui. ?intent73 s \<noteq> UntypedIntent ui
 3. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.UntypedCap dev {a..a + 2 ^ b - 1} (free_range_of_untyped idx b a); excaps = transform_cap_list excaps'; invoked_cap' = cap.UntypedCap dev a b idx; \<forall>ui. intent \<noteq> UntypedIntent ui\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!