theory ArchCSpace_AI

lemma cap_insert_cap_refs_in_kernel_window[wp, CSpace_AI_assms]:
  "\<lbrace>cap_refs_in_kernel_window
          and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c) src\<rbrace>
     cap_insert cap src dest
   \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" apply (simp add: cap_insert_def set_untyped_cap_as_full_def) apply (wp get_cap_wp | simp split del: if_split)+ apply (clarsimp simp: cte_wp_at_caps_of_state is_derived_def) apply (frule(1) cap_refs_in_kernel_windowD[where ptr=src]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c) src\<rbrace> cap_insert cap src dest \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c) src\<rbrace> do src_cap <- get_cap src;
old_cap <- get_cap dest;
y <- assert (old_cap = NullCap);
y <- if 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 then set_cap (max_free_index_update src_cap) src else return ();
y <- set_cap cap dest;
is_original <- gets is_original_cap;
src_p <- gets (\<lambda>s. cdt s src);
dest_p <- gets (\<lambda>s. cdt s dest);
y <- update_cdt (\<lambda>cdt. cdt(dest := if should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap) then Some src else cdt src));
y <- do_extended_op (cap_insert_ext (should_be_parent_of src_cap (is_original src) cap (is_cap_revocable cap src_cap)) src dest src_p dest_p);
set_original dest (is_cap_revocable cap src_cap)
od \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cap_refs_in_kernel_window s \<and> cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c) src s \<Longrightarrow> \<forall>capa. cte_wp_at ((=) capa) src s \<longrightarrow> cte_wp_at ((=) NullCap) dest s \<longrightarrow> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> (\<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>cap_refs_in_kernel_window s; cap_range cap \<subseteq> cap_range capa; caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap\<rbrakk> \<Longrightarrow> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> (\<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>cap_refs_in_kernel_window s; cap_range cap \<subseteq> cap_range capa; caps_of_state s src = Some capa; caps_of_state s dest = Some NullCap; \<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> (is_untyped_cap capa \<and> is_untyped_cap cap \<and> obj_ref_of capa = obj_ref_of cap \<and> cap_bits_untyped capa = cap_bits_untyped cap \<longrightarrow> (\<forall>ref\<in>cap_range capa. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow) \<and> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow)) \<and> ((obj_ref_of capa = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap capa \<longrightarrow> cap_bits_untyped capa \<noteq> cap_bits_untyped cap) \<longrightarrow> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow)) proof (prove)
goal:
No subgoals!