theory ArchDecode_IF

lemma arch_decode_irq_control_invocation_rev[Decode_IF_assms]:
  "reads_equiv_valid_inv A aag
     (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)))
     (arch_decode_irq_control_invocation label args slot caps)" unfolding arch_decode_irq_control_invocation_def arch_check_irq_def apply (wp ensure_empty_rev lookup_slot_for_cnode_op_rev
            is_irq_active_rev whenE_inv
         | wp (once) hoare_drop_imps
         | simp add: Let_def)+ apply safe apply simp+ apply (blast intro: aag_Control_into_owns_irq ) apply (drule_tac x="caps ! 0" in bspec) apply (fastforce intro: bang_0_in_set) apply (drule (1) is_cnode_into_is_subject; blast dest: prop_of_obj_ref_of_cnode_cap) apply (fastforce dest: is_cnode_into_is_subject intro: bang_0_in_set) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (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))) (arch_decode_irq_control_invocation label args slot caps) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (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))) (if invocation_type 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) proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> 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> invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler \<longrightarrow> 4 \<le> length args \<and> Suc 0 \<le> length caps \<longrightarrow> is_subject_irq aag (UCAST(32 \<rightarrow> 10) (args ! 0)) \<and> (0 < unat (args ! 3) \<and> unat (args ! 3) \<le> word_bits \<longrightarrow> is_cnode_cap (caps ! 0) \<longrightarrow> is_subject aag (obj_ref_of (caps ! 0))) \<and> (is_cnode_cap (caps ! 0) \<longrightarrow> (\<forall>x\<in>obj_refs_ac (caps ! 0). is_subject aag x)) proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length []; Suc 0 \<le> length caps; args = []; \<not> False\<rbrakk> \<Longrightarrow> is_subject_irq aag (UCAST(32 \<rightarrow> 10) ([] ! 0))
 2. \<And>s. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length []; Suc 0 \<le> length caps; args = []; \<not> False; 0 < unat ([] ! 3); unat ([] ! 3) \<le> word_bits; is_cnode_cap (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of (caps ! 0))
 3. \<And>s x. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length []; Suc 0 \<le> length caps; args = []; \<not> False; is_cnode_cap (caps ! 0); x \<in> obj_refs_ac (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag x
 4. \<And>s. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject_irq aag (UCAST(32 \<rightarrow> 10) (args ! 0))
 5. \<And>s. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag; 0 < unat (args ! 3); unat (args ! 3) \<le> word_bits; is_cnode_cap (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of (caps ! 0))
 6. \<And>s x. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag; is_cnode_cap (caps ! 0); x \<in> obj_refs_ac (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject_irq aag (UCAST(32 \<rightarrow> 10) (args ! 0))
 2. \<And>s. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag; 0 < unat (args ! 3); unat (args ! 3) \<le> word_bits; is_cnode_cap (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of (caps ! 0))
 3. \<And>s x. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag; is_cnode_cap (caps ! 0); x \<in> obj_refs_ac (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag; 0 < unat (args ! 3); unat (args ! 3) \<le> word_bits; is_cnode_cap (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of (caps ! 0))
 2. \<And>s x. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag; is_cnode_cap (caps ! 0); x \<in> obj_refs_ac (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag; 0 < unat (args ! 3); unat (args ! 3) \<le> word_bits; is_cnode_cap (caps ! 0)\<rbrakk> \<Longrightarrow> caps ! 0 \<in> set caps
 2. \<And>s. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag; 0 < unat (args ! 3); unat (args ! 3) \<le> word_bits; is_cnode_cap (caps ! 0); pas_cap_cur_auth aag (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of (caps ! 0))
 3. \<And>s x. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag; is_cnode_cap (caps ! 0); x \<in> obj_refs_ac (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag; 0 < unat (args ! 3); unat (args ! 3) \<le> word_bits; is_cnode_cap (caps ! 0); pas_cap_cur_auth aag (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag (obj_ref_of (caps ! 0))
 2. \<And>s x. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag; is_cnode_cap (caps ! 0); x \<in> obj_refs_ac (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pas_refined aag s; is_subject aag (fst slot); Ball (set caps) (pas_cap_cur_auth aag); invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler; 4 \<le> length args; Suc 0 \<le> length caps; (pasSubject aag, Control, pasIRQAbs aag (UCAST(32 \<rightarrow> 10) (args ! 0))) \<in> pasPolicy aag; is_cnode_cap (caps ! 0); x \<in> obj_refs_ac (caps ! 0)\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal:
No subgoals!