theory Tcb_R

lemma invokeTCB_WriteRegisters_corres:
  "corres (dc \<oplus> (=)) (einvs  and tcb_at dest and ex_nonz_cap_to dest)
        (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest)
        (invoke_tcb (tcb_invocation.WriteRegisters dest resume values arch))
        (invokeTCB (tcbinvocation.WriteRegisters dest resume values arch'))" apply (simp add: invokeTCB_def performTransfer_def arch_get_sanitise_register_info_def
                   frameRegisters_def gpRegisters_def getSanitiseRegisterInfo_def
                   sanitiseRegister_def sanitise_register_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getCurThread_corres]) apply (rule corres_split_nor) apply (rule asUser_corres) apply (simp add: zipWithM_mapM getRestartPC_def setNextPC_def) apply (rule corres_Id, simp+) apply (wpsimp wp: no_fail_mapM no_fail_setRegister)+ apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]]) apply (rule corres_split_nor[OF corres_when[OF refl restart_corres]]) apply (rule corres_split_nor[OF corres_when[OF refl rescheduleRequired_corres]]) apply (rule_tac P=\<top> and P'=\<top> in corres_inst) apply simp apply (wp+)[2] apply ((wp hoare_weak_lift_imp restart_invs'
                 | strengthen valid_sched_weak_strg einvs_valid_etcbs
                              invs_valid_queues' invs_queues invs_weak_sch_act_wf
                 | clarsimp simp: invs_def valid_state_def valid_sched_def invs'_def valid_state'_def
                            dest!: global'_no_ex_cap idle_no_ex_cap)+)[2] apply (rule_tac Q="\<lambda>_. einvs and tcb_at dest and ex_nonz_cap_to dest" in hoare_strengthen_post[rotated]) apply (fastforce simp: invs_def valid_sched_weak_strg valid_sched_def valid_state_def dest!: idle_no_ex_cap) prefer 2 apply (rule_tac Q="\<lambda>_. invs' and tcb_at' dest and ex_nonz_cap_to' dest" in hoare_strengthen_post[rotated]) apply (fastforce simp: sch_act_wf_weak invs'_def valid_state'_def dest!: global'_no_ex_cap) apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> (=)) (einvs and tcb_at dest and ex_nonz_cap_to dest) (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) (invoke_tcb (tcb_invocation.WriteRegisters dest resume values arch)) (invokeTCB (tcbinvocation.WriteRegisters dest resume values arch')) proof (prove)
goal (1 subgoal):
 1. corres (=) (einvs and tcb_at dest and ex_nonz_cap_to dest) (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) (do self <- gets cur_thread;
y <- as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od);
y <- arch_post_modify_registers self dest;
y <- when resume (Tcb_A.restart dest);
y <- when (dest = self) reschedule_required;
return []
od) (do self <- getCurThread;
y <- asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od);
y <- asUser dest (postModifyRegisters self dest);
y <- when resume (ThreadDecls_H.restart dest);
y <- when (dest = self) rescheduleRequired;
return []
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q1 ?Q'1 (do self <- gets cur_thread;
y <- as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od);
y <- arch_post_modify_registers self dest;
y <- when resume (Tcb_A.restart dest);
y <- when (dest = self) reschedule_required;
return []
od) (do self <- getCurThread;
y <- asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od);
y <- asUser dest (postModifyRegisters self dest);
y <- when resume (ThreadDecls_H.restart dest);
y <- when (dest = self) rescheduleRequired;
return []
od)
 2. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ?Q1 s
 3. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ?Q'1 s proof (prove)
