theory Ipc_DR

lemma dcorres_complete_signal:
  "dcorres dc \<top> (valid_idle and not_idle_thread thread and valid_etcbs) (corrupt_tcb_intent thread)
           (complete_signal aa thread)" apply (clarsimp simp: complete_signal_def get_simple_ko_def get_object_def gets_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (clarsimp split: option.splits) apply (clarsimp simp: assert_def corres_free_fail partial_inv_def a_type_def
          split: Structures_A.kernel_object.splits Structures_A.ntfn.splits) apply (rule corres_guard_imp) apply (rule corres_dummy_return_l) apply (rule corres_split[OF set_register_corres corres_dummy_set_notification]) apply (wp | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and not_idle_thread thread and valid_etcbs) (corrupt_tcb_intent thread) (complete_signal aa thread) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and not_idle_thread thread and valid_etcbs) (corrupt_tcb_intent thread) (do x <- get;
xa <- assert (\<exists>y. kheap x aa = Some y);
xa <- assert (a_type (the (kheap x aa)) = AEndpoint \<or> a_type (the (kheap x aa)) = ANTFN);
ntfn <- case partial_inv kernel_object.Notification (the (kheap x aa)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification aa $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>True; (valid_idle and not_idle_thread thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent thread) (do x <- assert (\<exists>y. kheap s' aa = Some y);
x <- assert (a_type (the (kheap s' aa)) = AEndpoint \<or> a_type (the (kheap s' aa)) = ANTFN);
ntfn <- case partial_inv kernel_object.Notification (the (kheap s' aa)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification aa $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>valid_idle s'; not_idle_thread thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (partial_inv kernel_object.Notification (the (kheap s' aa)) = None \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent thread) (do x <- assert (\<exists>y. kheap s' aa = Some y);
x <- assert (a_type (the (kheap s' aa)) = AEndpoint \<or> a_type (the (kheap s' aa)) = ANTFN);
fail
od)) \<and> (\<forall>x2. kernel_object.Notification x2 = the (kheap s' aa) \<longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent thread) (do x <- assert (\<exists>y. kheap s' aa = Some y);
x <- assert (a_type (the (kheap s' aa)) = AEndpoint \<or> a_type (the (kheap s' aa)) = ANTFN);
case ntfn_obj x2 of ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification aa $ ntfn_set_obj x2 IdleNtfn
od | _ \<Rightarrow> fail
od)) proof (prove)
goal (1 subgoal):
 1. \<And>s' x4 x3. \<lbrakk>valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; ntfn_obj x4 = ActiveNtfn x3; kheap s' aa = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification aa (ntfn_set_obj x4 IdleNtfn)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s' x4 x3. \<lbrakk>valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; ntfn_obj x4 = ActiveNtfn x3; kheap s' aa = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> dcorres dc (?Q40 s' x4 x3) (?Q'40 s' x4 x3) (corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification aa (ntfn_set_obj x4 IdleNtfn)
od)
 2. \<And>s' x4 x3 s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; ntfn_obj x4 = ActiveNtfn x3; kheap s' aa = Some (kernel_object.Notification x4); transform s' = s\<rbrakk> \<Longrightarrow> ?Q40 s' x4 x3 s
 3. \<And>s' x4 x3 s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; ntfn_obj x4 = ActiveNtfn x3; kheap s' aa = Some (kernel_object.Notification x4); s' = s\<rbrakk> \<Longrightarrow> ?Q'40 s' x4 x3 s proof (prove)
goal (3 subgoals):
 1. \<And>s' x4 x3. \<lbrakk>valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; ntfn_obj x4 = ActiveNtfn x3; kheap s' aa = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> dcorres dc (?Q40 s' x4 x3) (?Q'40 s' x4 x3) (corrupt_tcb_intent thread >>= return) (do y <- as_user thread (setRegister badge_register x3);
set_notification aa (ntfn_set_obj x4 IdleNtfn)
od)
 2. \<And>s' x4 x3 s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; ntfn_obj x4 = ActiveNtfn x3; kheap s' aa = Some (kernel_object.Notification x4); transform s' = s\<rbrakk> \<Longrightarrow> ?Q40 s' x4 x3 s
 3. \<And>s' x4 x3 s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; ntfn_obj x4 = ActiveNtfn x3; kheap s' aa = Some (kernel_object.Notification x4); s' = s\<rbrakk> \<Longrightarrow> ?Q'40 s' x4 x3 s proof (prove)
goal (4 subgoals):
 1. \<And>s' x4 x3. \<lbrakk>valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; ntfn_obj x4 = ActiveNtfn x3; kheap s' aa = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> \<lbrace>?Q46 s' x4 x3\<rbrace> corrupt_tcb_intent thread \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>s' x4 x3. \<lbrakk>valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; ntfn_obj x4 = ActiveNtfn x3; kheap s' aa = Some (kernel_object.Notification x4)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'46 s' x4 x3\<rbrace> as_user thread (setRegister badge_register x3) \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>s' x4 x3 s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; ntfn_obj x4 = ActiveNtfn x3; kheap s' aa = Some (kernel_object.Notification x4); transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q46 s' x4 x3) s
 4. \<And>s' x4 x3 s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; valid_etcbs s'; ntfn_obj x4 = ActiveNtfn x3; kheap s' aa = Some (kernel_object.Notification x4); s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread thread and valid_etcbs and ?Q'46 s' x4 x3) s proof (prove)
goal:
No subgoals!