theory ArchInterrupt_AI

lemma decode_irq_control_valid [Interrupt_AI_asms]:
  "\<lbrace>\<lambda>s. invs s \<and> (\<forall>cap \<in> set caps. s \<turnstile> cap)
        \<and> (\<forall>cap \<in> set caps. is_cnode_cap cap \<longrightarrow>
                (\<forall>r \<in> cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s))
        \<and> cte_wp_at ((=) cap.IRQControlCap) slot s\<rbrace>
     decode_irq_control_invocation label args slot caps
   \<lbrace>irq_control_inv_valid\<rbrace>,-" apply (simp add: decode_irq_control_invocation_def Let_def split_def
                   whenE_def arch_check_irq_def
                   arch_decode_irq_control_invocation_def
                 split del: if_split cong: if_cong) apply (wpsimp wp: ensure_empty_stronger simp: cte_wp_at_eq_simp arch_irq_control_inv_valid_def
        | wp (once) hoare_drop_imps)+ apply (clarsimp simp: linorder_not_less word_le_nat_alt unat_ucast maxIRQ_def) apply (cases caps ; fastforce simp: cte_wp_at_eq_simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> (\<forall>cap\<in>set caps. s \<turnstile> cap) \<and> (\<forall>cap\<in>set caps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) \<and> cte_wp_at ((=) IRQControlCap) slot s\<rbrace> decode_irq_control_invocation label args slot caps \<lbrace>irq_control_inv_valid\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs s \<and> (\<forall>cap\<in>set caps. s \<turnstile> cap) \<and> (\<forall>cap\<in>set caps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) \<and> cte_wp_at ((=) IRQControlCap) slot s\<rbrace> if gen_invocation_type label = IRQIssueIRQHandler then if 3 \<le> length args \<and> Suc 0 \<le> length caps then doE y <- if UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0 then throwError (RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)) else returnOk ();
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 else throwError TruncatedMessage else liftME ArchIRQControl (if invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler then if 4 \<le> length args \<and> Suc 0 \<le> length caps then doE y <- if UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0 then throwError (RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)) else returnOk ();
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 else throwError TruncatedMessage else throwError IllegalOperation) \<lbrace>irq_control_inv_valid\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; \<forall>cap\<in>set caps. s \<turnstile> cap; \<forall>cap\<in>set caps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s); cte_wp_at (\<lambda>c. c = IRQControlCap) slot s\<rbrakk> \<Longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> 3 \<le> length args \<and> Suc 0 \<le> length caps \<longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0 \<longrightarrow> (is_cnode_cap (caps ! 0) \<longrightarrow> (\<forall>r\<in>cte_refs (caps ! 0) (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) \<and> valid_objs s \<and> s \<turnstile> caps ! 0 \<and> UCAST(32 \<rightarrow> 10) (args ! 0) \<le> maxIRQ) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> 4 \<le> length args \<and> Suc 0 \<le> length caps \<longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0 \<longrightarrow> (is_cnode_cap (caps ! 0) \<longrightarrow> (\<forall>r\<in>cte_refs (caps ! 0) (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) \<and> valid_objs s \<and> s \<turnstile> caps ! 0 \<and> UCAST(32 \<rightarrow> 10) (args ! 0) \<le> maxIRQ) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; \<forall>cap\<in>set caps. s \<turnstile> cap; \<forall>cap\<in>set caps. is_cnode_cap cap \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s); cte_wp_at (\<lambda>c. c = IRQControlCap) slot s\<rbrakk> \<Longrightarrow> (gen_invocation_type label = IRQIssueIRQHandler \<longrightarrow> 3 \<le> length args \<and> Suc 0 \<le> length caps \<longrightarrow> unat (args ! 0) \<le> 159 \<longrightarrow> (is_cnode_cap (caps ! 0) \<longrightarrow> (\<forall>r\<in>cte_refs (caps ! 0) (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) \<and> valid_objs s \<and> s \<turnstile> caps ! 0) \<and> (gen_invocation_type label \<noteq> IRQIssueIRQHandler \<longrightarrow> invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> 4 \<le> length args \<and> Suc 0 \<le> length caps \<longrightarrow> unat (args ! 0) \<le> 159 \<longrightarrow> (is_cnode_cap (caps ! 0) \<longrightarrow> (\<forall>r\<in>cte_refs (caps ! 0) (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) \<and> valid_objs s \<and> s \<turnstile> caps ! 0) proof (prove)
goal:
No subgoals!