kings-crown/FVELER_Isabelle huggingface dataset:
theory Tcb_AI

lemma real_cte_at_not_tcb_at:
  "real_cte_at (x, y) s \<Longrightarrow> \<not> tcb_at x s" by (clarsimp simp: obj_at_def is_tcb is_cap_table)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. real_cte_at (x, y) s \<Longrightarrow> \<not> tcb_at x s
theory Tcb_AI

lemma decode_unbind_notification_wf:
  "\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace>
     decode_unbind_notification (cap.ThreadCap t)
   \<lbrace>tcb_inv_wf\<rbrace>,-" apply (simp add: decode_unbind_notification_def) apply (rule hoare_pre) apply (wp gbn_wp | wpc)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> decode_unbind_notification (ThreadCap t) \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> doE nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk (NotificationControl t None)
odE \<lbrace>tcb_inv_wf\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> throwError IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk (NotificationControl t None)
odE \<lbrace>tcb_inv_wf\<rbrace>, -
 2. \<And>s. (invs and tcb_at t and ex_nonz_cap_to t) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and tcb_at t and ex_nonz_cap_to t) s \<Longrightarrow> True \<and> (\<forall>ntfn. bound_tcb_at ((=) ntfn) t s \<longrightarrow> True \<and> (ntfn = None \<longrightarrow> True) \<and> (\<forall>x. ntfn = Some x \<longrightarrow> tcb_inv_wf (NotificationControl t None) s)) proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma out_pred_tcb_at_preserved:
  "\<lbrakk> \<And>tcb x. tcb_state (f x tcb) = tcb_state tcb \<rbrakk> \<Longrightarrow>
   \<lbrace>st_tcb_at P t\<rbrace> option_update_thread t' f opt \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" apply (cases opt, simp_all add: option_update_thread_def) apply (rule thread_set_no_change_tcb_state) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb x. tcb_state (f x tcb) = tcb_state tcb) \<Longrightarrow> \<lbrace>st_tcb_at P t\<rbrace> option_update_thread t' f opt \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<And>tcb x. tcb_state (f x tcb) = tcb_state tcb; opt = Some a\<rbrakk> \<Longrightarrow> \<lbrace>st_tcb_at P t\<rbrace> thread_set (f a) t' \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a tcb. \<lbrakk>\<And>tcb x. tcb_state (f x tcb) = tcb_state tcb; opt = Some a\<rbrakk> \<Longrightarrow> tcb_state (f a tcb) = tcb_state tcb proof (prove)
goal:
No subgoals!
theory Tcb_AI

lemma pred_tcb_at_arch_state[simp]:
  "pred_tcb_at proj P t (arch_state_update f s) = pred_tcb_at proj P t s" by (simp add: pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at proj P t (arch_state_update f s) = pred_tcb_at proj P t s
theory Tcb_AI

lemma invoke_domain_invs:
  "\<lbrace>invs\<rbrace>
     invoke_domain t d
   \<lbrace>\<lambda>rv. invs\<rbrace>" by (simp add: invoke_domain_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> invoke_domain t d \<lbrace>\<lambda>rv. invs\<rbrace>
theory Tcb_AI

lemma invoke_domain_typ_at[wp]:
  "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace>
     invoke_domain t d
   \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" by (simp add: invoke_domain_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> invoke_domain t d \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
theory Tcb_AI

lemma decode_domain_inv_inv:
  "\<lbrace>P\<rbrace>
     decode_domain_invocation label args excs
   \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: decode_domain_invocation_def whenE_def split del: if_split | wp hoare_vcg_if_splitE | wpc)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_domain_invocation label args excs \<lbrace>\<lambda>rv. P\<rbrace>
theory Tcb_AI

lemma tcb_bound_refs_no_NTFNBound:
  "(x, NTFNBound) \<notin> tcb_bound_refs a" by (simp add: tcb_bound_refs_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, NTFNBound) \<notin> tcb_bound_refs a
theory Tcb_AI

