kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_DP

lemma is_pending_cap_reset_cap_asid:
  "reset_cap_asid c = reset_cap_asid c'
  \<Longrightarrow> is_pending_cap c = is_pending_cap c'" apply (case_tac c') apply (clarsimp simp: is_pending_cap_def dest!:reset_cap_asid_simps2)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid c = reset_cap_asid c' \<Longrightarrow> is_pending_cap c = is_pending_cap c' proof (prove)
goal (27 subgoals):
 1. \<lbrakk>reset_cap_asid c = reset_cap_asid c'; c' = NullCap\<rbrakk> \<Longrightarrow> is_pending_cap c = is_pending_cap c'
 2. \<And>x21 x22 x23. \<lbrakk>reset_cap_asid c = reset_cap_asid c'; c' = UntypedCap x21 x22 x23\<rbrakk> \<Longrightarrow> is_pending_cap c = is_pending_cap c'
 3. \<And>x31 x32 x33. \<lbrakk>reset_cap_asid c = reset_cap_asid c'; c' = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> is_pending_cap c = is_pending_cap c'
 4. \<And>x41 x42 x43. \<lbrakk>reset_cap_asid c = reset_cap_asid c'; c' = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> is_pending_cap c = is_pending_cap c'
 5. \<And>x51 x52. \<lbrakk>reset_cap_asid c = reset_cap_asid c'; c' = ReplyCap x51 x52\<rbrakk> \<Longrightarrow> is_pending_cap c = is_pending_cap c'
 6. \<And>x6. \<lbrakk>reset_cap_asid c = reset_cap_asid c'; c' = MasterReplyCap x6\<rbrakk> \<Longrightarrow> is_pending_cap c = is_pending_cap c'
 7. \<And>x71 x72 x73 x74. \<lbrakk>reset_cap_asid c = reset_cap_asid c'; c' = CNodeCap x71 x72 x73 x74\<rbrakk> \<Longrightarrow> is_pending_cap c = is_pending_cap c'
 8. \<And>x8. \<lbrakk>reset_cap_asid c = reset_cap_asid c'; c' = TcbCap x8\<rbrakk> \<Longrightarrow> is_pending_cap c = is_pending_cap c'
 9. \<lbrakk>reset_cap_asid c = reset_cap_asid c'; c' = DomainCap\<rbrakk> \<Longrightarrow> is_pending_cap c = is_pending_cap c'
 10. \<And>x101 x102 x103 x104 x105 x106. \<lbrakk>reset_cap_asid c = reset_cap_asid c'; c' = PendingSyncSendCap x101 x102 x103 x104 x105 x106\<rbrakk> \<Longrightarrow> is_pending_cap c = is_pending_cap c'
A total of 27 subgoals... proof (prove)
goal:
No subgoals!
theory Arch_DP

lemma cdl_get_pde_result_pt:
  "\<lbrace> < (pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p b None \<and>* sep_true> \<rbrace>
    cdl_get_pde (cdl_lookup_pd_slot pd ptr)
  \<lbrace>\<lambda>r s. \<exists>asid. r = PageTableCap p b asid\<rbrace>" apply (clarsimp simp:cdl_get_pde_def cdl_lookup_pd_slot_def) apply wp apply (clarsimp dest!:opt_cap_sep_imp) apply (clarsimp simp:reset_cap_asid_def split:cdl_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p b None \<and>* (\<lambda>s. True))\<rbrace> cdl_get_pde (cdl_lookup_pd_slot pd ptr) \<lbrace>\<lambda>r s. \<exists>asid. r = PageTableCap p b asid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p b None \<and>* (\<lambda>s. True))\<rbrace> get_cap (pd, unat (ptr >> 20)) \<lbrace>\<lambda>r s. \<exists>asid. r = PageTableCap p b asid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift ((pd, unat (ptr >> 20)) \<mapsto>c PageTableCap p b None \<and>* (\<lambda>s. True)) s \<Longrightarrow> opt_cap (pd, unat (ptr >> 20)) s \<noteq> None \<longrightarrow> (\<exists>asid. the (opt_cap (pd, unat (ptr >> 20)) s) = PageTableCap p b asid) proof (prove)
