theory Ipc_R

lemma hf_invs' [wp]:
  "\<lbrace>invs' and sch_act_not t
          and (\<lambda>s. \<forall>p. t \<notin> set(ksReadyQueues s p))
          and st_tcb_at' simple' t
          and ex_nonz_cap_to' t and (\<lambda>s. t \<noteq> ksIdleThread s)\<rbrace>
   handleFault t f \<lbrace>\<lambda>r. invs'\<rbrace>" apply (simp add: handleFault_def) apply wp apply (simp add: handleDoubleFault_def) apply (wp sts_invs_minor'' dmo_invs')+ apply (rule hoare_post_impErr, rule sfi_invs_plus',
         simp_all) apply (strengthen no_refs_simple_strg') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' t and ex_nonz_cap_to' t and (\<lambda>s. t \<noteq> ksIdleThread s)\<rbrace> handleFault t f \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' t and ex_nonz_cap_to' t and (\<lambda>s. t \<noteq> ksIdleThread s)\<rbrace> sendFaultIPC t f <catch> handleDoubleFault t f \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?E1 x\<rbrace> handleDoubleFault t f x \<lbrace>\<lambda>r. invs'\<rbrace>
 2. \<lbrace>?Q\<rbrace> sendFaultIPC t f \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>?E1\<rbrace>
 3. \<And>s. (invs' and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' t and ex_nonz_cap_to' t and (\<lambda>s. t \<noteq> ksIdleThread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?E1 x\<rbrace> do y <- setThreadState Structures_H.thread_state.Inactive t;
faultPC <- asUser t getRestartPC;
return ()
od \<lbrace>\<lambda>r. invs'\<rbrace>
 2. \<lbrace>?Q\<rbrace> sendFaultIPC t f \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>?E1\<rbrace>
 3. \<And>s. (invs' and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' t and ex_nonz_cap_to' t and (\<lambda>s. t \<noteq> ksIdleThread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> sendFaultIPC t f \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>x s. st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t s \<and> (t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) \<and> (runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> (\<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) \<and> invs' s \<and> tcb_at' t s\<rbrace>
 2. \<And>s. (invs' and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) and st_tcb_at' simple' t and ex_nonz_cap_to' t and (\<lambda>s. t \<noteq> ksIdleThread s)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> st_tcb_at' simple' t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not t s \<and> ksIdleThread s \<noteq> t \<Longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {}) t s \<and> t \<noteq> ksIdleThread s \<and> tcb_at' t s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> st_tcb_at' simple' t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not t s \<and> ksIdleThread s \<noteq> t \<Longrightarrow> (st_tcb_at' simple' t s \<and> {} = {}) \<and> t \<noteq> ksIdleThread s \<and> tcb_at' t s proof (prove)
goal:
No subgoals!