kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_AI

lemma clear_revokable [iff]:
  "pspace_clear t (is_original_cap_update f s) = is_original_cap_update f (pspace_clear t s)" by (simp add: pspace_clear_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_clear t (is_original_cap_update f s) = is_original_cap_update f (pspace_clear t s)
theory Ipc_AI

lemma ri_tcb [wp]:
  "\<lbrace>tcb_at t' :: 'state_ext state \<Rightarrow> bool\<rbrace>
    receive_ipc t cap is_blocking
   \<lbrace>\<lambda>rv. tcb_at t'\<rbrace>" by (simp add: tcb_at_typ, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t'\<rbrace> receive_ipc t cap is_blocking \<lbrace>\<lambda>rv. tcb_at t'\<rbrace>
theory Ipc_AI

lemma rai_tcb [wp]:
  "\<lbrace>tcb_at t'\<rbrace> receive_signal t cap is_blocking \<lbrace>\<lambda>rv. tcb_at t'\<rbrace>" by (simp add: tcb_at_typ) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t'\<rbrace> receive_signal t cap is_blocking \<lbrace>\<lambda>rv. tcb_at t'\<rbrace>
theory Ipc_AI

lemma setup_caller_cap_makes_simple:
  "\<lbrace>st_tcb_at simple t and K (t \<noteq> t')\<rbrace>
     setup_caller_cap t' t'' grant
   \<lbrace>\<lambda>rv. st_tcb_at simple t\<rbrace>" unfolding setup_caller_cap_def apply (wp sts_st_tcb_at_cases | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and K (t \<noteq> t')\<rbrace> setup_caller_cap t' t'' grant \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and K (t \<noteq> t')\<rbrace> do set_thread_state t' BlockedOnReply;
cap_insert (ReplyCap t' False (if grant then {AllowGrant, AllowWrite} else {AllowWrite})) (t', tcb_cnode_index 2) (t'', tcb_cnode_index 3)
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma ep_ntfn_cap_case_helper:
  "(case x of cap.EndpointCap ref bdg r \<Rightarrow> P ref bdg r
           |  cap.NotificationCap ref bdg r \<Rightarrow> Q ref bdg r
           |  _ \<Rightarrow> R)
   = (if is_ep_cap x then P (cap_ep_ptr x) (cap_ep_badge x) (cap_rights x) else
      if is_ntfn_cap x then Q (cap_ep_ptr x) (cap_ep_badge x) (cap_rights x) else
      R)" by (cases x, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case x of EndpointCap ref bdg r \<Rightarrow> P ref bdg r | NotificationCap ref bdg r \<Rightarrow> Q ref bdg r | _ \<Rightarrow> R) = (if is_ep_cap x then P (cap_ep_ptr x) (cap_ep_badge x) (cap_rights x) else if is_ntfn_cap x then Q (cap_ep_ptr x) (cap_ep_badge x) (cap_rights x) else R)
theory Ipc_AI

