theory Syscall_AI

lemma complete_signal_state_refs_of:
  "\<lbrace>\<lambda>s. P (state_refs_of s) \<rbrace> complete_signal ntfnc t \<lbrace>\<lambda>rv s. P (state_refs_of s) \<rbrace>" unfolding complete_signal_def apply (rule hoare_pre) apply (wp get_simple_ko_wp | wpc | simp)+ apply clarsimp apply (subgoal_tac " ntfn_bound_refs (ntfn_bound_tcb ntfn) = state_refs_of s ntfnc") apply (clarsimp simp: if_apply_def2 split: if_splits if_split_asm) subgoal by (subst eq_commute, auto cong: if_cong) apply (clarsimp simp: state_refs_of_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> complete_signal ntfnc t \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> do ntfn <- get_notification ntfnc;
case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfnc $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do ntfn <- get_notification ntfnc;
case ntfn_obj ntfn of ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfnc $ ntfn_set_obj ntfn IdleNtfn
od | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>
 2. \<And>s. P (state_refs_of s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (state_refs_of s) \<Longrightarrow> \<forall>ntfn. ko_at (Notification ntfn) ntfnc s \<longrightarrow> (\<exists>x. ntfn_obj ntfn = ActiveNtfn x) \<longrightarrow> P (\<lambda>a. if a = ntfnc then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>P (state_refs_of s); ko_at (Notification ntfn) ntfnc s; ntfn_obj ntfn = ActiveNtfn x\<rbrakk> \<Longrightarrow> P (\<lambda>a. if a = ntfnc then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x. \<lbrakk>P (state_refs_of s); ko_at (Notification ntfn) ntfnc s; ntfn_obj ntfn = ActiveNtfn x; ntfn_bound_refs (ntfn_bound_tcb ntfn) = state_refs_of s ntfnc\<rbrakk> \<Longrightarrow> P (\<lambda>a. if a = ntfnc then ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a)
 2. \<And>s ntfn x. \<lbrakk>P (state_refs_of s); ko_at (Notification ntfn) ntfnc s; ntfn_obj ntfn = ActiveNtfn x\<rbrakk> \<Longrightarrow> ntfn_bound_refs (ntfn_bound_tcb ntfn) = state_refs_of s ntfnc proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x. \<lbrakk>P (state_refs_of s); ko_at (Notification ntfn) ntfnc s; ntfn_obj ntfn = ActiveNtfn x; ntfn_bound_refs (ntfn_bound_tcb ntfn) = state_refs_of s ntfnc\<rbrakk> \<Longrightarrow> P (\<lambda>a. if a = ntfnc then state_refs_of s ntfnc else state_refs_of s a)
 2. \<And>s ntfn x. \<lbrakk>P (state_refs_of s); ko_at (Notification ntfn) ntfnc s; ntfn_obj ntfn = ActiveNtfn x\<rbrakk> \<Longrightarrow> ntfn_bound_refs (ntfn_bound_tcb ntfn) = state_refs_of s ntfnc proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (state_refs_of s_); ko_at (Notification ntfn_) ntfnc s_; ntfn_obj ntfn_ = ActiveNtfn x_; ntfn_bound_refs (ntfn_bound_tcb ntfn_) = state_refs_of s_ ntfnc\<rbrakk> \<Longrightarrow> P (\<lambda>a. if a = ntfnc then state_refs_of s_ ntfnc else state_refs_of s_ a) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>P (state_refs_of s); ko_at (Notification ntfn) ntfnc s; ntfn_obj ntfn = ActiveNtfn x\<rbrakk> \<Longrightarrow> ntfn_bound_refs (ntfn_bound_tcb ntfn) = state_refs_of s ntfnc proof (prove)
goal:
No subgoals!