kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_AI

lemma set_mrs_def2:
  "set_mrs thread buf msgs \<equiv>
   do thread_set
        (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers
                     (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers)
                           then msgs ! the_index msg_registers reg
                           else (arch_tcb_get_registers o tcb_arch) tcb reg) (tcb_arch tcb)\<rparr>)
        thread;
      remaining_msgs \<leftarrow> return (drop (length msg_registers) msgs);
      case buf of
      None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length msgs))
      | Some pptr \<Rightarrow>
          do zipWithM_x (store_word_offs pptr)
              [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
             return $ nat_to_len $ min (length msgs) msg_max_length
          od
   od" by (rule eq_reflection) (simp add: set_mrs_def thread_set_def bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_mrs thread buf msgs \<equiv> do thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else (arch_tcb_get_registers \<circ> tcb_arch) tcb reg) (tcb_arch tcb)\<rparr>) thread;
remaining_msgs <- return (drop (length msg_registers) msgs);
case buf of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length msgs)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length msgs) msg_max_length
od
od
theory Ipc_AI

lemma set_mrs_vms[wp]:
  notes if_split [split del]
  shows "\<And>thread buf msgs.
    \<lbrace>valid_machine_state::'state_ext state \<Rightarrow> bool\<rbrace>
      set_mrs thread buf msgs
    \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" unfolding set_mrs_def2 by (wpsimp simp: zipWithM_x_mapM_x split_def
               wp: mapM_x_wp_inv hoare_vcg_all_lift hoare_drop_imps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>thread buf msgs. \<lbrace>valid_machine_state\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>thread buf msgs. \<lbrace>valid_machine_state\<rbrace> do thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else (arch_tcb_get_registers \<circ> tcb_arch) tcb reg) (tcb_arch tcb)\<rparr>) thread;
remaining_msgs <- return (drop (length msg_registers) msgs);
case buf of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length msgs)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length msgs) msg_max_length
od
od \<lbrace>\<lambda>_. valid_machine_state\<rbrace>
theory Ipc_AI

lemma do_ipc_transfer_invs[wp]:
  "\<lbrace>invs and tcb_at r and tcb_at s :: 'state_ext state \<Rightarrow> bool\<rbrace>
   do_ipc_transfer s ep bg grt r
   \<lbrace>\<lambda>rv. invs\<rbrace>" unfolding do_ipc_transfer_def apply (wpsimp simp: do_normal_transfer_def transfer_caps_def bind_assoc ball_conj_distrib
                  wp:  hoare_drop_imps get_rs_cte_at2 thread_get_wp
                       hoare_vcg_ball_lift hoare_vcg_all_lift hoare_vcg_conj_lift) apply (clarsimp simp: obj_at_def is_tcb invs_valid_objs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at r and tcb_at s\<rbrace> do_ipc_transfer s ep bg grt r \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at r and tcb_at s\<rbrace> do recv_buffer <- lookup_ipc_buffer True r;
fault <- thread_get tcb_fault s;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r recv_buffer
od | Some f \<Rightarrow> do_fault_transfer bg s r recv_buffer
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>invs sa; tcb_at r sa; tcb_at s sa\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. (\<exists>tcb. ko = TCB tcb) \<and> valid_objs sa) s sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma dit_tcb_at [wp]:
  "\<And>t s ep bg grt r.
    \<lbrace>tcb_at t :: 'state_ext state \<Rightarrow> bool\<rbrace>
      do_ipc_transfer s ep bg grt r
    \<lbrace>\<lambda>rv. tcb_at t\<rbrace>" by (simp add: tcb_at_typ) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>t s ep bg grt r. \<lbrace>tcb_at t\<rbrace> do_ipc_transfer s ep bg grt r \<lbrace>\<lambda>rv. tcb_at t\<rbrace>
theory Ipc_AI

lemma dit_cte_at [wp]:
  "\<And>t s ep bg grt r.
    \<lbrace>cte_at t :: 'state_ext state \<Rightarrow> bool\<rbrace>
      do_ipc_transfer s ep bg grt r
    \<lbrace>\<lambda>rv. cte_at t\<rbrace>" by (wp valid_cte_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>t s ep bg grt r. \<lbrace>cte_wp_at (\<lambda>_. True) t\<rbrace> do_ipc_transfer s ep bg grt r \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) t\<rbrace>
theory Ipc_AI

