theory TcbAcc_R

lemma sbn'_valid_pspace'_inv[wp]:
  "\<lbrace> valid_pspace' and tcb_at' t and valid_bound_ntfn' ntfn \<rbrace>
  setBoundNotification ntfn t
  \<lbrace> \<lambda>rv. valid_pspace' \<rbrace>" apply (simp add: valid_pspace'_def) apply (rule hoare_pre) apply (wp sbn_valid_objs') apply (simp add: setBoundNotification_def threadSet_def bind_assoc valid_mdb'_def) apply (wp getObject_obj_at_tcb | simp)+ apply (clarsimp simp: valid_mdb'_def) apply (drule obj_at_ko_at') apply clarsimp apply (erule obj_at'_weakenE) apply (simp add: tcb_cte_cases_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace' and tcb_at' t and valid_bound_ntfn' ntfn\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' t and valid_bound_ntfn' ntfn\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace>
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' t and valid_bound_ntfn' ntfn) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'8\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s\<rbrace>
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' t and valid_bound_ntfn' ntfn) s \<Longrightarrow> (valid_objs' and valid_bound_ntfn' ntfn) s \<and> ?P'8 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'8\<rbrace> do tcb <- getObject t;
setObject t (tcbBoundNotification_update (\<lambda>_. ntfn) tcb)
od \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb_ctes (ctes_of s)\<rbrace>
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and tcb_at' t and valid_bound_ntfn' ntfn) s \<Longrightarrow> (valid_objs' and valid_bound_ntfn' ntfn) s \<and> ?P'8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> tcb_at' t s \<and> valid_bound_ntfn' ntfn s \<Longrightarrow> valid_mdb_ctes (ctes_of s) \<and> obj_at' (\<lambda>t. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF t = getF (tcbBoundNotification_update (\<lambda>_. ntfn) t)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); tcb_at' t s; valid_bound_ntfn' ntfn s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>t. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF t = getF (tcbBoundNotification_update (\<lambda>_. ntfn) t)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); valid_bound_ntfn' ntfn s; \<exists>ko. ko_at' ko t s \<and> True\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>t. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF t = getF (tcbBoundNotification_update (\<lambda>_. ntfn) t)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); valid_bound_ntfn' ntfn s; ko_at' ko t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>t. \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF t = getF (tcbBoundNotification_update (\<lambda>_. ntfn) t)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s ko k. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb_ctes (ctes_of s); valid_bound_ntfn' ntfn s; k = ko\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF k = getF (tcbBoundNotification_update (\<lambda>_. ntfn) k) proof (prove)
goal:
No subgoals!