theory SyscallArgs_C

lemma replyOnRestart_invs'[wp]:
  "\<lbrace>invs'\<rbrace> replyOnRestart thread reply isCall \<lbrace>\<lambda>rv. invs'\<rbrace>" including no_pre apply (simp add: replyOnRestart_def) apply (wp setThreadState_nonqueued_state_update rfk_invs' hoare_weak_lift_imp) apply (rule hoare_vcg_all_lift) apply (wp setThreadState_nonqueued_state_update rfk_invs' hoare_vcg_all_lift rfk_ksQ) apply (rule hoare_strengthen_post, rule gts_sp') apply (clarsimp simp: pred_tcb_at') apply (auto elim!: pred_tcb'_weakenE st_tcb_ex_cap''
               dest: st_tcb_at_idle_thread') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> replyOnRestart thread reply isCall \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> replyOnRestart thread reply isCall \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do state <- getThreadState thread;
when (state = Structures_H.thread_state.Restart) (do _ <- when isCall (replyFromKernel thread (0, reply));
setThreadState Structures_H.thread_state.Running thread
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state. \<lbrakk>state = Structures_H.thread_state.Restart; isCall\<rbrakk> \<Longrightarrow> \<lbrace>?P'19 state\<rbrace> replyFromKernel thread (0, reply) \<lbrace>\<lambda>rv s. \<forall>p. thread \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<lbrace>invs'\<rbrace> getThreadState thread \<lbrace>\<lambda>state. if state = Structures_H.thread_state.Restart then if isCall then \<lambda>s. (invs' and tcb_at' thread) s \<and> st_tcb_at' simple' thread s \<and> Structures_H.thread_state.Running \<in> {Structures_H.thread_state.Inactive, Structures_H.thread_state.Running, Structures_H.thread_state.Restart, Structures_H.thread_state.IdleThreadState} \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' thread s) \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> ?P'19 state s) else (\<lambda>s. invs' s \<and> st_tcb_at' simple' thread s \<and> Structures_H.thread_state.Running \<in> {Structures_H.thread_state.Inactive, Structures_H.thread_state.Running, Structures_H.thread_state.Restart, Structures_H.thread_state.IdleThreadState} \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' thread s) \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> (\<forall>p. thread \<notin> set (ksReadyQueues s p)))) else invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state p. \<lbrakk>state = Structures_H.thread_state.Restart; isCall\<rbrakk> \<Longrightarrow> \<lbrace>?P20 state p\<rbrace> replyFromKernel thread (0, reply) \<lbrace>\<lambda>rv s. thread \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<lbrace>invs'\<rbrace> getThreadState thread \<lbrace>\<lambda>state. if state = Structures_H.thread_state.Restart then if isCall then \<lambda>s. (invs' and tcb_at' thread) s \<and> st_tcb_at' simple' thread s \<and> Structures_H.thread_state.Running \<in> {Structures_H.thread_state.Inactive, Structures_H.thread_state.Running, Structures_H.thread_state.Restart, Structures_H.thread_state.IdleThreadState} \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' thread s) \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> (\<forall>x. ?P20 state x s)) else (\<lambda>s. invs' s \<and> st_tcb_at' simple' thread s \<and> Structures_H.thread_state.Running \<in> {Structures_H.thread_state.Inactive, Structures_H.thread_state.Running, Structures_H.thread_state.Restart, Structures_H.thread_state.IdleThreadState} \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' thread s) \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> (\<forall>p. thread \<notin> set (ksReadyQueues s p)))) else invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> getThreadState thread \<lbrace>\<lambda>state. if state = Structures_H.thread_state.Restart then if isCall then \<lambda>s. (invs' and tcb_at' thread) s \<and> st_tcb_at' simple' thread s \<and> Structures_H.thread_state.Running \<in> {Structures_H.thread_state.Inactive, Structures_H.thread_state.Running, Structures_H.thread_state.Restart, Structures_H.thread_state.IdleThreadState} \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' thread s) \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> (\<forall>x. thread \<notin> set (ksReadyQueues s x))) else (\<lambda>s. invs' s \<and> st_tcb_at' simple' thread s \<and> Structures_H.thread_state.Running \<in> {Structures_H.thread_state.Inactive, Structures_H.thread_state.Running, Structures_H.thread_state.Restart, Structures_H.thread_state.IdleThreadState} \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' thread s) \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> (\<forall>p. thread \<notin> set (ksReadyQueues s p)))) else invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (st_tcb_at' (\<lambda>st. st = rv) thread and invs') s \<Longrightarrow> (if rv = Structures_H.thread_state.Restart then if isCall then \<lambda>s. (invs' and tcb_at' thread) s \<and> st_tcb_at' simple' thread s \<and> Structures_H.thread_state.Running \<in> {Structures_H.thread_state.Inactive, Structures_H.thread_state.Running, Structures_H.thread_state.Restart, Structures_H.thread_state.IdleThreadState} \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' thread s) \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> (\<forall>x. thread \<notin> set (ksReadyQueues s x))) else (\<lambda>s. invs' s \<and> st_tcb_at' simple' thread s \<and> Structures_H.thread_state.Running \<in> {Structures_H.thread_state.Inactive, Structures_H.thread_state.Running, Structures_H.thread_state.Restart, Structures_H.thread_state.IdleThreadState} \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' thread s) \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> (\<forall>p. thread \<notin> set (ksReadyQueues s p)))) else invs') s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Restart) thread s; invs' s\<rbrakk> \<Longrightarrow> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s proof (prove)
goal:
No subgoals!