theory Ipc_AI

lemma complete_signal_invs:
  "\<lbrace>invs and tcb_at tcb\<rbrace>
     complete_signal ntfnptr tcb
   \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: complete_signal_def) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (rule hoare_pre) apply (wp set_ntfn_minor_invs | wpc | simp)+ apply (rule_tac Q="\<lambda>_ s. (state_refs_of s ntfnptr = ntfn_bound_refs (ntfn_bound_tcb ntfn))
                      \<and> (\<exists>T. typ_at T ntfnptr s) \<and> valid_ntfn (ntfn_set_obj ntfn IdleNtfn) s
                      \<and> ((\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> ex_nonz_cap_to ntfnptr s)"
                      in hoare_strengthen_post) apply (wp hoare_vcg_all_lift hoare_weak_lift_imp hoare_vcg_ex_lift | wpc
         | simp add: live_def valid_ntfn_def valid_bound_tcb_def split: option.splits)+ apply ((clarsimp simp: obj_at_def state_refs_of_def)+)[2] apply (rule_tac obj_at_valid_objsE[OF _ invs_valid_objs]; clarsimp) apply assumption+ by (fastforce simp: ko_at_state_refs_ofD valid_ntfn_def valid_obj_def obj_at_def is_ntfn live_def elim: if_live_then_nonz_capD[OF invs_iflive])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at tcb\<rbrace> complete_signal ntfnptr tcb \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at tcb\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user tcb $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ntfnptr and (invs and tcb_at tcb)\<rbrace> case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user tcb $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q4 ntfn\<rbrace> case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user tcb $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail \<lbrace>\<lambda>_. invs\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and (invs and tcb_at tcb)) s \<Longrightarrow> ?Q4 ntfn s proof (prove)
goal (2 subgoals):
 1. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?P'42 ntfn x3\<rbrace> as_user tcb (setRegister badge_register x3) \<lbrace>\<lambda>rv s. obj_at (\<lambda>ko. refs_of ko = ntfn_bound_refs (ntfn_bound_tcb ntfn)) ntfnptr s \<and> valid_ntfn (ntfn_set_obj ntfn IdleNtfn) s \<and> (live (Notification (ntfn_set_obj ntfn IdleNtfn)) \<longrightarrow> ex_nonz_cap_to ntfnptr s)\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and (invs and tcb_at tcb)) s \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> invs s \<and> ntfn_at ntfnptr s \<and> ?P'42 ntfn x s) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x3. ntfn_obj ntfn = ActiveNtfn x3 \<Longrightarrow> \<lbrace>?P'42 ntfn x3\<rbrace> as_user tcb (setRegister badge_register x3) \<lbrace>\<lambda>_ s. state_refs_of s ntfnptr = ntfn_bound_refs (ntfn_bound_tcb ntfn) \<and> (\<exists>T. typ_at T ntfnptr s) \<and> valid_ntfn (ntfn_set_obj ntfn IdleNtfn) s \<and> ((\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> ex_nonz_cap_to ntfnptr s)\<rbrace>
 2. \<And>ntfn x3 rv s. \<lbrakk>ntfn_obj ntfn = ActiveNtfn x3; state_refs_of s ntfnptr = ntfn_bound_refs (ntfn_bound_tcb ntfn) \<and> (\<exists>T. typ_at T ntfnptr s) \<and> valid_ntfn (ntfn_set_obj ntfn IdleNtfn) s \<and> ((\<exists>y. ntfn_bound_tcb ntfn = Some y) \<longrightarrow> ex_nonz_cap_to ntfnptr s)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. refs_of ko = ntfn_bound_refs (ntfn_bound_tcb ntfn)) ntfnptr s \<and> valid_ntfn (ntfn_set_obj ntfn IdleNtfn) s \<and> (live (Notification (ntfn_set_obj ntfn IdleNtfn)) \<longrightarrow> ex_nonz_cap_to ntfnptr s)
 3. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and (invs and tcb_at tcb)) s \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> invs s \<and> ntfn_at ntfnptr s \<and> ?P'42 ntfn x s) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn x3 s. \<lbrakk>ntfn_obj ntfn = ActiveNtfn x3; ntfn_bound_tcb ntfn = None; state_refs_of s ntfnptr = {} \<and> (\<exists>T. typ_at T ntfnptr s)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. refs_of ko = {}) ntfnptr s
 2. \<And>ntfn x3 s x2. \<lbrakk>ntfn_obj ntfn = ActiveNtfn x3; ntfn_bound_tcb ntfn = Some x2; state_refs_of s ntfnptr = {(x2, NTFNBound)} \<and> (\<exists>T. typ_at T ntfnptr s) \<and> tcb_at x2 s \<and> ex_nonz_cap_to ntfnptr s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. refs_of ko = {(x2, NTFNBound)}) ntfnptr s
 3. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and (invs and tcb_at tcb)) s \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> invs s \<and> ntfn_at ntfnptr s \<and> state_refs_of s ntfnptr = ntfn_bound_refs (ntfn_bound_tcb ntfn) \<and> (\<exists>x. typ_at x ntfnptr s) \<and> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> tcb_at x s \<and> ex_nonz_cap_to ntfnptr s)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and (invs and tcb_at tcb)) s \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> True) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> invs s \<and> ntfn_at ntfnptr s \<and> state_refs_of s ntfnptr = ntfn_bound_refs (ntfn_bound_tcb ntfn) \<and> (\<exists>x. typ_at x ntfnptr s) \<and> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> tcb_at x s \<and> ex_nonz_cap_to ntfnptr s)) proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; invs s; tcb_at tcb s\<rbrakk> \<Longrightarrow> obj_at (?P99 ntfn s) (?p99 ntfn s) (?s99 ntfn s)
 2. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; invs s; tcb_at tcb s\<rbrakk> \<Longrightarrow> invs (?s99 ntfn s)
 3. \<And>ntfn s ko x. \<lbrakk>kheap (?s99 ntfn s) (?p99 ntfn s) = Some ko; ?P99 ntfn s ko; valid_obj (?p99 ntfn s) ko (?s99 ntfn s); ko_at (Notification ntfn) ntfnptr s; invs s; tcb_at tcb s; ntfn_obj ntfn = ActiveNtfn x\<rbrakk> \<Longrightarrow> ntfn_at ntfnptr s \<and> state_refs_of s ntfnptr = ntfn_bound_refs (ntfn_bound_tcb ntfn) \<and> (\<exists>x. typ_at x ntfnptr s) \<and> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> tcb_at x s \<and> ex_nonz_cap_to ntfnptr s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s ko x. \<lbrakk>kheap s ntfnptr = Some ko; Notification ntfn = ko; valid_obj ntfnptr ko s; ko_at (Notification ntfn) ntfnptr s; invs s; tcb_at tcb s; ntfn_obj ntfn = ActiveNtfn x\<rbrakk> \<Longrightarrow> ntfn_at ntfnptr s \<and> state_refs_of s ntfnptr = ntfn_bound_refs (ntfn_bound_tcb ntfn) \<and> (\<exists>x. typ_at x ntfnptr s) \<and> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> tcb_at x s \<and> ex_nonz_cap_to ntfnptr s)