theory Ipc_R

lemma si_blk_makes_simple':
  "\<lbrace>st_tcb_at' simple' t and K (t \<noteq> t')\<rbrace>
     sendIPC True call bdg x x' t' ep
   \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>" apply (simp add: sendIPC_def) apply (rule hoare_seq_ext [OF _ get_ep_inv']) apply (case_tac xa, simp_all) apply (rename_tac list) apply (case_tac list, simp_all add: case_bool_If case_option_If
                             split del: if_split cong: if_cong) apply (rule hoare_pre) apply (wp sts_st_tcb_at'_cases setupCallerCap_pred_tcb_unchanged
               hoare_drop_imps) apply (clarsimp simp: pred_tcb_at' del: disjCI) apply (wp sts_st_tcb_at'_cases) apply clarsimp apply (wp sts_st_tcb_at'_cases) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' simple' t and K (t \<noteq> t')\<rbrace> sendIPC True call bdg x x' t' ep \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> getEndpoint ep >>= Structures_H.endpoint.case_endpoint (case_list (haskell_fail []) (\<lambda>dest queue. do setEndpoint ep $ case queue of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.RecvEP queue;
recvState <- getThreadState dest;
haskell_assert (isReceive recvState) [];
doIPCTransfer t' (Just ep) bdg x dest;
setThreadState Structures_H.thread_state.Running dest;
possibleSwitchTo dest;
case (call, x \<or> x') of (True, True) \<Rightarrow> setupCallerCap t' dest (blockingIPCCanGrant recvState) | (True, False) \<Rightarrow> setThreadState Structures_H.thread_state.Inactive t' | (False, xa) \<Rightarrow> return ()
od)) (do setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep $ Structures_H.endpoint.SendEP [t']
od) (\<lambda>queue. if True then do setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep $ Structures_H.endpoint.SendEP $ queue @ [t']
od else return ()) \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> case xa of Structures_H.endpoint.RecvEP [] \<Rightarrow> haskell_fail [] | Structures_H.endpoint.RecvEP (dest # queue) \<Rightarrow> do setEndpoint ep $ case queue of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.RecvEP queue;
recvState <- getThreadState dest;
haskell_assert (isReceive recvState) [];
doIPCTransfer t' (Just ep) bdg x dest;
setThreadState Structures_H.thread_state.Running dest;
possibleSwitchTo dest;
case (call, x \<or> x') of (True, True) \<Rightarrow> setupCallerCap t' dest (blockingIPCCanGrant recvState) | (True, False) \<Rightarrow> setThreadState Structures_H.thread_state.Inactive t' | (False, xa) \<Rightarrow> return ()
od | Structures_H.endpoint.IdleEP \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep $ Structures_H.endpoint.SendEP [t']
od | Structures_H.endpoint.SendEP queue \<Rightarrow> if True then do setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep $ Structures_H.endpoint.SendEP $ queue @ [t']
od else return () \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>xa x1. xa = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> case x1 of [] \<Rightarrow> haskell_fail [] | dest # queue \<Rightarrow> do setEndpoint ep $ case queue of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.RecvEP queue;
recvState <- getThreadState dest;
haskell_assert (isReceive recvState) [];
doIPCTransfer t' (Just ep) bdg x dest;
setThreadState Structures_H.thread_state.Running dest;
possibleSwitchTo dest;
case (call, x \<or> x') of (True, True) \<Rightarrow> setupCallerCap t' dest (blockingIPCCanGrant recvState) | (True, False) \<Rightarrow> setThreadState Structures_H.thread_state.Inactive t' | (False, xa) \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>
 2. \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP [t'])
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>
 3. \<And>xa x3. xa = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP (x3 @ [t']))
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>xa list. xa = Structures_H.endpoint.RecvEP list \<Longrightarrow> \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> case list of [] \<Rightarrow> haskell_fail [] | dest # queue \<Rightarrow> do setEndpoint ep $ case queue of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.RecvEP queue;
recvState <- getThreadState dest;
haskell_assert (isReceive recvState) [];
doIPCTransfer t' (Just ep) bdg x dest;
setThreadState Structures_H.thread_state.Running dest;
possibleSwitchTo dest;
case (call, x \<or> x') of (True, True) \<Rightarrow> setupCallerCap t' dest (blockingIPCCanGrant recvState) | (True, False) \<Rightarrow> setThreadState Structures_H.thread_state.Inactive t' | (False, xa) \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>
 2. \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP [t'])
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>
 3. \<And>xa x3. xa = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP (x3 @ [t']))
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>xa list a lista. \<lbrakk>xa = Structures_H.endpoint.RecvEP (a # lista); list = a # lista\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setEndpoint ep (case lista of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.RecvEP lista);
recvState <- getThreadState a;
y <- assert (isReceive recvState);
y <- doIPCTransfer t' (Some ep) bdg x a;
y <- setThreadState Structures_H.thread_state.Running a;
y <- possibleSwitchTo a;
if call then if x \<or> x' then setupCallerCap t' a (blockingIPCCanGrant recvState) else setThreadState Structures_H.thread_state.Inactive t' else return ()
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>
 2. \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP [t'])
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>
 3. \<And>xa x3. xa = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP (x3 @ [t']))
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>xa list a lista. \<lbrakk>xa = Structures_H.endpoint.RecvEP (a # lista); list = a # lista\<rbrakk> \<Longrightarrow> \<lbrace>?Q10 xa list a lista\<rbrace> do y <- setEndpoint ep (case lista of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.RecvEP lista);
recvState <- getThreadState a;
y <- assert (isReceive recvState);
y <- doIPCTransfer t' (Some ep) bdg x a;
y <- setThreadState Structures_H.thread_state.Running a;
y <- possibleSwitchTo a;
if call then if x \<or> x' then setupCallerCap t' a (blockingIPCCanGrant recvState) else setThreadState Structures_H.thread_state.Inactive t' else return ()
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>
 2. \<And>x list a lista s. \<lbrakk>x = Structures_H.endpoint.RecvEP (a # lista); list = a # lista; (st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')) s\<rbrakk> \<Longrightarrow> ?Q10 x list a lista s
 3. \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP [t'])
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>
 4. \<And>xa x3. xa = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP (x3 @ [t']))
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x list a lista s. \<lbrakk>x = Structures_H.endpoint.RecvEP (a # lista); list = a # lista; (st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')) s\<rbrakk> \<Longrightarrow> simple' Structures_H.thread_state.Running \<and> tcb_at' t s \<and> st_tcb_at' simple' t s \<and> K (t \<noteq> t') s \<and> simple' Structures_H.thread_state.Inactive \<and> tcb_at' t s \<and> simple' Structures_H.thread_state.Running \<and> tcb_at' t s \<and> st_tcb_at' simple' t s \<and> simple' Structures_H.thread_state.Running \<and> tcb_at' t s \<and> st_tcb_at' simple' t s
 2. \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP [t'])
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>
 3. \<And>xa x3. xa = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP (x3 @ [t']))
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP [t'])
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace>
 2. \<And>xa x3. xa = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP (x3 @ [t']))
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')) s \<Longrightarrow> (t' = t \<longrightarrow> simple' (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) \<and> tcb_at' t s) \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' simple' t s)
 2. \<And>xa x3. xa = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP (x3 @ [t']))
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>xa x3. xa = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- setThreadState (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) t';
setEndpoint ep (Structures_H.endpoint.SendEP (x3 @ [t']))
od \<lbrace>\<lambda>rv. st_tcb_at' simple' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>xa x3 s. \<lbrakk>xa = Structures_H.endpoint.SendEP x3; (st_tcb_at' simple' t and (\<lambda>y. t \<noteq> t')) s\<rbrakk> \<Longrightarrow> (t' = t \<longrightarrow> simple' (Structures_H.thread_state.BlockedOnSend ep bdg x x' call) \<and> tcb_at' t s) \<and> (t' \<noteq> t \<longrightarrow> st_tcb_at' simple' t s) proof (prove)
goal:
No subgoals!