lemma sfi_makes_simple:
  "\<lbrace>st_tcb_at simple t and K (t \<noteq> t') :: 'state_ext state \<Rightarrow> bool\<rbrace>
     send_fault_ipc t' ft
   \<lbrace>\<lambda>rv. st_tcb_at simple t\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: send_fault_ipc_def Let_def ep_ntfn_cap_case_helper
             cong: if_cong) apply (wp si_blk_makes_simple hoare_drop_imps
            thread_set_no_change_tcb_state
       | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t and K (t \<noteq> t')\<rbrace> send_fault_ipc t' ft \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> send_fault_ipc t' ft \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. t \<noteq> t' \<Longrightarrow> \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> doE handler_cptr <- liftE (thread_get tcb_fault_handler t');
handler_cap <- cap_fault_on_failure (of_bl handler_cptr) False (lookup_cap t' handler_cptr);
if is_ep_cap handler_cap then if AllowSend \<in> cap_rights handler_cap \<and> (AllowGrant \<in> cap_rights handler_cap \<or> AllowGrantReply \<in> cap_rights handler_cap) then liftE (do y <- thread_set (tcb_fault_update (\<lambda>_. Some ft)) t';
send_ipc True True (cap_ep_badge handler_cap) (AllowGrant \<in> cap_rights handler_cap) True t' (cap_ep_ptr handler_cap)
od) else throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0)) else throwError (CapFault (of_bl handler_cptr) False (MissingCapability 0))
odE \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_AI

lemma hf_makes_simple:
  "\<lbrace>st_tcb_at simple t' and K (t \<noteq> t') :: 'state_ext state \<Rightarrow> bool\<rbrace>
     handle_fault t ft
   \<lbrace>\<lambda>rv. st_tcb_at simple t'\<rbrace>" unfolding handle_fault_def by (wpsimp wp: sfi_makes_simple sts_st_tcb_at_cases hoare_drop_imps simp: handle_double_fault_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' and K (t \<noteq> t')\<rbrace> handle_fault t ft \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' and K (t \<noteq> t')\<rbrace> do _ <- gets_the $ get_tcb t;
send_fault_ipc t ft <catch> handle_double_fault t ft;
return ()
od \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
theory Ipc_AI

lemma rai_makes_simple:
  "\<lbrace>st_tcb_at simple t' and K (t \<noteq> t')\<rbrace>
     receive_signal t cap is_blocking
   \<lbrace>\<lambda>rv. st_tcb_at simple t'\<rbrace>" by (rule rai_pred_tcb_neq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t' and K (t \<noteq> t')\<rbrace> receive_signal t cap is_blocking \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>st. inactive st \<or> st = Running \<or> st = Restart \<or> idle st \<or> awaiting_reply st) t'\<rbrace>
theory Ipc_AI

lemma thread_set_Pmdb:
  "\<lbrace>\<lambda>s. P (cdt s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>" unfolding thread_set_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> thread_set f t \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> do tcb <- gets_the $ get_tcb t;
set_object t $ TCB $ f tcb
od \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>
theory ArchIpc_AI

lemma cap_asid_PageCap_None [simp]:
  "cap_asid (ArchObjectCap (PageCap dev r R pgsz None)) = None" by (simp add: cap_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_asid (ArchObjectCap (PageCap dev r R pgsz None)) = None
theory ArchIpc_AI

lemma data_to_message_info_valid [Ipc_AI_assms]:
  "valid_message_info (data_to_message_info w)" by (simp add: valid_message_info_def data_to_message_info_def  word_and_le1 msg_max_length_def
                msg_max_extra_caps_def Let_def not_less mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_message_info (data_to_message_info w)
theory ArchIpc_AI

lemma get_extra_cptrs_length[wp, Ipc_AI_assms]:
  "\<lbrace>\<lambda>s . valid_message_info mi\<rbrace>
   get_extra_cptrs buf mi
   \<lbrace>\<lambda>rv s. length rv \<le> msg_max_extra_caps\<rbrace>" apply (cases buf) apply (simp, wp, simp) apply (simp add: msg_max_length_def) apply (subst hoare_liftM_subst, simp add: o_def) apply (rule hoare_pre) apply (rule mapM_length, simp) apply (clarsimp simp: valid_message_info_def msg_max_extra_caps_def
                        word_le_nat_alt
                 intro: length_upt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_message_info mi\<rbrace> get_extra_cptrs buf mi \<lbrace>\<lambda>rv s. length rv \<le> msg_max_extra_caps\<rbrace> proof (prove)
goal (2 subgoals):
 1. buf = None \<Longrightarrow> \<lbrace>\<lambda>s. valid_message_info mi\<rbrace> get_extra_cptrs buf mi \<lbrace>\<lambda>rv s. length rv \<le> msg_max_extra_caps\<rbrace>
 2. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>\<lambda>s. valid_message_info mi\<rbrace> get_extra_cptrs buf mi \<lbrace>\<lambda>rv s. length rv \<le> msg_max_extra_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>\<lambda>s. valid_message_info mi\<rbrace> get_extra_cptrs buf mi \<lbrace>\<lambda>rv s. length rv \<le> msg_max_extra_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>\<lambda>s. valid_message_info mi\<rbrace> liftM (map to_bl) (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)]) \<lbrace>\<lambda>rv s. length rv \<le> msg_max_extra_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>\<lambda>s. valid_message_info mi\<rbrace> mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)] \<lbrace>\<lambda>x s. length x \<le> msg_max_extra_caps\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>?Q6 a\<rbrace> mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps mi)] \<lbrace>\<lambda>x s. length x \<le> msg_max_extra_caps\<rbrace>
 2. \<And>a s. \<lbrakk>buf = Some a; valid_message_info mi\<rbrakk> \<Longrightarrow> ?Q6 a s proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>buf = Some a; valid_message_info mi\<rbrakk> \<Longrightarrow> unat (mi_extra_caps mi) \<le> msg_max_extra_caps proof (prove)
goal:
No subgoals!
theory ArchIpc_AI

lemma cap_asid_rights_update [simp, Ipc_AI_assms]:
  "cap_asid (cap_rights_update R c) = cap_asid c" apply (simp add: cap_rights_update_def acap_rights_update_def split: cap.splits arch_cap.splits bool.splits) apply (clarsimp simp: cap_asid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_asid (cap_rights_update R c) = cap_asid c proof (prove)
goal (1 subgoal):
 1. \<forall>x31 x32 x33 x34 x35. c = ArchObjectCap (PageCap x31 x32 x33 x34 x35) \<longrightarrow> cap_asid (ArchObjectCap (PageCap x31 x32 (validate_vm_rights R) x34 x35)) = cap_asid (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) proof (prove)
goal:
No subgoals!
theory ArchIpc_AI

lemma cap_rights_update_vs_cap_ref[simp, Ipc_AI_assms]:
  "vs_cap_ref (cap_rights_update rs cap) = vs_cap_ref cap" by (simp add: vs_cap_ref_def cap_rights_update_def
                acap_rights_update_def
         split: cap.split arch_cap.split bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_cap_ref (cap_rights_update rs cap) = vs_cap_ref cap
theory ArchIpc_AI

lemma cap_range_update [simp, Ipc_AI_assms]:
  "cap_range (cap_rights_update R cap) = cap_range cap" by (auto simp add: cap_range_def cap_rights_update_def acap_rights_update_def
         split: cap.splits arch_cap.splits bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_range (cap_rights_update R cap) = cap_range cap
theory ArchIpc_AI

lemma obj_refs_remove_rights[simp, Ipc_AI_assms]:
  "obj_refs (remove_rights rs cap) = obj_refs cap" by (auto simp add: remove_rights_def cap_rights_update_def
                acap_rights_update_def
         split: cap.splits arch_cap.splits bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_refs (remove_rights rs cap) = obj_refs cap
theory ArchIpc_AI

lemma storeWord_um_inv:
  "\<lbrace>\<lambda>s. underlying_memory s = um\<rbrace>
   storeWord a v
   \<lbrace>\<lambda>_ s. is_aligned a 2 \<and> x \<in> {a,a+1,a+2,a+3} \<or> underlying_memory s x = um x\<rbrace>" apply (simp add: storeWord_def is_aligned_mask) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. underlying_memory s = um\<rbrace> storeWord a v \<lbrace>\<lambda>_ s. is_aligned a 2 \<and> x \<in> {a, a + 1, a + 2, a + 3} \<or> underlying_memory s x = um x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. underlying_memory s = um\<rbrace> do y <- assert (a && mask 2 = 0);
modify (underlying_memory_update (\<lambda>m. m(a := word_rsplit v ! 3, a + 1 := word_rsplit v ! 2, a + 2 := word_rsplit v ! Suc 0, a + 3 := word_rsplit v ! 0)))
od \<lbrace>\<lambda>_ s. a && mask 2 = 0 \<and> (x = a \<or> x = a + 1 \<or> x = a + 2 \<or> x = a + 3) \<or> underlying_memory s x = um x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. underlying_memory s = um \<Longrightarrow> a && mask 2 = 0 \<longrightarrow> a && mask 2 = 0 \<and> (x = a \<or> x = a + 1 \<or> x = a + 2 \<or> x = a + 3) \<or> underlying_memory (underlying_memory_update (\<lambda>m. m(a := word_rsplit v ! 3, a + 1 := word_rsplit v ! 2, a + 2 := word_rsplit v ! Suc 0, a + 3 := word_rsplit v ! 0)) s) x = um x proof (prove)
goal:
No subgoals!
theory ArchIpc_AI

lemma is_zombie_update_cap_data[simp, Ipc_AI_assms]:
  "is_zombie (update_cap_data P data cap) = is_zombie cap" by (simp add: update_cap_data_closedform is_zombie_def arch_update_cap_data_def
         split: cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_zombie (update_cap_data P data cap) = is_zombie cap
theory ArchIpc_AI

lemma valid_msg_length_strengthen [Ipc_AI_assms]:
  "valid_message_info mi \<longrightarrow> unat (mi_length mi) \<le> msg_max_length" apply (clarsimp simp: valid_message_info_def) apply (subgoal_tac "unat (mi_length mi) \<le> unat (of_nat msg_max_length :: word32)") apply (clarsimp simp: unat_of_nat msg_max_length_def) apply (clarsimp simp: un_ui_le word_le_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_message_info mi \<longrightarrow> unat (mi_length mi) \<le> msg_max_length proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mi_length mi \<le> word_of_nat msg_max_length; mi_extra_caps mi \<le> word_of_nat msg_max_extra_caps\<rbrakk> \<Longrightarrow> unat (mi_length mi) \<le> msg_max_length proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mi_length mi \<le> word_of_nat msg_max_length; mi_extra_caps mi \<le> word_of_nat msg_max_extra_caps; unat (mi_length mi) \<le> unat (word_of_nat msg_max_length)\<rbrakk> \<Longrightarrow> unat (mi_length mi) \<le> msg_max_length
 2. \<lbrakk>mi_length mi \<le> word_of_nat msg_max_length; mi_extra_caps mi \<le> word_of_nat msg_max_extra_caps\<rbrakk> \<Longrightarrow> unat (mi_length mi) \<le> unat (word_of_nat msg_max_length) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mi_length mi \<le> word_of_nat msg_max_length; mi_extra_caps mi \<le> word_of_nat msg_max_extra_caps\<rbrakk> \<Longrightarrow> unat (mi_length mi) \<le> unat (word_of_nat msg_max_length) proof (prove)
goal:
No subgoals!
theory ArchIpc_AI

lemma copy_mrs_in_user_frame[wp, Ipc_AI_assms]:
  "\<lbrace>in_user_frame p\<rbrace> copy_mrs t buf t' buf' n \<lbrace>\<lambda>rv. in_user_frame p\<rbrace>" by (simp add: in_user_frame_def) (wp hoare_vcg_ex_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_user_frame p\<rbrace> copy_mrs t buf t' buf' n \<lbrace>\<lambda>rv. in_user_frame p\<rbrace>
theory ArchIpc_AI

lemma as_user_getRestart_invs[wp]: "\<lbrace>P\<rbrace> as_user t getRestartPC \<lbrace>\<lambda>_. P\<rbrace>" by (simp add: getRestartPC_def, rule user_getreg_inv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> as_user t getRestartPC \<lbrace>\<lambda>_. P\<rbrace>
theory ArchIpc_AI

lemma make_arch_fault_msg_inv[wp]: "\<lbrace>P\<rbrace> make_arch_fault_msg f t \<lbrace>\<lambda>_. P\<rbrace>" apply (cases f) apply simp apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> make_arch_fault_msg f t \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. f = VMFault x1 x2 \<Longrightarrow> \<lbrace>P\<rbrace> make_arch_fault_msg f t \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. f = VMFault x1 x2 \<Longrightarrow> \<lbrace>P\<rbrace> do pc <- as_user t getRestartPC;
return (5, pc # x1 # x2)
od \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchIpc_AI

lemma make_fault_message_inv[wp, Ipc_AI_assms]:
  "\<lbrace>P\<rbrace> make_fault_msg ft t \<lbrace>\<lambda>rv. P\<rbrace>" apply (cases ft, simp_all split del: if_split) apply (wp as_user_inv getRestartPC_inv mapM_wp'
              | simp add: getRegister_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> make_fault_msg ft t \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13. ft = CapFault x11 x12 x13 \<Longrightarrow> \<lbrace>P\<rbrace> do pc <- as_user t getRestartPC;
return (1, pc # x11 # (if x12 then 1 else 0) # msg_from_lookup_failure x13)
od \<lbrace>\<lambda>rv. P\<rbrace>
 2. \<And>x2. ft = UnknownSyscallException x2 \<Longrightarrow> \<lbrace>P\<rbrace> do msg <- as_user t (mapM getRegister syscallMessage);
return (2, msg @ [x2])
od \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>x31 x32. ft = UserException x31 x32 \<Longrightarrow> \<lbrace>P\<rbrace> do msg <- as_user t (mapM getRegister exceptionMessage);
return (3, msg @ [x31, x32])
od \<lbrace>\<lambda>rv. P\<rbrace>
 4. \<And>x4. ft = ArchFault x4 \<Longrightarrow> \<lbrace>P\<rbrace> make_arch_fault_msg x4 t \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchIpc_AI

lemma do_fault_transfer_invs[wp, Ipc_AI_assms]:
  "\<lbrace>invs and tcb_at receiver\<rbrace>
      do_fault_transfer badge sender receiver recv_buf
   \<lbrace>\<lambda>rv. invs\<rbrace>" by (simp add: do_fault_transfer_def split_def | wp
    | clarsimp split: option.split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at receiver\<rbrace> do_fault_transfer badge sender receiver recv_buf \<lbrace>\<lambda>rv. invs\<rbrace>
theory ArchIpc_AI

lemma do_normal_transfer_non_null_cte_wp_at [Ipc_AI_assms]:
  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\<rbrace>
   do_normal_transfer st send_buffer ep b gr rt recv_buffer
   \<lbrace>\<lambda>_. cte_wp_at (P and ((\<noteq>) cap.NullCap)) ptr\<rbrace>" unfolding do_normal_transfer_def apply simp apply (wp transfer_caps_non_null_cte_wp_at
    | clarsimp simp: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_normal_transfer st send_buffer ep b gr rt recv_buffer \<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 mi <- get_message_info st;
caps <- if gr then lookup_extra_caps st send_buffer mi <catch> K (return []) else return [];
mrs_transferred <- copy_mrs st send_buffer rt recv_buffer (mi_length mi);
mi' <- transfer_caps mi caps ep rt recv_buffer;
set_message_info rt $ MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi);
as_user rt $ setRegister badge_register b
od \<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 mi <- get_message_info st;
caps <- if gr then lookup_extra_caps st send_buffer mi <catch> (\<lambda>y. return []) else return [];
mrs_transferred <- copy_mrs st send_buffer rt recv_buffer (mi_length mi);
mi' <- transfer_caps mi caps ep rt recv_buffer;
y <- set_message_info rt (MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user rt (setRegister badge_register b)
od \<lbrace>\<lambda>_. cte_wp_at (P and (\<noteq>) NullCap) ptr\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchIpc_AI

lemma is_derived_ReplyCap [simp, Ipc_AI_assms]:
  "\<And>m p R. is_derived m p (cap.ReplyCap t False R) = (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t)" apply (subst fun_eq_iff) apply clarsimp apply (case_tac x, simp_all add: is_derived_def is_cap_simps
                                   cap_master_cap_def conj_comms is_pt_cap_def
                                   vs_cap_ref_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>m p R. is_derived m p (ReplyCap t False R) = (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) proof (prove)
goal (1 subgoal):
 1. \<And>m p R. \<forall>x. is_derived m p (ReplyCap t False R) x = (is_master_reply_cap x \<and> obj_ref_of x = t) proof (prove)
goal (1 subgoal):
 1. \<And>m a b R x. is_derived m (a, b) (ReplyCap t False R) x = (is_master_reply_cap x \<and> obj_ref_of x = t) proof (prove)
goal:
No subgoals!
theory ArchIpc_AI

lemma do_normal_transfer_tcb_caps:
  assumes imp: "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c"
  shows
  "\<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t\<rbrace>
   do_normal_transfer st sb ep badge grant rt rb
   \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace>" apply (simp add: do_normal_transfer_def) apply (rule hoare_pre) apply (wp hoare_drop_imps transfer_caps_tcb_caps
     | simp add:imp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t\<rbrace> do_normal_transfer st sb ep badge grant rt rb \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t\<rbrace> do mi <- get_message_info st;
caps <- if grant then lookup_extra_caps st sb mi <catch> (\<lambda>y. return []) else return [];
mrs_transferred <- copy_mrs st sb rt rb (mi_length mi);
mi' <- transfer_caps mi caps ep rt rb;
y <- set_message_info rt (MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user rt (setRegister badge_register badge)
od \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do mi <- get_message_info st;
caps <- if grant then lookup_extra_caps st sb mi <catch> (\<lambda>y. return []) else return [];
mrs_transferred <- copy_mrs st sb rt rb (mi_length mi);
mi' <- transfer_caps mi caps ep rt rb;
y <- set_message_info rt (MI mrs_transferred (mi_extra_caps mi') (mi_caps_unwrapped mi') (mi_label mi));
as_user rt (setRegister badge_register badge)
od \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace>
 2. \<And>s. (valid_objs and cte_wp_at P (t, ref) and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!