kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_AI

lemma setup_reply_master_globals[wp]:
  "\<lbrace>valid_global_refs and ex_nonz_cap_to t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. valid_global_refs\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp hoare_drop_imps | simp add: if_fun_split)+ apply (clarsimp simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state
                        cap_range_def
                  dest: valid_global_refsD2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and ex_nonz_cap_to t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs and ex_nonz_cap_to t\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<lbrace>\<lambda>rv. valid_global_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_global_refs s \<and> ex_nonz_cap_to t s \<Longrightarrow> global_refs s \<inter> cap_range (ReplyCap t True {AllowGrant, AllowWrite}) = {} proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma setup_reply_master_irq_handlers[wp]:
  "\<lbrace>valid_irq_handlers and tcb_at t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp set_cap_irq_handlers hoare_drop_imps | simp add: if_fun_split)+ apply (fastforce elim: tcb_at_cte_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers and tcb_at t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers and tcb_at t\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<lbrace>\<lambda>rv. valid_irq_handlers\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_handlers s \<and> tcb_at t s \<Longrightarrow> cte_wp_at (\<lambda>cap'. True) (t, tcb_cnode_index 2) s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma setup_reply_master_cap_refs_respects_device_region[wp]:
  "\<lbrace>cap_refs_respects_device_region and tcb_at t and pspace_in_kernel_window\<rbrace>
      setup_reply_master t
   \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp get_cap_wp set_cap_cap_refs_respects_device_region) apply (clarsimp simp: obj_at_def
                        cap_range_def) apply (auto simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region and tcb_at t and pspace_in_kernel_window\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region and tcb_at t and pspace_in_kernel_window\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cap_refs_respects_device_region and tcb_at t and pspace_in_kernel_window) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (if cap = NullCap then \<lambda>s. (cap_refs_respects_device_region and (\<lambda>s. \<exists>ptr. cte_wp_at (\<lambda>c. cap_range (ReplyCap t True {AllowGrant, AllowWrite}) \<subseteq> cap_range c \<and> (cap_range (ReplyCap t True {AllowGrant, AllowWrite}) \<noteq> {} \<longrightarrow> cap_is_device (ReplyCap t True {AllowGrant, AllowWrite}) = cap_is_device c)) ptr s)) (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) else cap_refs_respects_device_region) s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>cap_refs_respects_device_region s; pspace_in_kernel_window s; kheap s t = Some ko; is_tcb ko; cte_wp_at ((=) NullCap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>c. True) (a, b) s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma setup_reply_master_valid_ioc[wp]:
  "\<lbrace>valid_ioc\<rbrace> setup_reply_master t \<lbrace>\<lambda>_. valid_ioc\<rbrace>" apply (simp add: setup_reply_master_def set_original_set_cap_comm) apply (wp get_cap_wp set_cap_cte_wp_at) apply (simp add: valid_ioc_def cte_wp_cte_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> setup_reply_master t \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2);
