theory Syscall_R

lemma doReplyTransfer_ct_not_ksQ:
  "\<lbrace> invs' and sch_act_simple
           and tcb_at' thread and tcb_at' word
           and ct_in_state' simple'
           and (\<lambda>s. ksCurThread s \<noteq> word)
           and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set(ksReadyQueues s p))\<rbrace>
   doReplyTransfer thread word callerSlot g
   \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set(ksReadyQueues s p)\<rbrace>" proof - have astct: "\<And>t p.
       \<lbrace>(\<lambda>s. ksCurThread s \<notin> set(ksReadyQueues s p) \<and> sch_act_sane s)
             and (\<lambda>s. ksCurThread s \<noteq> t)\<rbrace>
       possibleSwitchTo t \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set(ksReadyQueues s p)\<rbrace>" apply (rule hoare_weaken_pre) apply (wps possibleSwitchTo_ct') apply (wp possibleSwitchTo_ksQ') apply (clarsimp simp: sch_act_sane_def) done have stsct: "\<And>t st p.
       \<lbrace>(\<lambda>s. ksCurThread s \<notin> set(ksReadyQueues s p)) and sch_act_simple\<rbrace>
       setThreadState st t
       \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set(ksReadyQueues s p)\<rbrace>" apply (rule hoare_weaken_pre) apply (wps setThreadState_ct') apply (wp hoare_vcg_all_lift sts_ksQ) apply (clarsimp) done show ?thesis apply (simp add: doReplyTransfer_def) apply (wp, wpc) apply (wp astct stsct hoare_vcg_all_lift
                      cteDeleteOne_ct_not_ksQ hoare_drop_imp
                      hoare_lift_Pf2 [OF cteDeleteOne_sch_act_not cteDeleteOne_ct']
                      hoare_lift_Pf2 [OF doIPCTransfer_pred_tcb_at' doIPCTransfer_ct']
                      hoare_lift_Pf2 [OF doIPCTransfer_ksQ doIPCTransfer_ct']
                      hoare_lift_Pf2 [OF threadSet_ksQ threadSet_ct]
                      hoare_lift_Pf2 [OF handleFaultReply_ksQ handleFaultReply_ct']
                   | simp add: ct_in_state'_def)+ apply (fastforce simp: sch_act_simple_def sch_act_sane_def ct_in_state'_def)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' thread and tcb_at' word and ct_in_state' simple' and (\<lambda>s. ksCurThread s \<noteq> word) and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> doReplyTransfer thread word callerSlot g \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' thread and tcb_at' word and ct_in_state' simple' and (\<lambda>s. ksCurThread s \<noteq> word) and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> doReplyTransfer thread word callerSlot g \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t p. \<lbrace>(\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> sch_act_sane s) and (\<lambda>s. ksCurThread s \<noteq> t)\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t p. \<lbrace>?Q t p\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>t p s. ((\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> sch_act_sane s) and (\<lambda>s. ksCurThread s \<noteq> t)) s \<Longrightarrow> ?Q t p s proof (prove)
goal (2 subgoals):
 1. \<And>t p prev_s. \<lbrace>?P3 t p prev_s\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>rv s'. ksCurThread prev_s \<notin> set (ksReadyQueues s' p)\<rbrace>
 2. \<And>t p s. ((\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> sch_act_sane s) and (\<lambda>s. ksCurThread s \<noteq> t)) s \<Longrightarrow> ?P3 t p s s proof (prove)
goal (1 subgoal):
 1. \<And>t p s. ((\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p) \<and> sch_act_sane s) and (\<lambda>s. ksCurThread s \<noteq> t)) s \<Longrightarrow> ((\<lambda>sa. ksCurThread s \<notin> set (ksReadyQueues sa p) \<and> sch_act_not (ksCurThread s) sa) and K (ksCurThread s \<noteq> t)) s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>(\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s ?p) \<and> sch_act_sane s) and (\<lambda>s. ksCurThread s \<noteq> ?t)\<rbrace> possibleSwitchTo ?t \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s ?p)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' thread and tcb_at' word and ct_in_state' simple' and (\<lambda>s. ksCurThread s \<noteq> word) and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> doReplyTransfer thread word callerSlot g \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t st p. \<lbrace>(\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and sch_act_simple\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t st p. \<lbrace>?Q t st p\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>t st p s. ((\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and sch_act_simple) s \<Longrightarrow> ?Q t st p s proof (prove)
goal (2 subgoals):
 1. \<And>t st p prev_s. \<lbrace>?P3 t st p prev_s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv s'. ksCurThread prev_s \<notin> set (ksReadyQueues s' p)\<rbrace>
 2. \<And>t st p s. ((\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and sch_act_simple) s \<Longrightarrow> ?P3 t st p s s proof (prove)
goal (1 subgoal):
 1. \<And>t st p s. ((\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and sch_act_simple) s \<Longrightarrow> sch_act_simple s \<and> ksCurThread s \<notin> set (ksReadyQueues s p) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>(\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s ?p)) and sch_act_simple\<rbrace> setThreadState ?st ?t \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s ?p)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' thread and tcb_at' word and ct_in_state' simple' and (\<lambda>s. ksCurThread s \<noteq> word) and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> doReplyTransfer thread word callerSlot g \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' thread and tcb_at' word and ct_in_state' simple' and (\<lambda>s. ksCurThread s \<noteq> word) and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> doReplyTransfer thread word callerSlot g \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and tcb_at' thread and tcb_at' word and ct_in_state' simple' and (\<lambda>s. ksCurThread s \<noteq> word) and (\<lambda>s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b)))\<rbrace> do state <- getThreadState word;