lemma tcb_st_refs_of_no_NTFNBound:
  "(x, NTFNBound) \<notin> tcb_st_refs_of z" by (simp add: tcb_st_refs_of_def split: thread_state.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, NTFNBound) \<notin> tcb_st_refs_of z
theory Tcb_AI

lemma ntfn_bound_refs_def2:
  "ntfn_bound_refs t = set_option t \<times> {NTFNBound}" by (clarsimp simp: ntfn_bound_refs_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfn_bound_refs t = set_option t \<times> {NTFNBound}
theory Tcb_AI

lemma tcb_cap_cases_tcb_mcpriority:
  "\<forall>(getF, v)\<in>ran tcb_cap_cases.
         getF (tcb_mcpriority_update F tcb) = getF tcb" by (rule ball_tcb_cap_casesI, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>(getF, v)\<in>ran tcb_cap_cases. getF (tcb_mcpriority_update F tcb) = getF tcb
theory Tcb_AI

lemma set_mcpriority_no_cap_to_obj_with_diff_ref[wp]:
  "\<lbrace>no_cap_to_obj_with_diff_ref c S\<rbrace> set_mcpriority t mcp \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref c S\<rbrace>" by (simp add: set_mcpriority_def thread_set_no_cap_to_trivial tcb_cap_cases_tcb_mcpriority)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_cap_to_obj_with_diff_ref c S\<rbrace> set_mcpriority t mcp \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref c S\<rbrace>
theory ArchTcb_AI

lemma activate_idle_invs[Tcb_AI_asms]:
  "\<lbrace>invs and ct_idle\<rbrace>
     arch_activate_idle_thread thread
   \<lbrace>\<lambda>rv. invs and ct_idle\<rbrace>" by (simp add: arch_activate_idle_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_idle\<rbrace> arch_activate_idle_thread thread \<lbrace>\<lambda>rv. invs and ct_idle\<rbrace>
theory ArchTcb_AI

lemma empty_fail_getRegister [intro!, simp, Tcb_AI_asms]:
  "empty_fail (getRegister r)" by (simp add: getRegister_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getRegister r)
theory ArchTcb_AI

lemma same_object_also_valid:  (* arch specific *)
  "\<lbrakk> same_object_as cap cap'; s \<turnstile> cap'; wellformed_cap cap;
     cap_asid cap = None \<or> (\<exists>asid. cap_asid cap = Some asid \<and> 0 < asid \<and> asid \<le> 2^asid_bits - 1);
     cap_vptr cap = None; cap_asid_base cap = None \<rbrakk>
     \<Longrightarrow> s \<turnstile> cap" apply (cases cap,
         (clarsimp simp: same_object_as_def is_cap_simps cap_asid_def
                         wellformed_cap_def wellformed_acap_def
                         valid_cap_def bits_of_def cap_aligned_def
                   split: cap.split_asm arch_cap.split_asm option.splits)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>same_object_as cap cap'; s \<turnstile> cap'; wellformed_cap cap; cap_asid cap = None \<or> (\<exists>asid. cap_asid cap = Some asid \<and> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1); cap_vptr cap = None; cap_asid_base cap = None\<rbrakk> \<Longrightarrow> s \<turnstile> cap proof (prove)
goal:
No subgoals!
theory ArchTcb_AI

lemma same_object_obj_refs[Tcb_AI_asms]:
  "\<lbrakk> same_object_as cap cap' \<rbrakk>
     \<Longrightarrow> obj_refs cap = obj_refs cap'" apply (cases cap, simp_all add: same_object_as_def) apply ((clarsimp simp: is_cap_simps bits_of_def same_aobject_as_def
                      split: cap.split_asm )+) by (cases "the_arch_cap cap"; cases "the_arch_cap cap'"; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. same_object_as cap cap' \<Longrightarrow> obj_refs cap = obj_refs cap' proof (prove)
goal (7 subgoals):
 1. \<And>x32 x33. \<lbrakk>is_ep_cap cap'; cap = EndpointCap (obj_ref_of cap') x32 x33\<rbrakk> \<Longrightarrow> {obj_ref_of cap'} = obj_refs cap'
 2. \<And>x42 x43. \<lbrakk>is_ntfn_cap cap'; cap = NotificationCap (obj_ref_of cap') x42 x43\<rbrakk> \<Longrightarrow> {obj_ref_of cap'} = obj_refs cap'
 3. \<And>x51 x52 x53. \<lbrakk>\<exists>m' cr. cap' = ReplyCap x51 m' cr; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> {} = obj_refs cap'
 4. \<And>x63. \<lbrakk>is_cnode_cap cap'; cap = CNodeCap (obj_ref_of cap') (bits_of cap') x63\<rbrakk> \<Longrightarrow> {obj_ref_of cap'} = obj_refs cap'
 5. \<lbrakk>is_thread_cap cap'; cap = ThreadCap (obj_ref_of cap')\<rbrakk> \<Longrightarrow> {obj_ref_of cap'} = obj_refs cap'
 6. \<lbrakk>case cap' of IRQHandlerCap n \<Rightarrow> False | _ \<Rightarrow> same_region_as IRQControlCap cap'; cap = IRQControlCap\<rbrakk> \<Longrightarrow> {} = obj_refs cap'
 7. \<And>x12. \<lbrakk>case cap' of ArchObjectCap x \<Rightarrow> same_aobject_as x12 x | _ \<Rightarrow> same_region_as (ArchObjectCap x12) cap'; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> set_option (aobj_ref x12) = obj_refs cap' proof (prove)
goal (1 subgoal):
 1. \<And>x12 x12a. \<lbrakk>cap = ArchObjectCap x12; cap' = ArchObjectCap x12a; case x12 of PageCap dev ref x pgsz xa \<Rightarrow> case x12a of PageCap dev' ref' xb pgsz' xc \<Rightarrow> (dev, ref, pgsz) = (dev', ref', pgsz') \<and> ref \<le> ref + 2 ^ pageBitsForSize pgsz - 1 | _ \<Rightarrow> arch_same_region_as x12 x12a | _ \<Rightarrow> arch_same_region_as x12 x12a\<rbrakk> \<Longrightarrow> set_option (aobj_ref x12) = set_option (aobj_ref x12a)
theory ArchTcb_AI

lemma is_cnode_or_valid_arch_cap_asid: (* arch specific *)
  "is_cnode_or_valid_arch cap
       \<Longrightarrow> (is_pt_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
             \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None)" by (auto simp add: is_cnode_or_valid_arch_def
                     is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cnode_or_valid_arch cap \<Longrightarrow> (is_pt_cap cap \<longrightarrow> cap_asid cap \<noteq> None) \<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
theory ArchTcb_AI

lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]:
  "table_cap_ref (max_free_index_update cap) = table_cap_ref cap" by (simp add: free_index_update_def table_cap_ref_def split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. table_cap_ref (max_free_index_update cap) = table_cap_ref cap
theory ArchTcb_AI

lemma as_user_valid_cap[wp]:
  "\<lbrace>valid_cap c\<rbrace> as_user a b \<lbrace>\<lambda>rv. valid_cap c\<rbrace>" by (wp valid_cap_typ)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> as_user a b \<lbrace>\<lambda>rv. valid_cap c\<rbrace>
theory ArchTcb_AI

lemma as_user_ipc_tcb_cap_valid4[wp]:
  "\<lbrace>\<lambda>s. tcb_cap_valid cap (t, tcb_cnode_index 4) s\<rbrace>
    as_user a b
   \<lbrace>\<lambda>rv. tcb_cap_valid cap (t, tcb_cnode_index 4)\<rbrace>" apply (simp add: as_user_def set_object_def get_object_def) apply (wp | wpc | simp)+ apply (clarsimp simp: tcb_cap_valid_def obj_at_def
                        pred_tcb_at_def is_tcb
                 dest!: get_tcb_SomeD) apply (clarsimp simp: get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_cap_valid cap (t, tcb_cnode_index 4)\<rbrace> as_user a b \<lbrace>\<lambda>rv. tcb_cap_valid cap (t, tcb_cnode_index 4)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_cap_valid cap (t, tcb_cnode_index 4)\<rbrace> do tcb <- gets_the (get_tcb a);
(aa, uc') <- select_f (b (arch_tcb_context_get (tcb_arch tcb)));
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh a = Some y);
return (the (kh a))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>))\<rparr>)
od;
return aa
od \<lbrace>\<lambda>rv. tcb_cap_valid cap (t, tcb_cnode_index 4)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_cap_valid cap (t, tcb_cnode_index 4) s \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> (\<forall>x\<in>fst (b (arch_tcb_context_get (tcb_arch (the (get_tcb a s))))). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<exists>y. kheap s a = Some y) \<longrightarrow> a_type (the (kheap s a)) = ATCB \<longrightarrow> tcb_cap_valid cap (t, tcb_cnode_index 4) (s\<lparr>kheap := \<lambda>b. if b = a then Some (TCB (the (get_tcb a s)\<lparr>tcb_arch := arch_tcb_context_set xb (tcb_arch (the (get_tcb a s)))\<rparr>)) else kheap s b\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba tcb. \<lbrakk>(aa, ba) \<in> fst (b (arch_tcb_context_get (tcb_arch (the (get_tcb a s))))); t = a; kheap s a = Some (TCB tcb); is_nondevice_page_cap cap \<or> NullCap = cap; valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)\<rbrakk> \<Longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer (the (get_tcb a s))) proof (prove)
goal:
No subgoals!
theory ArchTcb_AI

