theory KHeap_DR

lemma dcorres_ntfn_bound_tcb:
  "dcorres (\<lambda>rv rv'. rv = set_option (ntfn_bound_tcb rv'))  \<top> (valid_state and valid_etcbs)
     (gets $ get_bound_notification_threads ntfn)
     (get_notification ntfn)" apply (clarsimp simp: gets_def get_simple_ko_def
                  get_object_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (rule dcorres_absorb_get_l) apply (clarsimp simp: assert_def corres_free_fail a_type_def partial_inv_def
                 split: Structures_A.kernel_object.splits, rule conjI, clarsimp+) apply (frule get_notification_pick, simp) apply (clarsimp simp: valid_ntfn_abstract_def ntfn_bound_set_lift valid_state_def option_select_def split del: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>rv rv'. rv = set_option (ntfn_bound_tcb rv')) (\<lambda>_. True) (valid_state and valid_etcbs) (gets $ get_bound_notification_threads ntfn) (get_notification ntfn) proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>rv rv'. rv = set_option (ntfn_bound_tcb rv')) (\<lambda>_. True) (valid_state and valid_etcbs) (do s <- get;
return (get_bound_notification_threads ntfn s)
od) (do x <- get;
y <- assert (\<exists>y. kheap x ntfn = Some y);
y <- assert (a_type (the (kheap x ntfn)) = AEndpoint \<or> a_type (the (kheap x ntfn)) = ANTFN);
case partial_inv kernel_object.Notification (the (kheap x ntfn)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (valid_state and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = set_option (ntfn_bound_tcb rv')) ((=) (transform s')) ((=) s') (do s <- get;
return (get_bound_notification_threads ntfn s)
od) (do y <- assert (\<exists>y. kheap s' ntfn = Some y);
y <- assert (a_type (the (kheap s' ntfn)) = AEndpoint \<or> a_type (the (kheap s' ntfn)) = ANTFN);
case partial_inv kernel_object.Notification (the (kheap s' ntfn)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a. \<lbrakk>True; (valid_state and valid_etcbs) s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = set_option (ntfn_bound_tcb rv')) ((=) (transform s'a)) ((=) s'a) (return (get_bound_notification_threads ntfn (transform s'a))) (do y <- assert (\<exists>y. kheap s' ntfn = Some y);
y <- assert (a_type (the (kheap s' ntfn)) = AEndpoint \<or> a_type (the (kheap s' ntfn)) = ANTFN);
case partial_inv kernel_object.Notification (the (kheap s' ntfn)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'a x4. \<lbrakk>valid_state s'a; valid_etcbs s'a; kheap s'a ntfn = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> get_bound_notification_threads ntfn (transform s'a) = set_option (ntfn_bound_tcb x4) proof (prove)
goal (1 subgoal):
 1. \<And>s'a x4. \<lbrakk>valid_state s'a; valid_etcbs s'a; kheap s'a ntfn = Some (kernel_object.Notification x4); valid_ntfn_abstract x4 ntfn s'a\<rbrakk> \<Longrightarrow> get_bound_notification_threads ntfn (transform s'a) = set_option (ntfn_bound_tcb x4) proof (prove)
goal:
No subgoals!