theory Tcb_DR

lemma invoke_tcb_corres_setTLSBase:
  "\<lbrakk> t' = tcb_invocation.SetTLSBase obj_id' tls_base;
     t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
   dcorres (dc \<oplus> dc) \<top> (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs)
  (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')" apply (clarsimp simp: Tcb_D.invoke_tcb_def translate_tcb_invocation_def) apply (rule corres_dummy_return_l) apply (rule corres_guard_imp) apply (rule corres_split[where r'=dc]) apply (rule corrupt_tcb_intent_as_user_corres) apply (rule corres_symb_exec_r) apply (rule corres_split_noop_rhs[OF corres_trivial]) apply simp apply (clarsimp simp: when_def) apply (rule reschedule_required_dcorres[THEN corres_trivial]) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = translate_tcb_invocation t'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (corrupt_tcb_intent obj_id') (do y <- as_user obj_id' (setRegister tlsBaseRegister tls_base);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) (corrupt_tcb_intent obj_id' >>= return) (do y <- as_user obj_id' (setRegister tlsBaseRegister tls_base);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> dcorres dc ?Q3 ?Q'3 (corrupt_tcb_intent obj_id' >>= return) (do y <- as_user obj_id' (setRegister tlsBaseRegister tls_base);
cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 2. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; True\<rbrakk> \<Longrightarrow> ?Q3 s
 3. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> ?Q'3 s proof (prove)
goal (6 subgoals):
 1. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> dcorres dc ?P7 ?P'7 (corrupt_tcb_intent obj_id') (as_user obj_id' (setRegister tlsBaseRegister tls_base))
 2. \<And>x y. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R7 x) (?R'7 y) (return x) (do cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 3. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R7\<rbrace>
 4. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> as_user obj_id' (setRegister tlsBaseRegister tls_base) \<lbrace>?R'7\<rbrace>
 5. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; True\<rbrakk> \<Longrightarrow> (?P7 and ?Q7) s
 6. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (?P'7 and ?Q'7) s proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R7 x) (?R'7 y) (return x) (do cur <- gets cur_thread;
y <- when (obj_id' = cur) reschedule_required;
return []
od)
 2. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R7\<rbrace>
 3. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> as_user obj_id' (setRegister tlsBaseRegister tls_base) \<lbrace>?R'7\<rbrace>
 4. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 5. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id' and valid_etcbs and ?Q'7) s proof (prove)
goal (8 subgoals):
 1. \<And>x y cur. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R7 x) (?Q'13 x y cur) (return x) (do y <- when (obj_id' = cur) reschedule_required;
return []
od)
 2. \<And>x y. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?R'7 y\<rbrace> gets cur_thread \<lbrace>?Q'13 x y\<rbrace>
 3. \<And>x y s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y; ?R'7 y s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>x y. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y; False\<rbrakk> \<Longrightarrow> no_fail (?R'7 y) (gets cur_thread)
 5. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>?R7\<rbrace>
 6. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> as_user obj_id' (setRegister tlsBaseRegister tls_base) \<lbrace>?R'7\<rbrace>
 7. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 8. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id' and valid_etcbs and ?Q'7) s proof (prove)
goal (10 subgoals):
 1. \<And>x y cur. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (when (obj_id' = cur) reschedule_required)
 2. \<And>x y cur. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R20 x) (?R'18 x y cur) (return x) (return [])
 3. \<And>x y cur. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 x y cur\<rbrace> when (obj_id' = cur) reschedule_required \<lbrace>\<lambda>xa. ?R'18 x y cur\<rbrace>
 4. \<And>x y. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?R'7 y\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. (\<lambda>_. True) and ?Q'18 x y cur\<rbrace>
 5. \<And>x y s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y; ?R'7 y s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>x y. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y; False\<rbrakk> \<Longrightarrow> no_fail (?R'7 y) (gets cur_thread)
 7. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R20 x\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> as_user obj_id' (setRegister tlsBaseRegister tls_base) \<lbrace>?R'7\<rbrace>
 9. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 10. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id' and valid_etcbs and ?Q'7) s proof (prove)
goal (10 subgoals):
 1. \<And>cur. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (when (obj_id' = cur) reschedule_required)
 2. \<And>x y cur. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R20 x) (?R'18 x y cur) (return x) (return [])
 3. \<And>x y cur. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 x y cur\<rbrace> when (obj_id' = cur) reschedule_required \<lbrace>\<lambda>xa. ?R'18 x y cur\<rbrace>
 4. \<And>x y. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?R'7 y\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. (\<lambda>_. True) and ?Q'18 x y cur\<rbrace>
 5. \<And>x y s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y; ?R'7 y s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>x y. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y; False\<rbrakk> \<Longrightarrow> no_fail (?R'7 y) (gets cur_thread)
 7. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R20 x\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> as_user obj_id' (setRegister tlsBaseRegister tls_base) \<lbrace>?R'7\<rbrace>
 9. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 10. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id' and valid_etcbs and ?Q'7) s proof (prove)
goal (10 subgoals):
 1. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) reschedule_required
 2. \<And>x y cur. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R20 x) (?R'18 x y cur) (return x) (return [])
 3. \<And>x y cur. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 x y cur\<rbrace> when (obj_id' = cur) reschedule_required \<lbrace>\<lambda>xa. ?R'18 x y cur\<rbrace>
 4. \<And>x y. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?R'7 y\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. (\<lambda>_. True) and ?Q'18 x y cur\<rbrace>
 5. \<And>x y s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y; ?R'7 y s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>x y. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y; False\<rbrakk> \<Longrightarrow> no_fail (?R'7 y) (gets cur_thread)
 7. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R20 x\<rbrace>
 8. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> as_user obj_id' (setRegister tlsBaseRegister tls_base) \<lbrace>?R'7\<rbrace>
 9. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 10. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id' and valid_etcbs and ?Q'7) s proof (prove)
goal (9 subgoals):
 1. \<And>x y cur. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R20 x) (?R'18 x y cur) (return x) (return [])
 2. \<And>x y cur. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 x y cur\<rbrace> when (obj_id' = cur) reschedule_required \<lbrace>\<lambda>xa. ?R'18 x y cur\<rbrace>
 3. \<And>x y. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y\<rbrakk> \<Longrightarrow> \<lbrace>?R'7 y\<rbrace> gets cur_thread \<lbrace>\<lambda>cur. (\<lambda>_. True) and ?Q'18 x y cur\<rbrace>
 4. \<And>x y s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y; ?R'7 y s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> gets cur_thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>x y. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; dc x y; False\<rbrakk> \<Longrightarrow> no_fail (?R'7 y) (gets cur_thread)
 6. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q7\<rbrace> corrupt_tcb_intent obj_id' \<lbrace>\<lambda>x. (\<lambda>_. True) and ?R20 x\<rbrace>
 7. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7\<rbrace> as_user obj_id' (setRegister tlsBaseRegister tls_base) \<lbrace>?R'7\<rbrace>
 8. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 9. \<And>s. \<lbrakk>t' = tcb_invocation.SetTLSBase obj_id' tls_base; t = cdl_tcb_invocation.SetTLSBase obj_id'; (invs and not_idle_thread obj_id' and tcb_at obj_id' and valid_etcbs) s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread obj_id' and valid_etcbs and ?Q'7) s proof (prove)
goal:
No subgoals!