kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_AI

lemma lookup_extra_caps_eq [wp]:
  "\<lbrace>valid_objs\<rbrace> lookup_extra_caps thread xb info
  \<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. cte_wp_at ((=) (fst x)) (snd x) s)\<rbrace>,-" by (wpsimp wp: mapME_set simp: lookup_extra_caps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_extra_caps thread xb info \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at ((=) (fst x)) (snd x) s\<rbrace>, -
theory Syscall_AI

lemma valid_validE_R_gen:
  "\<lbrakk>\<And>rv s. Q' (Inr rv) s \<Longrightarrow> Q rv s; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -" by (fastforce simp: validE_R_def validE_def valid_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv s. Q' (Inr rv) s \<Longrightarrow> Q rv s; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -
theory Syscall_AI

lemma valid_validE_R_eq:
  "\<lbrakk>Q = Q'\<circ>Inr; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -" by (fastforce simp: validE_R_def validE_def valid_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Q = Q' \<circ> Inr; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -
theory Syscall_AI

lemma ts_Restart_case_helper:
  "(case ts of Structures_A.Restart \<Rightarrow> A | _ \<Rightarrow> B)
 = (if ts = Structures_A.Restart then A else B)" by (case_tac ts, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case ts of Restart \<Rightarrow> A | _ \<Rightarrow> B) = (if ts = Restart then A else B)
theory Syscall_AI

lemma lcs_ex_cap_to2[wp]:
  "\<lbrace>invs and K (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace>
      lookup_cap_and_slot t cref \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (snd rv)\<rbrace>,-" apply (rule hoare_pre) apply (simp add: lookup_cap_and_slot_def split_def) apply (wp lsft_ex_cte_cap_to | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> lookup_cap_and_slot t cref \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (snd rv)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> lookup_cap_and_slot t cref \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (snd rv)\<rbrace>, -
 2. \<And>s. (invs and K (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)) s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE p <- lookup_slot_for_thread t cref;
cap <- liftE (get_cap (fst p));
returnOk (cap, fst p)
odE \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P (snd rv)\<rbrace>, -
 2. \<And>s. (invs and K (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)) s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma hs_tcb_on_err:
  "\<lbrace>st_tcb_at active t and invs and ct_active\<rbrace>
     handle_send blocking
   -,\<lbrace>\<lambda>e. tcb_at t :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (unfold handle_send_def whenE_def fun_app_def validE_E_def validE_def) apply (rule hoare_strengthen_post [OF hinv_tcb]) apply (clarsimp split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at active t and invs and ct_active\<rbrace> handle_send blocking -, \<lbrace>\<lambda>e. tcb_at t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at active t and invs and ct_active\<rbrace> handle_invocation False blocking \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> tcb_at t s | Inr r \<Rightarrow> True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. tcb_at t s \<Longrightarrow> case rv of Inl e \<Rightarrow> tcb_at t s | Inr r \<Rightarrow> True proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma hs_invs[wp]: "\<lbrace>invs and ct_active\<rbrace> handle_send blocking \<lbrace>\<lambda>r. invs :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (rule validE_valid) apply (simp add: handle_send_def whenE_def) apply (wp | simp add: ct_in_state_def tcb_at_invs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active\<rbrace> handle_send blocking \<lbrace>\<lambda>r. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active\<rbrace> handle_send blocking \<lbrace>\<lambda>r. invs\<rbrace>, \<lbrace>\<lambda>r. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active\<rbrace> handle_invocation False blocking \<lbrace>\<lambda>r. invs\<rbrace>, \<lbrace>\<lambda>r. invs\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma tcb_cnode_index_3_reply_or_null:
  "\<lbrakk> tcb_at t s; tcb_cap_valid cap (t, tcb_cnode_index 3) s \<rbrakk> \<Longrightarrow> is_reply_cap cap \<or> cap = cap.NullCap" apply (clarsimp  simp: tcb_cap_valid_def st_tcb_def2 tcb_at_def) apply (clarsimp split: Structures_A.thread_state.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at t s; tcb_cap_valid cap (t, tcb_cnode_index 3) s\<rbrakk> \<Longrightarrow> is_reply_cap cap \<or> cap = NullCap proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>get_tcb t s = Some tcb; (case tcb_state tcb of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> is_reply_cap cap proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma ex_nonz_cap_to_tcb_strg:
  "(\<exists>cref. cte_wp_at (\<lambda>cap. is_thread_cap cap \<and> p \<in> zobj_refs cap) cref s)
       \<longrightarrow> ex_nonz_cap_to p s" by (fastforce simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>cref. cte_wp_at (\<lambda>cap. is_thread_cap cap \<and> p \<in> zobj_refs cap) cref s) \<longrightarrow> ex_nonz_cap_to p s
theory Syscall_AI

lemma ex_tcb_cap_to_tcb_at_strg:
  "ex_nonz_cap_to p s \<and> tcb_at p s \<and> valid_objs s \<longrightarrow>
   (\<exists>cref. cte_wp_at (\<lambda>cap. is_thread_cap cap \<and> p \<in> zobj_refs cap) cref s)" apply (clarsimp simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state
                        zobj_refs_to_obj_refs) apply (drule(1) caps_of_state_valid_cap[rotated]) apply (drule(2) valid_cap_tcb_at_tcb_or_zomb) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_nonz_cap_to p s \<and> tcb_at p s \<and> valid_objs s \<longrightarrow> (\<exists>cref. cte_wp_at (\<lambda>cap. is_thread_cap cap \<and> p \<in> zobj_refs cap) cref s) proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>tcb_at p s; valid_objs s; caps_of_state s (a, b) = Some cap; p \<in> obj_refs cap; \<not> is_zombie cap\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_thread_cap cap \<and> p \<in> obj_refs cap \<and> \<not> is_zombie cap proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>tcb_at p s; caps_of_state s (a, b) = Some cap; p \<in> obj_refs cap; \<not> is_zombie cap; s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_thread_cap cap \<and> p \<in> obj_refs cap \<and> \<not> is_zombie cap proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>tcb_at p s; caps_of_state s (a, b) = Some cap; p \<in> obj_refs cap; \<not> is_zombie cap; is_thread_cap cap \<or> is_zombie cap\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_thread_cap cap \<and> p \<in> obj_refs cap \<and> \<not> is_zombie cap proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma delete_caller_cap_invs[wp]:
  "\<lbrace>invs and tcb_at t\<rbrace> delete_caller_cap t \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: delete_caller_cap_def, wp) apply (clarsimp simp: emptyable_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t\<rbrace> delete_caller_cap t \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and tcb_at t) s \<Longrightarrow> (invs and emptyable (t, tcb_cnode_index 3)) s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma delete_caller_cap_simple[wp]:
  "\<lbrace>st_tcb_at active t\<rbrace> delete_caller_cap t' \<lbrace>\<lambda>rv. st_tcb_at active t\<rbrace>" apply (simp add: delete_caller_cap_def) apply (wp cap_delete_one_st_tcb_at) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at active t\<rbrace> delete_caller_cap t' \<lbrace>\<lambda>rv. st_tcb_at active t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at active t\<rbrace> cap_delete_one (t', tcb_cnode_index 3) \<lbrace>\<lambda>rv. st_tcb_at active t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at active t s \<Longrightarrow> (st_tcb_at active t and K (\<forall>st. active st \<longrightarrow> active st)) s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma delete_caller_deletes_caller[wp]:
  "\<lbrace>\<top>\<rbrace> delete_caller_cap t \<lbrace>\<lambda>rv. cte_wp_at ((=) cap.NullCap) (t, tcb_cnode_index 3)\<rbrace>" apply (rule_tac Q="\<lambda>rv. cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 3)"
               in hoare_post_imp,
         clarsimp elim!: cte_wp_at_weakenE) apply (simp add: delete_caller_cap_def cap_delete_one_def unless_def, wp) apply (simp add: if_apply_def2, wp get_cap_wp) apply (clarsimp elim!: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> delete_caller_cap t \<lbrace>\<lambda>rv. cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> delete_caller_cap t \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap) (t, tcb_cnode_index 3)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q7\<rbrace> get_cap (t, tcb_cnode_index 3) \<lbrace>\<lambda>cap. if cap \<noteq> NullCap then \<lambda>s. True else cte_wp_at (\<lambda>c. c = NullCap) (t, tcb_cnode_index 3)\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q7 s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 3) s \<longrightarrow> cap = NullCap \<longrightarrow> cte_wp_at (\<lambda>c. c = NullCap) (t, tcb_cnode_index 3) s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma delete_caller_cap_deleted[wp]:
  "\<lbrace>\<top>\<rbrace> delete_caller_cap thread \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = cap.NullCap) (thread, tcb_cnode_index 3)\<rbrace>" by (simp add: delete_caller_cap_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> delete_caller_cap thread \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap) (thread, tcb_cnode_index 3)\<rbrace>
theory Syscall_AI

lemma invs_valid_tcb_ctable_strengthen:
  "invs s \<longrightarrow> ((\<exists>y. get_tcb thread s = Some y) \<longrightarrow>
               invs s \<and> s \<turnstile> tcb_ctable (the (get_tcb thread s)))" by (clarsimp simp: invs_valid_tcb_ctable)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> invs s \<and> s \<turnstile> tcb_ctable (the (get_tcb thread s))
theory Syscall_AI

lemma hw_tcb[wp]: "\<lbrace>tcb_at t\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>rv. tcb_at t\<rbrace>" apply (simp add: handle_recv_def Let_def ep_ntfn_cap_case_helper
             cong: if_cong) apply (wp hoare_vcg_if_lift2 hoare_vcg_conj_lift hoare_drop_imps | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>rv. tcb_at t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> do thread <- gets cur_thread;
ep_cptr <- liftM to_bl (as_user thread (getRegister cap_register));
cap_fault_on_failure (of_bl ep_cptr) True (doE ep_cap <- lookup_cap thread ep_cptr;
if is_ep_cap ep_cap then if AllowRecv \<in> cap_rights ep_cap then liftE (do y <- delete_caller_cap thread;
receive_ipc thread ep_cap is_blocking
od) else throwError (MissingCapability 0) else if is_ntfn_cap ep_cap then if AllowRecv \<in> cap_rights ep_cap then doE ntfn <- liftE (get_notification (cap_ep_ptr ep_cap));
if ntfn_bound_tcb ntfn = Some thread \<or> ntfn_bound_tcb ntfn = None then liftE (receive_signal thread ep_cap is_blocking) else throwError (MissingCapability 0)
odE else throwError (MissingCapability 0) else throwError (MissingCapability 0)
odE) <catch> handle_fault thread
od \<lbrace>\<lambda>rv. tcb_at t\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma sts_st_tcb_at'':
  "\<lbrace>K (t = t' \<and> P st)\<rbrace>
     set_thread_state t st
   \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace>" apply (cases "t = t'") apply (simp only: simp_thms) apply (rule sts_st_tcb_at') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (t = t' \<and> P st)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = t' \<Longrightarrow> \<lbrace>K (t = t' \<and> P st)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace>
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>K (t = t' \<and> P st)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace> proof (prove)
goal (2 subgoals):
 1. t = t' \<Longrightarrow> \<lbrace>K (P st)\<rbrace> set_thread_state t' st \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace>
 2. t \<noteq> t' \<Longrightarrow> \<lbrace>K (t = t' \<and> P st)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>K (t = t' \<and> P st)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. st_tcb_at P t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma null_cap_on_failure_wp[wp]:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>rv. Q cap.NullCap\<rbrace>"
  shows      "\<lbrace>P\<rbrace> null_cap_on_failure f \<lbrace>Q\<rbrace>" unfolding ncof_is_a_catch by (wp x)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> null_cap_on_failure f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f <catch> (\<lambda>e. return NullCap) \<lbrace>Q\<rbrace>
theory Syscall_AI

lemma hy_inv: "(\<And>s f. P (trans_state f s) = P s) \<Longrightarrow> \<lbrace>P\<rbrace> handle_yield \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: handle_yield_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s f. P (trans_state f s) = P s) \<Longrightarrow> \<lbrace>P\<rbrace> handle_yield \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>s f. P (trans_state f s) = P s) \<Longrightarrow> \<lbrace>P\<rbrace> do thread <- gets cur_thread;
y <- do_extended_op (tcb_sched_action tcb_sched_dequeue thread);
y <- do_extended_op (tcb_sched_action tcb_sched_append thread);
do_extended_op reschedule_required
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma ct_active_simple [elim!]:
  "ct_active s \<Longrightarrow> st_tcb_at simple (cur_thread s) s" by (fastforce simp: ct_in_state_def elim!: pred_tcb_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_active s \<Longrightarrow> st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) (cur_thread s) s
theory Syscall_AI

lemma active_from_running:
  "ct_running  s  \<Longrightarrow> ct_active  s" by (clarsimp elim!: pred_tcb_weakenE
               simp: ct_in_state_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_running s \<Longrightarrow> ct_active s
theory Syscall_AI

lemma tcb_caller_cap:
  "\<lbrakk>tcb_at t s; valid_objs s\<rbrakk> \<Longrightarrow>
   cte_wp_at (is_reply_cap or (=) cap.NullCap) (t, tcb_cnode_index 3) s" by (fastforce intro: tcb_cap_wp_at split: Structures_A.thread_state.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at t s; valid_objs s\<rbrakk> \<Longrightarrow> cte_wp_at (is_reply_cap or (=) NullCap) (t, tcb_cnode_index 3) s
theory Syscall_AI

lemma simple_if_Restart_Inactive:
  "simple (if P then Structures_A.Restart else Structures_A.Inactive)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inactive (if P then Restart else Inactive) \<or> (if P then Restart else Inactive) = Running \<or> (if P then Restart else Inactive) = Restart \<or> idle (if P then Restart else Inactive) \<or> awaiting_reply (if P then Restart else Inactive)
theory Syscall_AI

lemma drop_when_dxo_wp: "(\<And>f s. P (trans_state f s) = P s ) \<Longrightarrow> \<lbrace>P\<rbrace> when b (do_extended_op e) \<lbrace>\<lambda>_.P\<rbrace>" apply (clarsimp simp add: when_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>f s. P (trans_state f s) = P s) \<Longrightarrow> \<lbrace>P\<rbrace> when b (do_extended_op e) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>f s. P (trans_state f s) = P s; b\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> do_extended_op e \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma handle_reply_nonz_cap_to_ct:
  "\<lbrace>\<lambda>s. ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s \<and> valid_mdb s \<and> tcb_at (cur_thread s) s\<rbrace>
     handle_reply
   \<lbrace>\<lambda>rv s :: 'state_ext state. ex_nonz_cap_to (cur_thread s) s\<rbrace>" apply (rule_tac Q="\<lambda>rv s. \<exists>ct. (ct = cur_thread s) \<and> ex_nonz_cap_to ct s"
               in hoare_post_imp) apply simp apply (wp hoare_vcg_ex_lift handle_reply_nonz_cap) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s \<and> valid_mdb s \<and> tcb_at (cur_thread s) s\<rbrace> handle_reply \<lbrace>\<lambda>rv s. ex_nonz_cap_to (cur_thread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<exists>ct. ct = cur_thread s \<and> ex_nonz_cap_to ct s \<Longrightarrow> ex_nonz_cap_to (cur_thread s) s
 2. \<lbrace>\<lambda>s. ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s \<and> valid_mdb s \<and> tcb_at (cur_thread s) s\<rbrace> handle_reply \<lbrace>\<lambda>rv s. \<exists>ct. ct = cur_thread s \<and> ex_nonz_cap_to ct s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s \<and> valid_mdb s \<and> tcb_at (cur_thread s) s\<rbrace> handle_reply \<lbrace>\<lambda>rv s. \<exists>ct. ct = cur_thread s \<and> ex_nonz_cap_to ct s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ex_nonz_cap_to (cur_thread s) s \<and> valid_objs s \<and> valid_mdb s \<and> tcb_at (cur_thread s) s \<Longrightarrow> \<exists>x. x = cur_thread s \<and> ex_nonz_cap_to x s \<and> valid_objs s \<and> valid_mdb s \<and> tcb_at x s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma hc_invs[wp]:
  "\<lbrace>invs and ct_active\<rbrace> handle_call \<lbrace>\<lambda>rv. invs :: 'state_ext state \<Rightarrow> bool\<rbrace>" by (simp add: handle_call_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active\<rbrace> handle_call \<lbrace>\<lambda>rv. invs\<rbrace>
theory Syscall_AI

lemma select_insert:
  "select (insert x X) = (return x \<sqinter> select X)" by (simp add: alternative_def select_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select (insert x X) = (return x \<sqinter> select X)
theory Syscall_AI

lemma do_nbrecv_failed_transfer_state_refs_of[wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of s) \<rbrace> do_nbrecv_failed_transfer t \<lbrace>\<lambda>rv s. P (state_refs_of s) \<rbrace>" unfolding do_nbrecv_failed_transfer_def apply (rule hoare_pre) apply (wp get_simple_ko_wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> do_nbrecv_failed_transfer 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 as_user t $ setRegister badge_register 0;
return ()
od \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do as_user t $ setRegister badge_register 0;
return ()
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:
No subgoals!
theory Syscall_AI

lemma fast_finalise_sym_refs:
  "\<lbrace>invs\<rbrace> fast_finalise cap final \<lbrace>\<lambda>y s. sym_refs (state_refs_of s)\<rbrace>" apply (cases cap; clarsimp simp: when_def) apply (wp cancel_all_signals_invs cancel_all_ipc_invs unbind_maybe_notification_invs
             | strengthen invs_sym_refs
             | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> fast_finalise cap final \<lbrace>\<lambda>y s. sym_refs (state_refs_of s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>y s. sym_refs (state_refs_of s)\<rbrace>
 2. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> (final \<longrightarrow> \<lbrace>invs\<rbrace> cancel_all_ipc x31 \<lbrace>\<lambda>y s. sym_refs (state_refs_of s)\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>y s. sym_refs (state_refs_of s)\<rbrace>)
 3. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> (final \<longrightarrow> \<lbrace>invs\<rbrace> do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od \<lbrace>\<lambda>y s. sym_refs (state_refs_of s)\<rbrace>) \<and> (\<not> final \<longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>y s. sym_refs (state_refs_of s)\<rbrace>)
 4. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs\<rbrace> return () \<lbrace>\<lambda>y s. sym_refs (state_refs_of s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma if_pred_distrib: "(if b then f else g) = (\<lambda>s. (b \<longrightarrow> f s) \<and> (\<not> b \<longrightarrow> g s))" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if b then f else g) = (\<lambda>s. (b \<longrightarrow> f s) \<and> (\<not> b \<longrightarrow> g s))