theory TcbAcc_AI

lemma as_user_mdb [wp]:
  "\<lbrace>valid_mdb\<rbrace> as_user f t \<lbrace>\<lambda>_. valid_mdb\<rbrace>" apply (simp add: as_user_def split_def) apply (rule valid_mdb_lift) prefer 2 apply wp apply simp prefer 2 apply (simp add: set_object_def get_object_def) apply wpsimp apply (simp add: set_object_def get_object_def) apply wp apply clarsimp apply (subst cte_wp_caps_of_lift) prefer 2 apply assumption apply (simp add: cte_wp_at_cases) apply (drule get_tcb_SomeD) apply (auto simp: tcb_cap_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> as_user f t \<lbrace>\<lambda>_. valid_mdb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_. valid_mdb\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (is_original_cap s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (is_original_cap s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P s. P (cdt s) \<Longrightarrow> get_tcb f s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (t (arch_tcb_context_get (tcb_arch (the (get_tcb f s))))). P (cdt s))
 2. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (is_original_cap s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (is_original_cap s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (is_original_cap s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh f = Some y);
return (the (kh f))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(f \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
return (fst p)
od \<lbrace>\<lambda>_ s. P (is_original_cap s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>));
return (fst p)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> do tcb <- gets_the (get_tcb f);
p <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh f = Some y);
return (the (kh f))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(f \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
return (fst p)
od \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P s. P (caps_of_state s) \<Longrightarrow> get_tcb f s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (t (arch_tcb_context_get (tcb_arch (the (get_tcb f s))))). (\<exists>y. kheap s f = Some y) \<longrightarrow> a_type (the (kheap s f)) = ATCB \<longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(f \<mapsto> TCB (the (get_tcb f s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb f s)))\<rparr>))\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>P s y tcb a b. \<lbrakk>P (caps_of_state s); get_tcb f s = Some y; kheap s f = Some (TCB tcb); (a, b) \<in> fst (t (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> P (caps_of_state (s\<lparr>kheap := \<lambda>c. if c = f then Some (TCB (the (get_tcb f s)\<lparr>tcb_arch := arch_tcb_context_set (snd (a, b)) (tcb_arch (the (get_tcb f s)))\<rparr>)) else kheap s c\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P s y tcb a b p Pa. \<lbrakk>P (caps_of_state s); get_tcb f s = Some y; kheap s f = Some (TCB tcb); (a, b) \<in> fst (t (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> cte_wp_at Pa p (s\<lparr>kheap := \<lambda>c. if c = f then Some (TCB (the (get_tcb f s)\<lparr>tcb_arch := arch_tcb_context_set (snd (a, b)) (tcb_arch (the (get_tcb f s)))\<rparr>)) else kheap s c\<rparr>) = cte_wp_at Pa p (?s'64 P s y tcb a b)
 2. \<And>P s y tcb a b. \<lbrakk>P (caps_of_state s); get_tcb f s = Some y; kheap s f = Some (TCB tcb); (a, b) \<in> fst (t (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> P (caps_of_state (?s'64 P s y tcb a b)) proof (prove)
goal (2 subgoals):
 1. \<And>P s y tcb a b. \<lbrakk>P (caps_of_state s); get_tcb f s = Some y; kheap s f = Some (TCB tcb); (a, b) \<in> fst (t (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> P (caps_of_state (?s'64 P s y tcb a b))
 2. \<And>P s y tcb a b p Pa. \<lbrakk>P (caps_of_state s); get_tcb f s = Some y; kheap s f = Some (TCB tcb); (a, b) \<in> fst (t (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> cte_wp_at Pa p (s\<lparr>kheap := \<lambda>c. if c = f then Some (TCB (the (get_tcb f s)\<lparr>tcb_arch := arch_tcb_context_set (snd (a, b)) (tcb_arch (the (get_tcb f s)))\<rparr>)) else kheap s c\<rparr>) = cte_wp_at Pa p (?s'64 P s y tcb a b) proof (prove)
goal (1 subgoal):
 1. \<And>P s y tcb a b p Pa. \<lbrakk>P (caps_of_state s); get_tcb f s = Some y; kheap s f = Some (TCB tcb); (a, b) \<in> fst (t (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> cte_wp_at Pa p (s\<lparr>kheap := \<lambda>c. if c = f then Some (TCB (the (get_tcb f s)\<lparr>tcb_arch := arch_tcb_context_set (snd (a, b)) (tcb_arch (the (get_tcb f s)))\<rparr>)) else kheap s c\<rparr>) = cte_wp_at Pa p s proof (prove)
goal (1 subgoal):
 1. \<And>P s y tcb a b p Pa. \<lbrakk>P (caps_of_state s); get_tcb f s = Some y; kheap s f = Some (TCB tcb); (a, b) \<in> fst (t (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> fst p = f \<longrightarrow> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> Pa (get (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>))) = (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> Pa (get tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>P s y tcb a b p Pa. \<lbrakk>P (caps_of_state s); kheap s f = Some (TCB tcb); (a, b) \<in> fst (t (arch_tcb_context_get (tcb_arch y))); kheap s f = Some (TCB y)\<rbrakk> \<Longrightarrow> fst p = f \<longrightarrow> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> Pa (get (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>))) = (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> Pa (get tcb)) proof (prove)
goal:
No subgoals!