goal (1 subgoal):
 1. \<And>s cap'. \<lbrakk>reset_cap_asid cap' = PageTableCap p b None; opt_cap (pd, unat (ptr >> 20)) s = Some cap'\<rbrakk> \<Longrightarrow> \<exists>asid. cap' = PageTableCap p b asid proof (prove)
goal:
No subgoals!
theory Arch_DP

lemma invoke_page_table_wp:
  "pinv = PageTableMap real_pt_cap pt_cap pt_cap_ref pt_target_slot \<Longrightarrow>
  \<lbrace> < pt_cap_ref \<mapsto>c - \<and>* pt_target_slot \<mapsto>c - \<and>* P> \<rbrace>
  invoke_page_table pinv
  \<lbrace>\<lambda>_.  <pt_cap_ref \<mapsto>c real_pt_cap \<and>* pt_target_slot \<mapsto>c pt_cap \<and>* P>\<rbrace>" apply (clarsimp simp:invoke_page_table_def) apply (wp sep_wp: insert_cap_orphan_wp set_cap_wp, sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pinv = PageTableMap real_pt_cap pt_cap pt_cap_ref pt_target_slot \<Longrightarrow> \<lbrace>cdl.lift (pt_cap_ref \<mapsto>c - \<and>* pt_target_slot \<mapsto>c - \<and>* P)\<rbrace> invoke_page_table pinv \<lbrace>\<lambda>_. cdl.lift (pt_cap_ref \<mapsto>c real_pt_cap \<and>* pt_target_slot \<mapsto>c pt_cap \<and>* P)\<rbrace> proof (prove)
goal (1 subgoal):
 1. pinv = PageTableMap real_pt_cap pt_cap pt_cap_ref pt_target_slot \<Longrightarrow> \<lbrace>cdl.lift (pt_cap_ref \<mapsto>c - \<and>* pt_target_slot \<mapsto>c - \<and>* P)\<rbrace> do y <- set_cap pt_cap_ref real_pt_cap;
insert_cap_orphan pt_cap pt_target_slot
od \<lbrace>\<lambda>_. cdl.lift (pt_cap_ref \<mapsto>c real_pt_cap \<and>* pt_target_slot \<mapsto>c pt_cap \<and>* P)\<rbrace> proof (prove)
goal:
No subgoals!
theory Arch_DP

lemma set_split_single:
  "a \<in>A \<Longrightarrow> A = A - {a} \<union> {a}" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<in> A \<Longrightarrow> A = A - {a} \<union> {a}
theory Arch_DP

lemma sep_map_c_asid_simp:
  "(slot \<mapsto>c FrameCap dev ptr rights sz real_type option) = (slot \<mapsto>c FrameCap dev ptr rights sz real_type None)"
  "(slot \<mapsto>c PageTableCap ptr real_type option) = (slot \<mapsto>c PageTableCap ptr real_type None)"
  "(slot \<mapsto>c PageDirectoryCap ptr real_type option') = (slot \<mapsto>c PageDirectoryCap ptr real_type None)" by (simp_all add:sep_map_c_asid_reset)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slot \<mapsto>c FrameCap dev ptr rights sz real_type option = slot \<mapsto>c FrameCap dev ptr rights sz real_type None &&& slot \<mapsto>c PageTableCap ptr real_type option = slot \<mapsto>c PageTableCap ptr real_type None &&& slot \<mapsto>c PageDirectoryCap ptr real_type option' = slot \<mapsto>c PageDirectoryCap ptr real_type None
theory TCB_DP

