theory FinalCaps

lemma thread_set_silc_inv:
  assumes cap_inv: "\<And>tcb. \<forall>(getF, v) \<in> ran tcb_cap_cases. getF (f tcb) = getF tcb"
  shows "\<lbrace>silc_inv aag st\<rbrace> thread_set f t \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (rule silc_inv_pres) apply (subst thread_set_def) apply (wp set_object_wp) apply (simp split: kernel_object.splits) apply (rule impI | simp)+ apply (fastforce simp: silc_inv_def dest: get_tcb_SomeD simp: obj_at_def is_cap_table_def) apply (rule thread_set_Pmdb) apply (rule thread_set_cte_wp_at_trivial[OF cap_inv]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st\<rbrace> thread_set f t \<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> thread_set f t \<lbrace>\<lambda>_ s. P (kheap s ptr)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> thread_set f t \<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 K (pasObjectAbs aag ptr = SilcLabel)\<rbrace> do tcb <- gets_the $ get_tcb t;
set_object t $ TCB $ f tcb
od \<lbrace>\<lambda>_ s. P (kheap s ptr)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> thread_set f t \<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 K (pasObjectAbs aag ptr = SilcLabel)) s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> P (kheap (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB $ f (the (get_tcb t s)))\<rparr>) ptr)
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> thread_set f t \<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> ptr = t \<longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> P (Some (TCB (f (the (get_tcb t s)))))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ptr P s. \<lbrakk>silc_inv aag st s \<and> P (kheap s t) \<and> pasObjectAbs aag t = SilcLabel; ptr = t; \<exists>y. get_tcb t s = Some y\<rbrakk> \<Longrightarrow> P (Some (TCB (f (the (get_tcb t s)))))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 3. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> thread_set f t \<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> thread_set f t \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>
 2. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P slot. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> thread_set f t \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal:
No subgoals!