theory FinalCaps

lemma set_bound_notification_silc_inv[wp]:
  "\<lbrace>silc_inv aag st\<rbrace>
   set_bound_notification tptr ntfn
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding set_bound_notification_def apply (rule silc_inv_pres) apply (wp set_object_wp|simp split del: if_split)+ 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 (wp set_object_wp | simp)+ apply (case_tac "tptr = 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> set_bound_notification tptr ntfn \<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 tptr;
set_object tptr (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
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 tptr;
set_object tptr (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
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 tptr;
set_object tptr (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
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 tptr;
set_object tptr (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
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 tptr s = Some y) \<longrightarrow> P (if ptr = tptr then Some (TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s ptr)
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the $ get_tcb tptr;
set_object tptr (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
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 tptr;
set_object tptr (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
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> ptr = tptr \<longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> P (Some (TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>)))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the $ get_tcb tptr;
set_object tptr (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
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 tptr;
set_object tptr (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<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 tptr) \<and> pasObjectAbs aag tptr = SilcLabel; ptr = tptr; \<exists>y. get_tcb tptr s = Some y\<rbrakk> \<Longrightarrow> P (Some (TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>)))
 2. \<And>P. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the $ get_tcb tptr;
set_object tptr (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
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 tptr;
set_object tptr (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
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 tptr;
set_object tptr (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
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 tptr;
set_object tptr (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
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 tptr s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; tptr = fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; tptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>P b s y. \<lbrakk>\<not> cte_wp_at P (tptr, b) s; get_tcb tptr s = Some y; cte_wp_at P (tptr, b) (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)\<rbrakk> \<Longrightarrow> False
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; tptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>P b s y. \<lbrakk>get_tcb tptr s = Some y; cte_wp_at P (tptr, b) (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)\<rbrakk> \<Longrightarrow> cte_wp_at P (tptr, b) s
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; tptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>P b s y sz fun cte. \<lbrakk>get_tcb tptr s = Some y; kheap (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) (fst (tptr, b)) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd (tptr, b)) = Some cte; P cte\<rbrakk> \<Longrightarrow> cte_wp_at P (tptr, b) s
 2. \<And>P b s y tcb getF setF restr. \<lbrakk>get_tcb tptr s = Some y; kheap (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) (fst (tptr, b)) = Some (TCB tcb); tcb_cap_cases (snd (tptr, b)) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P (tptr, b) s
 3. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; tptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>P b s y tcb getF setF restr. \<lbrakk>get_tcb tptr s = Some y; kheap (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) (fst (tptr, b)) = Some (TCB tcb); tcb_cap_cases (snd (tptr, b)) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P (tptr, b) s
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; tptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) (fst (tptr, b)) = Some (TCB tcb); tcb_cap_cases (snd (tptr, b)) = Some (getF, setF, restr); P (getF tcb); kheap s tptr = Some (TCB y)\<rbrakk> \<Longrightarrow> cte_wp_at P (tptr, b) s
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; tptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) (fst (tptr, b)) = Some (TCB tcb); tcb_cap_cases (snd (tptr, b)) = Some (getF, setF, restr); P (getF tcb); kheap s tptr = Some (TCB y)\<rbrakk> \<Longrightarrow> kheap s (fst (tptr, b)) = Some (TCB (?tcb69 P b s y tcb getF setF restr))
 2. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) (fst (tptr, b)) = Some (TCB tcb); tcb_cap_cases (snd (tptr, b)) = Some (getF, setF, restr); P (getF tcb); kheap s tptr = Some (TCB y)\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd (tptr, b)) = Some (?getF69 P b s y tcb getF setF restr, ?setF69 P b s y tcb getF setF restr)
 3. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) (fst (tptr, b)) = Some (TCB tcb); tcb_cap_cases (snd (tptr, b)) = Some (getF, setF, restr); P (getF tcb); kheap s tptr = Some (TCB y)\<rbrakk> \<Longrightarrow> P (?getF69 P b s y tcb getF setF restr (?tcb69 P b s y tcb getF setF restr))
 4. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; tptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) (fst (tptr, b)) = Some (TCB tcb); tcb_cap_cases (snd (tptr, b)) = Some (getF, setF, restr); P (getF tcb); kheap s tptr = Some (TCB y)\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd (tptr, b)) = Some (?getF69 P b s y tcb getF setF restr, ?setF69 P b s y tcb getF setF restr)
 2. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) (fst (tptr, b)) = Some (TCB tcb); tcb_cap_cases (snd (tptr, b)) = Some (getF, setF, restr); P (getF tcb); kheap s tptr = Some (TCB y)\<rbrakk> \<Longrightarrow> P (?getF69 P b s y tcb getF setF restr y)
 3. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; tptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>P b s y tcb getF setF restr. \<lbrakk>kheap (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) (fst (tptr, b)) = Some (TCB tcb); tcb_cap_cases (snd (tptr, b)) = Some (getF, setF, restr); P (getF tcb); kheap s tptr = Some (TCB y)\<rbrakk> \<Longrightarrow> P (getF y)
 2. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; tptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>P slot s. \<lbrakk>\<not> cte_wp_at P slot s; tptr \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb tptr s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(tptr \<mapsto> TCB (the (get_tcb tptr s)\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!