theory Tcb_C

lemma setThreadState_getMRs_rel:
  "\<lbrace>getMRs_rel args buffer and cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer
           and (\<lambda>_. runnable' st)\<rbrace>
      setThreadState st t \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace>" apply (rule hoare_gen_asm') apply (simp add: setThreadState_runnable_simp) apply (simp add: threadSet_def) apply wp apply (simp add: setObject_def split_def updateObject_default_def) apply wp apply (simp del: fun_upd_apply) apply (wp getObject_tcb_wp) apply (clarsimp simp del: fun_upd_apply) apply (drule obj_at_ko_at')+ apply (clarsimp simp del: fun_upd_apply) apply (rule exI, rule conjI, assumption) apply (clarsimp split: if_split simp del: fun_upd_apply) apply (simp add: getMRs_rel_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>_. runnable' st)\<rbrace> setThreadState st t \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace> proof (prove)
goal (1 subgoal):
 1. runnable' st \<Longrightarrow> \<lbrace>getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> setThreadState st t \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace> proof (prove)
goal (1 subgoal):
 1. runnable' st \<Longrightarrow> \<lbrace>getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> threadSet (tcbState_update (\<lambda>x. st)) t \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace> proof (prove)
goal (1 subgoal):
 1. runnable' st \<Longrightarrow> \<lbrace>getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> do tcb <- getObject t;
setObject t (tcbState_update (\<lambda>x. st) tcb)
od \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. runnable' st \<Longrightarrow> \<lbrace>?B3 tcb\<rbrace> setObject t (tcbState_update (\<lambda>x. st) tcb) \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace>
 2. runnable' st \<Longrightarrow> \<lbrace>?Q2\<rbrace> getObject t \<lbrace>?B3\<rbrace>
 3. \<And>s. \<lbrakk>runnable' st; (getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. runnable' st \<Longrightarrow> \<lbrace>?B3 tcb\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- do y <- assert (t = fst p);
_ <- projectKO (snd p);
y <- alignCheck t (objBits (tcbState_update (\<lambda>x. st) tcb));
y <- magnitudeCheck t (snd (lookupAround2 t ps)) (objBits (tcbState_update (\<lambda>x. st) tcb));
return (KOTCB (tcbState_update (\<lambda>x. st) tcb))
od;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace>
 2. runnable' st \<Longrightarrow> \<lbrace>?Q2\<rbrace> getObject t \<lbrace>?B3\<rbrace>
 3. \<And>s. \<lbrakk>runnable' st; (getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. runnable' st \<Longrightarrow> \<lbrace>?Q2\<rbrace> getObject t \<lbrace>\<lambda>tcb s. fst (lookupAround2 t (ksPSpace s)) \<noteq> None \<longrightarrow> t = fst (the (fst (lookupAround2 t (ksPSpace s)))) \<longrightarrow> getMRs_rel args buffer (s\<lparr>ksPSpace := (ksPSpace s)(fst (the (fst (lookupAround2 t (ksPSpace s)))) \<mapsto> KOTCB (tcbState_update (\<lambda>x. st) tcb))\<rparr>)\<rbrace>
 2. \<And>s. \<lbrakk>runnable' st; (getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (2 subgoals):
 1. runnable' st \<Longrightarrow> \<lbrace>?Q2\<rbrace> getObject t \<lbrace>\<lambda>tcb s. (\<exists>a b. fst (lookupAround2 t (ksPSpace s)) = Some (a, b)) \<longrightarrow> t = fst (the (fst (lookupAround2 t (ksPSpace s)))) \<longrightarrow> getMRs_rel args buffer (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>x. st) tcb))\<rparr>)\<rbrace>
 2. \<And>s. \<lbrakk>runnable' st; (getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>runnable' st; (getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s\<rbrakk> \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> ((\<exists>a b. fst (lookupAround2 t (ksPSpace s)) = Some (a, b)) \<longrightarrow> t = fst (the (fst (lookupAround2 t (ksPSpace s)))) \<longrightarrow> getMRs_rel args buffer (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>x. st) ta))\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>runnable' st; getMRs_rel args buffer s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; tcb_at' t s\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> ((\<exists>a b. fst (lookupAround2 t (ksPSpace s)) = Some (a, b)) \<longrightarrow> t = fst (the (fst (lookupAround2 t (ksPSpace s)))) \<longrightarrow> getMRs_rel args buffer (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>x. st) ta))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>runnable' st; getMRs_rel args buffer s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; \<exists>ko. ko_at' ko t s \<and> True\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> ((\<exists>a b. fst (lookupAround2 t (ksPSpace s)) = Some (a, b)) \<longrightarrow> t = fst (the (fst (lookupAround2 t (ksPSpace s)))) \<longrightarrow> getMRs_rel args buffer (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>x. st) ta))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>runnable' st; getMRs_rel args buffer s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; ko_at' ko t s\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> ((\<exists>a b. fst (lookupAround2 t (ksPSpace s)) = Some (a, b)) \<longrightarrow> t = fst (the (fst (lookupAround2 t (ksPSpace s)))) \<longrightarrow> getMRs_rel args buffer (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>x. st) ta))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>runnable' st; getMRs_rel args buffer s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; ko_at' ko t s\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 t (ksPSpace s)) = Some (a, b)) \<longrightarrow> t = fst (the (fst (lookupAround2 t (ksPSpace s)))) \<longrightarrow> getMRs_rel args buffer (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>x. st) ko))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko b. \<lbrakk>runnable' st; getMRs_rel args buffer s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; ko_at' ko t s; ksPSpace s t = Some b\<rbrakk> \<Longrightarrow> getMRs_rel args buffer (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbState_update (\<lambda>x. st) ko))\<rparr>) proof (prove)
goal:
No subgoals!