goal (5 subgoals):
 1. \<And>self selfa. self = selfa \<Longrightarrow> corres (=) (?R5 self) (?R'5 selfa) (do y <- as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od);
y <- arch_post_modify_registers self dest;
y <- when resume (Tcb_A.restart dest);
y <- when (dest = self) reschedule_required;
return []
od) (do y <- asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od);
y <- asUser dest (postModifyRegisters selfa dest);
y <- when resume (ThreadDecls_H.restart dest);
y <- when (dest = selfa) rescheduleRequired;
return []
od)
 2. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>?R5\<rbrace>
 3. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>?R'5\<rbrace>
 4. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>self selfa. self = selfa \<Longrightarrow> corres dc (?P10 self) (?P'12 selfa) (as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od)) (asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od))
 2. \<And>self selfa. self = selfa \<Longrightarrow> corres (=) (?R9 self selfa) (?R'9 self selfa) (do y <- arch_post_modify_registers self dest;
y <- when resume (Tcb_A.restart dest);
y <- when (dest = self) reschedule_required;
return []
od) (do y <- asUser dest (postModifyRegisters selfa dest);
y <- when resume (ThreadDecls_H.restart dest);
y <- when (dest = selfa) rescheduleRequired;
return []
od)
 3. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. ?R9 self selfa\<rbrace>
 4. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. ?R'9 self selfa\<rbrace>
 5. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. ?P10 self and ?Q11 self\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. ?P'12 selfa and ?Q'13 selfa\<rbrace>
 7. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 8. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>self selfa. self = selfa \<Longrightarrow> corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od)
 2. \<And>self selfa. self = selfa \<Longrightarrow> corres (=) (?R9 self selfa) (?R'9 self selfa) (do y <- arch_post_modify_registers self dest;
y <- when resume (Tcb_A.restart dest);
y <- when (dest = self) reschedule_required;
return []
od) (do y <- asUser dest (postModifyRegisters selfa dest);
y <- when resume (ThreadDecls_H.restart dest);
y <- when (dest = selfa) rescheduleRequired;
return []
od)
 3. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. ?R9 self selfa\<rbrace>
 4. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. ?R'9 self selfa\<rbrace>
 5. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 7. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 8. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (do y <- mapM (\<lambda>(r, v). setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (zip (MachineExports.frameRegisters @ MachineExports.gpRegisters) values);
getRegister FaultIP >>= setRegister NextIP
od) (do y <- mapM (\<lambda>(r, v). setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (zip (MachineExports.frameRegisters @ MachineExports.gpRegisters) values);
getRegister FaultIP >>= setRegister NextIP
od)
 2. \<And>self selfa. self = selfa \<Longrightarrow> corres (=) (?R9 self selfa) (?R'9 self selfa) (do y <- arch_post_modify_registers self dest;
y <- when resume (Tcb_A.restart dest);
y <- when (dest = self) reschedule_required;
return []
od) (do y <- asUser dest (postModifyRegisters selfa dest);
y <- when resume (ThreadDecls_H.restart dest);
y <- when (dest = selfa) rescheduleRequired;
return []
od)
 3. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. ?R9 self selfa\<rbrace>
 4. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. ?R'9 self selfa\<rbrace>
 5. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 7. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 8. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. no_fail (\<lambda>_. True) (do y <- mapM (\<lambda>(r, v). setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (zip (MachineExports.frameRegisters @ MachineExports.gpRegisters) values);
getRegister FaultIP >>= setRegister NextIP
od)
 2. \<And>self selfa. self = selfa \<Longrightarrow> corres (=) (?R9 self selfa) (?R'9 self selfa) (do y <- arch_post_modify_registers self dest;
y <- when resume (Tcb_A.restart dest);
y <- when (dest = self) reschedule_required;
return []
od) (do y <- asUser dest (postModifyRegisters selfa dest);
y <- when resume (ThreadDecls_H.restart dest);
y <- when (dest = selfa) rescheduleRequired;
return []
od)
 3. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. ?R9 self selfa\<rbrace>
 4. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. ?R'9 self selfa\<rbrace>
 5. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 7. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 8. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (7 subgoals):
 1. \<And>self. corres (=) (?R9 self self) (?R'9 self self) (do y <- arch_post_modify_registers self dest;
y <- when resume (Tcb_A.restart dest);
y <- when (dest = self) reschedule_required;
return []
od) (do y <- asUser dest (postModifyRegisters self dest);
y <- when resume (ThreadDecls_H.restart dest);
y <- when (dest = self) rescheduleRequired;
return []
od)
 2. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. ?R9 self selfa\<rbrace>
 3. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. ?R'9 self selfa\<rbrace>
 4. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 5. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 6. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 7. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>self. corres (=) (?R49 self) (?R'49 self) (do y <- when resume (Tcb_A.restart dest);
y <- when (dest = self) reschedule_required;
return []
od) (do y <- when resume (ThreadDecls_H.restart dest);
y <- when (dest = self) rescheduleRequired;
return []
od)
 2. \<And>self. \<lbrace>?Q54 self self\<rbrace> arch_post_modify_registers self dest \<lbrace>\<lambda>x. ?R49 self\<rbrace>
 3. \<And>self. \<lbrace>?Q'53 self self\<rbrace> asUser dest (postModifyRegisters self dest) \<lbrace>\<lambda>x. ?R'49 self\<rbrace>
 4. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q54 self selfa\<rbrace>
 5. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. tcb_at' dest and ?Q'53 self selfa\<rbrace>
 6. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 7. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 8. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 9. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (11 subgoals):
 1. \<And>self. corres (=) (?R58 self) (?R'58 self) (do y <- when (dest = self) reschedule_required;
return []
od) (do y <- when (dest = self) rescheduleRequired;
return []
od)
 2. \<And>self. \<lbrace>?Q58 self\<rbrace> when resume (Tcb_A.restart dest) \<lbrace>\<lambda>x. ?R58 self\<rbrace>
 3. \<And>self. \<lbrace>?Q'58 self\<rbrace> when resume (ThreadDecls_H.restart dest) \<lbrace>\<lambda>x. ?R'58 self\<rbrace>
 4. \<And>self. \<lbrace>?Q54 self self\<rbrace> arch_post_modify_registers self dest \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (einvs and tcb_at dest) x) and ?Q58 self\<rbrace>
 5. \<And>self. \<lbrace>?Q'53 self self\<rbrace> asUser dest (postModifyRegisters self dest) \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (invs' and tcb_at' dest) x) and ?Q'58 self\<rbrace>
 6. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q54 self selfa\<rbrace>
 7. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. tcb_at' dest and ?Q'53 self selfa\<rbrace>
 8. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 9. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 10. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>self. corres (=) (?R65 self) (?R'65 self) (return []) (return [])
 2. \<And>self. \<lbrace>?Q65 self\<rbrace> when (dest = self) reschedule_required \<lbrace>\<lambda>x. ?R65 self\<rbrace>
 3. \<And>self. \<lbrace>?Q'65 self\<rbrace> when (dest = self) rescheduleRequired \<lbrace>\<lambda>x. ?R'65 self\<rbrace>
 4. \<And>self. \<lbrace>?Q58 self\<rbrace> when resume (Tcb_A.restart dest) \<lbrace>\<lambda>x. (\<lambda>x. dest = self \<longrightarrow> (weak_valid_sched_action and valid_etcbs) x) and ?Q65 self\<rbrace>
 5. \<And>self. \<lbrace>?Q'58 self\<rbrace> when resume (ThreadDecls_H.restart dest) \<lbrace>\<lambda>x. (\<lambda>x. dest = self \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) x) and ?Q'65 self\<rbrace>
 6. \<And>self. \<lbrace>?Q54 self self\<rbrace> arch_post_modify_registers self dest \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (einvs and tcb_at dest) x) and ?Q58 self\<rbrace>
 7. \<And>self. \<lbrace>?Q'53 self self\<rbrace> asUser dest (postModifyRegisters self dest) \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (invs' and tcb_at' dest) x) and ?Q'58 self\<rbrace>
 8. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q54 self selfa\<rbrace>
 9. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. tcb_at' dest and ?Q'53 self selfa\<rbrace>
 10. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>self. corres (=) (\<lambda>_. True) (\<lambda>_. True) (return []) (return [])
 2. \<And>self. \<lbrace>?Q65 self\<rbrace> when (dest = self) reschedule_required \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>self. \<lbrace>?Q'65 self\<rbrace> when (dest = self) rescheduleRequired \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>self. \<lbrace>?Q58 self\<rbrace> when resume (Tcb_A.restart dest) \<lbrace>\<lambda>x. (\<lambda>x. dest = self \<longrightarrow> (weak_valid_sched_action and valid_etcbs) x) and ?Q65 self\<rbrace>
 5. \<And>self. \<lbrace>?Q'58 self\<rbrace> when resume (ThreadDecls_H.restart dest) \<lbrace>\<lambda>x. (\<lambda>x. dest = self \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) x) and ?Q'65 self\<rbrace>
 6. \<And>self. \<lbrace>?Q54 self self\<rbrace> arch_post_modify_registers self dest \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (einvs and tcb_at dest) x) and ?Q58 self\<rbrace>
 7. \<And>self. \<lbrace>?Q'53 self self\<rbrace> asUser dest (postModifyRegisters self dest) \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (invs' and tcb_at' dest) x) and ?Q'58 self\<rbrace>
 8. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q54 self selfa\<rbrace>
 9. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. tcb_at' dest and ?Q'53 self selfa\<rbrace>
 10. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>self. \<lbrace>?Q65 self\<rbrace> when (dest = self) reschedule_required \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>self. \<lbrace>?Q'65 self\<rbrace> when (dest = self) rescheduleRequired \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>self. \<lbrace>?Q58 self\<rbrace> when resume (Tcb_A.restart dest) \<lbrace>\<lambda>x. (\<lambda>x. dest = self \<longrightarrow> (weak_valid_sched_action and valid_etcbs) x) and ?Q65 self\<rbrace>
 4. \<And>self. \<lbrace>?Q'58 self\<rbrace> when resume (ThreadDecls_H.restart dest) \<lbrace>\<lambda>x. (\<lambda>x. dest = self \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) x) and ?Q'65 self\<rbrace>
 5. \<And>self. \<lbrace>?Q54 self self\<rbrace> arch_post_modify_registers self dest \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (einvs and tcb_at dest) x) and ?Q58 self\<rbrace>
 6. \<And>self. \<lbrace>?Q'53 self self\<rbrace> asUser dest (postModifyRegisters self dest) \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (invs' and tcb_at' dest) x) and ?Q'58 self\<rbrace>
 7. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q54 self selfa\<rbrace>
 8. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. tcb_at' dest and ?Q'53 self selfa\<rbrace>
 9. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 10. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