lemma reset_cap_asid_reset_mem_mapping:
  "reset_cap_asid (reset_mem_mapping cap) = reset_cap_asid cap" by (clarsimp simp: reset_cap_asid_def cap_type_def split:cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid (reset_mem_mapping cap) = reset_cap_asid cap
theory TCB_DP

lemma invoke_tcb_write:
  "cap = RunningCap \<or> cap = RestartCap
  \<Longrightarrow> \<lbrace>< (tcb,tcb_pending_op_slot) \<mapsto>c cap  \<and>*  R >\<rbrace>
  invoke_tcb  (WriteRegisters tcb x y z)
  \<lbrace>\<lambda>_. < (tcb,tcb_pending_op_slot) \<mapsto>c cap  \<and>*  R >\<rbrace>" apply (clarsimp simp: invoke_tcb_def) apply (wp restart_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap = RunningCap \<or> cap = RestartCap \<Longrightarrow> \<lbrace>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R)\<rbrace> invoke_tcb (WriteRegisters tcb x y z) \<lbrace>\<lambda>_. cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. cap = RunningCap \<or> cap = RestartCap \<Longrightarrow> \<lbrace>cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R)\<rbrace> liftE (do y <- corrupt_tcb_intent tcb;
when x (restart tcb)
od) \<lbrace>\<lambda>_. cdl.lift ((tcb, tcb_pending_op_slot) \<mapsto>c cap \<and>* R)\<rbrace> proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma not_memory_cap_reset_asid:
   " \<lbrakk> ~is_memory_cap tcb_cap; reset_cap_asid tcb_cap = reset_cap_asid cap\<rbrakk> \<Longrightarrow>
       cap = tcb_cap" apply (drule reset_cap_asid_id) apply (clarsimp simp: is_memory_cap_def split: cdl_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_memory_cap tcb_cap; reset_cap_asid tcb_cap = reset_cap_asid cap\<rbrakk> \<Longrightarrow> cap = tcb_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_memory_cap tcb_cap; tcb_cap = cap \<or> (\<exists>a b c d e f. tcb_cap = FrameCap f a b c d e) \<or> (\<exists>a b c. tcb_cap = PageTableCap a b c) \<or> (\<exists>a b c. tcb_cap = PageDirectoryCap a b c)\<rbrakk> \<Longrightarrow> cap = tcb_cap proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma not_memory_cap_reset_asid':
   " \<lbrakk>reset_cap_asid cap = reset_cap_asid tcb_cap; ~is_memory_cap tcb_cap\<rbrakk> \<Longrightarrow>
       cap = tcb_cap" apply (clarsimp simp: not_memory_cap_reset_asid) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reset_cap_asid cap = reset_cap_asid tcb_cap; \<not> is_memory_cap tcb_cap\<rbrakk> \<Longrightarrow> cap = tcb_cap proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma tcb_empty_thread_slot_wpE:
  "\<lbrace><(target_tcb,slot) \<mapsto>c NullCap \<and>* R>\<rbrace>
  tcb_empty_thread_slot target_tcb slot
  \<lbrace>\<lambda>_. <(target_tcb,slot) \<mapsto>c NullCap \<and>* R>\<rbrace>, \<lbrace>E\<rbrace>" apply (clarsimp simp: tcb_empty_thread_slot_def | wp hoare_FalseE[where f="delete_cap x" for x])+ apply (clarsimp dest!:opt_cap_sep_imp simp:reset_cap_asid_simps2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift ((target_tcb, slot) \<mapsto>c NullCap \<and>* R)\<rbrace> tcb_empty_thread_slot target_tcb slot \<lbrace>\<lambda>_. cdl.lift ((target_tcb, slot) \<mapsto>c NullCap \<and>* R)\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift ((target_tcb, slot) \<mapsto>c NullCap \<and>* R) s; the (opt_cap (target_tcb, slot) s) \<noteq> NullCap\<rbrakk> \<Longrightarrow> opt_cap (target_tcb, slot) s = None proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma sep_any_All_side: "\<lbrace><ptr \<mapsto>c - \<and>* R> and P\<rbrace> f \<lbrace>Q\<rbrace> = (\<forall>x. \<lbrace><ptr \<mapsto>c x \<and>* R> and P\<rbrace> f \<lbrace>Q\<rbrace>)" apply (clarsimp simp: valid_def validE_def pred_conj_def tcb_update_cspace_root_def sep_any_All) apply (rule iffI) apply (metis (full_types) sep_any_exist)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (ptr \<mapsto>c - \<and>* R) and P\<rbrace> f \<lbrace>Q\<rbrace> = (\<forall>x. \<lbrace>cdl.lift (ptr \<mapsto>c x \<and>* R) and P\<rbrace> f \<lbrace>Q\<rbrace>) proof (prove)
