theory Finalise_AC

lemma cancel_ipc_respects[wp]:
  "\<lbrace>integrity aag X st and einvs and tcb_at t and K (is_subject aag t) and pas_refined aag\<rbrace>
   cancel_ipc t
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: cancel_ipc_def) apply (rule hoare_seq_ext[OF _ gts_sp]) apply (rule hoare_pre) apply (wp set_thread_state_integrity_autarch set_endpoint_respects get_simple_ko_wp
          | wpc
          | simp (no_asm) add: blocked_cancel_ipc_def get_ep_queue_def get_blocking_object_def)+ apply clarsimp apply (frule st_tcb_at_to_thread_st_auth, clarsimp+) apply (fastforce simp: obj_at_def is_ep_def dest: pas_refined_mem[OF sta_ts_mem]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and einvs and tcb_at t and K (is_subject aag t) and pas_refined aag\<rbrace> cancel_ipc t \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and einvs and tcb_at t and (\<lambda>y. is_subject aag t) and pas_refined aag\<rbrace> do state <- get_thread_state t;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at ((=) state) t and (integrity aag X st and einvs and tcb_at t and (\<lambda>y. is_subject aag t) and pas_refined aag)\<rbrace> case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state. \<lbrace>?Q4 state\<rbrace> case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and einvs and tcb_at t and (\<lambda>y. is_subject aag t) and pas_refined aag)) s \<Longrightarrow> ?Q4 state s proof (prove)
goal (1 subgoal):
 1. \<And>state s. (st_tcb_at ((=) state) t and (integrity aag X st and einvs and tcb_at t and (\<lambda>y. is_subject aag t) and pas_refined aag)) s \<Longrightarrow> (state = Running \<longrightarrow> integrity aag X st s) \<and> (inactive state \<longrightarrow> integrity aag X st s) \<and> (state = Restart \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. (\<exists>xa. state = BlockedOnReceive x xa) \<longrightarrow> (\<forall>ntfn. ko_at (Endpoint ntfn) x s \<longrightarrow> ((\<exists>x. ntfn = SendEP x) \<longrightarrow> integrity aag X st s \<and> ep_at x s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> is_subject aag t) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> integrity aag X st s \<and> ep_at x s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> is_subject aag t))) \<and> (\<forall>x. (\<exists>xa. state = BlockedOnSend x xa) \<longrightarrow> (\<forall>ntfn. ko_at (Endpoint ntfn) x s \<longrightarrow> ((\<exists>x. ntfn = SendEP x) \<longrightarrow> integrity aag X st s \<and> ep_at x s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> is_subject aag t) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> integrity aag X st s \<and> ep_at x s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> is_subject aag t))) \<and> (awaiting_reply state \<longrightarrow> integrity aag X st s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> tcb_at t s \<and> is_subject aag t \<and> pas_refined aag s) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> integrity aag X st s \<and> is_subject aag t \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify))) \<and> (idle state \<longrightarrow> integrity aag X st s) proof (prove)
goal (1 subgoal):
 1. \<And>state s. \<lbrakk>st_tcb_at ((=) state) t s; integrity aag X st s; invs s; valid_list s; valid_sched s; tcb_at t s; is_subject aag t; pas_refined aag s\<rbrakk> \<Longrightarrow> (\<forall>x. (\<exists>xa. state = BlockedOnReceive x xa) \<longrightarrow> (\<forall>ntfn. ko_at (Endpoint ntfn) x s \<longrightarrow> ((\<exists>x. ntfn = SendEP x) \<longrightarrow> ep_at x s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> ep_at x s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))))) \<and> (\<forall>x. (\<exists>xa. state = BlockedOnSend x xa) \<longrightarrow> (\<forall>ntfn. ko_at (Endpoint ntfn) x s \<longrightarrow> ((\<exists>x. ntfn = SendEP x) \<longrightarrow> ep_at x s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> ep_at x s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))))) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify))) proof (prove)
goal (1 subgoal):
 1. \<And>state s. \<lbrakk>st_tcb_at ((=) state) t s; integrity aag X st s; invs s; valid_list s; valid_sched s; tcb_at t s; is_subject aag t; pas_refined aag s; thread_st_auth s t = tcb_st_to_auth state\<rbrakk> \<Longrightarrow> (\<forall>x. (\<exists>xa. state = BlockedOnReceive x xa) \<longrightarrow> (\<forall>ntfn. ko_at (Endpoint ntfn) x s \<longrightarrow> ((\<exists>x. ntfn = SendEP x) \<longrightarrow> ep_at x s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> ep_at x s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))))) \<and> (\<forall>x. (\<exists>xa. state = BlockedOnSend x xa) \<longrightarrow> (\<forall>ntfn. ko_at (Endpoint ntfn) x s \<longrightarrow> ((\<exists>x. ntfn = SendEP x) \<longrightarrow> ep_at x s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))) \<and> ((\<exists>x. ntfn = RecvEP x) \<longrightarrow> ep_at x s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))))) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag x) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = Notify))) proof (prove)
goal:
No subgoals!