theory Syscall_AC

lemma hacky_ipc_Send:
  "\<lbrakk> abs_has_auth_to aag Notify (interrupt_irq_node s irq) p;
     pas_refined aag s; pasMaySendIrqs aag \<rbrakk>
     \<Longrightarrow> aag_has_auth_to aag Notify p" unfolding pas_refined_def apply (clarsimp simp: policy_wellformed_def irq_map_wellformed_aux_def) apply (drule spec [where x = "pasIRQAbs aag irq"], drule spec [where x = "pasObjectAbs aag p"],
         erule mp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasObjectAbs aag (interrupt_irq_node s irq), Notify, pasObjectAbs aag p) \<in> pasPolicy aag; pas_refined aag s; pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Notify, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasObjectAbs aag (interrupt_irq_node s irq), Notify, pasObjectAbs aag p) \<in> pasPolicy aag; pas_wellformed aag \<and> irq_map_wellformed aag s \<and> tcb_domain_map_wellformed aag s \<and> state_objs_in_policy aag s \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag; pasMaySendIrqs aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Notify, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasIRQAbs aag irq, Notify, pasObjectAbs aag p) \<in> pasPolicy aag; pasMaySendIrqs aag; \<forall>agent'. (pasSubject aag, Control, agent') \<in> pasPolicy aag \<longrightarrow> pasSubject aag = agent'; \<forall>a. (pasSubject aag, a, pasSubject aag) \<in> pasPolicy aag; \<forall>s r. (\<exists>ep. (s, Grant, ep) \<in> pasPolicy aag \<and> (r, Receive, ep) \<in> pasPolicy aag) \<longrightarrow> (s, Control, r) \<in> pasPolicy aag \<and> (r, Control, s) \<in> pasPolicy aag; \<forall>irq ntfn. irq \<in> range (pasIRQAbs aag) \<and> (irq, Notify, ntfn) \<in> pasPolicy aag \<longrightarrow> (pasSubject aag, Notify, ntfn) \<in> pasPolicy aag; \<forall>s ep. (s, Call, ep) \<in> pasPolicy aag \<longrightarrow> (s, SyncSend, ep) \<in> pasPolicy aag; \<forall>s r. (\<exists>ep. (s, Call, ep) \<in> pasPolicy aag \<and> (r, Receive, ep) \<in> pasPolicy aag) \<longrightarrow> (r, Reply, s) \<in> pasPolicy aag; \<forall>s r. (s, Reply, r) \<in> pasPolicy aag \<longrightarrow> (r, DeleteDerived, s) \<in> pasPolicy aag; \<forall>l1 l2. (l1, DeleteDerived, l2) \<in> pasPolicy aag \<longrightarrow> (\<forall>l3. (l2, DeleteDerived, l3) \<in> pasPolicy aag \<longrightarrow> (l1, DeleteDerived, l3) \<in> pasPolicy aag); \<forall>s r. (\<exists>ep. (s, Call, ep) \<in> pasPolicy aag \<and> (r, Receive, ep) \<in> pasPolicy aag \<and> (r, Grant, ep) \<in> pasPolicy aag) \<longrightarrow> (s, Control, r) \<in> pasPolicy aag \<and> (r, Control, s) \<in> pasPolicy aag; \<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Notify, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasIRQAbs aag irq, Notify, pasObjectAbs aag p) \<in> pasPolicy aag; pasMaySendIrqs aag; \<forall>agent'. (pasSubject aag, Control, agent') \<in> pasPolicy aag \<longrightarrow> pasSubject aag = agent'; \<forall>a. (pasSubject aag, a, pasSubject aag) \<in> pasPolicy aag; \<forall>s r. (\<exists>ep. (s, Grant, ep) \<in> pasPolicy aag \<and> (r, Receive, ep) \<in> pasPolicy aag) \<longrightarrow> (s, Control, r) \<in> pasPolicy aag \<and> (r, Control, s) \<in> pasPolicy aag; \<forall>s ep. (s, Call, ep) \<in> pasPolicy aag \<longrightarrow> (s, SyncSend, ep) \<in> pasPolicy aag; \<forall>s r. (\<exists>ep. (s, Call, ep) \<in> pasPolicy aag \<and> (r, Receive, ep) \<in> pasPolicy aag) \<longrightarrow> (r, Reply, s) \<in> pasPolicy aag; \<forall>s r. (s, Reply, r) \<in> pasPolicy aag \<longrightarrow> (r, DeleteDerived, s) \<in> pasPolicy aag; \<forall>l1 l2. (l1, DeleteDerived, l2) \<in> pasPolicy aag \<longrightarrow> (\<forall>l3. (l2, DeleteDerived, l3) \<in> pasPolicy aag \<longrightarrow> (l1, DeleteDerived, l3) \<in> pasPolicy aag); \<forall>s r. (\<exists>ep. (s, Call, ep) \<in> pasPolicy aag \<and> (r, Receive, ep) \<in> pasPolicy aag \<and> (r, Grant, ep) \<in> pasPolicy aag) \<longrightarrow> (s, Control, r) \<in> pasPolicy aag \<and> (r, Control, s) \<in> pasPolicy aag; \<forall>irq. pasObjectAbs aag (interrupt_irq_node s irq) = pasIRQAbs aag irq; tcb_domain_map_wellformed aag s; state_objs_in_policy aag s; state_asids_to_policy aag s \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag\<rbrakk> \<Longrightarrow> pasIRQAbs aag irq \<in> range (pasIRQAbs aag) \<and> (pasIRQAbs aag irq, Notify, pasObjectAbs aag p) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!