theory Ipc_AI

lemma si_blk_makes_simple:
  "\<lbrace>st_tcb_at simple t and K (t \<noteq> t') :: 'state_ext state \<Rightarrow> bool\<rbrace>
     send_ipc True call bdg x gr t' ep
   \<lbrace>\<lambda>rv. st_tcb_at simple t\<rbrace>" apply (simp add: send_ipc_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_inv]) apply (case_tac epa, simp_all) apply (wp sts_st_tcb_at_cases) apply clarsimp apply (wp sts_st_tcb_at_cases) apply clarsimp apply (rule hoare_gen_asm[simplified]) apply (rename_tac list) apply (case_tac list, simp_all split del:if_split) apply (rule hoare_seq_ext [OF _ set_simple_ko_pred_tcb_at]) apply (rule hoare_seq_ext [OF _ gts_sp]) apply (case_tac recv_state, simp_all split del: if_split) apply (wp sts_st_tcb_at_cases setup_caller_cap_makes_simple
            hoare_drop_imps
            | simp add: if_apply_def2 split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and K (t \<noteq> t')\<rbrace> send_ipc True call bdg x gr t' ep \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')\<rbrace> do epa <- get_endpoint ep;
case epa of IdleEP \<Rightarrow> case True of True \<Rightarrow> do set_thread_state t' (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>);
set_endpoint ep $ SendEP [t']
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case True of True \<Rightarrow> do set_thread_state t' (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>);
set_endpoint ep $ SendEP (queue @ [t'])
od | False \<Rightarrow> return () | RecvEP [] \<Rightarrow> fail | RecvEP (dest # queue) \<Rightarrow> do set_endpoint ep $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive xa data \<Rightarrow> do do_ipc_transfer t' (Some ep) bdg x dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if x \<or> gr then setup_caller_cap t' dest reply_can_grant else set_thread_state t' Inactive
od
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epa. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')\<rbrace> case epa of IdleEP \<Rightarrow> case True of True \<Rightarrow> do set_thread_state t' (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>);
set_endpoint ep $ SendEP [t']
od | False \<Rightarrow> return () | SendEP queue \<Rightarrow> case True of True \<Rightarrow> do set_thread_state t' (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>);
set_endpoint ep $ SendEP (queue @ [t'])
od | False \<Rightarrow> return () | RecvEP [] \<Rightarrow> fail | RecvEP (dest # queue) \<Rightarrow> do set_endpoint ep $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive xa data \<Rightarrow> do do_ipc_transfer t' (Some ep) bdg x dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if x \<or> gr then setup_caller_cap t' dest reply_can_grant else set_thread_state t' Inactive
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- set_thread_state t' (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>);
set_endpoint ep (SendEP [t'])
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 2. \<And>epa x2. epa = SendEP x2 \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- set_thread_state t' (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>);
set_endpoint ep (SendEP (x2 @ [t']))
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 3. \<And>epa x3. epa = RecvEP x3 \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')\<rbrace> case x3 of [] \<Rightarrow> fail | dest # queue \<Rightarrow> do set_endpoint ep $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive xa data \<Rightarrow> do do_ipc_transfer t' (Some ep) bdg x dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if x \<or> gr then setup_caller_cap t' dest reply_can_grant else set_thread_state t' Inactive
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. (st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')) s \<Longrightarrow> (t' = t \<longrightarrow> inactive (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>) \<or> BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr> = Running \<or> BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr> = Restart \<or> idle (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>) \<or> awaiting_reply (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>)) \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t s)
 2. \<And>epa x2. epa = SendEP x2 \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- set_thread_state t' (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>);
set_endpoint ep (SendEP (x2 @ [t']))
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 3. \<And>epa x3. epa = RecvEP x3 \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')\<rbrace> case x3 of [] \<Rightarrow> fail | dest # queue \<Rightarrow> do set_endpoint ep $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive xa data \<Rightarrow> do do_ipc_transfer t' (Some ep) bdg x dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if x \<or> gr then setup_caller_cap t' dest reply_can_grant else set_thread_state t' Inactive
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>epa x2. epa = SendEP x2 \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- set_thread_state t' (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>);
set_endpoint ep (SendEP (x2 @ [t']))
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace>
 2. \<And>epa x3. epa = RecvEP x3 \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')\<rbrace> case x3 of [] \<Rightarrow> fail | dest # queue \<Rightarrow> do set_endpoint ep $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive xa data \<Rightarrow> do do_ipc_transfer t' (Some ep) bdg x dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if x \<or> gr then setup_caller_cap t' dest reply_can_grant else set_thread_state t' Inactive
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>epa x2 s. \<lbrakk>epa = SendEP x2; (st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')) s\<rbrakk> \<Longrightarrow> (t' = t \<longrightarrow> inactive (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>) \<or> BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr> = Running \<or> BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr> = Restart \<or> idle (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>) \<or> awaiting_reply (BlockedOnSend ep \<lparr>sender_badge = bdg, sender_can_grant = x, sender_can_grant_reply = gr, sender_is_call = call\<rparr>)) \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t s)
 2. \<And>epa x3. epa = RecvEP x3 \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')\<rbrace> case x3 of [] \<Rightarrow> fail | dest # queue \<Rightarrow> do set_endpoint ep $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive xa data \<Rightarrow> do do_ipc_transfer t' (Some ep) bdg x dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if x \<or> gr then setup_caller_cap t' dest reply_can_grant else set_thread_state t' Inactive
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epa x3. epa = RecvEP x3 \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and (\<lambda>y. t \<noteq> t')\<rbrace> case x3 of [] \<Rightarrow> fail | dest # queue \<Rightarrow> do set_endpoint ep $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive xa data \<Rightarrow> do do_ipc_transfer t' (Some ep) bdg x dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if x \<or> gr then setup_caller_cap t' dest reply_can_grant else set_thread_state t' Inactive
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epa x3. \<lbrakk>epa = RecvEP x3; t \<noteq> t'\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> case x3 of [] \<Rightarrow> fail | dest # queue \<Rightarrow> do set_endpoint ep $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive xa data \<Rightarrow> do do_ipc_transfer t' (Some ep) bdg x dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if x \<or> gr then setup_caller_cap t' dest reply_can_grant else set_thread_state t' Inactive
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epa list. \<lbrakk>epa = RecvEP list; t \<noteq> t'\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> case list of [] \<Rightarrow> fail | dest # queue \<Rightarrow> do set_endpoint ep $ case queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP queue;
recv_state <- get_thread_state dest;
reply_can_grant <- case recv_state of BlockedOnReceive xa data \<Rightarrow> do do_ipc_transfer t' (Some ep) bdg x dest;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
set_thread_state dest Running;
do_extended_op (possible_switch_to dest);
when call $ if x \<or> gr then setup_caller_cap t' dest reply_can_grant else set_thread_state t' Inactive
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epa list a lista. \<lbrakk>epa = RecvEP (a # lista); t \<noteq> t'; list = a # lista\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> do y <- set_endpoint ep (case lista of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> RecvEP lista);
recv_state <- get_thread_state a;
reply_can_grant <- case recv_state of BlockedOnReceive xa data \<Rightarrow> do do_ipc_transfer t' (Some ep) bdg x a;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
y <- set_thread_state a Running;
y <- do_extended_op (possible_switch_to a);
when call (if x \<or> gr then setup_caller_cap t' a reply_can_grant else set_thread_state t' Inactive)
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epa list a lista y. \<lbrakk>epa = RecvEP (a # lista); t \<noteq> t'; list = a # lista\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> do recv_state <- get_thread_state a;
reply_can_grant <- case recv_state of BlockedOnReceive xa data \<Rightarrow> do do_ipc_transfer t' (Some ep) bdg x a;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
y <- set_thread_state a Running;
y <- do_extended_op (possible_switch_to a);
when call (if x \<or> gr then setup_caller_cap t' a reply_can_grant else set_thread_state t' Inactive)
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epa list a lista y recv_state. \<lbrakk>epa = RecvEP (a # lista); t \<noteq> t'; list = a # lista\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at ((=) recv_state) a and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> do reply_can_grant <- case recv_state of BlockedOnReceive xa data \<Rightarrow> do do_ipc_transfer t' (Some ep) bdg x a;
return (receiver_can_grant data)
od | _ \<Rightarrow> fail;
y <- set_thread_state a Running;
y <- do_extended_op (possible_switch_to a);
when call (if x \<or> gr then setup_caller_cap t' a reply_can_grant else set_thread_state t' Inactive)
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epa list a lista recv_state x41 x42. \<lbrakk>epa = RecvEP (a # lista); t \<noteq> t'; list = a # lista; recv_state = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at ((=) (BlockedOnReceive x41 x42)) a and st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> do y <- do_ipc_transfer t' (Some ep) bdg x a;
y <- set_thread_state a Running;
y <- do_extended_op (possible_switch_to a);
when call (if x \<or> gr then setup_caller_cap t' a (receiver_can_grant x42) else set_thread_state t' Inactive)
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal:
No subgoals!