set_original (t, tcb_cnode_index 2) True
od)
od \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_ioc s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (if cap = NullCap then \<lambda>s. (valid_ioc and (\<lambda>s. ReplyCap t True {AllowGrant, AllowWrite} = NullCap \<longrightarrow> \<not> is_original_cap s (t, tcb_cnode_index 2))) s \<and> ((\<lambda>s. if (t, tcb_cnode_index 2) = (t, tcb_cnode_index 2) then True \<longrightarrow> ReplyCap t True {AllowGrant, AllowWrite} \<noteq> NullCap else cte_wp_at (\<lambda>x. True \<longrightarrow> x \<noteq> NullCap) (t, tcb_cnode_index 2) s) and cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2)) s else valid_ioc) s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma setup_reply_master_vms[wp]:
  "\<lbrace>valid_machine_state\<rbrace> setup_reply_master t \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp get_cap_wp) apply (simp add: valid_machine_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> setup_reply_master t \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_machine_state s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (if cap = NullCap then \<lambda>s. valid_machine_state (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) else valid_machine_state) s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma setup_reply_master_invs[wp]:
  "\<And>t.
    \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace>
      setup_reply_master t
    \<lbrace>\<lambda>rv. invs :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (simp add: invs_def valid_state_def) apply (wp valid_irq_node_typ
                 | simp add: valid_pspace_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrace>valid_pspace and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and tcb_at t and ex_nonz_cap_to t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. valid_pspace and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma safe_parent_not_Null [simp]:
  "safe_parent_for m p cap cap.NullCap = False" by (simp add: safe_parent_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. safe_parent_for m p cap NullCap = False
theory CSpace_AI

lemma safe_parent_ut_descendants:
  "\<And>m p cap pcap.
    \<lbrakk> safe_parent_for m p cap pcap; is_untyped_cap pcap \<rbrakk>
      \<Longrightarrow> descendants_of p m = {} \<and> obj_refs cap \<subseteq> untyped_range pcap" apply (rule conjI) apply (clarsimp simp: safe_parent_for_def) apply (safe; clarsimp simp: is_cap_simps safe_parent_for_arch_not_arch') apply (drule safe_parent_cap_range) apply (clarsimp simp: is_cap_simps cap_range_def) apply (drule (1) subsetD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>m p cap pcap. \<lbrakk>safe_parent_for m p cap pcap; is_untyped_cap pcap\<rbrakk> \<Longrightarrow> descendants_of p m = {} \<and> obj_refs cap \<subseteq> untyped_range pcap proof (prove)
goal (2 subgoals):
 1. \<And>m p cap pcap. \<lbrakk>safe_parent_for m p cap pcap; is_untyped_cap pcap\<rbrakk> \<Longrightarrow> descendants_of p m = {}
 2. \<And>m p cap pcap. \<lbrakk>safe_parent_for m p cap pcap; is_untyped_cap pcap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> untyped_range pcap proof (prove)
goal (2 subgoals):
 1. \<And>m a b cap pcap. \<lbrakk>is_untyped_cap pcap; cap_is_device cap = cap_is_device pcap; same_region_as pcap cap; (\<exists>irq. cap = IRQHandlerCap irq) \<and> pcap = IRQControlCap \<or> descendants_of (a, b) m = {} \<or> safe_parent_for_arch cap pcap\<rbrakk> \<Longrightarrow> descendants_of (a, b) m = {}
 2. \<And>m p cap pcap. \<lbrakk>safe_parent_for m p cap pcap; is_untyped_cap pcap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> untyped_range pcap proof (prove)
goal (1 subgoal):
 1. \<And>m p cap pcap. \<lbrakk>safe_parent_for m p cap pcap; is_untyped_cap pcap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> untyped_range pcap proof (prove)
goal (1 subgoal):
 1. \<And>m p cap pcap. \<lbrakk>is_untyped_cap pcap; cap_range cap \<subseteq> cap_range pcap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> untyped_range pcap proof (prove)
goal (1 subgoal):
 1. \<And>cap x r bits. \<lbrakk>x \<in> obj_refs cap; untyped_range cap \<subseteq> {r..r + 2 ^ bits - 1}; obj_refs cap \<subseteq> {r..r + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> r \<le> x \<and> x \<le> r + 2 ^ bits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>cap x r bits. \<lbrakk>x \<in> obj_refs cap; untyped_range cap \<subseteq> {r..r + 2 ^ bits - 1}; x \<in> {r..r + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> r \<le> x \<and> x \<le> r + 2 ^ bits - 1 proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma safe_parent_refs_or_descendants:
  fixes m p cap pcap
  shows
  "safe_parent_for m p cap pcap \<Longrightarrow>
    (obj_refs cap \<subseteq> obj_refs pcap) \<or> (descendants_of p m = {} \<and> obj_refs cap \<subseteq> untyped_range pcap) \<or> safe_parent_for_arch cap pcap" apply (cases "is_untyped_cap pcap") apply (drule (1) safe_parent_ut_descendants) apply simp apply (rule disjI1) apply (drule safe_parent_cap_range) apply (simp add: cap_range_def) apply (drule not_is_untyped_no_range) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. safe_parent_for m p cap pcap \<Longrightarrow> obj_refs cap \<subseteq> obj_refs pcap \<or> descendants_of p m = {} \<and> obj_refs cap \<subseteq> untyped_range pcap \<or> safe_parent_for_arch cap pcap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>safe_parent_for m p cap pcap; is_untyped_cap pcap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> obj_refs pcap \<or> descendants_of p m = {} \<and> obj_refs cap \<subseteq> untyped_range pcap \<or> safe_parent_for_arch cap pcap
 2. \<lbrakk>safe_parent_for m p cap pcap; \<not> is_untyped_cap pcap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> obj_refs pcap \<or> descendants_of p m = {} \<and> obj_refs cap \<subseteq> untyped_range pcap \<or> safe_parent_for_arch cap pcap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_untyped_cap pcap; descendants_of p m = {} \<and> obj_refs cap \<subseteq> untyped_range pcap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> obj_refs pcap \<or> descendants_of p m = {} \<and> obj_refs cap \<subseteq> untyped_range pcap \<or> safe_parent_for_arch cap pcap
 2. \<lbrakk>safe_parent_for m p cap pcap; \<not> is_untyped_cap pcap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> obj_refs pcap \<or> descendants_of p m = {} \<and> obj_refs cap \<subseteq> untyped_range pcap \<or> safe_parent_for_arch cap pcap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>safe_parent_for m p cap pcap; \<not> is_untyped_cap pcap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> obj_refs pcap \<or> descendants_of p m = {} \<and> obj_refs cap \<subseteq> untyped_range pcap \<or> safe_parent_for_arch cap pcap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>safe_parent_for m p cap pcap; \<not> is_untyped_cap pcap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> obj_refs pcap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_untyped_cap pcap; cap_range cap \<subseteq> cap_range pcap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> obj_refs pcap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_untyped_cap pcap; untyped_range cap \<subseteq> untyped_range pcap \<union> obj_refs pcap \<and> obj_refs cap \<subseteq> untyped_range pcap \<union> obj_refs pcap\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> obj_refs pcap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>untyped_range cap \<subseteq> untyped_range pcap \<union> obj_refs pcap \<and> obj_refs cap \<subseteq> untyped_range pcap \<union> obj_refs pcap; untyped_range pcap = {}\<rbrakk> \<Longrightarrow> obj_refs cap \<subseteq> obj_refs pcap proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma safe_parent_same_region:
  "safe_parent_for m p cap pcap \<Longrightarrow> same_region_as pcap cap" by (simp add: safe_parent_for_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. safe_parent_for m p cap pcap \<Longrightarrow> same_region_as pcap cap
theory CSpace_AI

lemma (in mdb_insert_abs) reply_mdb_simple:
  assumes u: "reply_mdb m cs"
  assumes src: "cs src = Some c"
  assumes sr: "\<not>is_reply_cap c \<and> \<not>is_master_reply_cap c"
  assumes nr: "\<not>is_reply_cap cap \<and> \<not>is_master_reply_cap cap"
  shows "reply_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))" using u src sr nr unfolding reply_mdb_def by (simp add: reply_caps_mdb_simple reply_masters_mdb_simple)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (prove)
using this:
reply_mdb m cs
cs src = Some c
\<not> is_reply_cap c \<and> \<not> is_master_reply_cap c
\<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap

goal (1 subgoal):
 1. reply_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (prove)
using this:
reply_caps_mdb m cs \<and> reply_masters_mdb m cs
cs src = Some c
\<not> is_reply_cap c \<and> \<not> is_master_reply_cap c
\<not> is_reply_cap cap \<and> \<not> is_master_reply_cap cap

goal (1 subgoal):
 1. reply_caps_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) \<and> reply_masters_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))
theory CSpace_AI

lemma set_untyped_cap_as_full_caps_of_state_diff:
  "\<lbrace>\<lambda>s. src \<noteq> dest \<and> P (caps_of_state s dest)\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s. P (caps_of_state s dest)\<rbrace>" apply (clarsimp simp:set_untyped_cap_as_full_def) apply (intro conjI impI allI) apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. src \<noteq> dest \<and> P (caps_of_state s dest)\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. P (caps_of_state s dest)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> \<lbrace>\<lambda>s. src \<noteq> dest \<and> P (caps_of_state s dest)\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. P (caps_of_state s dest)\<rbrace>) \<and> ((obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>\<lambda>s. src \<noteq> dest \<and> P (caps_of_state s dest)\<rbrace> return () \<lbrace>\<lambda>rv s. P (caps_of_state s dest)\<rbrace>) proof (prove)
goal (2 subgoals):
 1. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<Longrightarrow> \<lbrace>\<lambda>s. src \<noteq> dest \<and> P (caps_of_state s dest)\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. P (caps_of_state s dest)\<rbrace>
 2. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>\<lambda>s. src \<noteq> dest \<and> P (caps_of_state s dest)\<rbrace> return () \<lbrace>\<lambda>rv s. P (caps_of_state s dest)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma safe_parent_for_masked_as_full[simp]:
  "safe_parent_for m src a (masked_as_full src_cap b) =
   safe_parent_for m src a src_cap" apply (clarsimp simp:safe_parent_for_def) apply (rule iffI) apply (auto simp: masked_as_full_def free_index_update_def safe_parent_for_arch_not_arch' is_cap_simps
               split: if_splits cap.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. safe_parent_for m src a (masked_as_full src_cap b) = safe_parent_for m src a src_cap proof (prove)
goal (1 subgoal):
 1. (cap_is_device a = cap_is_device (masked_as_full src_cap b) \<and> same_region_as src_cap a \<and> ((\<exists>irq. a = IRQHandlerCap irq) \<and> masked_as_full src_cap b = IRQControlCap \<or> is_untyped_cap src_cap \<and> descendants_of src m = {} \<or> safe_parent_for_arch a (masked_as_full src_cap b))) = (cap_is_device a = cap_is_device src_cap \<and> same_region_as src_cap a \<and> ((\<exists>irq. a = IRQHandlerCap irq) \<and> src_cap = IRQControlCap \<or> is_untyped_cap src_cap \<and> descendants_of src m = {} \<or> safe_parent_for_arch a src_cap)) proof (prove)
goal (2 subgoals):
 1. cap_is_device a = cap_is_device (masked_as_full src_cap b) \<and> same_region_as src_cap a \<and> ((\<exists>irq. a = IRQHandlerCap irq) \<and> masked_as_full src_cap b = IRQControlCap \<or> is_untyped_cap src_cap \<and> descendants_of src m = {} \<or> safe_parent_for_arch a (masked_as_full src_cap b)) \<Longrightarrow> cap_is_device a = cap_is_device src_cap \<and> same_region_as src_cap a \<and> ((\<exists>irq. a = IRQHandlerCap irq) \<and> src_cap = IRQControlCap \<or> is_untyped_cap src_cap \<and> descendants_of src m = {} \<or> safe_parent_for_arch a src_cap)
 2. cap_is_device a = cap_is_device src_cap \<and> same_region_as src_cap a \<and> ((\<exists>irq. a = IRQHandlerCap irq) \<and> src_cap = IRQControlCap \<or> is_untyped_cap src_cap \<and> descendants_of src m = {} \<or> safe_parent_for_arch a src_cap) \<Longrightarrow> cap_is_device a = cap_is_device (masked_as_full src_cap b) \<and> same_region_as src_cap a \<and> ((\<exists>irq. a = IRQHandlerCap irq) \<and> masked_as_full src_cap b = IRQControlCap \<or> is_untyped_cap src_cap \<and> descendants_of src m = {} \<or> safe_parent_for_arch a (masked_as_full src_cap b)) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma lookup_cnode_slot_real_cte [wp]:
  "\<lbrace>valid_objs and valid_cap croot\<rbrace> lookup_slot_for_cnode_op s croot ptr depth \<lbrace>\<lambda>rv. real_cte_at rv\<rbrace>, -" apply (simp add: lookup_slot_for_cnode_op_def split_def unlessE_whenE cong: if_cong split del: if_split) apply (rule hoare_pre) apply (wp hoare_drop_imps resolve_address_bits_real_cte_at whenE_throwError_wp
          |wpc|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap croot\<rbrace> lookup_slot_for_cnode_op s croot ptr depth \<lbrace>real_cte_at\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap croot\<rbrace> if is_cnode_cap croot then doE y <- whenE (depth = 0 \<or> word_bits < depth) (throwError (RangeError 1 (word_of_nat word_bits)));
lookup_error_on_failure s (doE p <- resolve_address_bits (croot, drop (length ptr - depth) ptr);
case snd p of [] \<Rightarrow> returnOk (fst p) | a # list \<Rightarrow> throwError $ DepthMismatch (length (snd p)) 0
odE)
odE else throwError (FailedLookup s InvalidRoot) \<lbrace>real_cte_at\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'4\<rbrace> if is_cnode_cap croot then doE y <- whenE (depth = 0 \<or> word_bits < depth) (throwError (RangeError 1 (word_of_nat word_bits)));
lookup_error_on_failure s (doE p <- resolve_address_bits (croot, drop (length ptr - depth) ptr);
case snd p of [] \<Rightarrow> returnOk (fst p) | a # list \<Rightarrow> throwError $ DepthMismatch (length (snd p)) 0
odE)
odE else throwError (FailedLookup s InvalidRoot) \<lbrace>real_cte_at\<rbrace>, -
 2. \<And>s. (valid_objs and valid_cap croot) s \<Longrightarrow> ?P'4 s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma cte_refs_rights_update [simp]:
  "cte_refs (cap_rights_update R cap) x = cte_refs cap x" by (force simp: cap_rights_update_def split: cap.splits bool.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_refs (cap_rights_update R cap) x = cte_refs cap x