lemma (in Ipc_AI) handle_fault_reply_typ_at[wp]:
  "\<lbrace>\<lambda>s :: 'state_ext state. P (typ_at T p s)\<rbrace> handle_fault_reply ft t label msg \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" by(cases ft, simp_all, wp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> handle_fault_reply ft t label msg \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
theory Ipc_AI

lemma (in Ipc_AI) handle_fault_reply_cte[wp]:
  "\<lbrace>cte_at t' :: 'state_ext state \<Rightarrow> bool\<rbrace> handle_fault_reply ft t label msg \<lbrace>\<lambda>rv. cte_at t'\<rbrace>" by (wp valid_cte_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) t'\<rbrace> handle_fault_reply ft t label msg \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) t'\<rbrace>
theory Ipc_AI

lemma do_ipc_transfer_non_null_cte_wp_at:
  fixes P ptr st ep b gr rt
  assumes imp: "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c"
  shows
  "\<lbrace>valid_objs and cte_wp_at (P and ((\<noteq>) cap.NullCap)) ptr :: 'state_ext state \<Rightarrow> bool\<rbrace>
   do_ipc_transfer st ep b gr rt
   \<lbrace>\<lambda>_. cte_wp_at (P and ((\<noteq>) cap.NullCap)) ptr\<rbrace>" unfolding do_ipc_transfer_def apply (wp do_normal_transfer_non_null_cte_wp_at hoare_drop_imp hoare_allI
    | wpc | simp add:imp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr\<rbrace> do_ipc_transfer st ep b gr rt \<lbrace>\<lambda>_. cte_wp_at (P and (\<noteq>) NullCap) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at (P and (\<noteq>) NullCap) ptr\<rbrace> do recv_buffer <- lookup_ipc_buffer True rt;
fault <- thread_get tcb_fault st;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False st;
do_normal_transfer st send_buffer ep b gr rt recv_buffer
od | Some f \<Rightarrow> do_fault_transfer b st rt recv_buffer
od \<lbrace>\<lambda>_. cte_wp_at (P and (\<noteq>) NullCap) ptr\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma thread_get_tcb_at:
  "\<lbrace>\<top>\<rbrace> thread_get f tptr \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>" unfolding thread_get_def by (wp, clarsimp simp add: get_tcb_ko_at tcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> thread_get f tptr \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do tcb <- gets_the $ get_tcb tptr;
return $ f tcb
od \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>
theory Ipc_AI

lemma cap_delete_one_tcb_at [wp]:
  "\<lbrace>\<lambda>s. P (tcb_at p s)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s'. P (tcb_at p s')\<rbrace>" by (clarsimp simp add: tcb_at_typ, rule cap_delete_one_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (tcb_at p s)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s'. P (tcb_at p s')\<rbrace>
theory Ipc_AI

lemma cap_delete_one_ep_at [wp]:
  "\<lbrace>\<lambda>s. P (ep_at word s)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s'. P (ep_at word s')\<rbrace>" by (simp add: ep_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ep_at word s)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s'. P (ep_at word s')\<rbrace>
theory Ipc_AI

lemma cap_delete_one_ntfn_at [wp]:
  "\<lbrace>\<lambda>s. P (ntfn_at word s)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s'. P (ntfn_at word s')\<rbrace>" by (simp add: ntfn_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ntfn_at word s)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s'. P (ntfn_at word s')\<rbrace>
theory Ipc_AI

