theory ArchAcc_AI

lemma as_user_inv:
  assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x. P\<rbrace>"
  shows      "\<lbrace>P\<rbrace> as_user t f \<lbrace>\<lambda>x. P\<rbrace>" proof - have P: "\<And>a b input. (a, b) \<in> fst (f input) \<Longrightarrow> b = input" by (rule use_valid [OF _ x], assumption, rule refl) have Q: "\<And>s ps. ps (kheap s) = kheap s \<Longrightarrow> kheap_update ps s = s" by simp show ?thesis apply (simp add: as_user_def gets_the_def assert_opt_def set_object_def get_object_def split_def) apply wp apply (clarsimp dest!: P) apply (subst Q) prefer 2 apply assumption apply (rule ext) apply (simp add: get_tcb_def) apply (case_tac "kheap s t"; simp) apply (case_tac a; simp) apply (clarsimp simp: arch_tcb_context_set_def arch_tcb_context_get_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> as_user t f \<lbrace>\<lambda>x. P\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> as_user t f \<lbrace>\<lambda>x. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b input. (a, b) \<in> fst (f input) \<Longrightarrow> b = input proof (state)
this:
(?a, ?b) \<in> fst (f ?input) \<Longrightarrow> ?b = ?input

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> as_user t f \<lbrace>\<lambda>x. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ps. ps (kheap s) = kheap s \<Longrightarrow> kheap_update ps s = s proof (state)
this:
?ps (kheap ?s) = kheap ?s \<Longrightarrow> kheap_update ?ps ?s = ?s

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> as_user t f \<lbrace>\<lambda>x. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> as_user t f \<lbrace>\<lambda>x. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do tcb <- gets (get_tcb t) >>= assert_opt;
p <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>))\<rparr>)
od;
return (fst p)
od \<lbrace>\<lambda>x. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> P (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>s y tcb a. \<lbrakk>P s; get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P (s\<lparr>kheap := \<lambda>b. if b = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd (a, arch_tcb_context_get (tcb_arch (the (get_tcb t s))))) (tcb_arch (the (get_tcb t s)))\<rparr>)) else kheap s b\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb a. \<lbrakk>P s; get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (\<lambda>b. if b = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd (a, arch_tcb_context_get (tcb_arch (the (get_tcb t s))))) (tcb_arch (the (get_tcb t s)))\<rparr>)) else kheap s b) = kheap s
 2. \<And>s y tcb a. \<lbrakk>P s; get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P s proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb a. \<lbrakk>P s; get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> P s
 2. \<And>s y tcb a. \<lbrakk>P s; get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (\<lambda>b. if b = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd (a, arch_tcb_context_get (tcb_arch (the (get_tcb t s))))) (tcb_arch (the (get_tcb t s)))\<rparr>)) else kheap s b) = kheap s proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb a. \<lbrakk>P s; get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (\<lambda>b. if b = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd (a, arch_tcb_context_get (tcb_arch (the (get_tcb t s))))) (tcb_arch (the (get_tcb t s)))\<rparr>)) else kheap s b) = kheap s proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb a x. \<lbrakk>P s; get_tcb t s = Some y; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (if x = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set (snd (a, arch_tcb_context_get (tcb_arch (the (get_tcb t s))))) (tcb_arch (the (get_tcb t s)))\<rparr>)) else kheap s x) = kheap s x proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb x. \<lbrakk>P s; tcb = y; kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> x = t \<longrightarrow> y\<lparr>tcb_arch := arch_tcb_context_set (arch_tcb_context_get (tcb_arch y)) (tcb_arch y)\<rparr> = y proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb x a. \<lbrakk>P s; tcb = y; a = TCB y; kheap s t = Some (TCB y)\<rbrakk> \<Longrightarrow> x = t \<longrightarrow> y\<lparr>tcb_arch := arch_tcb_context_set (arch_tcb_context_get (tcb_arch y)) (tcb_arch y)\<rparr> = y proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb x a x2. \<lbrakk>P s; tcb = y; x2 = y; kheap s t = Some (TCB y); a = TCB y\<rbrakk> \<Longrightarrow> x = t \<longrightarrow> y\<lparr>tcb_arch := arch_tcb_context_set (arch_tcb_context_get (tcb_arch y)) (tcb_arch y)\<rparr> = y proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>P\<rbrace> as_user t f \<lbrace>\<lambda>x. P\<rbrace>

goal:
No subgoals!