theory Interrupt_DR

lemma decode_irq_control_error_corres:
  "\<not> (\<exists> ui. (Some (IrqControlIntent ui)) = (transform_intent (invocation_type label) args)) \<Longrightarrow>
     dcorres (dc \<oplus> anyrel) \<top> \<top>
      (throwError e)
      (Decode_A.decode_irq_control_invocation label args slot (map fst excaps))" unfolding decode_irq_control_invocation_def apply (cases "invocation_type label"; simp add: arch_decode_irq_control_invocation_def
                                                  arch_decode_irq_control_error_corres) apply (clarsimp simp: transform_intent_def transform_intent_issue_irq_handler_def
                         arch_transform_intent_issue_irq_handler_def
                   simp flip: gen_invocation_type_eq
                   split: list.splits arch_invocation_label.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<nexists>ui. Some (IrqControlIntent ui) = transform_intent (invocation_type label) args \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (Decode_A.decode_irq_control_invocation label args slot (map fst excaps)) proof (prove)
goal (1 subgoal):
 1. \<nexists>ui. Some (IrqControlIntent ui) = transform_intent (invocation_type label) args \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (if gen_invocation_type label = IRQIssueIRQHandler then if 3 \<le> length args \<and> 1 \<le> length (map fst excaps) then let irq_word = args ! 0; index = args ! 1; depth = args ! 2; cnode = map fst excaps ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE arch_check_irq irq_word;
irq_active <- liftE $ is_irq_active irq;
whenE irq_active $ throwError RevokeFirst;
dest_slot <- lookup_target_slot cnode (data_to_cptr index) (unat depth);
CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ IRQControl irq dest_slot slot
odE else throwError TruncatedMessage else liftME ArchIRQControl $ local.arch_decode_irq_control_invocation label args slot (map fst excaps)) proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>\<forall>ui. Some (IrqControlIntent ui) \<noteq> transform_intent (GenInvocationLabel x1) args; invocation_type label = GenInvocationLabel x1\<rbrakk> \<Longrightarrow> 3 \<le> length args \<and> Suc 0 \<le> length excaps \<longrightarrow> gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- arch_check_irq irq_word;
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError RevokeFirst);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (map fst excaps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- CSpaceAcc_A.ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE)
 2. \<And>x2. \<lbrakk>\<forall>ui. Some (IrqControlIntent ui) \<noteq> transform_intent (ArchInvocationLabel x2) args; invocation_type label = ArchInvocationLabel x2\<rbrakk> \<Longrightarrow> (4 \<le> length args \<longrightarrow> Suc 0 \<le> length excaps \<longrightarrow> (x2 = ARMIRQIssueIRQHandler \<longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- arch_check_irq irq_word;
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError RevokeFirst);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (map fst excaps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- CSpaceAcc_A.ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE)) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> dcorres (dc \<oplus> (\<lambda>x. anyrel x \<circ> ArchIRQControl)) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- arch_check_irq irq_word;
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError RevokeFirst);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (map fst excaps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
y <- CSpaceAcc_A.ensure_empty dest_slot;
returnOk (ArchIRQControlIssue irq dest_slot slot (args ! Suc 0 \<noteq> 0))
odE))) \<and> (x2 \<noteq> ARMIRQIssueIRQHandler \<longrightarrow> gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- arch_check_irq irq_word;
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError RevokeFirst);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (map fst excaps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- CSpaceAcc_A.ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE))) \<and> (\<not> 4 \<le> length args \<longrightarrow> 3 \<le> length args \<and> Suc 0 \<le> length excaps \<longrightarrow> gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- arch_check_irq irq_word;
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError RevokeFirst);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (map fst excaps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- CSpaceAcc_A.ensure_empty dest_slot;
returnOk (IRQControl irq dest_slot slot)
odE)) proof (prove)
goal:
No subgoals!