theory ArchInterrupt_AC

lemma arch_decode_irq_control_invocation_authorised[Interrupt_AC_assms]:
  "\<lbrace>pas_refined aag and
    K (is_subject aag (fst slot) \<and> (\<forall>cap \<in> set caps. pas_cap_cur_auth aag cap) \<and>
       (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (ucast (args ! 0))) \<in> pasPolicy aag))\<rbrace>
   arch_decode_irq_control_invocation info_label args slot caps
   \<lbrace>\<lambda>x _. arch_authorised_irq_ctl_inv aag x\<rbrace>, -" unfolding decode_irq_control_invocation_def arch_decode_irq_control_invocation_def
            authorised_irq_ctl_inv_def arch_authorised_irq_ctl_inv_def arch_check_irq_def apply (rule hoare_gen_asmE) apply (rule hoare_pre) apply (simp add: Let_def split del: if_split cong: if_cong) apply (wp whenE_throwError_wp hoare_vcg_imp_lift hoare_drop_imps
          | strengthen  aag_Control_owns_strg
          | simp add: o_def del: hoare_True_E_R)+ apply (cases args, simp_all) apply (cases caps, simp_all) apply (simp add: ucast_mask_drop) apply (auto simp: is_cap_simps cap_auth_conferred_def
                    pas_refined_wellformed
                    pas_refined_all_auth_is_owns aag_cap_auth_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag (fst slot) \<and> Ball (set caps) (pas_cap_cur_auth aag) \<and> (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag))\<rbrace> arch_decode_irq_control_invocation info_label args slot caps \<lbrace>\<lambda>x _. arch_authorised_irq_ctl_inv aag x\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and K (is_subject aag (fst slot) \<and> Ball (set caps) (pas_cap_cur_auth aag) \<and> (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag))\<rbrace> if invocation_type info_label = ArchInvocationLabel ARMIRQIssueIRQHandler then if 4 \<le> length args \<and> 1 \<le> length caps then let irq_word = args ! 0; trigger = args ! 1; index = args ! 2; depth = args ! 3; cnode = caps ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq_word) $ throwError (RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ));
