theory InfoFlow_IF

lemma as_user_rev:
  "reads_equiv_valid_inv A aag (K (det f \<and> (\<forall>P. f \<lbrace>P\<rbrace>) \<and> is_subject aag thread)) (as_user thread f)" unfolding as_user_def fun_app_def split_def apply (wp set_object_rev select_f_ev) apply (rule conjI, fastforce) apply (clarsimp split: option.split_asm kernel_object.split_asm simp: get_tcb_def) apply (drule state_unchanged[rotated,symmetric]) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (det f \<and> (\<forall>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<and> is_subject aag thread)) (as_user thread f) proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_inv A aag (K (det f \<and> (\<forall>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<and> is_subject aag thread)) (do tcb <- gets_the (get_tcb thread);
uc <- return (arch_tcb_context_get (tcb_arch tcb));
p <- select_f (f uc);
new_tcb <- return (tcb\<lparr>tcb_arch := arch_tcb_context_set (snd p) (tcb_arch tcb)\<rparr>);
set_object thread (TCB new_tcb);
return (fst p)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. K (det f \<and> (\<forall>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<and> is_subject aag thread) s \<Longrightarrow> K (\<forall>s t. reads_equiv aag s t \<and> A s t \<longrightarrow> get_tcb thread s = get_tcb thread t) s \<and> (get_tcb thread s \<noteq> None \<longrightarrow> True \<and> K (det f) s \<and> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb thread s))))). True \<and> (kheap s thread = Some (TCB (the (get_tcb thread s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb thread s)))\<rparr>)) \<and> is_subject aag thread) \<and> True)) proof (prove)
goal (1 subgoal):
 1. \<And>s. K (det f \<and> (\<forall>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>) \<and> is_subject aag thread) s \<Longrightarrow> get_tcb thread s \<noteq> None \<longrightarrow> True \<and> K (det f) s \<and> (\<forall>x\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb thread s))))). True \<and> (kheap s thread = Some (TCB (the (get_tcb thread s)\<lparr>tcb_arch := arch_tcb_context_set (snd x) (tcb_arch (the (get_tcb thread s)))\<rparr>)) \<and> is_subject aag thread) \<and> True) proof (prove)
goal (1 subgoal):
 1. \<And>s a b y. \<lbrakk>det f; \<forall>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; is_subject aag thread; (a, b) \<in> fst (f (arch_tcb_context_get (tcb_arch y))); kheap s thread = Some (TCB y)\<rbrakk> \<Longrightarrow> y = y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>s a b y P. \<lbrakk>det f; \<forall>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; is_subject aag thread; kheap s thread = Some (TCB y)\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s a b y. \<lbrakk>det f; \<forall>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>; is_subject aag thread; kheap s thread = Some (TCB y); b = arch_tcb_context_get (tcb_arch y)\<rbrakk> \<Longrightarrow> y = y\<lparr>tcb_arch := arch_tcb_context_set b (tcb_arch y)\<rparr> proof (prove)
goal:
No subgoals!