theory FinalCaps

lemma as_user_silc_inv[wp]:
  "as_user t f \<lbrace>silc_inv aag st\<rbrace>" unfolding as_user_def apply (rule silc_inv_pres) apply (wp set_object_wp | simp add: split_def)+ apply (clarsimp) apply (fastforce simp: silc_inv_def dest: get_tcb_SomeD simp: obj_at_def is_cap_table_def) apply (wp set_object_wp | simp add: split_def)+ apply (case_tac "t = fst slot") apply (clarsimp split: kernel_object.splits) apply (erule notE) apply (erule cte_wp_atE) apply (fastforce simp: obj_at_def) apply (drule get_tcb_SomeD) apply (rule cte_wp_at_tcbI) apply (simp) apply assumption apply (fastforce simp: tcb_cap_cases_def split: if_splits) apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> as_user t f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> do tcb <- gets_the $ get_tcb t;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object t (TCB new_tcb);
return a
od \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ptr P. \<lbrace>silc_inv aag st and (\<lambda>s. P (kheap s ptr)) and K (pasObjectAbs aag ptr = SilcLabel)\<rbrace> do tcb <- gets_the $ get_tcb t;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object t (TCB new_tcb);
return a
od \<lbrace>\<lambda>_ s. P (kheap s ptr)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the $ get_tcb t;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object t (TCB new_tcb);
return a
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do tcb <- gets_the $ get_tcb t;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object t (TCB new_tcb);
return a
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ptr P s. silc_inv aag st s \<and> P (kheap s ptr) \<and> pasObjectAbs aag ptr = SilcLabel \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> ptr = t \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). P (Some (TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the $ get_tcb t;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object t (TCB new_tcb);
return a
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do tcb <- gets_the $ get_tcb t;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object t (TCB new_tcb);
return a
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P s y a b. \<lbrakk>silc_inv aag st s; P (kheap s t); pasObjectAbs aag t = SilcLabel; get_tcb t s = Some y; (a, b) \<in> fst (f (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> P (Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr>)))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the $ get_tcb t;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object t (TCB new_tcb);
return a
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do tcb <- gets_the $ get_tcb t;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object t (TCB new_tcb);
return a
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the $ get_tcb t;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object t (TCB new_tcb);
return a
od \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 2. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do tcb <- gets_the $ get_tcb t;
uc <- return $ arch_tcb_context_get (tcb_arch tcb);
(a, uc') <- select_f $ f uc;
new_tcb <- return $ tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>;
set_object t (TCB new_tcb);
return a
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P slot s. \<not> cte_wp_at P slot s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; t = fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>))
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P b s aa ba y. \<lbrakk>\<not> cte_wp_at P (t, b) s; (aa, ba) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); get_tcb t s = Some y; cte_wp_at P (t, b) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch y)\<rparr>))\<rparr>)\<rbrakk> \<Longrightarrow> False
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P b s aa ba y. \<lbrakk>(aa, ba) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); get_tcb t s = Some y; cte_wp_at P (t, b) (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch y)\<rparr>))\<rparr>)\<rbrakk> \<Longrightarrow> cte_wp_at P (t, b) s
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>P b s aa ba y sz fun cte. \<lbrakk>(aa, ba) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); get_tcb t s = Some y; kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch y)\<rparr>))\<rparr>) (fst (t, b)) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd (t, b)) = Some cte; P cte\<rbrakk> \<Longrightarrow> cte_wp_at P (t, b) s
 2. \<And>P b s aa ba y tcb getF setF restr. \<lbrakk>(aa, ba) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); get_tcb t s = Some y; kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch y)\<rparr>))\<rparr>) (fst (t, b)) = Some (TCB tcb); tcb_cap_cases (snd (t, b)) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P (t, b) s
 3. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P b s aa ba y tcb getF setF restr. \<lbrakk>(aa, ba) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); get_tcb t s = Some y; kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch y)\<rparr>))\<rparr>) (fst (t, b)) = Some (TCB tcb); tcb_cap_cases (snd (t, b)) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P (t, b) s
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P b s aa ba y tcb getF setF restr. \<lbrakk>(aa, ba) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch y)\<rparr>))\<rparr>) (fst (t, b)) = Some (TCB tcb); tcb_cap_cases (snd (t, b)) = Some (getF, setF, restr); P (getF tcb); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> cte_wp_at P (t, b) s
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal (4 subgoals):
 1. \<And>P b s aa ba y tcb getF setF restr. \<lbrakk>(aa, ba) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch y)\<rparr>))\<rparr>) (fst (t, b)) = Some (TCB tcb); tcb_cap_cases (snd (t, b)) = Some (getF, setF, restr); P (getF tcb); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> kheap s (fst (t, b)) = Some (TCB (?tcb122 P b s aa ba y tcb getF setF restr))
 2. \<And>P b s aa ba y tcb getF setF restr. \<lbrakk>(aa, ba) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch y)\<rparr>))\<rparr>) (fst (t, b)) = Some (TCB tcb); tcb_cap_cases (snd (t, b)) = Some (getF, setF, restr); P (getF tcb); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd (t, b)) = Some (?getF122 P b s aa ba y tcb getF setF restr, ?setF122 P b s aa ba y tcb getF setF restr)
 3. \<And>P b s aa ba y tcb getF setF restr. \<lbrakk>(aa, ba) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch y)\<rparr>))\<rparr>) (fst (t, b)) = Some (TCB tcb); tcb_cap_cases (snd (t, b)) = Some (getF, setF, restr); P (getF tcb); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> P (?getF122 P b s aa ba y tcb getF setF restr (?tcb122 P b s aa ba y tcb getF setF restr))
 4. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>P b s aa ba y tcb getF setF restr. \<lbrakk>(aa, ba) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch y)\<rparr>))\<rparr>) (fst (t, b)) = Some (TCB tcb); tcb_cap_cases (snd (t, b)) = Some (getF, setF, restr); P (getF tcb); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd (t, b)) = Some (?getF122 P b s aa ba y tcb getF setF restr, ?setF122 P b s aa ba y tcb getF setF restr)
 2. \<And>P b s aa ba y tcb getF setF restr. \<lbrakk>(aa, ba) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch y)\<rparr>))\<rparr>) (fst (t, b)) = Some (TCB tcb); tcb_cap_cases (snd (t, b)) = Some (getF, setF, restr); P (getF tcb); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> P (?getF122 P b s aa ba y tcb getF setF restr y)
 3. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>P b s aa ba y tcb getF setF restr. \<lbrakk>(aa, ba) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (y\<lparr>tcb_arch := arch_tcb_context_set ba (tcb_arch y)\<rparr>))\<rparr>) (fst (t, b)) = Some (TCB tcb); tcb_cap_cases (snd (t, b)) = Some (getF, setF, restr); P (getF tcb); kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> P (getF y)
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!