irq_active <- liftE $ is_irq_active irq;
whenE irq_active $ throwError RevokeFirst;
dest_slot <- lookup_target_slot cnode (data_to_cptr index) (unat depth);
ensure_empty dest_slot;
returnOk $ ArchIRQControlIssue irq dest_slot slot (trigger \<noteq> 0)
odE else throwError TruncatedMessage else throwError IllegalOperation \<lbrace>\<lambda>x _. case x of ArchIRQControlIssue irq x1 x2 trigger \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst slot) \<and> Ball (set caps) (pas_cap_cur_auth aag) \<and> (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>pas_refined aag\<rbrace> if invocation_type info_label = ArchInvocationLabel ARMIRQIssueIRQHandler then if 4 \<le> length args \<and> 1 \<le> length caps then let irq_word = args ! 0; trigger = args ! 1; index = args ! 2; depth = args ! 3; cnode = caps ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq_word) $ throwError (RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ));
irq_active <- liftE $ is_irq_active irq;
whenE irq_active $ throwError RevokeFirst;
dest_slot <- lookup_target_slot cnode (data_to_cptr index) (unat depth);
ensure_empty dest_slot;
returnOk $ ArchIRQControlIssue irq dest_slot slot (trigger \<noteq> 0)
odE else throwError TruncatedMessage else throwError IllegalOperation \<lbrace>\<lambda>x _. case x of ArchIRQControlIssue irq x1 x2 trigger \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<and> Ball (set caps) (pas_cap_cur_auth aag) \<and> (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>?P'2\<rbrace> if invocation_type info_label = ArchInvocationLabel ARMIRQIssueIRQHandler then if 4 \<le> length args \<and> 1 \<le> length caps then let irq_word = args ! 0; trigger = args ! 1; index = args ! 2; depth = args ! 3; cnode = caps ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE whenE (UCAST(10 \<rightarrow> 32) maxIRQ < irq_word) $ throwError (RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ));
irq_active <- liftE $ is_irq_active irq;
whenE irq_active $ throwError RevokeFirst;
dest_slot <- lookup_target_slot cnode (data_to_cptr index) (unat depth);
ensure_empty dest_slot;
returnOk $ ArchIRQControlIssue irq dest_slot slot (trigger \<noteq> 0)
odE else throwError TruncatedMessage else throwError IllegalOperation \<lbrace>\<lambda>x _. case x of ArchIRQControlIssue irq x1 x2 trigger \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag\<rbrace>, -
 2. \<And>s. \<lbrakk>is_subject aag (fst slot) \<and> Ball (set caps) (pas_cap_cur_auth aag) \<and> (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag); pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (2 subgoals):
 1. is_subject aag (fst slot) \<and> Ball (set caps) (pas_cap_cur_auth aag) \<and> (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag) \<Longrightarrow> \<lbrace>?P'2\<rbrace> if invocation_type info_label = ArchInvocationLabel ARMIRQIssueIRQHandler then if 4 \<le> length args \<and> Suc 0 \<le> length caps then doE y <- whenE (UCAST(10 \<rightarrow> 32) maxIRQ < args ! 0) (throwError (RangeError 0 (UCAST(10 \<rightarrow> 32) maxIRQ)));
irq_active <- liftE (is_irq_active (UCAST(32 \<rightarrow> 10) (args ! 0)));
y <- whenE irq_active (throwError RevokeFirst);
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>\<lambda>x _. case x of ArchIRQControlIssue irq x1 x2 trigger \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag\<rbrace>, -
 2. \<And>s. \<lbrakk>is_subject aag (fst slot) \<and> Ball (set caps) (pas_cap_cur_auth aag) \<and> (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag); pas_refined aag s\<rbrakk> \<Longrightarrow> ?P'2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst slot) \<and> Ball (set caps) (pas_cap_cur_auth aag) \<and> (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag); pas_refined aag s\<rbrakk> \<Longrightarrow> invocation_type info_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>x\<in>obj_refs_ac (caps ! 0). is_subject aag x)) \<and> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s a list. \<lbrakk>is_subject aag (fst slot) \<and> Ball (set caps) (pas_cap_cur_auth aag) \<and> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) a)) \<in> pasPolicy aag; pas_refined aag s; args = a # list\<rbrakk> \<Longrightarrow> invocation_type info_label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> 3 \<le> length list \<and> Suc 0 \<le> length caps \<longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < a \<longrightarrow> is_cnode_cap (caps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (caps ! 0). is_subject aag x) proof (prove)
goal (1 subgoal):
 1. \<And>s a list aa lista. \<lbrakk>is_subject aag (fst slot) \<and> pas_cap_cur_auth aag aa \<and> Ball (set lista) (pas_cap_cur_auth aag) \<and> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) a)) \<in> pasPolicy aag; pas_refined aag s; args = a # list; caps = aa # lista\<rbrakk> \<Longrightarrow> invocation_type info_label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> 3 \<le> length list \<longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < a \<longrightarrow> is_cnode_cap aa \<longrightarrow> (\<forall>x\<in>obj_refs_ac aa. is_subject aag x) proof (prove)
goal (1 subgoal):
 1. \<And>s a list aa lista. \<lbrakk>is_subject aag (fst slot) \<and> pas_cap_cur_auth aag aa \<and> Ball (set lista) (pas_cap_cur_auth aag) \<and> (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) a)) \<in> pasPolicy aag; pas_refined aag s; args = a # list; caps = aa # lista\<rbrakk> \<Longrightarrow> invocation_type info_label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> 3 \<le> length list \<longrightarrow> \<not> UCAST(10 \<rightarrow> 32) maxIRQ < a \<longrightarrow> is_cnode_cap aa \<longrightarrow> (\<forall>x\<in>obj_refs_ac aa. is_subject aag x) proof (prove)
goal:
No subgoals!