theory KHeap_DR

lemma dcorres_unbind_notification:
  "dcorres dc \<top> (valid_etcbs and not_idle_thread t) (PageTableUnmap_D.unbind_notification t) (IpcCancel_A.unbind_notification t)" apply (simp add: PageTableUnmap_D.unbind_notification_def IpcCancel_A.unbind_notification_def
                   get_bound_notification_def thread_get_def) apply (rule dcorres_gets_the) apply (clarsimp simp: opt_object_tcb transform_tcb_def not_idle_thread_def) apply (frule (1) valid_etcbs_get_tcb_get_etcb) apply (clarsimp simp: opt_cap_tcb tcb_slots infer_tcb_bound_notification_def split: option.splits) apply (clarsimp simp: get_simple_ko_def get_object_def gets_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (clarsimp simp: assert_def corres_free_fail partial_inv_def a_type_def
                  split: Structures_A.kernel_object.splits, safe) apply (rule corres_dummy_return_pl[where b="()"]) apply (rule corres_split_forwards'[where r'=dc and Q="\<lambda>_. \<top>", OF _ _ set_ntfn_exec_wp]) apply (rule corres_dummy_set_notification[THEN corres_guard_imp],simp+) apply (rule corres_guard_imp) apply (rule set_bound_notification_corres[where ntfn_opt=None, unfolded infer_tcb_bound_notification_def
                                      not_idle_thread_def tcb_slots, simplified]) apply simp apply (clarsimp simp: valid_etcbs_def pred_tcb_at_def obj_at_def is_etcb_at_def)[1] apply (rule ccontr, clarsimp) apply (drule ekheap_tcb_at) apply ((clarsimp simp: valid_etcbs_def pred_tcb_at_def obj_at_def is_etcb_at_def is_tcb)+)[2] apply (clarsimp simp: not_idle_thread_def) apply (frule (1) valid_etcbs_get_tcb_get_etcb, clarsimp) apply (clarsimp simp: opt_cap_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_etcbs and not_idle_thread t) (PageTableUnmap_D.unbind_notification t) (IpcCancel_A.unbind_notification t) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_etcbs and not_idle_thread t) (do cap <- KHeap_D.get_cap (t, tcb_boundntfn_slot);
case cap of BoundNotificationCap x \<Rightarrow> PageTableUnmap_D.do_unbind_notification t | _ \<Rightarrow> return ()
od) (do tcb <- gets_the (get_tcb t);
case tcb_bound_notification tcb of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
IpcCancel_A.do_unbind_notification ntfnptr' ntfn t
od
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s' obj obj'. \<lbrakk>s = transform s'; True; (valid_etcbs and not_idle_thread t) s'; get_tcb t s' = Some obj'; opt_cap (t, tcb_boundntfn_slot) s = Some obj\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (case obj of BoundNotificationCap x \<Rightarrow> PageTableUnmap_D.do_unbind_notification t | _ \<Rightarrow> return ()) (case tcb_bound_notification obj' of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
IpcCancel_A.do_unbind_notification ntfnptr' ntfn t
od)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (valid_etcbs and not_idle_thread t) s'; get_tcb t s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (t, tcb_boundntfn_slot) s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>get_tcb t s' = Some obj'; opt_cap (t, tcb_boundntfn_slot) (transform s') = Some obj; valid_etcbs s'; t \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (case obj of BoundNotificationCap x \<Rightarrow> PageTableUnmap_D.do_unbind_notification t | _ \<Rightarrow> return ()) (case tcb_bound_notification obj' of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
IpcCancel_A.do_unbind_notification ntfnptr' ntfn t
od)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (valid_etcbs and not_idle_thread t) s'; get_tcb t s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (t, tcb_boundntfn_slot) s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj obj'. \<lbrakk>get_tcb t s' = Some obj'; opt_cap (t, tcb_boundntfn_slot) (transform s') = Some obj; valid_etcbs s'; t \<noteq> idle_thread s'; \<exists>etcb. get_etcb t s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (case obj of BoundNotificationCap x \<Rightarrow> PageTableUnmap_D.do_unbind_notification t | _ \<Rightarrow> return ()) (case tcb_bound_notification obj' of None \<Rightarrow> return () | Some ntfnptr' \<Rightarrow> do ntfn <- get_notification ntfnptr';
IpcCancel_A.do_unbind_notification ntfnptr' ntfn t
od)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (valid_etcbs and not_idle_thread t) s'; get_tcb t s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (t, tcb_boundntfn_slot) s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' x2 etcb. \<lbrakk>valid_etcbs s'; t \<noteq> idle_thread s'; get_tcb t s' = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (t, 6) cdl_cap.NullCap) (do ntfn <- get_notification x2;
y <- set_notification x2 (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (valid_etcbs and not_idle_thread t) s'; get_tcb t s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (t, tcb_boundntfn_slot) s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' x2 etcb. \<lbrakk>valid_etcbs s'; t \<noteq> idle_thread s'; get_tcb t s' = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (t, 6) cdl_cap.NullCap) (do x <- get;
xa <- assert (\<exists>y. kheap x x2 = Some y);
xa <- assert (a_type (the (kheap x x2)) = AEndpoint \<or> a_type (the (kheap x x2)) = ANTFN);
ntfn <- case partial_inv kernel_object.Notification (the (kheap x x2)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
y <- set_notification x2 (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (valid_etcbs and not_idle_thread t) s'; get_tcb t s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (t, tcb_boundntfn_slot) s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>s' obj' x2 etcb s'a. \<lbrakk>valid_etcbs s'; t \<noteq> idle_thread s'; get_tcb t s' = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s' = Some etcb; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (KHeap_D.set_cap (t, 6) cdl_cap.NullCap) (do x <- assert (\<exists>y. kheap s'a x2 = Some y);
x <- assert (a_type (the (kheap s'a x2)) = AEndpoint \<or> a_type (the (kheap s'a x2)) = ANTFN);
ntfn <- case partial_inv kernel_object.Notification (the (kheap s'a x2)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
y <- set_notification x2 (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od)
 2. \<And>s s'. \<lbrakk>s = transform s'; True; (valid_etcbs and not_idle_thread t) s'; get_tcb t s' \<noteq> None\<rbrakk> \<Longrightarrow> opt_cap (t, tcb_boundntfn_slot) s \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>obj' x2 etcb s'a x4 y. \<lbrakk>valid_etcbs s'a; t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; the (kheap s'a x2) = kernel_object.Notification x4; kheap s'a x2 = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (KHeap_D.set_cap (t, 6) cdl_cap.NullCap) (do y <- set_notification x2 (ntfn_set_bound_tcb x4 None);
set_bound_notification t None
od)
 2. \<And>s s' y. \<lbrakk>True; valid_etcbs s'; not_idle_thread t s'; get_tcb t s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal (2 subgoals):
 1. \<And>obj' x2 etcb s'a x4 y. \<lbrakk>valid_etcbs s'a; t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; the (kheap s'a x2) = kernel_object.Notification x4; kheap s'a x2 = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do return ();
KHeap_D.set_cap (t, 6) cdl_cap.NullCap
od) (do y <- set_notification x2 (ntfn_set_bound_tcb x4 None);
set_bound_notification t None
od)
 2. \<And>s s' y. \<lbrakk>True; valid_etcbs s'; not_idle_thread t s'; get_tcb t s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal (4 subgoals):
 1. \<And>obj' x2 etcb s'a x4 y. \<lbrakk>valid_etcbs s'a; t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; the (kheap s'a x2) = kernel_object.Notification x4; kheap s'a x2 = Some y\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (return ()) (set_notification x2 (ntfn_set_bound_tcb x4 None))
 2. \<And>obj' x2 etcb s'a x4 y. \<lbrakk>valid_etcbs s'a; t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; the (kheap s'a x2) = kernel_object.Notification x4; kheap s'a x2 = Some y\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s'a)\<rbrace> return () \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>obj' x2 etcb s'a x4 y rv ya. \<lbrakk>valid_etcbs s'a; t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; the (kheap s'a x2) = kernel_object.Notification x4; kheap s'a x2 = Some y; dc rv ya\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s'. s' = update_kheap ((kheap s'a)(x2 \<mapsto> kernel_object.Notification (ntfn_set_bound_tcb x4 None))) s'a) (K_bind (KHeap_D.set_cap (t, 6) cdl_cap.NullCap) rv) (set_bound_notification t None)
 4. \<And>s s' y. \<lbrakk>True; valid_etcbs s'; not_idle_thread t s'; get_tcb t s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal (2 subgoals):
 1. \<And>obj' x2 etcb s'a x4 y. \<lbrakk>valid_etcbs s'a; t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; y = kernel_object.Notification x4; kheap s'a x2 = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>s'. s' = update_kheap ((kheap s'a)(x2 \<mapsto> kernel_object.Notification (ntfn_set_bound_tcb x4 None))) s'a) (KHeap_D.set_cap (t, 6) cdl_cap.NullCap) (set_bound_notification t None)
 2. \<And>s s' y. \<lbrakk>True; valid_etcbs s'; not_idle_thread t s'; get_tcb t s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal (4 subgoals):
 1. \<And>obj' x2 etcb s'a x4 y. \<lbrakk>valid_etcbs s'a; t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; y = kernel_object.Notification x4; kheap s'a x2 = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> dcorres dc (?Q94 obj' x2 etcb s'a x4 y) (?Q'94 obj' x2 etcb s'a x4 y) (KHeap_D.set_cap (t, 6) cdl_cap.NullCap) (set_bound_notification t None)
 2. \<And>obj' x2 etcb s'a x4 y s. \<lbrakk>valid_etcbs s'a; t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; y = kernel_object.Notification x4; kheap s'a x2 = Some (kernel_object.Notification x4); True\<rbrakk> \<Longrightarrow> ?Q94 obj' x2 etcb s'a x4 y s
 3. \<And>obj' x2 etcb s'a x4 y s. \<lbrakk>valid_etcbs s'a; t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; y = kernel_object.Notification x4; kheap s'a x2 = Some (kernel_object.Notification x4); s = update_kheap ((kheap s'a)(x2 \<mapsto> kernel_object.Notification (ntfn_set_bound_tcb x4 None))) s'a\<rbrakk> \<Longrightarrow> ?Q'94 obj' x2 etcb s'a x4 y s
 4. \<And>s s' y. \<lbrakk>True; valid_etcbs s'; not_idle_thread t s'; get_tcb t s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal (3 subgoals):
 1. \<And>obj' x2 etcb s'a x4 y s. \<lbrakk>valid_etcbs s'a; t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; y = kernel_object.Notification x4; kheap s'a x2 = Some (kernel_object.Notification x4); True\<rbrakk> \<Longrightarrow> True
 2. \<And>obj' x2 etcb s'a x4 y s. \<lbrakk>valid_etcbs s'a; t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; y = kernel_object.Notification x4; kheap s'a x2 = Some (kernel_object.Notification x4); s = update_kheap ((kheap s'a)(x2 \<mapsto> kernel_object.Notification (ntfn_set_bound_tcb x4 None))) s'a\<rbrakk> \<Longrightarrow> ((\<lambda>s. t \<noteq> idle_thread s) and valid_etcbs and (\<lambda>y. cdl_cap.NullCap = cdl_cap.NullCap)) s
 3. \<And>s s' y. \<lbrakk>True; valid_etcbs s'; not_idle_thread t s'; get_tcb t s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal (2 subgoals):
 1. \<And>obj' x2 etcb s'a x4 y s. \<lbrakk>valid_etcbs s'a; t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; y = kernel_object.Notification x4; kheap s'a x2 = Some (kernel_object.Notification x4); s = update_kheap ((kheap s'a)(x2 \<mapsto> kernel_object.Notification (ntfn_set_bound_tcb x4 None))) s'a\<rbrakk> \<Longrightarrow> ((\<lambda>s. t \<noteq> idle_thread s) and valid_etcbs and (\<lambda>y. cdl_cap.NullCap = cdl_cap.NullCap)) s
 2. \<And>s s' y. \<lbrakk>True; valid_etcbs s'; not_idle_thread t s'; get_tcb t s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal (2 subgoals):
 1. \<And>obj' x2 etcb s'a x4. \<lbrakk>\<forall>ptr. (\<exists>ko. kheap s'a ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s'a ptr = Some y); t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; kheap s'a x2 = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> ekheap s'a x2 = None
 2. \<And>s s' y. \<lbrakk>True; valid_etcbs s'; not_idle_thread t s'; get_tcb t s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal (2 subgoals):
 1. \<And>obj' x2 etcb s'a x4 y. \<lbrakk>\<forall>ptr. (\<exists>ko. kheap s'a ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s'a ptr = Some y); t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; kheap s'a x2 = Some (kernel_object.Notification x4); ekheap s'a x2 = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' y. \<lbrakk>True; valid_etcbs s'; not_idle_thread t s'; get_tcb t s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal (3 subgoals):
 1. \<And>obj' x2 etcb s'a x4 y. \<lbrakk>\<forall>ptr. (\<exists>ko. kheap s'a ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s'a ptr = Some y); t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; kheap s'a x2 = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> valid_etcbs s'a
 2. \<And>obj' x2 etcb s'a x4 y. \<lbrakk>\<forall>ptr. (\<exists>ko. kheap s'a ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s'a ptr = Some y); t \<noteq> idle_thread s'a; get_tcb t s'a = Some obj'; tcb_bound_notification obj' = Some x2; get_etcb t s'a = Some etcb; kheap s'a x2 = Some (kernel_object.Notification x4); tcb_at x2 s'a\<rbrakk> \<Longrightarrow> False
 3. \<And>s s' y. \<lbrakk>True; valid_etcbs s'; not_idle_thread t s'; get_tcb t s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal (1 subgoal):
 1. \<And>s s' y. \<lbrakk>True; valid_etcbs s'; not_idle_thread t s'; get_tcb t s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal (1 subgoal):
 1. \<And>s' y. \<lbrakk>valid_etcbs s'; t \<noteq> idle_thread s'; get_tcb t s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal (1 subgoal):
 1. \<And>s' y etcb. \<lbrakk>valid_etcbs s'; t \<noteq> idle_thread s'; get_tcb t s' = Some y; get_etcb t s' = Some etcb\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (t, tcb_boundntfn_slot) (transform s') = Some y proof (prove)
goal:
No subgoals!