theory Syscall_DR

lemma transform_intent_irq_control_None:
  "\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.IRQControlCap\<rbrakk>
      \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r. \<bottom>\<rbrace>,
          \<lbrace>\<lambda>x. (=) s\<rbrace>" including no_pre supply gen_invocation_type_eq[symmetric, simp] if_cong[cong] apply (clarsimp simp:Decode_A.decode_invocation_def) apply wp apply (clarsimp simp:decode_irq_control_invocation_def arch_decode_irq_control_invocation_def
                  split del:if_split) apply (case_labels "invocation_type label"; (clarsimp, wp)?) apply (clarsimp simp:transform_intent_issue_irq_handler_def transform_intent_def
                   split:list.split_asm split del:if_split,wp+) apply (clarsimp simp:arch_transform_intent_issue_irq_handler_def transform_intent_def
                  split:list.split_asm split del:if_split,wp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_invocation label args cap_i slot cap excaps \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftME InvokeIRQControl (Decode_A.decode_irq_control_invocation label args slot (map fst excaps)) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_irq_control_invocation label args slot (map fst excaps) \<lbrace>(\<lambda>r _. False) \<circ> InvokeIRQControl\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> if invocation_type label = GenInvocationLabel IRQIssueIRQHandler then if 3 \<le> length args \<and> Suc 0 \<le> length excaps then 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 else throwError TruncatedMessage else liftME ArchIRQControl (if invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler then if 4 \<le> length args \<and> Suc 0 \<le> length excaps then 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 else throwError TruncatedMessage else throwError IllegalOperation) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap; invocation_type label = GenInvocationLabel x1; x1 = IRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> if invocation_type label = GenInvocationLabel IRQIssueIRQHandler then if 3 \<le> length args \<and> Suc 0 \<le> length excaps then 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 else throwError TruncatedMessage else liftME ArchIRQControl (if invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler then if 4 \<le> length args \<and> Suc 0 \<le> length excaps then 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 else throwError TruncatedMessage else throwError IllegalOperation) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>x2. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap; invocation_type label = ArchInvocationLabel x2; x2 = ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> if invocation_type label = GenInvocationLabel IRQIssueIRQHandler then if 3 \<le> length args \<and> Suc 0 \<le> length excaps then 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 else throwError TruncatedMessage else liftME ArchIRQControl (if invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler then if 4 \<le> length args \<and> Suc 0 \<le> length excaps then 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 else throwError TruncatedMessage else throwError IllegalOperation) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>transform_intent (invocation_type label) args = None; cap = IRQControlCap; invocation_type label = ArchInvocationLabel x2; x2 = ARMIRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> if invocation_type label = GenInvocationLabel IRQIssueIRQHandler then if 3 \<le> length args \<and> Suc 0 \<le> length excaps then 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 else throwError TruncatedMessage else liftME ArchIRQControl (if invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler then if 4 \<le> length args \<and> Suc 0 \<le> length excaps then 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 else throwError TruncatedMessage else throwError IllegalOperation) \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>x. (=) s\<rbrace> proof (prove)
goal:
No subgoals!