theory FinalCaps

lemma update_restart_pc_silc_inv[wp]:
  "\<lbrace>silc_inv aag st\<rbrace> update_restart_pc t \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding update_restart_pc_def apply (rule silc_inv_pres) apply (simp add: as_user_def) apply (wpsimp simp: set_object_wp) apply (wp set_object_wp)+ apply clarsimp+ apply (fastforce simp: silc_inv_def dest: get_tcb_SomeD simp: obj_at_def is_cap_table_def) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> update_restart_pc t \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<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> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<lbrace>\<lambda>_ s. P (kheap s ptr)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ptr P. \<lbrace>silc_inv aag st and (\<lambda>s. P (kheap s ptr)) and (\<lambda>y. pasObjectAbs aag ptr = SilcLabel)\<rbrace> do tcb <- gets_the (get_tcb t);
(a, uc') <- select_f ((getRegister nextInstructionRegister >>= setRegister faultRegister) (arch_tcb_context_get (tcb_arch tcb)));
set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))
od \<lbrace>\<lambda>_ s. P (kheap s ptr)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ptr P tcb x2. \<lbrace>?R15 ptr P tcb ((), x2) () x2\<rbrace> set_object t (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set x2 (tcb_arch tcb)\<rparr>)) \<lbrace>\<lambda>_ s. P (kheap s ptr)\<rbrace>
 2. \<And>ptr P tcb. \<lbrace>?B6 ptr P tcb\<rbrace> select_f ((getRegister nextInstructionRegister >>= setRegister faultRegister) (arch_tcb_context_get (tcb_arch tcb))) \<lbrace>\<lambda>x s. \<forall>xa xb. x = (xa, xb) \<longrightarrow> ?R15 ptr P tcb x xa xb s\<rbrace>
 3. \<And>ptr P. \<lbrace>?Q5 ptr P\<rbrace> gets_the (get_tcb t) \<lbrace>?B6 ptr P\<rbrace>
 4. \<And>ptr P s. (silc_inv aag st and (\<lambda>s. P (kheap s ptr)) and (\<lambda>y. pasObjectAbs aag ptr = SilcLabel)) s \<Longrightarrow> ?Q5 ptr P s
 5. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 6. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<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 and (\<lambda>s. P (kheap s ptr)) and (\<lambda>y. pasObjectAbs aag ptr = SilcLabel)) s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> (\<forall>x\<in>fst ((getRegister nextInstructionRegister >>= setRegister faultRegister) (arch_tcb_context_get (tcb_arch (the (get_tcb t s))))). \<forall>xa xb. x = (xa, xb) \<longrightarrow> P (kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_arch := arch_tcb_context_set xb (tcb_arch (the (get_tcb t s)))\<rparr>))\<rparr>) ptr))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>P s y x. \<lbrakk>silc_inv aag st s; P (kheap s t); pasObjectAbs aag t = SilcLabel; get_tcb t s = Some y; ((), x) \<in> fst ((getRegister nextInstructionRegister >>= setRegister faultRegister) (arch_tcb_context_get (tcb_arch y)))\<rbrakk> \<Longrightarrow> P (Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set x (tcb_arch y)\<rparr>)))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<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> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 2. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> as_user t (getRegister nextInstructionRegister >>= setRegister faultRegister) \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal:
No subgoals!