goal (1 subgoal):
 1. (\<forall>s. cdl.lift (ptr \<mapsto>c - \<and>* R) s \<and> P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q r s')) = (\<forall>x s. cdl.lift (ptr \<mapsto>c x \<and>* R) s \<and> P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q r s')) proof (prove)
goal (2 subgoals):
 1. \<forall>s. cdl.lift (ptr \<mapsto>c - \<and>* R) s \<and> P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q r s') \<Longrightarrow> \<forall>x s. cdl.lift (ptr \<mapsto>c x \<and>* R) s \<and> P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q r s')
 2. \<forall>x s. cdl.lift (ptr \<mapsto>c x \<and>* R) s \<and> P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q r s') \<Longrightarrow> \<forall>s. cdl.lift (ptr \<mapsto>c - \<and>* R) s \<and> P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q r s') proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma is_cnode_cap_not_memory_cap:
  "is_cnode_cap cap \<Longrightarrow> \<not> is_memory_cap cap" by (clarsimp simp: cap_type_def is_memory_cap_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cnode_cap cap \<Longrightarrow> \<not> is_memory_cap cap
theory TCB_DP

lemma sep_map_c_asid_reset': "\<lbrakk>(ptr \<mapsto>c cap) s ; reset_cap_asid cap = reset_cap_asid cap'\<rbrakk> \<Longrightarrow>  (ptr \<mapsto>c cap') s" apply (clarsimp dest!: sep_map_c_asid_reset[where ptr=ptr]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ptr \<mapsto>c cap) s; reset_cap_asid cap = reset_cap_asid cap'\<rbrakk> \<Longrightarrow> (ptr \<mapsto>c cap') s proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma sep_map_c_asid_reset'': "\<lbrakk>(ptr \<mapsto>c cap) s ; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow>  (ptr \<mapsto>c cap') s" apply (clarsimp dest!: sep_map_c_asid_reset[where ptr=ptr]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ptr \<mapsto>c cap) s; reset_cap_asid cap' = reset_cap_asid cap\<rbrakk> \<Longrightarrow> (ptr \<mapsto>c cap') s proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma decode_tcb_invocation_wp[wp]:
"\<lbrace>P\<rbrace>
decode_tcb_invocation cap cap_ref caps (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer)
\<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>" apply (clarsimp simp: decode_tcb_invocation_def) apply wp apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> decode_tcb_invocation cap cap_ref caps (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE cspace_root <- throw_on_none (get_index caps 0);
vspace_root <- throw_on_none (get_index caps (Suc 0));
buffer_frame <- throw_on_none (get_index caps 2);
returnOk (ThreadControl (cap_object cap) cap_ref (Some fault_ep) (Some (cdl_update_cnode_cap_data (fst cspace_root) cspace_root_data, snd cspace_root)) (Some vspace_root) (if buffer \<noteq> 0 then Some (reset_mem_mapping (fst buffer_frame), snd buffer_frame) else None))
odE \<sqinter> throw \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> ((\<lambda>s. P s \<and> P s \<and> P s \<and> P s) and (\<lambda>s. P s \<and> True)) s proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma throw_on_none_rvR:
 "\<lbrace>\<lambda>s. case x of None \<Rightarrow> True | Some y \<Rightarrow> P y s\<rbrace>
    throw_on_none x
  \<lbrace>P\<rbrace>, -" apply (clarsimp simp: throw_on_none_def split:option.splits) apply (safe, wp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case x of None \<Rightarrow> True | Some y \<Rightarrow> P y s\<rbrace> throw_on_none x \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. (x = None \<longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> throw \<lbrace>P\<rbrace>, -) \<and> (\<forall>x2. x = Some x2 \<longrightarrow> \<lbrace>P x2\<rbrace> returnOk x2 \<lbrace>P\<rbrace>, -) proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma hoare_whenE_R_wp:
     "\<lbrace>\<lambda>s. Q s \<and> ~P\<rbrace>
       whenE P f
       \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>E\<rbrace> " apply (clarsimp simp: whenE_def) apply (wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q s \<and> \<not> P\<rbrace> whenE P f \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> P \<Longrightarrow> \<lbrace>Q\<rbrace> returnOk () \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma sep_map_anyD:
  "(m p e \<and>* P ) s \<Longrightarrow> (sep_any m p \<and>* P) s" by sep_solve

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m p e \<and>* P) s \<Longrightarrow> (sep_any m p \<and>* P) s
theory TCB_DP

lemma tcb_update_vspace_root_inv:
"\<lbrace>\<lambda>s.  <(a, tcb_vspace_slot) \<mapsto>c NullCap \<and>* R> s \<and> P (cdl_current_thread s)\<rbrace>
   tcb_update_vspace_root a b c
 \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>" apply (clarsimp simp: tcb_update_vspace_root_def) apply (wp hoare_drop_imps whenE_wp
       | simp add: tcb_update_vspace_root_def tcb_update_thread_slot_def)+ apply (wp tcb_empty_thread_slot_wp_inv) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift ((a, tcb_vspace_slot) \<mapsto>c NullCap \<and>* R) s \<and> P (cdl_current_thread s)\<rbrace> tcb_update_vspace_root a b c \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift ((a, tcb_vspace_slot) \<mapsto>c NullCap \<and>* R) s \<and> P (cdl_current_thread s)\<rbrace> doE y <- tcb_empty_thread_slot a tcb_vspace_slot;
