theory Syscall_DR

lemma decode_invocation_domaincap_corres:
  "\<lbrakk> Some intent = transform_intent (invocation_type label) args;
     invoked_cap_ref = transform_cslot_ptr slot;
     invoked_cap = transform_cap cap;
      excaps = transform_cap_list excaps';
     cap = cap.DomainCap\<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 slot cap excaps')" apply (case_tac "\<exists>ti. intent = (DomainIntent ti)") apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def) apply (clarsimp simp: throw_opt_def get_domain_intent_def split: cdl_intent.split) apply (rule corres_rel_imp[OF decode_domain_corres],simp+) apply (clarsimp simp:Decode_D.decode_invocation_def throw_opt_def get_domain_intent_def Decode_A.decode_invocation_def
                  split:cdl_intent.splits) apply (rule absorb_imp,clarsimp)+ apply (rule dcorres_free_throw) apply (rule decode_domain_cap_label_not_match) apply (drule sym,clarsimp) 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 slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap\<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 slot cap excaps') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap; \<exists>ti. intent = DomainIntent ti\<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 slot cap excaps')
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap; \<nexists>ti. intent = DomainIntent ti\<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 slot cap excaps') proof (prove)
goal (2 subgoals):
 1. \<And>ti. \<lbrakk>Some (DomainIntent ti) = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = cdl_cap.DomainCap; excaps = transform_cap_list excaps'; cap = cap.DomainCap; intent = DomainIntent ti\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) (doE domain_intent <- throw_opt undefined (get_domain_intent (DomainIntent ti));
liftME cdl_invocation.InvokeDomain (Tcb_D.decode_domain_invocation (transform_cap_list excaps') domain_intent)
odE) (Decode_A.decode_domain_invocation label args excaps')
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap; \<nexists>ti. intent = DomainIntent ti\<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 slot cap excaps') proof (prove)
goal (2 subgoals):
 1. \<And>ti. \<lbrakk>Some (DomainIntent ti) = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = cdl_cap.DomainCap; excaps = transform_cap_list excaps'; cap = cap.DomainCap; intent = DomainIntent ti\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ((\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y)) \<circ> cdl_invocation.InvokeDomain)) (\<lambda>_. True) (\<lambda>_. True) (Tcb_D.decode_domain_invocation (transform_cap_list excaps') ti) (Decode_A.decode_domain_invocation label args excaps')
 2. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = transform_cap cap; excaps = transform_cap_list excaps'; cap = cap.DomainCap; \<nexists>ti. intent = DomainIntent ti\<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 slot cap excaps') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = cdl_cap.DomainCap; excaps = transform_cap_list excaps'; cap = cap.DomainCap; \<forall>ti. intent \<noteq> DomainIntent ti\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation cdl_cap.DomainCap (transform_cslot_ptr slot) (transform_cap_list excaps') intent) (Decode_A.decode_invocation label args cap_index slot cap.DomainCap excaps') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = cdl_cap.DomainCap; excaps = transform_cap_list excaps'; cap = cap.DomainCap; \<forall>ti. intent \<noteq> DomainIntent ti\<rbrakk> \<Longrightarrow> ((\<exists>x1. intent = CNodeIntent x1) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps')) \<and> ((\<exists>x2. intent = TcbIntent x2) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps')) \<and> ((\<exists>x3. intent = UntypedIntent x3) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps')) \<and> ((\<exists>x4. intent = IrqHandlerIntent x4) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps')) \<and> ((\<exists>x5. intent = IrqControlIntent x5) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps')) \<and> ((\<exists>x6. intent = PageTableIntent x6) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps')) \<and> ((\<exists>x7. intent = PageIntent x7) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps')) \<and> ((\<exists>x8. intent = PageDirectoryIntent x8) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps')) \<and> ((\<exists>x9. intent = AsidControlIntent x9) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps')) \<and> ((\<exists>x10. intent = AsidPoolIntent x10) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps')) \<and> ((\<exists>x11. intent = NotificationIntent x11) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps')) \<and> ((\<exists>x12. intent = EndpointIntent x12) \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = cdl_cap.DomainCap; excaps = transform_cap_list excaps'; cap = cap.DomainCap; \<forall>ti. intent \<noteq> DomainIntent ti\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>x. cdl_invocation_relation x \<circ> (\<lambda>(x, y). invocation.InvokeDomain x y))) (\<lambda>_. True) (\<lambda>_. True) throw (Decode_A.decode_domain_invocation label args excaps') proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = cdl_cap.DomainCap; excaps = transform_cap_list excaps'; cap = cap.DomainCap; \<forall>ti. intent \<noteq> DomainIntent ti\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label args excaps' \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Some intent = transform_intent (invocation_type label) args; invoked_cap_ref = transform_cslot_ptr slot; invoked_cap = cdl_cap.DomainCap; excaps = transform_cap_list excaps'; cap = cap.DomainCap; \<forall>ti. intent \<noteq> DomainIntent ti\<rbrakk> \<Longrightarrow> \<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label) args proof (prove)
goal:
No subgoals!