theory Finalise_AC

lemma cancel_badged_sends_respects[wp]:
  "\<lbrace>integrity aag X st and einvs and valid_objs
                       and (sym_refs \<circ> state_refs_of)
                       and K (aag_has_auth_to aag Reset epptr)\<rbrace>
   cancel_badged_sends epptr badge
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: cancel_badged_sends_def filterM_mapM
             cong: endpoint.case_cong) apply (wp set_endpoint_respects | wpc | simp)+ apply (rule mapM_mapM_x_valid[THEN iffD1]) apply (simp add: exI[where x=Reset]) apply (rule mapM_x_inv_wp2
                  [where V="\<lambda>q s. distinct q \<and> (\<forall>x \<in> set q. st_tcb_at (blocked_on epptr) x s)"
                     and Q="P" and I="P" for P]) apply simp apply (simp add: bind_assoc) apply (rule hoare_seq_ext[OF _ gts_sp]) apply (rule hoare_pre) apply (wp sts_respects_restart_ep hoare_vcg_const_Ball_lift sts_st_tcb_at_neq) apply clarsimp apply fastforce apply (wp set_endpoint_respects hoare_vcg_const_Ball_lift get_simple_ko_wp)+ apply clarsimp apply (frule(1) sym_refs_ko_atD) apply (frule ko_at_state_refs_ofD) apply (rule obj_at_valid_objsE, assumption, assumption) apply (clarsimp simp: st_tcb_at_refs_of_rev st_tcb_def2) apply (clarsimp simp: obj_at_def is_ep valid_obj_def valid_ep_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of and K ((pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag)\<rbrace> cancel_badged_sends epptr badge \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of\<rbrace> cancel_badged_sends epptr badge \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of\<rbrace> do ep <- get_endpoint epptr;
case ep of SendEP queue \<Rightarrow> do y <- set_endpoint epptr IdleEP;
ys <- mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = badge then do y <- set_thread_state x Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) queue;
y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (map fst (filter snd ys)));
reschedule_required
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B30 (SendEP x2) x2 ()\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = badge then do y <- set_thread_state x Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>ys s. integrity aag X st s \<and> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))\<rbrace>
 2. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>?B30 ep x2\<rbrace>
 3. \<And>ep x3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R23 ep x3\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R22 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R23 ep x s)\<rbrace>
 5. \<And>s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (5 subgoals):
 1. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B30 (SendEP x2) x2 ()\<rbrace> mapM_x (\<lambda>a. do v <- do st <- get_thread_state a;
if blocking_ipc_badge st = badge then do y <- set_thread_state a Restart;
y <- tcb_sched_action tcb_sched_enqueue a;
return False
od else return True
od;
return (a, v)
od) x2 \<lbrace>\<lambda>ys a. integrity aag X st a \<and> ep_at epptr a \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset))\<rbrace>
 2. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>?B30 ep x2\<rbrace>
 3. \<And>ep x3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R23 ep x3\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R22 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R23 ep x s)\<rbrace>
 5. \<And>s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (5 subgoals):
 1. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?B30 (SendEP x2) x2 ()\<rbrace> mapM_x (\<lambda>a. do v <- do st <- get_thread_state a;
if blocking_ipc_badge st = badge then do y <- set_thread_state a Restart;
y <- tcb_sched_action tcb_sched_enqueue a;
return False
od else return True
od;
return (a, v)
od) x2 \<lbrace>\<lambda>ys a. integrity aag X st a \<and> ep_at epptr a\<rbrace>
 2. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>?B30 ep x2\<rbrace>
 3. \<And>ep x3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R23 ep x3\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R22 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R23 ep x s)\<rbrace>
 5. \<And>s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (6 subgoals):
 1. \<And>ep x2 s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2; integrity aag X st s \<and> ep_at epptr s; distinct [] \<and> (\<forall>x\<in>set []. st_tcb_at (blocked_on epptr) x s)\<rbrakk> \<Longrightarrow> integrity aag X st s \<and> ep_at epptr s
 2. \<And>ep x2 a as. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2; suffix (a # as) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (integrity aag X st s \<and> ep_at epptr s) \<and> distinct (a # as) \<and> (\<forall>x\<in>set (a # as). st_tcb_at (blocked_on epptr) x s)\<rbrace> do v <- do st <- get_thread_state a;
if blocking_ipc_badge st = badge then do y <- set_thread_state a Restart;
y <- tcb_sched_action tcb_sched_enqueue a;
return False
od else return True
od;
return (a, v)
od \<lbrace>\<lambda>r s. (integrity aag X st s \<and> ep_at epptr s) \<and> distinct as \<and> (\<forall>x\<in>set as. st_tcb_at (blocked_on epptr) x s)\<rbrace>
 3. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>\<lambda>a. (\<lambda>a. integrity aag X st a \<and> ep_at epptr a) and (\<lambda>s. distinct x2 \<and> (\<forall>x\<in>set x2. st_tcb_at (blocked_on epptr) x s))\<rbrace>
 4. \<And>ep x3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R23 ep x3\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R22 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R23 ep x s)\<rbrace>
 6. \<And>s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (5 subgoals):
 1. \<And>ep x2 a as. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2; suffix (a # as) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (integrity aag X st s \<and> ep_at epptr s) \<and> distinct (a # as) \<and> (\<forall>x\<in>set (a # as). st_tcb_at (blocked_on epptr) x s)\<rbrace> do v <- do st <- get_thread_state a;
if blocking_ipc_badge st = badge then do y <- set_thread_state a Restart;
y <- tcb_sched_action tcb_sched_enqueue a;
return False
od else return True
od;
return (a, v)
od \<lbrace>\<lambda>r s. (integrity aag X st s \<and> ep_at epptr s) \<and> distinct as \<and> (\<forall>x\<in>set as. st_tcb_at (blocked_on epptr) x s)\<rbrace>
 2. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>\<lambda>a. (\<lambda>a. integrity aag X st a \<and> ep_at epptr a) and (\<lambda>s. distinct x2 \<and> (\<forall>x\<in>set x2. st_tcb_at (blocked_on epptr) x s))\<rbrace>
 3. \<And>ep x3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R23 ep x3\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R22 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R23 ep x s)\<rbrace>
 5. \<And>s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (5 subgoals):
 1. \<And>ep x2 a as. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2; suffix (a # as) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. integrity aag X st s \<and> ep_at epptr s \<and> a \<notin> set as \<and> distinct as \<and> st_tcb_at (blocked_on epptr) a s \<and> (\<forall>x\<in>set as. st_tcb_at (blocked_on epptr) x s)\<rbrace> do x <- get_thread_state a;
v <- if blocking_ipc_badge x = badge then do y <- set_thread_state a Restart;
y <- tcb_sched_action tcb_sched_enqueue a;
return False
od else return True;
return (a, v)
od \<lbrace>\<lambda>r s. integrity aag X st s \<and> ep_at epptr s \<and> distinct as \<and> (\<forall>x\<in>set as. st_tcb_at (blocked_on epptr) x s)\<rbrace>
 2. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>\<lambda>a. (\<lambda>a. integrity aag X st a \<and> ep_at epptr a) and (\<lambda>s. distinct x2 \<and> (\<forall>x\<in>set x2. st_tcb_at (blocked_on epptr) x s))\<rbrace>
 3. \<And>ep x3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R23 ep x3\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R22 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R23 ep x s)\<rbrace>
 5. \<And>s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (5 subgoals):
 1. \<And>ep x2 a as x. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2; suffix (a # as) x2\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at ((=) x) a and (\<lambda>s. integrity aag X st s \<and> ep_at epptr s \<and> a \<notin> set as \<and> distinct as \<and> st_tcb_at (blocked_on epptr) a s \<and> (\<forall>x\<in>set as. st_tcb_at (blocked_on epptr) x s))\<rbrace> do v <- if blocking_ipc_badge x = badge then do y <- set_thread_state a Restart;
y <- tcb_sched_action tcb_sched_enqueue a;
return False
od else return True;
return (a, v)
od \<lbrace>\<lambda>r s. integrity aag X st s \<and> ep_at epptr s \<and> distinct as \<and> (\<forall>x\<in>set as. st_tcb_at (blocked_on epptr) x s)\<rbrace>
 2. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>\<lambda>a. (\<lambda>a. integrity aag X st a \<and> ep_at epptr a) and (\<lambda>s. distinct x2 \<and> (\<forall>x\<in>set x2. st_tcb_at (blocked_on epptr) x s))\<rbrace>
 3. \<And>ep x3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R23 ep x3\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R22 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R23 ep x s)\<rbrace>
 5. \<And>s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (6 subgoals):
 1. \<And>ep x2 a as x. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2; suffix (a # as) x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q53 ep x2 a as x\<rbrace> do v <- if blocking_ipc_badge x = badge then do y <- set_thread_state a Restart;
y <- tcb_sched_action tcb_sched_enqueue a;
return False
od else return True;
return (a, v)
od \<lbrace>\<lambda>r s. integrity aag X st s \<and> ep_at epptr s \<and> distinct as \<and> (\<forall>x\<in>set as. st_tcb_at (blocked_on epptr) x s)\<rbrace>
 2. \<And>ep x2 a as x s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2; suffix (a # as) x2; (st_tcb_at ((=) x) a and (\<lambda>s. integrity aag X st s \<and> ep_at epptr s \<and> a \<notin> set as \<and> distinct as \<and> st_tcb_at (blocked_on epptr) a s \<and> (\<forall>x\<in>set as. st_tcb_at (blocked_on epptr) x s))) s\<rbrakk> \<Longrightarrow> ?Q53 ep x2 a as x s
 3. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>\<lambda>a. (\<lambda>a. integrity aag X st a \<and> ep_at epptr a) and (\<lambda>s. distinct x2 \<and> (\<forall>x\<in>set x2. st_tcb_at (blocked_on epptr) x s))\<rbrace>
 4. \<And>ep x3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R23 ep x3\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R22 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R23 ep x s)\<rbrace>
 6. \<And>s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (5 subgoals):
 1. \<And>ep x2 a as x s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2; suffix (a # as) x2; (st_tcb_at ((=) x) a and (\<lambda>s. integrity aag X st s \<and> ep_at epptr s \<and> a \<notin> set as \<and> distinct as \<and> st_tcb_at (blocked_on epptr) a s \<and> (\<forall>x\<in>set as. st_tcb_at (blocked_on epptr) x s))) s\<rbrakk> \<Longrightarrow> (blocking_ipc_badge x = badge \<longrightarrow> (integrity aag X st and (\<lambda>s. \<exists>ep. (pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> st_tcb_at (blocked_on ep) a s)) s \<and> ep_at epptr s \<and> distinct as \<and> (\<forall>x\<in>set as. (st_tcb_at (blocked_on epptr) x and K (x \<noteq> a)) s)) \<and> (blocking_ipc_badge x \<noteq> badge \<longrightarrow> integrity aag X st s \<and> ep_at epptr s \<and> distinct as \<and> (\<forall>x\<in>set as. st_tcb_at (blocked_on epptr) x s))
 2. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>\<lambda>a. (\<lambda>a. integrity aag X st a \<and> ep_at epptr a) and (\<lambda>s. distinct x2 \<and> (\<forall>x\<in>set x2. st_tcb_at (blocked_on epptr) x s))\<rbrace>
 3. \<And>ep x3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R23 ep x3\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R22 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R23 ep x s)\<rbrace>
 5. \<And>s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (5 subgoals):
 1. \<And>x2 a as x s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; suffix (a # as) x2; st_tcb_at ((=) x) a s; integrity aag X st s; ep_at epptr s; a \<notin> set as; distinct as; st_tcb_at (blocked_on epptr) a s; \<forall>x\<in>set as. st_tcb_at (blocked_on epptr) x s; badge = blocking_ipc_badge x\<rbrakk> \<Longrightarrow> (\<exists>ep. (pasSubject aag, Reset, pasObjectAbs aag ep) \<in> pasPolicy aag \<and> st_tcb_at (blocked_on ep) a s) \<and> (\<forall>x\<in>set as. x \<noteq> a)
 2. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>\<lambda>a. (\<lambda>a. integrity aag X st a \<and> ep_at epptr a) and (\<lambda>s. distinct x2 \<and> (\<forall>x\<in>set x2. st_tcb_at (blocked_on epptr) x s))\<rbrace>
 3. \<And>ep x3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R23 ep x3\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R22 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R23 ep x s)\<rbrace>
 5. \<And>s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (4 subgoals):
 1. \<And>ep x2. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?R22 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>\<lambda>a. (\<lambda>a. integrity aag X st a \<and> ep_at epptr a) and (\<lambda>s. distinct x2 \<and> (\<forall>x\<in>set x2. st_tcb_at (blocked_on epptr) x s))\<rbrace>
 2. \<And>ep x3. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; ep = RecvEP x3\<rbrakk> \<Longrightarrow> \<lbrace>?R23 ep x3\<rbrace> return () \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. (pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_endpoint epptr \<lbrace>\<lambda>ep s. (ep = IdleEP \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. ep = SendEP x \<longrightarrow> ?R22 ep x s) \<and> (\<forall>x. ep = RecvEP x \<longrightarrow> ?R23 ep x s)\<rbrace>
 4. \<And>s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of) s\<rbrakk> \<Longrightarrow> ?Q8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; (integrity aag X st and einvs and valid_objs and sym_refs \<circ> state_refs_of) s\<rbrakk> \<Longrightarrow> \<forall>ntfn. ko_at (Endpoint ntfn) epptr s \<longrightarrow> (ntfn = IdleEP \<longrightarrow> integrity aag X st s) \<and> (\<forall>x. ntfn = SendEP x \<longrightarrow> (integrity aag X st and ep_at epptr and K (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> auth \<in> {Receive, SyncSend, Reset})) s \<and> ep_at epptr s \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s)) \<and> (\<forall>x. ntfn = RecvEP x \<longrightarrow> integrity aag X st s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; invs s; valid_list s; valid_sched s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint (SendEP x)) epptr s\<rbrakk> \<Longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> ep_at epptr s \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; invs s; valid_list s; valid_sched s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint (SendEP x)) epptr s; state_refs_of s epptr = refs_of (Endpoint (SendEP x)) \<and> (\<forall>(x, tp)\<in>refs_of (Endpoint (SendEP x)). obj_at (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of ko) x s)\<rbrakk> \<Longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> ep_at epptr s \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; invs s; valid_list s; valid_sched s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint (SendEP x)) epptr s; state_refs_of s epptr = refs_of (Endpoint (SendEP x)) \<and> (\<forall>(x, tp)\<in>refs_of (Endpoint (SendEP x)). obj_at (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of ko) x s); state_refs_of s epptr = refs_of (Endpoint (SendEP x))\<rbrakk> \<Longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> ep_at epptr s \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x ko. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; invs s; valid_list s; valid_sched s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint (SendEP x)) epptr s; state_refs_of s epptr = refs_of (Endpoint (SendEP x)) \<and> (\<forall>(x, tp)\<in>refs_of (Endpoint (SendEP x)). obj_at (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of ko) x s); state_refs_of s epptr = refs_of (Endpoint (SendEP x)); kheap s epptr = Some ko; Endpoint (SendEP x) = ko; valid_obj epptr ko s\<rbrakk> \<Longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> ep_at epptr s \<and> distinct x \<and> (\<forall>x\<in>set x. st_tcb_at (blocked_on epptr) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; invs s; valid_list s; valid_sched s; valid_objs s; sym_refs (state_refs_of s); ko_at (Endpoint (SendEP x)) epptr s; \<forall>x\<in>set x. \<exists>tcb. get_tcb x s = Some tcb \<and> (\<exists>pl. tcb_state tcb = BlockedOnSend epptr pl); state_refs_of s epptr = set x \<times> {EPSend}; kheap s epptr = Some (Endpoint (SendEP x)); valid_obj epptr (Endpoint (SendEP x)) s\<rbrakk> \<Longrightarrow> ep_at epptr s \<and> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> ep_at epptr s \<and> distinct x \<and> (\<forall>x\<in>set x. \<exists>tcb. get_tcb x s = Some tcb \<and> blocked_on epptr (tcb_state tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>(pasSubject aag, Reset, pasObjectAbs aag epptr) \<in> pasPolicy aag; integrity aag X st s; invs s; valid_list s; valid_sched s; valid_objs s; sym_refs (state_refs_of s); \<forall>x\<in>set x. \<exists>tcb. get_tcb x s = Some tcb \<and> (\<exists>pl. tcb_state tcb = BlockedOnSend epptr pl); state_refs_of s epptr = set x \<times> {EPSend}; kheap s epptr = Some (Endpoint (SendEP x)); x \<noteq> []; \<forall>t\<in>set x. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; distinct x\<rbrakk> \<Longrightarrow> (\<exists>auth. (pasSubject aag, auth, pasObjectAbs aag epptr) \<in> pasPolicy aag \<and> (auth = Receive \<or> auth = SyncSend \<or> auth = Reset)) \<and> (\<forall>x\<in>set x. \<exists>tcb. get_tcb x s = Some tcb \<and> blocked_on epptr (tcb_state tcb)) proof (prove)
goal:
No subgoals!