src_cap <- liftE (get_cap (snd c));
whenE (cdl_same_arch_obj_as (fst c) src_cap) (tcb_update_thread_slot a b tcb_vspace_slot c)
odE \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> tcb_empty_thread_slot a tcb_vspace_slot \<lbrace>\<lambda>y s. (cdl_same_arch_obj_as (fst c) (the (opt_cap (snd c) s)) \<longrightarrow> (\<exists>y. opt_cap (snd c) s = Some y) \<longrightarrow> (\<exists>y. opt_cap b s = Some y) \<longrightarrow> P (cdl_current_thread s)) \<and> (\<not> cdl_same_arch_obj_as (fst c) (the (opt_cap (snd c) s)) \<longrightarrow> (\<exists>y. opt_cap (snd c) s = Some y) \<longrightarrow> P (cdl_current_thread s))\<rbrace>, \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 2. \<And>s. cdl.lift ((a, tcb_vspace_slot) \<mapsto>c NullCap \<and>* R) s \<and> P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift ((a, tcb_vspace_slot) \<mapsto>c NullCap \<and>* R) s \<and> P (cdl_current_thread s) \<Longrightarrow> (cdl.lift ((a, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ?R39) and (\<lambda>s. P (cdl_current_thread s))) s \<and> (cdl.lift ((a, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ?R41) and (\<lambda>s. cdl_same_arch_obj_as (fst c) (the (opt_cap (snd c) s)) \<longrightarrow> (\<exists>y. opt_cap (snd c) s = Some y) \<longrightarrow> (\<exists>y. opt_cap b s = Some y) \<longrightarrow> P (cdl_current_thread s))) s \<and> (cdl.lift ((a, tcb_vspace_slot) \<mapsto>c NullCap \<and>* ?R43) and (\<lambda>s. \<not> cdl_same_arch_obj_as (fst c) (the (opt_cap (snd c) s)) \<longrightarrow> (\<exists>y. opt_cap (snd c) s = Some y) \<longrightarrow> P (cdl_current_thread s))) s proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma tcb_update_cspace_root_inv:
"\<lbrace>\<lambda>s.  <(a, tcb_cspace_slot) \<mapsto>c NullCap \<and>* R> s \<and> P (cdl_current_thread s)\<rbrace>
   tcb_update_cspace_root a b c
 \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>" apply (clarsimp simp: tcb_update_cspace_root_def) apply (wp hoare_drop_imps whenE_wp
       | simp add: tcb_update_vspace_root_def tcb_update_thread_slot_def)+ apply (wp tcb_empty_thread_slot_wp_inv) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift ((a, tcb_cspace_slot) \<mapsto>c NullCap \<and>* R) s \<and> P (cdl_current_thread s)\<rbrace> tcb_update_cspace_root a b c \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift ((a, tcb_cspace_slot) \<mapsto>c NullCap \<and>* R) s \<and> P (cdl_current_thread s)\<rbrace> doE y <- tcb_empty_thread_slot a tcb_cspace_slot;
src_cap <- liftE (get_cap (snd c));
whenE (is_cnode_cap src_cap \<and> cap_object src_cap = cap_object (fst c)) (tcb_update_thread_slot a b tcb_cspace_slot c)
odE \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> tcb_empty_thread_slot a tcb_cspace_slot \<lbrace>\<lambda>y s. (is_cnode_cap (the (opt_cap (snd c) s)) \<and> cap_object (the (opt_cap (snd c) s)) = cap_object (fst c) \<longrightarrow> (\<exists>y. opt_cap (snd c) s = Some y) \<longrightarrow> (\<exists>y. opt_cap b s = Some y) \<longrightarrow> P (cdl_current_thread s)) \<and> ((is_cnode_cap (the (opt_cap (snd c) s)) \<longrightarrow> cap_object (the (opt_cap (snd c) s)) \<noteq> cap_object (fst c)) \<longrightarrow> (\<exists>y. opt_cap (snd c) s = Some y) \<longrightarrow> P (cdl_current_thread s))\<rbrace>, \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 2. \<And>s. cdl.lift ((a, tcb_cspace_slot) \<mapsto>c NullCap \<and>* R) s \<and> P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift ((a, tcb_cspace_slot) \<mapsto>c NullCap \<and>* R) s \<and> P (cdl_current_thread s) \<Longrightarrow> (cdl.lift ((a, tcb_cspace_slot) \<mapsto>c NullCap \<and>* ?R39) and (\<lambda>s. P (cdl_current_thread s))) s \<and> (cdl.lift ((a, tcb_cspace_slot) \<mapsto>c NullCap \<and>* ?R41) and (\<lambda>s. is_cnode_cap (the (opt_cap (snd c) s)) \<and> cap_object (the (opt_cap (snd c) s)) = cap_object (fst c) \<longrightarrow> (\<exists>y. opt_cap (snd c) s = Some y) \<longrightarrow> (\<exists>y. opt_cap b s = Some y) \<longrightarrow> P (cdl_current_thread s))) s \<and> (cdl.lift ((a, tcb_cspace_slot) \<mapsto>c NullCap \<and>* ?R43) and (\<lambda>s. (is_cnode_cap (the (opt_cap (snd c) s)) \<longrightarrow> cap_object (the (opt_cap (snd c) s)) \<noteq> cap_object (fst c)) \<longrightarrow> (\<exists>y. opt_cap (snd c) s = Some y) \<longrightarrow> P (cdl_current_thread s))) s proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma tcb_update_ipc_buffer_inv:
"\<lbrace>\<lambda>s.  <(a, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R> s \<and> P (cdl_current_thread s)\<rbrace>
   tcb_update_ipc_buffer a b c
 \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>" apply (clarsimp simp: tcb_update_ipc_buffer_def) apply (wp hoare_drop_imps whenE_wp
       | simp add: tcb_update_vspace_root_def tcb_update_thread_slot_def)+ apply (wp tcb_empty_thread_slot_wp_inv) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift ((a, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s \<and> P (cdl_current_thread s)\<rbrace> tcb_update_ipc_buffer a b c \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift ((a, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s \<and> P (cdl_current_thread s)\<rbrace> doE y <- tcb_empty_thread_slot a tcb_ipcbuffer_slot;
y <- liftE (corrupt_tcb_intent a);
src_cap <- liftE (get_cap (snd c));
whenE (cdl_same_arch_obj_as (fst c) src_cap) (tcb_update_thread_slot a b tcb_ipcbuffer_slot c)
odE \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> tcb_empty_thread_slot a tcb_ipcbuffer_slot \<lbrace>\<lambda>a b. P (cdl_current_thread b)\<rbrace>, \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>
 2. \<And>s. cdl.lift ((a, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s \<and> P (cdl_current_thread s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift ((a, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* R) s \<and> P (cdl_current_thread s) \<Longrightarrow> (cdl.lift ((a, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* ?R54) and (\<lambda>s. P (cdl_current_thread s))) s \<and> (cdl.lift ((a, tcb_ipcbuffer_slot) \<mapsto>c NullCap \<and>* ?R56) and (\<lambda>a. P (cdl_current_thread a))) s proof (prove)
goal:
No subgoals!