A total of 12 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>self. \<lbrace>?Q58 self\<rbrace> when resume (Tcb_A.restart dest) \<lbrace>\<lambda>x. (\<lambda>x. dest = self \<longrightarrow> (weak_valid_sched_action and valid_etcbs) x) and (\<lambda>_. True)\<rbrace>
 2. \<And>self. \<lbrace>?Q'58 self\<rbrace> when resume (ThreadDecls_H.restart dest) \<lbrace>\<lambda>x. (\<lambda>x. dest = self \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) x) and (\<lambda>_. True)\<rbrace>
 3. \<And>self. \<lbrace>?Q54 self self\<rbrace> arch_post_modify_registers self dest \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (einvs and tcb_at dest) x) and ?Q58 self\<rbrace>
 4. \<And>self. \<lbrace>?Q'53 self self\<rbrace> asUser dest (postModifyRegisters self dest) \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (invs' and tcb_at' dest) x) and ?Q'58 self\<rbrace>
 5. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q54 self selfa\<rbrace>
 6. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. tcb_at' dest and ?Q'53 self selfa\<rbrace>
 7. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 8. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 9. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 10. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>self. \<lbrace>?Q54 self self\<rbrace> arch_post_modify_registers self dest \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (einvs and tcb_at dest) x) and (\<lambda>s. (dest = self \<longrightarrow> (if resume then \<lambda>s. (valid_sched and (\<lambda>s. dest \<noteq> idle_thread s)) s \<and> (invs and tcb_at dest and ex_nonz_cap_to dest) s \<and> valid_list s \<and> (valid_sched and (\<lambda>s. dest \<noteq> idle_thread s)) s else (\<lambda>s. weak_valid_sched_action s \<and> valid_etcbs s)) s) \<and> True)\<rbrace>
 2. \<And>self. \<lbrace>?Q'53 self self\<rbrace> asUser dest (postModifyRegisters self dest) \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (invs' and tcb_at' dest) x) and (\<lambda>s. (dest = self \<longrightarrow> (if resume then \<lambda>s. (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s \<and> (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s \<and> (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s else (\<lambda>s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)) s) \<and> True)\<rbrace>
 3. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q54 self selfa\<rbrace>
 4. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. tcb_at' dest and ?Q'53 self selfa\<rbrace>
 5. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 7. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 8. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>self rv s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>x. resume \<longrightarrow> (einvs and tcb_at dest) x) and (\<lambda>s. (dest = self \<longrightarrow> (if resume then \<lambda>s. (valid_sched and (\<lambda>s. dest \<noteq> idle_thread s)) s \<and> (invs and tcb_at dest and ex_nonz_cap_to dest) s \<and> valid_list s \<and> (valid_sched and (\<lambda>s. dest \<noteq> idle_thread s)) s else (\<lambda>s. weak_valid_sched_action s \<and> valid_etcbs s)) s) \<and> True)) s
 2. \<And>self. \<lbrace>?Q54 self self\<rbrace> arch_post_modify_registers self dest \<lbrace>\<lambda>_. einvs and tcb_at dest and ex_nonz_cap_to dest\<rbrace>
 3. \<And>self. \<lbrace>?Q'53 self self\<rbrace> asUser dest (postModifyRegisters self dest) \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (invs' and tcb_at' dest) x) and (\<lambda>s. (dest = self \<longrightarrow> (if resume then \<lambda>s. (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s \<and> (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s \<and> (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s else (\<lambda>s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)) s) \<and> True)\<rbrace>
 4. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q54 self selfa\<rbrace>
 5. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. tcb_at' dest and ?Q'53 self selfa\<rbrace>
 6. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 7. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 8. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 9. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>self. \<lbrace>?Q54 self self\<rbrace> arch_post_modify_registers self dest \<lbrace>\<lambda>_. einvs and tcb_at dest and ex_nonz_cap_to dest\<rbrace>
 2. \<And>self. \<lbrace>?Q'53 self self\<rbrace> asUser dest (postModifyRegisters self dest) \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (invs' and tcb_at' dest) x) and (\<lambda>s. (dest = self \<longrightarrow> (if resume then \<lambda>s. (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s \<and> (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s \<and> (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s else (\<lambda>s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)) s) \<and> True)\<rbrace>
 3. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q54 self selfa\<rbrace>
 4. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. tcb_at' dest and ?Q'53 self selfa\<rbrace>
 5. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 7. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 8. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>self. \<lbrace>?Q'53 self self\<rbrace> asUser dest (postModifyRegisters self dest) \<lbrace>\<lambda>x. (\<lambda>x. resume \<longrightarrow> (invs' and tcb_at' dest) x) and (\<lambda>s. (dest = self \<longrightarrow> (if resume then \<lambda>s. (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s \<and> (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s \<and> (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s else (\<lambda>s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)) s) \<and> True)\<rbrace>
 2. \<And>self. \<lbrace>?Q54 self self\<rbrace> arch_post_modify_registers self dest \<lbrace>\<lambda>_. einvs and tcb_at dest and ex_nonz_cap_to dest\<rbrace>
 3. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q54 self selfa\<rbrace>
 4. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. tcb_at' dest and ?Q'53 self selfa\<rbrace>
 5. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 7. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 8. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (9 subgoals):
 1. \<And>self rv s. (invs' and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>x. resume \<longrightarrow> (invs' and tcb_at' dest) x) and (\<lambda>s. (dest = self \<longrightarrow> (if resume then \<lambda>s. (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s \<and> (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s \<and> (invs' and ex_nonz_cap_to' dest and (\<lambda>s. dest \<noteq> ksIdleThread s)) s else (\<lambda>s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)) s) \<and> True)) s
 2. \<And>self. \<lbrace>?Q'53 self self\<rbrace> asUser dest (postModifyRegisters self dest) \<lbrace>\<lambda>_. invs' and tcb_at' dest and ex_nonz_cap_to' dest\<rbrace>
 3. \<And>self. \<lbrace>?Q54 self self\<rbrace> arch_post_modify_registers self dest \<lbrace>\<lambda>_. einvs and tcb_at dest and ex_nonz_cap_to dest\<rbrace>
 4. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q54 self selfa\<rbrace>
 5. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. tcb_at' dest and ?Q'53 self selfa\<rbrace>
 6. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 7. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 8. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 9. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal (8 subgoals):
 1. \<And>self. \<lbrace>?Q'53 self self\<rbrace> asUser dest (postModifyRegisters self dest) \<lbrace>\<lambda>_. invs' and tcb_at' dest and ex_nonz_cap_to' dest\<rbrace>
 2. \<And>self. \<lbrace>?Q54 self self\<rbrace> arch_post_modify_registers self dest \<lbrace>\<lambda>_. einvs and tcb_at dest and ex_nonz_cap_to dest\<rbrace>
 3. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q11 self\<rbrace> as_user dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. (\<lambda>_. True) and ?Q54 self selfa\<rbrace>
 4. \<And>self selfa. self = selfa \<Longrightarrow> \<lbrace>?Q'13 selfa\<rbrace> asUser dest (do y <- zipWithM (\<lambda>r v. setRegister r (case r of CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v)) (MachineExports.frameRegisters @ MachineExports.gpRegisters) values;
getRestartPC >>= setNextPC
od) \<lbrace>\<lambda>x. tcb_at' dest and ?Q'53 self selfa\<rbrace>
 5. \<lbrace>?Q5\<rbrace> gets cur_thread \<lbrace>\<lambda>self. tcb_at dest and invs and ?Q11 self\<rbrace>
 6. \<lbrace>?Q'5\<rbrace> getCurThread \<lbrace>\<lambda>selfa. tcb_at' dest and invs' and ?Q'13 selfa\<rbrace>
 7. \<And>s. (einvs and tcb_at dest and ex_nonz_cap_to dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 8. \<And>s. (invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s proof (prove)
goal:
No subgoals!