lemma check_valid_ipc_buffer_inv:
  "\<lbrace>P\<rbrace> check_valid_ipc_buffer vptr cap \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: check_valid_ipc_buffer_def whenE_def
             cong: cap.case_cong arch_cap.case_cong
             split del: if_split) apply (rule hoare_pre) apply (wp | simp add: whenE_def if_apply_def2 | wpcw)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> check_valid_ipc_buffer vptr cap \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case cap of ArchObjectCap (PageCap True x xa xb xc) \<Rightarrow> throwError IllegalOperation | ArchObjectCap (PageCap False x xa xb xc) \<Rightarrow> doE whenE (\<not> is_aligned vptr msg_align_bits) $ throwError AlignmentError;
returnOk ()
odE | ArchObjectCap _ \<Rightarrow> throwError IllegalOperation | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case cap of ArchObjectCap (PageCap True x xa xb xc) \<Rightarrow> throwError IllegalOperation | ArchObjectCap (PageCap False x xa xb xc) \<Rightarrow> doE whenE (\<not> is_aligned vptr msg_align_bits) $ throwError AlignmentError;
returnOk ()
odE | ArchObjectCap _ \<Rightarrow> throwError IllegalOperation | _ \<Rightarrow> throwError IllegalOperation \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchTcb_AI

