theory ArchInterrupt_AI

lemma (* decode_irq_control_invocation_inv *)[Interrupt_AI_asms]:
  "\<lbrace>P\<rbrace> decode_irq_control_invocation label args slot caps \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: decode_irq_control_invocation_def Let_def arch_check_irq_def
                   arch_decode_irq_control_invocation_def whenE_def, safe) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_irq_control_invocation label args slot caps \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (36 subgoals):
 1. \<lbrakk>4 \<le> length args; Suc 0 \<le> length caps; UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; gen_invocation_type label = IRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> throwError (RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)) \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<lbrakk>4 \<le> length args; Suc 0 \<le> length caps; UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; gen_invocation_type label \<noteq> IRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> liftME ArchIRQControl (throwError (RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ))) \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<lbrakk>4 \<le> length args; Suc 0 \<le> length caps; UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0; invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler; gen_invocation_type label = IRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> throwError (RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)) \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<lbrakk>4 \<le> length args; Suc 0 \<le> length caps; UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0; invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler; gen_invocation_type label \<noteq> IRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> liftME ArchIRQControl (throwError IllegalOperation) \<lbrace>\<lambda>rv. P\<rbrace>
 5. \<lbrakk>4 \<le> length args; Suc 0 \<le> length caps; \<not> UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; gen_invocation_type label = IRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- if irq_active then throwError RevokeFirst else returnOk ();
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) (args ! 0)) dest_slot slot)
odE \<lbrace>\<lambda>rv. P\<rbrace>
 6. \<lbrakk>4 \<le> length args; Suc 0 \<le> length caps; \<not> UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; gen_invocation_type label \<noteq> IRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> liftME ArchIRQControl (doE irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- if irq_active then throwError RevokeFirst else returnOk ();
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
y <- ensure_empty dest_slot;
returnOk (ArchIRQControlIssue (UCAST(32 \<rightarrow> 10) (args ! 0)) dest_slot slot (args ! Suc 0 \<noteq> 0))
odE) \<lbrace>\<lambda>rv. P\<rbrace>
 7. \<lbrakk>4 \<le> length args; Suc 0 \<le> length caps; \<not> UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0; invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler; gen_invocation_type label = IRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- if irq_active then throwError RevokeFirst else returnOk ();
dest_slot <- lookup_slot_for_cnode_op False (caps ! 0) (to_bl (args ! Suc 0)) (unat (args ! 2));
y <- ensure_empty dest_slot;
returnOk (IRQControl (UCAST(32 \<rightarrow> 10) (args ! 0)) dest_slot slot)
odE \<lbrace>\<lambda>rv. P\<rbrace>
 8. \<lbrakk>4 \<le> length args; Suc 0 \<le> length caps; \<not> UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0; invocation_type label \<noteq> ArchInvocationLabel ARMIRQIssueIRQHandler; gen_invocation_type label \<noteq> IRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> liftME ArchIRQControl (throwError IllegalOperation) \<lbrace>\<lambda>rv. P\<rbrace>
 9. \<lbrakk>4 \<le> length args; \<not> Suc 0 \<le> length caps; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; gen_invocation_type label = IRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> throwError TruncatedMessage \<lbrace>\<lambda>rv. P\<rbrace>
 10. \<lbrakk>4 \<le> length args; \<not> Suc 0 \<le> length caps; invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; gen_invocation_type label \<noteq> IRQIssueIRQHandler\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> liftME ArchIRQControl (throwError TruncatedMessage) \<lbrace>\<lambda>rv. P\<rbrace>
A total of 36 subgoals... proof (prove)
goal:
No subgoals!