lemma cap_delete_one_valid_tcb_state:
  "\<lbrace>\<lambda>s. P (valid_tcb_state st s)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s'. P (valid_tcb_state st s')\<rbrace>" apply (simp add: valid_tcb_state_def) apply (cases st, (wp | simp)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (valid_tcb_state st s)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s'. P (valid_tcb_state st s')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (case st of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s | BlockedOnSend ref sp \<Rightarrow> ep_at ref s | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s | _ \<Rightarrow> True)\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s'. P (case st of BlockedOnReceive ref sp \<Rightarrow> ep_at ref s' | BlockedOnSend ref sp \<Rightarrow> ep_at ref s' | BlockedOnNotification ref \<Rightarrow> ntfn_at ref s' | _ \<Rightarrow> True)\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma cte_wp_at_reply_cap_can_fast_finalise:
  "cte_wp_at ((=) (cap.ReplyCap tcb v R)) slot s \<longrightarrow> cte_wp_at can_fast_finalise slot s" by (clarsimp simp: cte_wp_at_caps_of_state can_fast_finalise_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at ((=) (ReplyCap tcb v R)) slot s \<longrightarrow> cte_wp_at can_fast_finalise slot s
theory Ipc_AI

lemma cancel_ipc_ex_nonz_tcb_cap:
  "\<lbrace>\<lambda>s. \<exists>ptr. cte_wp_at ((=) (cap.ThreadCap p)) ptr s\<rbrace>
     cancel_ipc t
   \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>" apply (simp add: ex_nonz_cap_to_def cte_wp_at_caps_of_state
              del: split_paired_Ex) apply (wp cancel_ipc_caps_of_state) apply (clarsimp simp del: split_paired_Ex split_paired_All) apply (intro conjI allI impI) apply (rule_tac x="(a, b)" in exI) apply (clarsimp simp: cte_wp_at_caps_of_state can_fast_finalise_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>ptr. cte_wp_at ((=) (ThreadCap p)) ptr s\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>ptr. caps_of_state s ptr = Some (ThreadCap p)\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> p \<in> zobj_refs cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>ptr. caps_of_state s ptr = Some (ThreadCap p) \<Longrightarrow> (\<forall>pa. cte_wp_at can_fast_finalise pa s \<longrightarrow> (\<exists>cref cap. ((caps_of_state s)(pa \<mapsto> NullCap)) cref = Some cap \<and> p \<in> zobj_refs cap)) \<and> (\<exists>cref cap. caps_of_state s cref = Some cap \<and> p \<in> zobj_refs cap) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. caps_of_state s (a, b) = Some (ThreadCap p) \<Longrightarrow> (\<forall>pa. cte_wp_at can_fast_finalise pa s \<longrightarrow> (\<exists>cref. cref \<noteq> pa \<and> (cref \<noteq> pa \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> p \<in> zobj_refs cap)))) \<and> (\<exists>cref cap. caps_of_state s cref = Some cap \<and> p \<in> zobj_refs cap) proof (prove)
goal (2 subgoals):
 1. \<And>s a b pa. \<lbrakk>caps_of_state s (a, b) = Some (ThreadCap p); cte_wp_at can_fast_finalise pa s\<rbrakk> \<Longrightarrow> \<exists>cref. cref \<noteq> pa \<and> (cref \<noteq> pa \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> p \<in> zobj_refs cap))
 2. \<And>s a b. caps_of_state s (a, b) = Some (ThreadCap p) \<Longrightarrow> \<exists>cref cap. caps_of_state s cref = Some cap \<and> p \<in> zobj_refs cap proof (prove)
goal (2 subgoals):
 1. \<And>s a b pa. \<lbrakk>caps_of_state s (a, b) = Some (ThreadCap p); cte_wp_at can_fast_finalise pa s\<rbrakk> \<Longrightarrow> (a, b) \<noteq> pa \<and> ((a, b) \<noteq> pa \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> p \<in> zobj_refs cap))
 2. \<And>s a b. caps_of_state s (a, b) = Some (ThreadCap p) \<Longrightarrow> \<exists>cref cap. caps_of_state s cref = Some cap \<and> p \<in> zobj_refs cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b. caps_of_state s (a, b) = Some (ThreadCap p) \<Longrightarrow> \<exists>cref cap. caps_of_state s cref = Some cap \<and> p \<in> zobj_refs cap proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma valid_cap_tcb_at_tcb_or_zomb:
  "\<lbrakk> s \<turnstile> cap; t \<in> obj_refs cap; tcb_at t s \<rbrakk>
       \<Longrightarrow> is_thread_cap cap \<or> is_zombie cap" by (rule obj_ref_is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> cap; t \<in> obj_refs cap; tcb_at t s\<rbrakk> \<Longrightarrow> is_thread_cap cap \<or> is_zombie cap
theory Ipc_AI

lemma cancel_ipc_ex_nonz_cap_to_tcb:
  "\<lbrace>\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s\<rbrace>
     cancel_ipc t
   \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>" apply (wp cancel_ipc_ex_nonz_tcb_cap) apply (clarsimp simp: ex_nonz_cap_to_def) apply (drule cte_wp_at_norm, clarsimp) apply (frule(1) cte_wp_at_valid_objs_valid_cap, clarsimp) apply (drule valid_cap_tcb_at_tcb_or_zomb[where t=p]) apply (simp add: zobj_refs_to_obj_refs) apply assumption apply (fastforce simp: is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<Longrightarrow> \<exists>ptr. cte_wp_at ((=) (ThreadCap p)) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>cte_wp_at (\<lambda>c. p \<in> zobj_refs c) (a, b) s; valid_objs s; tcb_at p s\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at ((=) (ThreadCap p)) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b c. \<lbrakk>valid_objs s; tcb_at p s; cte_wp_at ((=) c) (a, b) s; p \<in> zobj_refs c\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at ((=) (ThreadCap p)) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b c. \<lbrakk>valid_objs s; tcb_at p s; cte_wp_at ((=) c) (a, b) s; p \<in> zobj_refs c; s \<turnstile> c\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at ((=) (ThreadCap p)) (a, b) s proof (prove)
goal (3 subgoals):
 1. \<And>s a b c. \<lbrakk>valid_objs s; tcb_at p s; cte_wp_at ((=) c) (a, b) s; p \<in> zobj_refs c\<rbrakk> \<Longrightarrow> p \<in> obj_refs c
 2. \<And>s a b c. \<lbrakk>valid_objs s; tcb_at p s; cte_wp_at ((=) c) (a, b) s; p \<in> zobj_refs c\<rbrakk> \<Longrightarrow> tcb_at p s
 3. \<And>s a b c. \<lbrakk>valid_objs s; tcb_at p s; cte_wp_at ((=) c) (a, b) s; p \<in> zobj_refs c; is_thread_cap c \<or> is_zombie c\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at ((=) (ThreadCap p)) (a, b) s proof (prove)
goal (2 subgoals):
 1. \<And>s a b c. \<lbrakk>valid_objs s; tcb_at p s; cte_wp_at ((=) c) (a, b) s; p \<in> zobj_refs c\<rbrakk> \<Longrightarrow> tcb_at p s
 2. \<And>s a b c. \<lbrakk>valid_objs s; tcb_at p s; cte_wp_at ((=) c) (a, b) s; p \<in> zobj_refs c; is_thread_cap c \<or> is_zombie c\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at ((=) (ThreadCap p)) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b c. \<lbrakk>valid_objs s; tcb_at p s; cte_wp_at ((=) c) (a, b) s; p \<in> zobj_refs c; is_thread_cap c \<or> is_zombie c\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at ((=) (ThreadCap p)) (a, b) s proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma cancel_ipc_simple2:
  "\<lbrace>K (\<forall>st. simple st \<longrightarrow> P st)\<rbrace>
     cancel_ipc t
   \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" apply (rule hoare_assume_pre) apply (rule hoare_chain, rule cancel_ipc_simple, simp_all) apply (clarsimp simp: st_tcb_def2) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (\<forall>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st \<longrightarrow> P st)\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. K (\<forall>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st \<longrightarrow> P st) s \<Longrightarrow> \<lbrace>K (\<forall>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st \<longrightarrow> P st)\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>\<forall>st. (inactive st \<longrightarrow> P Inactive) \<and> (st = Running \<longrightarrow> P Running) \<and> (st = Restart \<longrightarrow> P Restart) \<and> (idle st \<longrightarrow> P IdleThreadState) \<and> (awaiting_reply st \<longrightarrow> P BlockedOnReply); st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t sa\<rbrakk> \<Longrightarrow> st_tcb_at P t sa proof (prove)
goal (1 subgoal):
 1. \<And>sa tcb. \<lbrakk>\<forall>st. (inactive st \<longrightarrow> P Inactive) \<and> (st = Running \<longrightarrow> P Running) \<and> (st = Restart \<longrightarrow> P Restart) \<and> (idle st \<longrightarrow> P IdleThreadState) \<and> (awaiting_reply st \<longrightarrow> P BlockedOnReply); get_tcb t sa = Some tcb; inactive (tcb_state tcb) \<or> tcb_state tcb = Running \<or> tcb_state tcb = Restart \<or> idle (tcb_state tcb) \<or> awaiting_reply (tcb_state tcb)\<rbrakk> \<Longrightarrow> P (tcb_state tcb) proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma cancel_ipc_cte_wp_at_not_reply_state:
  "\<lbrace>st_tcb_at ((\<noteq>) BlockedOnReply) t and cte_wp_at P p\<rbrace>
    cancel_ipc t
   \<lbrace>\<lambda>r. cte_wp_at P p\<rbrace>" apply (simp add: cancel_ipc_def) apply (rule hoare_pre) apply (wp hoare_pre_cont[where f="reply_cancel_ipc t"] gts_wp | wpc)+ apply (clarsimp simp: st_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at ((\<noteq>) BlockedOnReply) t and cte_wp_at P p\<rbrace> cancel_ipc t \<lbrace>\<lambda>r. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at ((\<noteq>) BlockedOnReply) t and cte_wp_at P p\<rbrace> do state <- get_thread_state t;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>r. cte_wp_at P p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do state <- get_thread_state t;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state t | BlockedOnReply \<Rightarrow> reply_cancel_ipc t | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>r. cte_wp_at P p\<rbrace>
 2. \<And>s. (st_tcb_at ((\<noteq>) BlockedOnReply) t and cte_wp_at P p) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (st_tcb_at ((\<noteq>) BlockedOnReply) t and cte_wp_at P p) s \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> (st = Running \<longrightarrow> cte_wp_at P p s) \<and> (inactive st \<longrightarrow> cte_wp_at P p s) \<and> (st = Restart \<longrightarrow> cte_wp_at P p s) \<and> (\<forall>x xa. st = BlockedOnReceive x xa \<longrightarrow> cte_wp_at P p s) \<and> (\<forall>x xa. st = BlockedOnSend x xa \<longrightarrow> cte_wp_at P p s) \<and> (awaiting_reply st \<longrightarrow> False) \<and> (\<forall>x. st = BlockedOnNotification x \<longrightarrow> cte_wp_at P p s) \<and> (idle st \<longrightarrow> cte_wp_at P p s) proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma tcb_at_typ_at:
  "\<lbrace>typ_at ATCB t\<rbrace> f \<lbrace>\<lambda>_. typ_at ATCB t\<rbrace> \<Longrightarrow> \<lbrace>tcb_at t\<rbrace> f \<lbrace>\<lambda>_. tcb_at t\<rbrace>" by (simp add: tcb_at_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>typ_at ATCB t\<rbrace> f \<lbrace>\<lambda>_. typ_at ATCB t\<rbrace> \<Longrightarrow> \<lbrace>tcb_at t\<rbrace> f \<lbrace>\<lambda>_. tcb_at t\<rbrace>
theory Ipc_AI

lemma ncof_invs [wp]:
  "\<lbrace>invs\<rbrace> null_cap_on_failure (lookup_cap t ref) \<lbrace>\<lambda>rv. invs\<rbrace>" by (simp add: null_cap_on_failure_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> null_cap_on_failure (lookup_cap t ref) \<lbrace>\<lambda>rv. invs\<rbrace>
theory Ipc_AI

lemma ncof_is_a_catch:
  "null_cap_on_failure m = (m <catch> (\<lambda>e. return Structures_A.NullCap))" apply (simp add: null_cap_on_failure_def liftM_def catch_def) apply (rule bind_cong [OF refl]) apply (case_tac v, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. null_cap_on_failure m = (m <catch> (\<lambda>e. return NullCap)) proof (prove)
goal (1 subgoal):
 1. do x <- m;
return (case x of Inl x \<Rightarrow> NullCap | Inr x \<Rightarrow> id x)
od = do x <- m;
case x of Inl e \<Rightarrow> return NullCap | Inr b \<Rightarrow> return b
od proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. (v, s') \<in> fst (m s) \<Longrightarrow> return (case v of Inl x \<Rightarrow> NullCap | Inr x \<Rightarrow> id x) s' = (case v of Inl e \<Rightarrow> return NullCap | Inr b \<Rightarrow> return b) s' proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma recv_ep_distinct:
  assumes inv: "invs s"
  assumes ep: "obj_at (\<lambda>k. k = Endpoint (Structures_A.endpoint.RecvEP
                                           q)) word1 s"
  shows "distinct q" using assms apply - apply (drule invs_valid_objs) apply (erule(1) obj_at_valid_objsE) apply (clarsimp simp: valid_obj_def valid_ep_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct q proof (prove)
using this:
invs s
obj_at (\<lambda>k. k = Endpoint (RecvEP q)) word1 s

goal (1 subgoal):
 1. distinct q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; obj_at (\<lambda>k. k = Endpoint (RecvEP q)) word1 s\<rbrakk> \<Longrightarrow> distinct q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at (\<lambda>k. k = Endpoint (RecvEP q)) word1 s; valid_objs s\<rbrakk> \<Longrightarrow> distinct q proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>valid_objs s; kheap s word1 = Some ko; ko = Endpoint (RecvEP q); valid_obj word1 ko s\<rbrakk> \<Longrightarrow> distinct q proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma rfk_invs: "\<lbrace>invs and tcb_at t\<rbrace> reply_from_kernel t r \<lbrace>\<lambda>rv. invs\<rbrace>" unfolding reply_from_kernel_def by (cases r; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t\<rbrace> reply_from_kernel t r \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t\<rbrace> do (label, msg) <- return r;
buf <- lookup_ipc_buffer True t;
as_user t $ setRegister badge_register 0;
len <- set_mrs t buf msg;
set_message_info t $ MI len 0 0 label
od \<lbrace>\<lambda>rv. invs\<rbrace>