lemma decode_set_ipc_inv[wp,Tcb_AI_asms]:
  "\<lbrace>P::'state_ext::state_ext state \<Rightarrow> bool\<rbrace> decode_set_ipc_buffer args cap slot excaps \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp   add: decode_set_ipc_buffer_def whenE_def
                     split_def
          split del: if_split) apply (rule hoare_pre, wp check_valid_ipc_buffer_inv) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_set_ipc_buffer args cap slot excaps \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE y <- if args = [] then throwError TruncatedMessage else returnOk ();
y <- if excaps = [] then throwError TruncatedMessage else returnOk ();
newbuf <- if args ! 0 = 0 then returnOk None else doE buffer_cap <- derive_cap (snd (excaps ! 0)) (fst (excaps ! 0));
y <- check_valid_ipc_buffer (args ! 0) buffer_cap;
returnOk (Some (buffer_cap, snd (excaps ! 0)))
odE;
returnOk (ThreadControl (obj_ref_of cap) slot None None None None None (Some (args ! 0, newbuf)))
odE \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (args = [] \<longrightarrow> P s \<and> True) \<and> (args \<noteq> [] \<longrightarrow> (excaps = [] \<longrightarrow> P s \<and> True) \<and> (excaps \<noteq> [] \<longrightarrow> (args ! 0 = 0 \<longrightarrow> P s) \<and> (args ! 0 \<noteq> 0 \<longrightarrow> P s \<and> P s \<and> P s))) proof (prove)
goal:
No subgoals!
theory ArchTcb_AI

lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]:
  "no_cap_to_obj_with_diff_ref c S s \<longrightarrow>
    no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s" apply (case_tac "update_cap_data P x c = NullCap") apply (simp add: no_cap_to_obj_with_diff_ref_Null) apply (subgoal_tac "vs_cap_ref (update_cap_data P x c)
                                 = vs_cap_ref c") apply (simp add: no_cap_to_obj_with_diff_ref_def
                    update_cap_objrefs) apply (clarsimp simp: update_cap_data_closedform
                        table_cap_ref_def
                        arch_update_cap_data_def
                 split: cap.split) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_cap_to_obj_with_diff_ref c S s \<longrightarrow> no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s proof (prove)
goal (2 subgoals):
 1. update_cap_data P x c = NullCap \<Longrightarrow> no_cap_to_obj_with_diff_ref c S s \<longrightarrow> no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s
 2. update_cap_data P x c \<noteq> NullCap \<Longrightarrow> no_cap_to_obj_with_diff_ref c S s \<longrightarrow> no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s proof (prove)
goal (1 subgoal):
 1. update_cap_data P x c \<noteq> NullCap \<Longrightarrow> no_cap_to_obj_with_diff_ref c S s \<longrightarrow> no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>update_cap_data P x c \<noteq> NullCap; vs_cap_ref (update_cap_data P x c) = vs_cap_ref c\<rbrakk> \<Longrightarrow> no_cap_to_obj_with_diff_ref c S s \<longrightarrow> no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s
 2. update_cap_data P x c \<noteq> NullCap \<Longrightarrow> vs_cap_ref (update_cap_data P x c) = vs_cap_ref c proof (prove)
goal (2 subgoals):
 1. update_cap_data P x c \<noteq> NullCap \<Longrightarrow> (\<forall>p\<in>UNIV - S. \<not> cte_wp_at (\<lambda>ca. obj_refs ca = obj_refs c \<and> table_cap_ref ca \<noteq> table_cap_ref c) p s) \<longrightarrow> (\<forall>p\<in>UNIV - S. \<not> cte_wp_at (\<lambda>ca. obj_refs ca = obj_refs c \<and> table_cap_ref ca \<noteq> table_cap_ref (update_cap_data P x c)) p s)
 2. update_cap_data P x c \<noteq> NullCap \<Longrightarrow> vs_cap_ref (update_cap_data P x c) = vs_cap_ref c proof (prove)
