theory Tcb_DR

lemma dcorres_bind_notification:
  "dcorres dc (\<lambda>_. True) (valid_etcbs and not_idle_thread t)
   (Tcb_D.bind_notification t a) (Tcb_A.bind_notification t a)" apply (clarsimp simp: Tcb_D.bind_notification_def Tcb_A.bind_notification_def
                        get_simple_ko_def get_object_def gets_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (simp split: option.splits) apply (clarsimp simp: assert_def corres_free_fail partial_inv_def a_type_def
                 split: Structures_A.kernel_object.splits) apply (rule corres_dummy_return_pl) apply (rule corres_guard_imp) apply (rule corres_split[OF corres_dummy_set_notification], simp) apply (rule set_bound_notification_corres) apply (wp |simp add: not_idle_thread_def infer_tcb_bound_notification_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_etcbs and not_idle_thread t) (Tcb_D.bind_notification t a) (Tcb_A.bind_notification t a) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_etcbs and not_idle_thread t) (KHeap_D.set_cap (t, tcb_boundntfn_slot) (BoundNotificationCap a)) (do x <- get;
xa <- assert (\<exists>y. kheap x a = Some y);
xa <- assert (a_type (the (kheap x a)) = AEndpoint \<or> a_type (the (kheap x a)) = ANTFN);
ntfn <- case partial_inv kernel_object.Notification (the (kheap x a)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
y <- set_notification a (ntfn_set_bound_tcb ntfn (Some t));
set_bound_notification t (Some a)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (valid_etcbs and not_idle_thread t) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (t, tcb_boundntfn_slot) (BoundNotificationCap a)) (do x <- assert (\<exists>y. kheap s' a = Some y);
x <- assert (a_type (the (kheap s' a)) = AEndpoint \<or> a_type (the (kheap s' a)) = ANTFN);
ntfn <- case partial_inv kernel_object.Notification (the (kheap s' a)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
y <- set_notification a (ntfn_set_bound_tcb ntfn (Some t));
set_bound_notification t (Some a)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. valid_etcbs s' \<and> not_idle_thread t s' \<Longrightarrow> (partial_inv kernel_object.Notification (the (kheap s' a)) = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (t, tcb_boundntfn_slot) (BoundNotificationCap a)) (do x <- assert (\<exists>y. kheap s' a = Some y);
x <- assert (a_type (the (kheap s' a)) = AEndpoint \<or> a_type (the (kheap s' a)) = ANTFN);
fail
od)) \<and> (\<forall>x2. kernel_object.Notification x2 = the (kheap s' a) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (t, tcb_boundntfn_slot) (BoundNotificationCap a)) (do x <- assert (\<exists>y. kheap s' a = Some y);
x <- assert (a_type (the (kheap s' a)) = AEndpoint \<or> a_type (the (kheap s' a)) = ANTFN);
y <- set_notification a (ntfn_set_bound_tcb x2 (Some t));
set_bound_notification t (Some a)
od)) proof (prove)
goal (1 subgoal):
 1. \<And>s' x4. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (t, tcb_boundntfn_slot) (BoundNotificationCap a)) (do y <- set_notification a (ntfn_set_bound_tcb x4 (Some t));
set_bound_notification t (Some a)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x4. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do return (?b30 s' x4);
KHeap_D.set_cap (t, tcb_boundntfn_slot) (BoundNotificationCap a)
od) (do y <- set_notification a (ntfn_set_bound_tcb x4 (Some t));
set_bound_notification t (Some a)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s' x4. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> dcorres dc (?Q32 s' x4) (?Q'32 s' x4) (do return (?b30 s' x4);
KHeap_D.set_cap (t, tcb_boundntfn_slot) (BoundNotificationCap a)
od) (do y <- set_notification a (ntfn_set_bound_tcb x4 (Some t));
set_bound_notification t (Some a)
od)
 2. \<And>s' x4 s. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4); transform s' = s\<rbrakk> \<Longrightarrow> ?Q32 s' x4 s
 3. \<And>s' x4 s. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4); s' = s\<rbrakk> \<Longrightarrow> ?Q'32 s' x4 s proof (prove)
goal (5 subgoals):
 1. \<And>s' x4 rv. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> dcorres dc (?R36 s' x4 rv) (?R'36 s' x4 ()) (KHeap_D.set_cap (t, tcb_boundntfn_slot) (BoundNotificationCap a)) (set_bound_notification t (Some a))
 2. \<And>s' x4. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> \<lbrace>?Q36 s' x4\<rbrace> return (?b30 s' x4) \<lbrace>?R36 s' x4\<rbrace>
 3. \<And>s' x4. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'36 s' x4\<rbrace> set_notification a (ntfn_set_bound_tcb x4 (Some t)) \<lbrace>?R'36 s' x4\<rbrace>
 4. \<And>s' x4 s. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4); transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q36 s' x4) s
 5. \<And>s' x4 s. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4); s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'36 s' x4) s proof (prove)
goal (4 subgoals):
 1. \<And>s' x4. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> \<lbrace>?Q36 s' x4\<rbrace> return (?b30 s' x4) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>s' x4. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'36 s' x4\<rbrace> set_notification a (ntfn_set_bound_tcb x4 (Some t)) \<lbrace>\<lambda>b. not_idle_thread t and valid_etcbs and K (BoundNotificationCap a = infer_tcb_bound_notification (Some a))\<rbrace>
 3. \<And>s' x4 s. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4); transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q36 s' x4) s
 4. \<And>s' x4 s. \<lbrakk>valid_etcbs s'; not_idle_thread t s'; kheap s' a = Some (kernel_object.Notification x4); s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'36 s' x4) s proof (prove)
goal:
No subgoals!