kings-crown/FVELER_Isabelle huggingface dataset:
theory TCB_DP

lemma decode_invocation_tcb_current_thread_inv[wp]:
 "\<lbrace>\<lambda>s. is_tcb_cap c \<and> P (cdl_current_thread s)\<rbrace>
       decode_invocation c (a, b) cs
        (TcbIntent (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr))
  \<lbrace>\<lambda>_ s. P (cdl_current_thread s) \<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: decode_tcb_invocation_simps) apply (wp) apply (clarsimp simp: comp_def) apply (wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_tcb_cap c \<and> P (cdl_current_thread s)\<rbrace> decode_invocation c (a, b) cs (TcbIntent (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr)) \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. is_tcb_cap c \<and> P (cdl_current_thread s) \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_invocation c (a, b) cs (TcbIntent (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr)) \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_tcb_cap c; P (cdl_current_thread s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftME InvokeTcb (decode_tcb_invocation c (a, b) cs (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr)) \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_tcb_cap c; P (cdl_current_thread s)\<rbrakk> \<Longrightarrow> \<lbrace>?P'6 s\<rbrace> decode_tcb_invocation c (a, b) cs (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr) \<lbrace>(\<lambda>_ s. P (cdl_current_thread s)) \<circ> InvokeTcb\<rbrace>, -
 2. \<And>s sa. \<lbrakk>is_tcb_cap c; P (cdl_current_thread s); s = sa\<rbrakk> \<Longrightarrow> P (cdl_current_thread sa) \<and> ?P'6 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_tcb_cap c; P (cdl_current_thread s)\<rbrakk> \<Longrightarrow> \<lbrace>?P'6 s\<rbrace> decode_tcb_invocation c (a, b) cs (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr) \<lbrace>\<lambda>_ s. P (cdl_current_thread s)\<rbrace>, -
 2. \<And>s sa. \<lbrakk>is_tcb_cap c; P (cdl_current_thread s); s = sa\<rbrakk> \<Longrightarrow> P (cdl_current_thread sa) \<and> ?P'6 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>is_tcb_cap c; P (cdl_current_thread s); s = sa\<rbrakk> \<Longrightarrow> P (cdl_current_thread sa) \<and> P (cdl_current_thread sa) proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma is_tcb_cap_is_object:  "is_tcb_cap tcb_cap  \<Longrightarrow> TcbCap (cap_object tcb_cap) = tcb_cap" by (clarsimp simp: cap_type_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_tcb_cap tcb_cap \<Longrightarrow> TcbCap (cap_object tcb_cap) = tcb_cap
theory TCB_DP

lemma reset_cap_asid_mem_mapping:
  "\<lbrakk>is_frame_cap buffer_frame_cap; reset_cap_asid xc = reset_cap_asid buffer_frame_cap\<rbrakk> \<Longrightarrow>
    reset_cap_asid buffer_frame_cap = reset_cap_asid (reset_mem_mapping xc)" apply (clarsimp simp: cap_type_def split:cdl_cap.splits) apply (clarsimp simp: reset_cap_asid_def split:cdl_cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_frame_cap buffer_frame_cap; reset_cap_asid xc = reset_cap_asid buffer_frame_cap\<rbrakk> \<Longrightarrow> reset_cap_asid buffer_frame_cap = reset_cap_asid (reset_mem_mapping xc) proof (prove)
goal (1 subgoal):
 1. \<And>x171 x172 x173 x174 x175 x176. \<lbrakk>reset_cap_asid xc = FrameCap x171 x172 x173 x174 x175 None; buffer_frame_cap = FrameCap x171 x172 x173 x174 x175 x176\<rbrakk> \<Longrightarrow> FrameCap x171 x172 x173 x174 x175 None = reset_cap_asid (reset_mem_mapping xc) proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma split_error_validE: "\<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - \<rbrakk> \<Longrightarrow> \<lbrace>P and E\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>\<lambda>_. E\<rbrace>" apply (clarsimp simp: valid_def validE_def validE_R_def split: sum.splits) apply (safe, fastforce+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P and E\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> \<forall>x2. r = Inr x2 \<longrightarrow> Q x2 s'); \<And>P. \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, x) \<Rightarrow> P x); (a, b) \<in> fst (f s); P s; E s\<rbrakk> \<Longrightarrow> ((\<exists>x1. a = Inl x1) \<longrightarrow> E b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> Q x2 b) proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma "\<lbrakk><cur_thread \<mapsto>f root_tcb \<and>* R> s; is_tcb root_tcb \<rbrakk> \<Longrightarrow> \<exists>x. <cur_thread \<mapsto>f Tcb x \<and>* R> s" apply (clarsimp simp: is_tcb_def split: cdl_object.splits) apply (rule) apply (sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl.lift (cur_thread \<mapsto>f root_tcb \<and>* R) s; is_tcb root_tcb\<rbrakk> \<Longrightarrow> \<exists>x. cdl.lift (cur_thread \<mapsto>f Tcb x \<and>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>cdl.lift (cur_thread \<mapsto>f Tcb x3 \<and>* R) s; root_tcb = Tcb x3\<rbrakk> \<Longrightarrow> \<exists>x. cdl.lift (cur_thread \<mapsto>f Tcb x \<and>* R) s proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>cdl.lift (cur_thread \<mapsto>f Tcb x3 \<and>* R) s; root_tcb = Tcb x3\<rbrakk> \<Longrightarrow> cdl.lift (cur_thread \<mapsto>f Tcb (?x42 x3) \<and>* R) s proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma decode_invocation_tcb_configure_wp:
 "is_tcb_cap c \<Longrightarrow>
   \<lbrace>\<lambda>s. P s\<rbrace>
       decode_invocation c (a, b) cs
        (TcbIntent (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr))
  \<lbrace>\<lambda>_ s. P s\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: decode_tcb_invocation_simps) apply (wp) apply (clarsimp simp: comp_def) apply (wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_tcb_cap c \<Longrightarrow> \<lbrace>P\<rbrace> decode_invocation c (a, b) cs (TcbIntent (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr)) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_tcb_cap c; P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> decode_invocation c (a, b) cs (TcbIntent (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr)) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_tcb_cap c; P s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> liftME InvokeTcb (decode_tcb_invocation c (a, b) cs (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr)) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_tcb_cap c; P s\<rbrakk> \<Longrightarrow> \<lbrace>?P'5 s\<rbrace> decode_tcb_invocation c (a, b) cs (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr) \<lbrace>(\<lambda>_. P) \<circ> InvokeTcb\<rbrace>, -
 2. \<And>s sa. \<lbrakk>is_tcb_cap c; P s; s = sa\<rbrakk> \<Longrightarrow> P sa \<and> ?P'5 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_tcb_cap c; P s\<rbrakk> \<Longrightarrow> \<lbrace>?P'5 s\<rbrace> decode_tcb_invocation c (a, b) cs (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr) \<lbrace>\<lambda>_. P\<rbrace>, -
 2. \<And>s sa. \<lbrakk>is_tcb_cap c; P s; s = sa\<rbrakk> \<Longrightarrow> P sa \<and> ?P'5 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>is_tcb_cap c; P s; s = sa\<rbrakk> \<Longrightarrow> P sa \<and> P sa proof (prove)
goal:
No subgoals!
theory TCB_DP

lemma cap_object_update_cnode_data[simp]:
  "cap_object (cdl_update_cnode_cap_data cap data) = cap_object cap" by (simp add:cdl_update_cnode_cap_data_def cap_object_def
    split:cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_object (cdl_update_cnode_cap_data cap data) = cap_object cap
theory TCB_DP

lemma reset_cap_asid_tcb:
  "is_tcb_cap cap \<Longrightarrow> reset_cap_asid cap = cap" by (simp add:cap_type_def split:cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_tcb_cap cap \<Longrightarrow> reset_cap_asid cap = cap
theory TCB_DP

lemma cap_typeD:
  "is_tcb_cap tcb_cap \<Longrightarrow> \<exists>x. tcb_cap = TcbCap x" by (simp add:cap_type_def split:cdl_cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_tcb_cap tcb_cap \<Longrightarrow> \<exists>x. tcb_cap = TcbCap x
theory TCB_DP

lemma reset_cap_asid_pending:
  "reset_cap_asid cap' = reset_cap_asid cap
    \<Longrightarrow> is_pending_cap cap' = is_pending_cap cap" by (simp add: reset_cap_asid_def is_pending_cap_def split: cdl_cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap' = reset_cap_asid cap \<Longrightarrow> is_pending_cap cap' = is_pending_cap cap
theory CNode_DP

lemma invoke_cnode_insert_cdl_current_domain[wp]:
  "\<lbrace>\<lambda>s. P (cdl_current_domain s)\<rbrace>
    invoke_cnode (InsertCall cap src_slot dest_slot)
   \<lbrace>\<lambda>_ s. P (cdl_current_domain s) \<rbrace>" apply (simp add: invoke_cnode_def) apply (rule hoare_pre) apply (wp | wpc | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdl_current_domain s)\<rbrace> invoke_cnode (InsertCall cap src_slot dest_slot) \<lbrace>\<lambda>_ s. P (cdl_current_domain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdl_current_domain s)\<rbrace> liftE (insert_cap_sibling cap src_slot dest_slot \<sqinter> insert_cap_child cap src_slot dest_slot) \<lbrace>\<lambda>_ s. P (cdl_current_domain s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> liftE (insert_cap_sibling cap src_slot dest_slot \<sqinter> insert_cap_child cap src_slot dest_slot) \<lbrace>\<lambda>_ s. P (cdl_current_domain s)\<rbrace>
 2. \<And>s. P (cdl_current_domain s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory CNode_DP

lemma invoke_cnode_move_cdl_current_domain[wp]:
  "\<lbrace>\<lambda>s. P (cdl_current_domain s)\<rbrace>
    invoke_cnode (MoveCall a b c)
   \<lbrace>\<lambda>_ s. P (cdl_current_domain s) \<rbrace>" apply (simp add: invoke_cnode_def) apply (rule hoare_pre) apply (wp | wpc | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdl_current_domain s)\<rbrace> invoke_cnode (MoveCall a b c) \<lbrace>\<lambda>_ s. P (cdl_current_domain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdl_current_domain s)\<rbrace> liftE (move_cap a b c) \<lbrace>\<lambda>_ s. P (cdl_current_domain s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> liftE (move_cap a b c) \<lbrace>\<lambda>_ s. P (cdl_current_domain s)\<rbrace>
 2. \<And>s. P (cdl_current_domain s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory CNode_DP

lemma update_cap_rights_reset_cap_asid:
  "\<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; rights = rights'\<rbrakk>
  \<Longrightarrow> reset_cap_asid (update_cap_rights rights cap) = reset_cap_asid (update_cap_rights rights' cap')" by (case_tac cap',auto simp: update_cap_rights_def dest!:reset_cap_asid_simps2 )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; rights = rights'\<rbrakk> \<Longrightarrow> reset_cap_asid (update_cap_rights rights cap) = reset_cap_asid (update_cap_rights rights' cap')
theory IRQ_DP

lemma delete_cap_simple_format:
  "\<lbrace><ptr \<mapsto>c cap \<and>* R>  and K (\<not> ep_related_cap cap)\<rbrace> (\<lambda>s. delete_cap_simple ptr s) \<lbrace>\<lambda>_. <ptr \<mapsto>c NullCap \<and>* R>\<rbrace>" apply (clarsimp simp: pred_conj_def) apply (rule delete_cap_simple_wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (ptr \<mapsto>c cap \<and>* R) and K (\<not> ep_related_cap cap)\<rbrace> delete_cap_simple ptr \<lbrace>\<lambda>_. cdl.lift (ptr \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. cdl.lift (ptr \<mapsto>c cap \<and>* R) x \<and> \<not> ep_related_cap cap\<rbrace> delete_cap_simple ptr \<lbrace>\<lambda>_. cdl.lift (ptr \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal:
No subgoals!
theory IRQ_DP

lemma sep_map_i_cdl_irq: "<irq \<mapsto>irq irq_obj \<and>* R> s \<Longrightarrow> cdl_irq_node s irq = irq_obj" apply (clarsimp simp: sep_map_c_def sep_map_irq_def sep_conj_def sep_state_projection_def plus_sep_state_def sep_state_add_def) apply (clarsimp simp: map_add_def) apply (drule fun_cong[where x=irq]) apply (clarsimp split: option.splits) apply (clarsimp simp: sep_disj_sep_state_def sep_state_disj_def) by (metis (lifting) fun_upd_same map_disj_None_left' option.distinct(1))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl.lift (irq \<mapsto>irq irq_obj \<and>* R) s \<Longrightarrow> cdl_irq_node s irq = irq_obj proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) = sep_heap y; (\<lambda>irq. Some (cdl_irq_node s irq)) = [irq \<mapsto> irq_obj] ++ sep_irq_node y; sep_heap x = (\<lambda>x. None); sep_irq_node x = [irq \<mapsto> irq_obj]; R y\<rbrakk> \<Longrightarrow> cdl_irq_node s irq = irq_obj proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) = sep_heap y; (\<lambda>irq. Some (cdl_irq_node s irq)) = (\<lambda>x. case sep_irq_node y x of None \<Rightarrow> [irq \<mapsto> irq_obj] x | Some y \<Rightarrow> Some y); sep_heap x = (\<lambda>x. None); sep_irq_node x = [irq \<mapsto> irq_obj]; R y\<rbrakk> \<Longrightarrow> cdl_irq_node s irq = irq_obj proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) = sep_heap y; sep_heap x = (\<lambda>x. None); sep_irq_node x = [irq \<mapsto> irq_obj]; R y; Some (cdl_irq_node s irq) = (case sep_irq_node y irq of None \<Rightarrow> [irq \<mapsto> irq_obj] irq | Some y \<Rightarrow> Some y)\<rbrakk> \<Longrightarrow> cdl_irq_node s irq = irq_obj proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x ## y; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) = sep_heap y; sep_heap x = (\<lambda>x. None); sep_irq_node x = [irq \<mapsto> irq_obj]; R y; sep_irq_node y irq = Some (cdl_irq_node s irq)\<rbrakk> \<Longrightarrow> cdl_irq_node s irq = irq_obj proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>[irq \<mapsto> irq_obj] \<bottom> sep_irq_node y; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) = sep_heap y; sep_heap x = (\<lambda>x. None); sep_irq_node x = [irq \<mapsto> irq_obj]; R y; sep_irq_node y irq = Some (cdl_irq_node s irq)\<rbrakk> \<Longrightarrow> cdl_irq_node s irq = irq_obj
theory IRQ_DP

lemma sep_map_i_map_c:
  "<irq \<mapsto>irq irq_obj \<and>* (irq_obj, 0) \<mapsto>c cap \<and>* R> s \<Longrightarrow>
   <irq \<mapsto>irq irq_obj \<and>* (get_irq_slot irq s \<mapsto>c cap) \<and>* R> s" by (frule sep_map_i_cdl_irq, clarsimp simp: get_irq_slot_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl.lift (irq \<mapsto>irq irq_obj \<and>* (irq_obj, 0) \<mapsto>c cap \<and>* R) s \<Longrightarrow> cdl.lift (irq \<mapsto>irq irq_obj \<and>* get_irq_slot irq s \<mapsto>c cap \<and>* R) s
theory IRQ_DP

lemma invoke_irq_handler_clear_handler_wp:
  "\<lbrace>< irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R> and K (\<not> ep_related_cap cap)\<rbrace>
      invoke_irq_handler (ClearIrqHandler irq)
   \<lbrace>\<lambda>_. < irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c NullCap \<and>* R> \<rbrace>" apply (clarsimp simp: invoke_irq_handler_def, wp) apply (sep_wp delete_cap_simple_format[where cap=cap])+ apply (safe) apply (frule sep_map_i_cdl_irq, clarsimp simp: get_irq_slot_def) apply (sep_solve) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) and K (\<not> ep_related_cap cap)\<rbrace> invoke_irq_handler (ClearIrqHandler irq) \<lbrace>\<lambda>_. cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c NullCap \<and>* R)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B1 x\<rbrace> delete_cap_simple x \<lbrace>\<lambda>_. cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c NullCap \<and>* R)\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets (get_irq_slot irq) \<lbrace>?B1\<rbrace>
 3. \<And>s. (cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) and (\<lambda>y. \<not> ep_related_cap cap)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) and (\<lambda>y. \<not> ep_related_cap cap)) s \<Longrightarrow> cdl.lift (get_irq_slot irq s \<mapsto>c cap \<and>* (get_irq_slot irq s \<mapsto>c NullCap \<longrightarrow>* irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c NullCap \<and>* R) and K (\<not> ep_related_cap cap)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap\<rbrakk> \<Longrightarrow> cdl.lift (get_irq_slot irq s \<mapsto>c cap \<and>* (get_irq_slot irq s \<mapsto>c NullCap \<longrightarrow>* irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c NullCap \<and>* R)) s
 2. \<And>s. \<lbrakk>cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap\<rbrakk> \<Longrightarrow> cdl.lift (K (\<not> ep_related_cap cap)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift (irq \<mapsto>irq cdl_irq_node s irq \<and>* (cdl_irq_node s irq, 0) \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap; obj = cdl_irq_node s irq\<rbrakk> \<Longrightarrow> cdl.lift ((cdl_irq_node s irq, 0) \<mapsto>c cap \<and>* ((cdl_irq_node s irq, 0) \<mapsto>c NullCap \<longrightarrow>* irq \<mapsto>irq cdl_irq_node s irq \<and>* (cdl_irq_node s irq, 0) \<mapsto>c NullCap \<and>* R)) s
 2. \<And>s. \<lbrakk>cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap\<rbrakk> \<Longrightarrow> cdl.lift (K (\<not> ep_related_cap cap)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift (irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R) s; \<not> ep_related_cap cap\<rbrakk> \<Longrightarrow> cdl.lift (K (\<not> ep_related_cap cap)) s proof (prove)
goal:
No subgoals!
theory IRQ_DP

lemma invoke_irq_control_issue_handler_wp:
       "\<lbrace> <(dest_slot) \<mapsto>c cap \<and>* R> \<rbrace>
        invoke_irq_control (IssueIrqHandler irq control_slot dest_slot)
       \<lbrace>\<lambda>_. < (dest_slot) \<mapsto>c (IrqHandlerCap irq) \<and>* R> \<rbrace>" apply (clarsimp simp: invoke_irq_control_def, wp sep_wp: insert_cap_child_wp) apply (clarsimp) apply (sep_safe,sep_solve) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (dest_slot \<mapsto>c cap \<and>* R)\<rbrace> invoke_irq_control (IssueIrqHandler irq control_slot dest_slot) \<lbrace>\<lambda>_. cdl.lift (dest_slot \<mapsto>c IrqHandlerCap irq \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (dest_slot \<mapsto>c cap \<and>* R) s \<Longrightarrow> cdl.lift (dest_slot \<mapsto>c - \<and>* (dest_slot \<mapsto>c IrqHandlerCap irq \<longrightarrow>* dest_slot \<mapsto>c IrqHandlerCap irq \<and>* R) and K (cap_type (IrqHandlerCap irq) \<noteq> Some UntypedType)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (dest_slot \<mapsto>c cap \<and>* R) s \<Longrightarrow> cdl.lift (dest_slot \<mapsto>c - \<and>* (dest_slot \<mapsto>c IrqHandlerCap irq \<longrightarrow>* dest_slot \<mapsto>c IrqHandlerCap irq \<and>* R)) s proof (prove)
goal:
No subgoals!
theory IRQ_DP

lemma decode_invocation_irq_ack_rv':
"\<lbrace>\<lambda>s. P (AckIrq (the $ cdl_cap_irq cap)) s \<rbrace>
decode_irq_handler_invocation cap cap_ref caps (IrqHandlerAckIntent)
\<lbrace>P\<rbrace>, -" apply (clarsimp simp: decode_irq_handler_invocation_def) apply wp apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P (AckIrq (the $ cdl_cap_irq cap))\<rbrace> decode_irq_handler_invocation cap cap_ref caps IrqHandlerAckIntent \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>P (AckIrq (the (cdl_cap_irq cap)))\<rbrace> doE irq <- liftE (assert_opt (cdl_cap_irq cap));
returnOk (AckIrq irq)
odE \<sqinter> throw \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. P (AckIrq (the (cdl_cap_irq cap))) s \<Longrightarrow> ((\<lambda>s. True \<and> True \<and> (cdl_cap_irq cap \<noteq> None \<longrightarrow> P (AckIrq (the (cdl_cap_irq cap))) s)) and (\<lambda>s. True \<and> True)) s proof (prove)
goal:
No subgoals!
theory IRQ_DP

lemma decode_invocation_irq_clear_rv':
"\<lbrace>\<lambda>s. P (ClearIrqHandler (the $ cdl_cap_irq cap)) s \<rbrace>
decode_irq_handler_invocation cap cap_ref caps (IrqHandlerClearIntent)
\<lbrace>P\<rbrace>, -" apply (clarsimp simp: decode_irq_handler_invocation_def) apply wp apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P (ClearIrqHandler (the $ cdl_cap_irq cap))\<rbrace> decode_irq_handler_invocation cap cap_ref caps IrqHandlerClearIntent \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>P (ClearIrqHandler (the (cdl_cap_irq cap)))\<rbrace> doE irq <- liftE (assert_opt (cdl_cap_irq cap));
returnOk (ClearIrqHandler irq)
odE \<sqinter> throw \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ClearIrqHandler (the (cdl_cap_irq cap))) s \<Longrightarrow> ((\<lambda>s. True \<and> True \<and> (cdl_cap_irq cap \<noteq> None \<longrightarrow> P (ClearIrqHandler (the (cdl_cap_irq cap))) s)) and (\<lambda>s. True \<and> True)) s proof (prove)
goal:
No subgoals!
theory IRQ_DP

lemma irq_inner_lemma: "\<lbrace>\<lambda>s. P i s \<and> a = (NotificationCap x y z) \<rbrace> case a of NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw \<lbrace>P\<rbrace>, -" apply (unfold validE_R_def) apply (rule hoare_name_pre_stateE) apply (clarsimp) apply (wp, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P i s \<and> a = NotificationCap x y z\<rbrace> case a of NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw \<lbrace>P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P i s \<and> a = NotificationCap x y z\<rbrace> case a of NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P i s \<and> a = NotificationCap x y z \<Longrightarrow> \<lbrace>(=) s\<rbrace> case a of NotificationCap x xa xb \<Rightarrow> returnOk () | _ \<Rightarrow> throw \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P () s; a = NotificationCap x y z\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> returnOk () \<lbrace>P\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals!