theory Syscall_C

lemma handleFault_ccorres:
  "ccorres dc xfdc (invs' and st_tcb_at' simple' t and
        sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)))
      (UNIV \<inter> {s. (cfault_rel (Some flt) (seL4_Fault_lift(current_fault_' (globals s)))
                       (lookup_fault_lift(current_lookup_fault_' (globals s))) )}
            \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr t})
      [] (handleFault t flt)
         (Call handleFault_'proc)" apply (cinit lift: tptr_') apply (simp add: catch_def) apply (rule ccorres_symb_exec_r) apply (rule ccorres_split_nothrow_novcg_case_sum) apply (ctac (no_vcg) add: sendFaultIPC_ccorres) apply ceqv apply clarsimp apply (rule ccorres_cond_empty) apply (rule ccorres_return_Skip') apply clarsimp apply (rule ccorres_cond_univ) apply (ctac (no_vcg) add: handleDoubleFault_ccorres) apply (simp add: sendFaultIPC_def) apply wp apply ((wp hoare_vcg_all_lift_R hoare_drop_impE_R |wpc |simp add: throw_def)+)[1] apply clarsimp apply ((wp hoare_vcg_all_lift_R hoare_drop_impE_R |wpc |simp add: throw_def)+)[1] apply (wp) apply (simp add: guard_is_UNIV_def) apply (simp add: guard_is_UNIV_def) apply clarsimp apply vcg apply clarsimp apply (rule conseqPre, vcg) apply clarsimp apply (clarsimp simp: pred_tcb_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))) (UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>) [] (handleFault t flt) (Call handleFault_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Q115 tptr) (?Q'115 tptr) [SKIP] (sendFaultIPC t flt <catch> handleDoubleFault t flt) (\<acute>fault :== \<acute>current_fault;;
(\<acute>status :== CALL sendFaultIPC_'proc(tptr);;
IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleDoubleFault_'proc(tptr,\<acute>fault)
FI))
 2. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> ?Q115 tptr s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc (?Q115 (tcb_ptr_to_ctcb_ptr t)) (?Q'115 (tcb_ptr_to_ctcb_ptr t)) [SKIP] (sendFaultIPC t flt >>= case_sum (handleDoubleFault t flt) return) (\<acute>fault :== \<acute>current_fault;;
(\<acute>status :== CALL sendFaultIPC_'proc(tcb_ptr_to_ctcb_ptr t);;
IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleDoubleFault_'proc(tcb_ptr_to_ctcb_ptr t,\<acute>fault)
FI))
 2. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> ?Q115 tptr s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (4 subgoals):
 1. ccorres dc xfdc (?Q115 (tcb_ptr_to_ctcb_ptr t)) ?Q'127 [SKIP] (sendFaultIPC t flt >>= case_sum (handleDoubleFault t flt) return) (\<acute>status :== CALL sendFaultIPC_'proc(tcb_ptr_to_ctcb_ptr t);;
IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleDoubleFault_'proc(tcb_ptr_to_ctcb_ptr t,\<acute>fault)
FI)
 2. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault ?Q'127
 3. \<And>s. ?Q115 (tcb_ptr_to_ctcb_ptr t) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 4. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> ?Q115 tptr s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (10 subgoals):
 1. ccorres (?f'131 \<currency> ?r'131) (liftxf ?es131 ?ef'131 ?vf'131 ?xf'131) (?P135 (tcb_ptr_to_ctcb_ptr t)) ?Q'127 [] (sendFaultIPC t flt) (\<acute>status :== CALL sendFaultIPC_'proc(tcb_ptr_to_ctcb_ptr t))
 2. \<And>rv' ta t'. ceqv \<Gamma> ?xf'131 rv' ta t' (IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleDoubleFault_'proc(tcb_ptr_to_ctcb_ptr t,\<acute>fault)
FI) (?d'131 rv')
 3. \<And>rv rv'. \<lbrakk>?r'131 rv (?vf'131 rv'); ?ef'131 rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q131 rv) (?Q'131 rv rv') [SKIP] (return rv) (?d'131 rv')
 4. \<And>err rv' err'. \<lbrakk>?ef'131 rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; ?f'131 err (?ef'131 rv') err'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?QE131 err) (?Q''131 err rv' err') [SKIP] (handleDoubleFault t flt err) (?d'131 rv')
 5. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> sendFaultIPC t flt \<lbrace>?Q131\<rbrace>, \<lbrace>?QE131\<rbrace>
 6. guard_is_UNIV (\<lambda>rv rv'. ?r'131 rv (?vf'131 rv')) ?xf'131 (\<lambda>rv rv'. {s. ?ef'131 rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q'131 rv rv'})
 7. \<And>err. guard_is_UNIV (\<lambda>rv. ?f'131 err (?ef'131 rv)) ?es131 (\<lambda>rv rv'. {s. ?ef'131 (?xf'131 s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q''131 err rv rv'})
 8. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault ?Q'127
 9. \<And>s. (?P135 (tcb_ptr_to_ctcb_ptr t) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 10. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (?P135 tptr and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (9 subgoals):
 1. \<And>rv' ta t'. ceqv \<Gamma> status_' rv' ta t' (IF \<acute>status \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleDoubleFault_'proc(tcb_ptr_to_ctcb_ptr t,\<acute>fault)
FI) (?d'131 rv')
 2. \<And>rv rv'. \<lbrakk>dc rv (K () rv'); id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q131 rv) (?Q'131 rv rv') [SKIP] (return rv) (?d'131 rv')
 3. \<And>err rv' err'. \<lbrakk>id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cfault_rel2 err (id rv') err'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?QE131 err) (?Q''131 err rv' err') [SKIP] (handleDoubleFault t flt err) (?d'131 rv')
 4. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> sendFaultIPC t flt \<lbrace>?Q131\<rbrace>, \<lbrace>?QE131\<rbrace>
 5. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q'131 rv rv'})
 6. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q''131 err rv rv'})
 7. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 8. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 9. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (8 subgoals):
 1. \<And>rv rv'. \<lbrakk>dc rv (K () rv'); id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q131 rv) (?Q'131 rv rv') [SKIP] (return rv) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleDoubleFault_'proc(tcb_ptr_to_ctcb_ptr t,\<acute>fault)
FI)
 2. \<And>err rv' err'. \<lbrakk>id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cfault_rel2 err (id rv') err'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?QE131 err) (?Q''131 err rv' err') [SKIP] (handleDoubleFault t flt err) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleDoubleFault_'proc(tcb_ptr_to_ctcb_ptr t,\<acute>fault)
FI)
 3. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> sendFaultIPC t flt \<lbrace>?Q131\<rbrace>, \<lbrace>?QE131\<rbrace>
 4. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q'131 rv rv'})
 5. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q''131 err rv rv'})
 6. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 7. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 8. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (8 subgoals):
 1. ccorres dc xfdc (?Q131 ()) (?Q'131 () (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) [SKIP] (return ()) (Cond {} (CALL handleDoubleFault_'proc(tcb_ptr_to_ctcb_ptr t,\<acute>fault)) SKIP)
 2. \<And>err rv' err'. \<lbrakk>id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cfault_rel2 err (id rv') err'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?QE131 err) (?Q''131 err rv' err') [SKIP] (handleDoubleFault t flt err) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleDoubleFault_'proc(tcb_ptr_to_ctcb_ptr t,\<acute>fault)
FI)
 3. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> sendFaultIPC t flt \<lbrace>?Q131\<rbrace>, \<lbrace>?QE131\<rbrace>
 4. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q'131 rv rv'})
 5. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q''131 err rv rv'})
 6. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 7. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 8. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (8 subgoals):
 1. ccorres dc xfdc (?Q131 ()) (?Q'131 () (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) [SKIP] (return ()) SKIP
 2. \<And>err rv' err'. \<lbrakk>id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cfault_rel2 err (id rv') err'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?QE131 err) (?Q''131 err rv' err') [SKIP] (handleDoubleFault t flt err) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleDoubleFault_'proc(tcb_ptr_to_ctcb_ptr t,\<acute>fault)
FI)
 3. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> sendFaultIPC t flt \<lbrace>?Q131\<rbrace>, \<lbrace>?QE131\<rbrace>
 4. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q'131 rv rv'})
 5. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q''131 err rv rv'})
 6. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 7. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 8. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (7 subgoals):
 1. \<And>err rv' err'. \<lbrakk>id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cfault_rel2 err (id rv') err'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?QE131 err) (?Q''131 err rv' err') [SKIP] (handleDoubleFault t flt err) (IF rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE THEN
  CALL handleDoubleFault_'proc(tcb_ptr_to_ctcb_ptr t,\<acute>fault)
FI)
 2. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> sendFaultIPC t flt \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>?QE131\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)}})
 4. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q''131 err rv rv'})
 5. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 6. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 7. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (7 subgoals):
 1. \<And>err rv' err'. \<lbrakk>rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cfault_rel2 err rv' err'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?QE131 err) (?Q''131 err rv' err') [SKIP] (handleDoubleFault t flt err) (Cond UNIV (CALL handleDoubleFault_'proc(tcb_ptr_to_ctcb_ptr t,\<acute>fault)) SKIP)
 2. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> sendFaultIPC t flt \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>?QE131\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)}})
 4. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q''131 err rv rv'})
 5. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 6. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 7. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (7 subgoals):
 1. \<And>err rv' err'. \<lbrakk>rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cfault_rel2 err rv' err'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?QE131 err) (?Q''131 err rv' err') [SKIP] (handleDoubleFault t flt err) (CALL handleDoubleFault_'proc(tcb_ptr_to_ctcb_ptr t,\<acute>fault))
 2. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> sendFaultIPC t flt \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>?QE131\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)}})
 4. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> ?Q''131 err rv rv'})
 5. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 6. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 7. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (6 subgoals):
 1. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> sendFaultIPC t flt \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>err. invs' and tcb_at' t and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))\<rbrace>
 2. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)}})
 3. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> {s. ex1_'_update (\<lambda>_. fault_' s) (tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s) \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}})
 4. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 5. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 6. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (6 subgoals):
 1. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> doE handlerCPtr <- liftE (threadGet tcbFaultHandler t);
handlerCap <- capFaultOnFailure handlerCPtr False (lookupCap t handlerCPtr);
case handlerCap of capability.EndpointCap epptr x True xa canGrant canGrantReply \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just flt)) t;
sendIPC True True (capEPBadge handlerCap) canGrant True t (capEPPtr handlerCap)
od else throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap epptr x False xa canGrant canGrantReply \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault handlerCPtr False $ Fault_H.lookup_failure.MissingCapability 0
odE \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>err a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b)))\<rbrace>
 2. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)}})
 3. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> {s. ex1_'_update (\<lambda>_. fault_' s) (tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s) \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}})
 4. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 5. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 6. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (8 subgoals):
 1. \<And>x xa. \<lbrace>?B213 x xa\<rbrace> case xa of capability.EndpointCap epptr xb bool1 xaa canGrant canGrantReply \<Rightarrow> case bool1 of True \<Rightarrow> if canGrant \<or> canGrantReply then withoutFailure $ do threadSet (tcbFault_update (\<lambda>_. Just flt)) t;
sendIPC True True (capEPBadge xa) canGrant True t (capEPPtr xa)
od else throw $ Fault_H.fault.CapFault x False $ Fault_H.lookup_failure.MissingCapability 0 | False \<Rightarrow> throw $ Fault_H.fault.CapFault x False $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.fault.CapFault x False $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>err a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b)))\<rbrace>
 2. \<And>x. \<lbrace>?B211 x\<rbrace> capFaultOnFailure x False (lookupCap t x) \<lbrace>?B213 x\<rbrace>, \<lbrace>\<lambda>err a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b)))\<rbrace>
 3. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> liftE (threadGet tcbFaultHandler t) \<lbrace>?B211\<rbrace>, \<lbrace>\<lambda>err a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b)))\<rbrace>
 4. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)}})
 5. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> {s. ex1_'_update (\<lambda>_. fault_' s) (tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s) \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}})
 6. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 7. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 8. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrace>?B211 x\<rbrace> capFaultOnFailure x False (lookupCap t x) \<lbrace>\<lambda>xa s. (\<forall>x. xa = capability.ThreadCap x \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True) \<and> (xa = capability.NullCap \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True) \<and> (\<forall>x xb xc xd. xa = capability.NotificationCap x xb xc xd \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True) \<and> (\<forall>x. xa = capability.IRQHandlerCap x \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True) \<and> (\<forall>x xb xc xd xe xf. xa = capability.EndpointCap x xb xc xd xe xf \<longrightarrow> (xc = True \<longrightarrow> (xe \<or> xf \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True) \<and> (\<not> (xe \<or> xf) \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True)) \<and> (xc = False \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True)) \<and> (xa = capability.DomainCap \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True) \<and> (\<forall>x xb xc. xa = capability.Zombie x xb xc \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True) \<and> (\<forall>x. xa = capability.ArchObjectCap x \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True) \<and> (\<forall>x xb xc. xa = capability.ReplyCap x xb xc \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True) \<and> (\<forall>x xb xc xd. xa = capability.UntypedCap x xb xc xd \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True) \<and> (\<forall>x xb xc xd. xa = capability.CNodeCap x xb xc xd \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True) \<and> (xa = capability.IRQControlCap \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> True)\<rbrace>, \<lbrace>\<lambda>err a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b)))\<rbrace>
 2. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> liftE (threadGet tcbFaultHandler t) \<lbrace>?B211\<rbrace>, \<lbrace>\<lambda>err a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b)))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)}})
 4. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> {s. ex1_'_update (\<lambda>_. fault_' s) (tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s) \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}})
 5. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 6. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 7. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (7 subgoals):
 1. \<And>x. \<lbrace>?B211 x\<rbrace> capFaultOnFailure x False (lookupCap t x) \<lbrace>\<lambda>xa s. ((\<exists>x. xa = capability.ThreadCap x) \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) \<and> (xa = capability.NullCap \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) \<and> ((\<exists>x xb xc xd. xa = capability.NotificationCap x xb xc xd) \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) \<and> ((\<exists>x. xa = capability.IRQHandlerCap x) \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) \<and> (\<forall>x xb xc xd xe xf. xa = capability.EndpointCap x xb xc xd xe xf \<longrightarrow> (xc \<longrightarrow> \<not> xe \<and> \<not> xf \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) \<and> (\<not> xc \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))))) \<and> (xa = capability.DomainCap \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) \<and> ((\<exists>x xb xc. xa = capability.Zombie x xb xc) \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) \<and> ((\<exists>x. xa = capability.ArchObjectCap x) \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) \<and> ((\<exists>x xb xc. xa = capability.ReplyCap x xb xc) \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) \<and> ((\<exists>x xb xc xd. xa = capability.UntypedCap x xb xc xd) \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) \<and> ((\<exists>x xb xc xd. xa = capability.CNodeCap x xb xc xd) \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) \<and> (xa = capability.IRQControlCap \<longrightarrow> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))))\<rbrace>, \<lbrace>\<lambda>err a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b)))\<rbrace>
 2. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> liftE (threadGet tcbFaultHandler t) \<lbrace>?B211\<rbrace>, \<lbrace>\<lambda>err a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b)))\<rbrace>
 3. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)}})
 4. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> {s. ex1_'_update (\<lambda>_. fault_' s) (tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s) \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}})
 5. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 6. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 7. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (6 subgoals):
 1. \<lbrace>?R134 (tcb_ptr_to_ctcb_ptr t)\<rbrace> liftE (threadGet tcbFaultHandler t) \<lbrace>\<lambda>x s. invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> (invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> (invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> (invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> (invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> (invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> (invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> (invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> (invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> (invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))) \<and> invs' s \<and> tcb_at' t s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> sch_act_not t s \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa)))\<rbrace>, \<lbrace>\<lambda>err a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b)))\<rbrace>
 2. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)}})
 3. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> {s. ex1_'_update (\<lambda>_. fault_' s) (tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s) \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}})
 4. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 5. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 (tcb_ptr_to_ctcb_ptr t)) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 6. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and ?R134 tptr) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (5 subgoals):
 1. guard_is_UNIV (\<lambda>rv rv'. dc rv (K () rv')) status_' (\<lambda>rv rv'. {s. id rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> UNIV \<inter> {s. dc rv (xfdc s)}})
 2. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> {s. ex1_'_update (\<lambda>_. fault_' s) (tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s) \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}})
 3. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 4. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 5. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (4 subgoals):
 1. \<And>err. guard_is_UNIV (\<lambda>rv. cfault_rel2 err (id rv)) errstate (\<lambda>rv rv'. {s. id (status_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> s \<in> {s. ex1_'_update (\<lambda>_. fault_' s) (tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s) \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}})
 2. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 3. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 4. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (3 subgoals):
 1. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t) s \<in> UNIV \<inter> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace>}
 2. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 3. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (3 subgoals):
 1. \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t)) \<acute>fault :== \<acute>current_fault \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>
 2. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<Longrightarrow> \<Gamma>\<turnstile> (?Q'115 (tcb_ptr_to_ctcb_ptr t) \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 3. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<and> s' \<in> ?Q'115 tptr proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 2. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<and> s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at' simple' t s; invs' s; tcb_at' t s; weak_sch_act_wf (ksSchedulerAction s) s; sch_act_not t s; \<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (\<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>fault :== \<acute>current_fault {s'. (s, s') \<in> rf_sr}
 2. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<and> s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at' simple' t s; invs' s; tcb_at' t s; weak_sch_act_wf (ksSchedulerAction s) s; sch_act_not t s; \<forall>x xa. t \<notin> set (ksReadyQueues s (x, xa))\<rbrakk> \<Longrightarrow> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (s, fault_'_update (\<lambda>_. current_fault_' (globals sa)) sa) \<in> rf_sr}
 2. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<and> s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s; s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace>\<rbrakk> \<Longrightarrow> (invs' and st_tcb_at' simple' t and sch_act_not t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>a. invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>aa b. t \<notin> set (ksReadyQueues a (aa, b))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (\<forall>x xa xb xc xd xe. (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> (invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa)))) \<and> invs' a \<and> tcb_at' t a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> sch_act_not t a \<and> (\<forall>x xa. t \<notin> set (ksReadyQueues a (x, xa))))) s \<and> s' \<in> \<lbrace>cfault_rel (Some flt) (seL4_Fault_lift \<acute>current_fault) (lookup_fault_lift \<acute>current_lookup_fault)\<rbrace> proof (prove)
goal:
No subgoals!