theory SyscallArgs_C

lemma asUser_cur_obj_at':
  assumes f: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
  shows "\<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s\<rbrace>
          asUser t f \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. Q rv (atcbContextGet (tcbArch tcb))) (ksCurThread s) s\<rbrace>" apply (simp add: asUser_def split_def) apply (wp) apply (rule hoare_lift_Pf2 [where f=ksCurThread]) apply (wp threadSet_obj_at'_really_strongest)+ apply (clarsimp simp: threadGet_def) apply (wp getObject_tcb_wp) apply clarsimp apply (drule obj_at_ko_at') apply clarsimp apply (rename_tac tcb) apply (rule_tac x=tcb in exI) apply clarsimp apply (drule use_valid, rule f, assumption) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s\<rbrace> asUser t f \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. Q rv (atcbContextGet (tcbArch tcb))) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (f uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv s. obj_at' (\<lambda>tcb. Q rv (atcbContextGet (tcbArch tcb))) (ksCurThread s) s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>uc p. \<lbrace>?B2 uc p\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>y a. obj_at' (\<lambda>tcb. Q (fst p) (atcbContextGet (tcbArch tcb))) (ksCurThread a) a\<rbrace>
 2. \<And>uc. \<lbrace>?B1 uc\<rbrace> select_f (f uc) \<lbrace>?B2 uc\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B1\<rbrace>
 4. \<And>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>uc p x. \<lbrace>?Q5 uc p x\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. Q (fst p) (atcbContextGet (tcbArch tcb))) x\<rbrace>
 2. \<And>uc p P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 3. \<And>uc. \<lbrace>?B1 uc\<rbrace> select_f (f uc) \<lbrace>\<lambda>p s. ?Q5 uc p (ksCurThread s) s\<rbrace>
 4. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>?B1\<rbrace>
 5. \<And>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>uc s. \<forall>x\<in>fst (f uc). tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = ksCurThread s then Q (fst x) (atcbContextGet (tcbArch (tcbArch_update (\<lambda>_. atcbContextSet (snd x) (tcbArch obj)) obj))) else Q (fst x) (atcbContextGet (tcbArch obj))) (ksCurThread s) s\<rbrace>
 2. \<And>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> liftM (atcbContextGet \<circ> tcbArch) (getObject t) \<lbrace>\<lambda>uc s. tcb_at' t s \<longrightarrow> (\<forall>x\<in>fst (f uc). obj_at' (\<lambda>obj. if t = ksCurThread s then Q (fst x) (atcbContextGet (tcbArch (tcbArch_update (\<lambda>_. atcbContextSet (snd x) (tcbArch obj)) obj))) else Q (fst x) (atcbContextGet (tcbArch obj))) (ksCurThread s) s)\<rbrace>
 2. \<And>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s \<and> t = ksCurThread s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> ((\<lambda>uc s. tcb_at' t s \<longrightarrow> (\<forall>x\<in>fst (f uc). obj_at' (\<lambda>obj. if t = ksCurThread s then Q (fst x) (atcbContextGet (tcbArch (tcbArch_update (\<lambda>_. atcbContextSet (snd x) (tcbArch obj)) obj))) else Q (fst x) (atcbContextGet (tcbArch obj))) (ksCurThread s) s)) \<circ> (atcbContextGet \<circ> tcbArch)) ta s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) (ksCurThread s) s; t = ksCurThread s; tcb_at' (ksCurThread s) s\<rbrakk> \<Longrightarrow> \<exists>t. ko_at' t (ksCurThread s) s \<and> (\<forall>x\<in>fst (f (atcbContextGet (tcbArch t))). obj_at' (\<lambda>obj. Q (fst x) (snd x)) (ksCurThread s) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>t = ksCurThread s; tcb_at' (ksCurThread s) s; \<exists>ko. ko_at' ko (ksCurThread s) s \<and> P (atcbContextGet (tcbArch ko))\<rbrakk> \<Longrightarrow> \<exists>t. ko_at' t (ksCurThread s) s \<and> (\<forall>x\<in>fst (f (atcbContextGet (tcbArch t))). obj_at' (\<lambda>obj. Q (fst x) (snd x)) (ksCurThread s) s) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>t = ksCurThread s; tcb_at' (ksCurThread s) s; ko_at' ko (ksCurThread s) s; P (atcbContextGet (tcbArch ko))\<rbrakk> \<Longrightarrow> \<exists>t. ko_at' t (ksCurThread s) s \<and> (\<forall>x\<in>fst (f (atcbContextGet (tcbArch t))). obj_at' (\<lambda>obj. Q (fst x) (snd x)) (ksCurThread s) s) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>t = ksCurThread s; tcb_at' (ksCurThread s) s; ko_at' tcb (ksCurThread s) s; P (atcbContextGet (tcbArch tcb))\<rbrakk> \<Longrightarrow> \<exists>t. ko_at' t (ksCurThread s) s \<and> (\<forall>x\<in>fst (f (atcbContextGet (tcbArch t))). obj_at' (\<lambda>obj. Q (fst x) (snd x)) (ksCurThread s) s) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>t = ksCurThread s; tcb_at' (ksCurThread s) s; ko_at' tcb (ksCurThread s) s; P (atcbContextGet (tcbArch tcb))\<rbrakk> \<Longrightarrow> ko_at' tcb (ksCurThread s) s \<and> (\<forall>x\<in>fst (f (atcbContextGet (tcbArch tcb))). obj_at' (\<lambda>obj. Q (fst x) (snd x)) (ksCurThread s) s) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb a b. \<lbrakk>t = ksCurThread s; tcb_at' (ksCurThread s) s; ko_at' tcb (ksCurThread s) s; P (atcbContextGet (tcbArch tcb)); (a, b) \<in> fst (f (atcbContextGet (tcbArch tcb)))\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>obj. Q a b) (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb a b. \<lbrakk>t = ksCurThread s; tcb_at' (ksCurThread s) s; ko_at' tcb (ksCurThread s) s; P (atcbContextGet (tcbArch tcb)); Q a b\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>obj. Q a b) (ksCurThread s) s proof (prove)
goal:
No subgoals!