goal (1 subgoal):
 1. update_cap_data P x c \<noteq> NullCap \<Longrightarrow> vs_cap_ref (update_cap_data P x c) = vs_cap_ref c proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma empty_on_failure_empty_fail[wp]:
  "empty_fail f \<Longrightarrow> empty_fail (empty_on_failure f)" by (simp add: empty_on_failure_def catch_def split: sum.splits | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (empty_on_failure f)
theory EmptyFail_AI

lemma unify_failure_empty_fail[wp]:
  "empty_fail f \<Longrightarrow> empty_fail (unify_failure f)" by (simp add: unify_failure_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (unify_failure f)
theory EmptyFail_AI

lemma const_on_failure_empty_fail[wp]:
  "empty_fail f \<Longrightarrow> empty_fail (const_on_failure a f)" by (simp add: const_on_failure_def catch_def split: sum.splits | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (const_on_failure a f)
theory EmptyFail_AI

lemma select_ext_empty_fail:
  "S \<noteq> {} \<Longrightarrow> empty_fail (select_ext a S)" by (simp add: select_ext_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> empty_fail (select_ext a S)
theory EmptyFail_AI

lemma do_extended_op_empty_fail[wp]:
  "empty_fail (do_extended_op f)" apply(simp add: do_extended_op_def) apply (wp | simp add: mk_ef_def split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (do_extended_op f) proof (prove)
goal (1 subgoal):
 1. empty_fail (do ex <- get;
(uu_, es') <- select_f (mk_ef (wrap_ext_op f ex));
modify (exst_update (\<lambda>_. exst es'))
od) proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma do_machine_op_empty_fail[wp]:
  "empty_fail f \<Longrightarrow> empty_fail (do_machine_op f)" apply (simp add: do_machine_op_def | wp)+ apply (simp add: empty_fail_def) apply (simp add: split_def empty_fail_cond) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (do_machine_op f) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>empty_fail f; fst (f x) = {}\<rbrakk> \<Longrightarrow> snd (f x)
 2. \<And>x xa. empty_fail f \<Longrightarrow> empty_fail (case xa of (r, ms') \<Rightarrow> do y <- modify (machine_state_update (\<lambda>_. ms'));
return r
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. empty_fail f \<Longrightarrow> empty_fail (case xa of (r, ms') \<Rightarrow> do y <- modify (machine_state_update (\<lambda>_. ms'));
return r
od) proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma throw_on_false_empty_fail[wp]:
  "empty_fail f \<Longrightarrow> empty_fail (throw_on_false ex f)" by (simp add: throw_on_false_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (throw_on_false ex f)
theory EmptyFail_AI

lemma without_preemption_empty_fail[wp]:
  "empty_fail f \<Longrightarrow> empty_fail (without_preemption f)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (without_preemption f)
theory EmptyFail_AI

lemma check_cap_at_empty_fail[wp]:
  "empty_fail m \<Longrightarrow> empty_fail (check_cap_at cap slot m)" by (simp add: check_cap_at_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (check_cap_at cap slot m)
theory EmptyFail_AI

lemma as_user_empty_fail[wp]:
  "empty_fail f \<Longrightarrow> empty_fail (as_user t f)" apply (simp add: as_user_def | wp)+ apply (simp add: empty_fail_def) apply (case_tac xa) apply (simp | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (as_user t f) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>empty_fail f; fst (f (arch_tcb_context_get (tcb_arch x))) = {}\<rbrakk> \<Longrightarrow> snd (f (arch_tcb_context_get (tcb_arch x)))
 2. \<And>x xa. empty_fail f \<Longrightarrow> empty_fail (case xa of (a, uc') \<Rightarrow> do y <- set_object t (TCB (x\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch x)\<rparr>));
return a
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. empty_fail f \<Longrightarrow> empty_fail (case xa of (a, uc') \<Rightarrow> do y <- set_object t (TCB (x\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch x)\<rparr>));
return a
od) proof (prove)
goal (1 subgoal):
 1. \<And>x xa a b. \<lbrakk>empty_fail f; xa = (a, b)\<rbrakk> \<Longrightarrow> empty_fail (case xa of (a, uc') \<Rightarrow> do y <- set_object t (TCB (x\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch x)\<rparr>));
return a
od) proof (prove)
goal:
No subgoals!
theory EmptyFail_AI

lemma cap_fault_on_failure_empty_fail[wp]:
  "empty_fail f \<Longrightarrow> empty_fail (cap_fault_on_failure a b f)" by (simp add: cap_fault_on_failure_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (cap_fault_on_failure a b f)
theory EmptyFail_AI

lemma drop_spec_empty_fail:
  "empty_fail m \<Longrightarrow> spec_empty_fail m s" by (simp add: empty_fail_def spec_empty_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> spec_empty_fail m s
theory EmptyFail_AI

lemma spec_empty_fail_bind:
  "\<lbrakk>spec_empty_fail f s; \<And>x. empty_fail (g x)\<rbrakk>
    \<Longrightarrow> spec_empty_fail (f >>= g) s" by (fastforce simp: bind_def spec_empty_fail_def empty_fail_def image_def split_def split_paired_Bex intro: prod_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>spec_empty_fail f s; \<And>x. empty_fail (g x)\<rbrakk> \<Longrightarrow> spec_empty_fail (f >>= g) s