theory Tcb_C

lemma asUser_getMRs_rel:
  "\<lbrace>(\<lambda>s. t \<noteq> ksCurThread s) and getMRs_rel args buffer and cur_tcb'
        and case_option \<top> valid_ipc_buffer_ptr' buffer \<rbrace>
  asUser t f \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace>" apply (simp add: asUser_def) apply (rule hoare_pre, wp) apply (simp add: threadSet_def) apply (simp add: setObject_def split_def updateObject_default_def) apply wp apply (simp del: fun_upd_apply) apply (wp getObject_tcb_wp) apply (wp threadGet_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 (erule getMRs_rel_context, simp) apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def projectKOs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. t \<noteq> ksCurThread s) and getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> asUser t f \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. t \<noteq> ksCurThread s) and 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 uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
(a, uc') <- select_f (f uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) t;
return a
od \<lbrace>\<lambda>_. getMRs_rel args buffer\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>uc x a uc'. \<lbrace>?P6 uc x a uc'\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) t \<lbrace>\<lambda>y. getMRs_rel args buffer\<rbrace>
 2. \<And>uc. \<lbrace>?B4 uc\<rbrace> select_f (f uc) \<lbrace>\<lambda>x. case x of (xa, xb) \<Rightarrow> ?P6 uc x xa xb\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B4\<rbrace>
 4. \<And>s. ((\<lambda>s. t \<noteq> ksCurThread s) and getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>uc x a uc'. \<lbrace>?P6 uc x a uc'\<rbrace> do tcb <- getObject t;
setObject t (tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb)
od \<lbrace>\<lambda>y. getMRs_rel args buffer\<rbrace>
 2. \<And>uc. \<lbrace>?B4 uc\<rbrace> select_f (f uc) \<lbrace>\<lambda>x. case x of (xa, xb) \<Rightarrow> ?P6 uc x xa xb\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B4\<rbrace>
 4. \<And>s. ((\<lambda>s. t \<noteq> ksCurThread s) and getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>uc x a uc'. \<lbrace>?P6 uc x a uc'\<rbrace> do tcb <- getObject t;
ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- do y <- assert (t = fst p);
_ <- projectKO (snd p);
y <- alignCheck t (objBits (tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb));
y <- magnitudeCheck t (snd (lookupAround2 t ps)) (objBits (tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb));
return (KOTCB (tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb))
od;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>y. getMRs_rel args buffer\<rbrace>
 2. \<And>uc. \<lbrace>?B4 uc\<rbrace> select_f (f uc) \<lbrace>\<lambda>x. case x of (xa, xb) \<Rightarrow> ?P6 uc x xa xb\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B4\<rbrace>
 4. \<And>s. ((\<lambda>s. t \<noteq> ksCurThread s) and getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>uc x a uc'. \<lbrace>?P6 uc x a uc'\<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 (tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb))\<rparr>)\<rbrace>
 2. \<And>uc. \<lbrace>?B4 uc\<rbrace> select_f (f uc) \<lbrace>\<lambda>x. case x of (xa, xb) \<Rightarrow> ?P6 uc x xa xb\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B4\<rbrace>
 4. \<And>s. ((\<lambda>s. t \<noteq> ksCurThread s) and getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>uc x a uc'. \<lbrace>?P6 uc x a uc'\<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 (tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb))\<rparr>)\<rbrace>
 2. \<And>uc. \<lbrace>?B4 uc\<rbrace> select_f (f uc) \<lbrace>\<lambda>x. case x of (xa, xb) \<Rightarrow> ?P6 uc x xa xb\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B4\<rbrace>
 4. \<And>s. ((\<lambda>s. t \<noteq> ksCurThread s) and getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>uc. \<lbrace>?B4 uc\<rbrace> select_f (f uc) \<lbrace>\<lambda>x. case x of (a, uc') \<Rightarrow> \<lambda>s. 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 (tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch ta)) ta))\<rparr>)))\<rbrace>
 2. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B4\<rbrace>
 3. \<And>s. ((\<lambda>s. t \<noteq> ksCurThread s) and getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. t \<noteq> ksCurThread s) and getMRs_rel args buffer and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) s \<Longrightarrow> \<forall>tcb. ko_at' tcb t s \<longrightarrow> (\<forall>x\<in>fst (f ((atcbContextGet \<circ> tcbArch) tcb)). (case x of (a, uc') \<Rightarrow> \<lambda>s. 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 (tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch ta)) ta))\<rparr>)))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb a b. \<lbrakk>t \<noteq> ksCurThread s; 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' tcb t s; (a, b) \<in> fst (f (atcbContextGet (tcbArch tcb))); 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 (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch ta)) ta))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb a b. \<lbrakk>t \<noteq> ksCurThread s; getMRs_rel args buffer s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (a, b) \<in> fst (f (atcbContextGet (tcbArch tcb))); \<exists>ko. ko_at' ko t s \<and> ko = tcb; \<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 (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch ta)) ta))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb a b ko. \<lbrakk>t \<noteq> ksCurThread s; getMRs_rel args buffer s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (a, b) \<in> fst (f (atcbContextGet (tcbArch tcb))); ko_at' tcb t 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 (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch ta)) ta))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb a b ko. \<lbrakk>t \<noteq> ksCurThread s; getMRs_rel args buffer s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (a, b) \<in> fst (f (atcbContextGet (tcbArch tcb))); ko_at' tcb t 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 (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb a b ko ba. \<lbrakk>t \<noteq> ksCurThread s; getMRs_rel args buffer s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (a, b) \<in> fst (f (atcbContextGet (tcbArch tcb))); ko_at' tcb t s; ko_at' ko t s; ksPSpace s t = Some ba\<rbrakk> \<Longrightarrow> getMRs_rel args buffer (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbArch_update (\<lambda>_. atcbContextSet b (tcbArch tcb)) tcb))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s tcb a b ko ba. \<lbrakk>t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (a, b) \<in> fst (f (atcbContextGet (tcbArch tcb))); ko_at' tcb t s; ko_at' ko t s; ksPSpace s t = Some ba\<rbrakk> \<Longrightarrow> ko_at' tcb t s
 2. \<And>s tcb a b ko ba. \<lbrakk>t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (a, b) \<in> fst (f (atcbContextGet (tcbArch tcb))); ko_at' tcb t s; ko_at' ko t s; ksPSpace s t = Some ba\<rbrakk> \<Longrightarrow> t \<noteq> ksCurThread s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb a b ko ba. \<lbrakk>t \<noteq> ksCurThread s; cur_tcb' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; (a, b) \<in> fst (f (atcbContextGet (tcbArch tcb))); ko_at' tcb t s; ko_at' ko t s; ksPSpace s t = Some ba\<rbrakk> \<Longrightarrow> t \<noteq> ksCurThread s proof (prove)
goal:
No subgoals!