y <- assert (isReply state);
mdbNode <- liftM cteMDBNode (getCTE callerSlot);
y <- assert (mdbPrev mdbNode \<noteq> nullPointer \<and> mdbNext mdbNode = nullPointer);
parentCap <- getSlotCap (mdbPrev mdbNode);
y <- assert (isReplyCap parentCap \<and> capReplyMaster parentCap);
threadGet tcbFault word >>= case_option (do y <- doIPCTransfer thread None 0 g word;
y <- cteDeleteOne callerSlot;
y <- setThreadState Structures_H.thread_state.Running word;
possibleSwitchTo word
od) (\<lambda>f. do y <- cteDeleteOne callerSlot;
tag <- getMessageInfo thread;
sendBuffer <- lookupIPCBuffer False thread;
mrs <- getMRs thread sendBuffer tag;
restart <- handleFaultReply f word (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) word;
if restart then do y <- setThreadState Structures_H.thread_state.Restart word;
possibleSwitchTo word
od else setThreadState Structures_H.thread_state.Inactive word
od)
od \<lbrace>\<lambda>rv s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>state y mdbNode ya parentCap yb x. x = None \<Longrightarrow> \<lbrace>?R22 state y mdbNode ya parentCap yb x\<rbrace> do y <- doIPCTransfer thread None 0 g word;
y <- cteDeleteOne callerSlot;
y <- setThreadState Structures_H.thread_state.Running word;
possibleSwitchTo word
od \<lbrace>\<lambda>rv s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))\<rbrace>
 2. \<And>state y mdbNode ya parentCap yb x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R23 state y mdbNode ya parentCap yb x x2\<rbrace> do y <- cteDeleteOne callerSlot;
tag <- getMessageInfo thread;
sendBuffer <- lookupIPCBuffer False thread;
mrs <- getMRs thread sendBuffer tag;
restart <- handleFaultReply x2 word (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) word;
if restart then do y <- setThreadState Structures_H.thread_state.Restart word;
possibleSwitchTo word
od else setThreadState Structures_H.thread_state.Inactive word
od \<lbrace>\<lambda>rv s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))\<rbrace>
 3. \<And>state y mdbNode ya parentCap yb. \<lbrace>?B12 state y mdbNode ya parentCap yb\<rbrace> threadGet tcbFault word \<lbrace>\<lambda>x s. (x = None \<longrightarrow> ?R22 state y mdbNode ya parentCap yb x s) \<and> (\<forall>xa. x = Some xa \<longrightarrow> ?R23 state y mdbNode ya parentCap yb x xa s)\<rbrace>
 4. \<And>state y mdbNode ya parentCap. \<lbrace>?B11 state y mdbNode ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B12 state y mdbNode ya parentCap\<rbrace>
 5. \<And>state y mdbNode ya. \<lbrace>?B10 state y mdbNode ya\<rbrace> getSlotCap (mdbPrev mdbNode) \<lbrace>?B11 state y mdbNode ya\<rbrace>
 6. \<And>state y mdbNode. \<lbrace>?B9 state y mdbNode\<rbrace> assert (mdbPrev mdbNode \<noteq> nullPointer \<and> mdbNext mdbNode = nullPointer) \<lbrace>?B10 state y mdbNode\<rbrace>
 7. \<And>state y. \<lbrace>?B8 state y\<rbrace> liftM cteMDBNode (getCTE callerSlot) \<lbrace>?B9 state y\<rbrace>
 8. \<And>state. \<lbrace>?B7 state\<rbrace> assert (isReply state) \<lbrace>?B8 state\<rbrace>
 9. \<lbrace>?Q6\<rbrace> getThreadState word \<lbrace>?B7\<rbrace>
 10. \<And>s. (invs' and sch_act_simple and tcb_at' thread and tcb_at' word and ct_in_state' simple' and (\<lambda>s. ksCurThread s \<noteq> word) and (\<lambda>s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b)))) s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> sch_act_simple s \<and> tcb_at' thread s \<and> tcb_at' word s \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ksCurThread s \<noteq> word \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<Longrightarrow> sch_act_sane s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>invs' and sch_act_simple and tcb_at' thread and tcb_at' word and ct_in_state' simple' and (\<lambda>s. ksCurThread s \<noteq> word) and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> doReplyTransfer thread word callerSlot g \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>

goal:
No subgoals!