kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchAcc_AI

lemma store_pde_state_hyp_refs_of:
  "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>" apply (simp add: store_pde_def set_pd_def set_object_def) apply (wp get_object_wp) apply (clarsimp elim!: rsubst[where P=P] intro!: ext) apply (clarsimp simp: state_hyp_refs_of_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> do pd <- get_pd (ptr && ~~ mask pd_bits);
kobj <- get_object (ptr && ~~ mask pd_bits);
y <- assert (a_type kobj = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := val)))));
s <- get;
put (s\<lparr>kheap := (kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := val))))\<rparr>)
od \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (state_hyp_refs_of s) \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (ptr && ~~ mask pd_bits) s \<longrightarrow> (\<forall>ko. ko_at ko (ptr && ~~ mask pd_bits) s \<longrightarrow> a_type ko = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := val)))) \<longrightarrow> P (state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := val))))\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s pd ko x. \<lbrakk>ako_at (PageDirectory pd) (ptr && ~~ mask pd_bits) s; ko_at ko (ptr && ~~ mask pd_bits) s; a_type ko = a_type (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := val))))\<rbrakk> \<Longrightarrow> state_hyp_refs_of s x = state_hyp_refs_of (s\<lparr>kheap := \<lambda>a. if a = ptr && ~~ mask pd_bits then Some (ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) then val else pd a))) else kheap s a\<rparr>) x proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma valid_asid_map_next_asid [iff]:
  "valid_asid_map (s\<lparr>arch_state := arm_next_asid_update f (arch_state s)\<rparr>) =
  valid_asid_map s" by (simp add: valid_asid_map_def vspace_at_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_asid_map (s\<lparr>arch_state := arm_next_asid_update f (arch_state s)\<rparr>) = valid_asid_map s
theory ArchAcc_AI

lemma pspace_respects_device_region_dmo:
  assumes valid_f: "\<And>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> f \<lbrace>\<lambda>r ms. P (device_state ms)\<rbrace>"
  shows "\<lbrace>pspace_respects_device_region\<rbrace>do_machine_op f\<lbrace>\<lambda>r. pspace_respects_device_region\<rbrace>" apply (clarsimp simp: do_machine_op_def gets_def select_f_def simpler_modify_def bind_def valid_def
    get_def return_def) apply (drule_tac P1 = "(=) (device_state (machine_state s))" in use_valid[OF _ valid_f]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> do_machine_op f \<lbrace>\<lambda>r. pspace_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>pspace_respects_device_region s; (a, b) \<in> fst (f (machine_state s))\<rbrakk> \<Longrightarrow> pspace_respects_device_region (s\<lparr>machine_state := b\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. pspace_respects_device_region s \<Longrightarrow> device_state (machine_state s) = device_state (machine_state s)
 2. \<And>s a b. \<lbrakk>pspace_respects_device_region s; device_state (machine_state s) = device_state b\<rbrakk> \<Longrightarrow> pspace_respects_device_region (s\<lparr>machine_state := b\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma machine_op_lift_device_state[wp]:
  "\<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> machine_op_lift f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>" by (clarsimp simp: machine_op_lift_def Nondet_VCG.valid_def bind_def
                     machine_rest_lift_def gets_def simpler_modify_def get_def return_def
                     select_def ignore_failure_def select_f_def
              split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> machine_op_lift f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>
theory CSpaceInvPre_AI

lemma ObjRef_nonempty_ArchRef_empty:
  "x \<in> ObjRef ` (obj_refs c) \<Longrightarrow> ArchRef ` arch_gen_refs c = {}" by (clarsimp simp: obj_ref_not_arch_gen_ref)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> ObjRef ` obj_refs c \<Longrightarrow> ArchRef ` arch_gen_refs c = {}
theory CSpaceInvPre_AI

lemma ArchRef_nonempty_ObjRef_empty:
  "x \<in> ArchRef ` arch_gen_refs c \<Longrightarrow> ObjRef ` (obj_refs c) = {}" by (clarsimp simp: arch_gen_ref_not_obj_ref)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> ArchRef ` arch_gen_refs c \<Longrightarrow> ObjRef ` obj_refs c = {}
theory CSpaceInvPre_AI

lemma gen_obj_refs_inD:
  "x \<in> gen_obj_refs cap \<Longrightarrow> gen_obj_refs cap = {x}" apply (case_tac cap; clarsimp simp: gen_obj_refs_def dest!:arch_gen_obj_refs_inD) apply (auto dest: gen_obj_ref_arch_cap_simps simp: arch_gen_obj_refs_inD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> gen_obj_refs cap \<Longrightarrow> gen_obj_refs cap = {x} proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>x \<in> ObjRef ` set_option (aobj_ref x12) \<or> x \<in> ArchRef ` arch_gen_obj_refs x12; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> ObjRef ` set_option (aobj_ref x12) \<union> ArchRef ` arch_gen_obj_refs x12 = {x} proof (prove)
goal:
No subgoals!
theory CSpaceInvPre_AI

lemma gen_obj_refs_distinct_or_equal:
  "\<lbrakk> gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {} \<rbrakk>
     \<Longrightarrow> gen_obj_refs cap = gen_obj_refs cap'" by (clarsimp elim!: nonemptyE dest!: gen_obj_refs_inD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gen_obj_refs cap \<inter> gen_obj_refs cap' \<noteq> {} \<Longrightarrow> gen_obj_refs cap = gen_obj_refs cap'
theory CSpaceInvPre_AI

lemma obj_ref_is_gen_obj_ref:
  "x \<in> obj_refs cap \<Longrightarrow> ObjRef x \<in> gen_obj_refs cap" by (simp add: gen_obj_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> obj_refs cap \<Longrightarrow> ObjRef x \<in> gen_obj_refs cap
theory CSpaceInvPre_AI

lemma wf_cs_ran_nonempty:
  "well_formed_cnode_n sz cs \<Longrightarrow> ran cs \<noteq> {}" apply (clarsimp simp: well_formed_cnode_n_def) apply (drule_tac f="\<lambda>S. replicate sz False \<in> S" in arg_cong) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. well_formed_cnode_n sz cs \<Longrightarrow> ran cs \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom cs = {x. length x = sz}; ran cs = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ran cs = {}; (replicate sz False \<in> dom cs) = (replicate sz False \<in> {x. length x = sz})\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpaceInvPre_AI

lemma empty_table_caps_of:
  "empty_table S ko \<Longrightarrow> caps_of ko = {}" by (cases ko, simp_all add: empty_table_def caps_of_def cap_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_table S ko \<Longrightarrow> caps_of ko = {}
theory ArchCSpaceInvPre_AI

lemma aobj_ref_acap_rights_update[simp]:
  "aobj_ref (acap_rights_update f x) = aobj_ref x" by (cases x; simp add: acap_rights_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. aobj_ref (acap_rights_update f x) = aobj_ref x
theory ArchCSpaceInvPre_AI

lemma arch_obj_size_acap_rights_update[simp]:
  "arch_obj_size (acap_rights_update f x) = arch_obj_size x" by (cases x; simp add: acap_rights_update_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_obj_size (acap_rights_update f x) = arch_obj_size x
theory ArchCSpaceInvPre_AI

lemma valid_arch_cap_acap_rights_update[intro]:
  "valid_arch_cap x s \<Longrightarrow> valid_arch_cap (acap_rights_update f x) s" by (cases x; simp add: acap_rights_update_def valid_arch_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_cap x s \<Longrightarrow> valid_arch_cap (acap_rights_update f x) s
theory ArchCSpaceInvPre_AI

lemma unique_table_refsD:
  "\<lbrakk> unique_table_refs cps; cps p = Some cap; cps p' = Some cap';
     obj_refs cap = obj_refs cap'\<rbrakk>
     \<Longrightarrow> table_cap_ref cap = table_cap_ref cap'" unfolding unique_table_refs_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unique_table_refs cps; cps p = Some cap; cps p' = Some cap'; obj_refs cap = obj_refs cap'\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p p' cap cap'. cps p = Some cap \<longrightarrow> cps p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap; cps p = Some cap; cps p' = Some cap'; obj_refs cap = obj_refs cap'\<rbrakk> \<Longrightarrow> table_cap_ref cap = table_cap_ref cap'
theory ArchCSpaceInvPre_AI

lemma table_cap_ref_vs_cap_ref_Some:
  "table_cap_ref x = Some y \<Longrightarrow> vs_cap_ref x = Some y" by (clarsimp simp: table_cap_ref_def vs_cap_ref_def
                 split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. table_cap_ref x = Some y \<Longrightarrow> vs_cap_ref x = Some y
theory ArchCSpaceInvPre_AI

lemma set_cap_unique_table_refs:
  "\<lbrace>\<lambda>s. unique_table_refs (caps_of_state s)
      \<and> no_cap_to_obj_with_diff_ref cap {ptr} s\<rbrace>
     set_cap cap ptr
   \<lbrace>\<lambda>rv s. unique_table_refs (caps_of_state s)\<rbrace>" apply wp apply clarsimp apply (simp add: unique_table_refs_def
              split del: if_split del: split_paired_All) apply (erule allEI, erule allEI) apply (clarsimp split del: if_split) apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def
                        cte_wp_at_caps_of_state
                 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. unique_table_refs (caps_of_state s) \<and> no_cap_to_obj_with_diff_ref cap {ptr} s\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. unique_table_refs (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. unique_table_refs (caps_of_state s) \<and> no_cap_to_obj_with_diff_ref cap {ptr} s \<Longrightarrow> unique_table_refs ((caps_of_state s)(ptr \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>unique_table_refs (caps_of_state s); no_cap_to_obj_with_diff_ref cap {ptr} s\<rbrakk> \<Longrightarrow> unique_table_refs (\<lambda>a. if a = ptr then Some cap else caps_of_state s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>p p' cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap); no_cap_to_obj_with_diff_ref cap {ptr} s\<rbrakk> \<Longrightarrow> \<forall>p p' capa. (if p = ptr then Some cap else caps_of_state s p) = Some capa \<longrightarrow> (\<forall>cap'. (if p' = ptr then Some cap else caps_of_state s p') = Some cap' \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> table_cap_ref cap' = table_cap_ref capa) proof (prove)
goal (1 subgoal):
 1. \<And>s p p'. \<lbrakk>no_cap_to_obj_with_diff_ref cap {ptr} s; \<forall>cap. caps_of_state s p = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap)\<rbrakk> \<Longrightarrow> \<forall>capa. (if p = ptr then Some cap else caps_of_state s p) = Some capa \<longrightarrow> (\<forall>cap'. (if p' = ptr then Some cap else caps_of_state s p') = Some cap' \<longrightarrow> obj_refs cap' = obj_refs capa \<longrightarrow> table_cap_ref cap' = table_cap_ref capa) proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba capa cap'. \<lbrakk>no_cap_to_obj_with_diff_ref cap {ptr} s; \<forall>cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (\<forall>cap'. caps_of_state s (aa, ba) = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap); (if (a, b) = ptr then Some cap else caps_of_state s (a, b)) = Some capa; (if (aa, ba) = ptr then Some cap else caps_of_state s (aa, ba)) = Some cap'; obj_refs cap' = obj_refs capa\<rbrakk> \<Longrightarrow> table_cap_ref cap' = table_cap_ref capa proof (prove)
goal:
No subgoals!
theory ArchCSpaceInvPre_AI

lemma valid_table_capsD:
  "\<lbrakk> cte_wp_at ((=) cap) ptr s; valid_table_caps s;
        is_pt_cap cap | is_pd_cap cap; cap_asid cap = None \<rbrakk>
        \<Longrightarrow> \<forall>r \<in> obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s" apply (clarsimp simp: cte_wp_at_caps_of_state valid_table_caps_def) apply (cases ptr, fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) cap) ptr s; valid_table_caps s; is_pt_cap cap \<or> is_pd_cap cap; cap_asid cap = None\<rbrakk> \<Longrightarrow> \<forall>r\<in>obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>caps_of_state s ptr = Some cap; \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s) \<and> (is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s); is_pt_cap cap \<or> is_pd_cap cap; cap_asid cap = None; r \<in> obj_refs cap\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s proof (prove)
goal:
No subgoals!
theory ArchCSpaceInvPre_AI

lemma unique_table_capsD:
  "\<lbrakk> unique_table_caps cps; cps ptr = Some cap; cps ptr' = Some cap';
     obj_refs cap = obj_refs cap'; cap_asid cap = None \<or> cap_asid cap' = None;
     (is_pd_cap cap \<and> is_pd_cap cap') \<or> (is_pt_cap cap \<and> is_pt_cap cap') \<rbrakk>
     \<Longrightarrow> ptr = ptr'" unfolding unique_table_caps_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unique_table_caps cps; cps ptr = Some cap; cps ptr' = Some cap'; obj_refs cap = obj_refs cap'; cap_asid cap = None \<or> cap_asid cap' = None; is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap'\<rbrakk> \<Longrightarrow> ptr = ptr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p p' cap cap'. cps p = Some cap \<longrightarrow> cps p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p); cps ptr = Some cap; cps ptr' = Some cap'; obj_refs cap = obj_refs cap'; cap_asid cap = None \<or> cap_asid cap' = None; is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap'\<rbrakk> \<Longrightarrow> ptr = ptr'
theory ArchCSpaceInvPre_AI

lemma set_cap_cap_refs_in_kernel_window[wp]:
  "\<lbrace>cap_refs_in_kernel_window
         and (\<lambda>s. \<forall>ref \<in> cap_range cap. arm_kernel_vspace (arch_state s) ref
                         = ArmVSpaceKernelWindow)\<rbrace>
     set_cap cap p
   \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" apply (simp add: cap_refs_in_kernel_window_def valid_refs_def2
                   pred_conj_def) apply (rule hoare_lift_Pf2[where f=arch_state]) apply wp apply (fastforce elim!: ranE split: if_split_asm) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window and (\<lambda>s. \<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. (\<forall>c\<in>ran (caps_of_state x). {xa. arm_kernel_vspace (arch_state x) xa \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range c = {}) \<and> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state x) ref = ArmVSpaceKernelWindow)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<forall>c\<in>ran (caps_of_state s). {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range c = {}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>xa. (\<forall>c\<in>ran (caps_of_state xa). {xa. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range c = {}) \<and> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace x ref = ArmVSpaceKernelWindow)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ a. \<forall>c\<in>ran (caps_of_state a). {xa. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range c = {}\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>x. P (arch_state x)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ x. P (arch_state x)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. (\<forall>c\<in>ran (caps_of_state s). {xa. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range c = {}) \<and> (\<forall>ref\<in>cap_range cap. arm_kernel_vspace x ref = ArmVSpaceKernelWindow) \<Longrightarrow> \<forall>c\<in>ran ((caps_of_state s)(p \<mapsto> cap)). {xa. arm_kernel_vspace x xa \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range c = {}
 2. \<And>P. \<lbrace>\<lambda>x. P (arch_state x)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ x. P (arch_state x)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>x. P (arch_state x)\<rbrace> set_cap cap p \<lbrace>\<lambda>_ x. P (arch_state x)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchCSpaceInvPre_AI

lemma cap_refs_in_kernel_windowD:
  "\<lbrakk> caps_of_state s ptr = Some cap; cap_refs_in_kernel_window s \<rbrakk>
   \<Longrightarrow> \<forall>ref \<in> cap_range cap.
         arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow" apply (clarsimp simp: cap_refs_in_kernel_window_def valid_refs_def
                        cte_wp_at_caps_of_state) apply (cases ptr, fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s ptr = Some cap; cap_refs_in_kernel_window s\<rbrakk> \<Longrightarrow> \<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>ref. \<lbrakk>caps_of_state s ptr = Some cap; \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> {x. arm_kernel_vspace (arch_state s) x \<noteq> ArmVSpaceKernelWindow} \<inter> cap_range cap = {}; ref \<in> cap_range cap\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal:
No subgoals!
theory ArchCSpaceInvPre_AI

lemma valid_cap_imp_valid_vm_rights:
  "valid_cap (cap.ArchObjectCap (PageCap dev mw rs sz m)) s \<Longrightarrow>
   rs \<in> valid_vm_rights" by (simp add: valid_cap_def valid_vm_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> ArchObjectCap (PageCap dev mw rs sz m) \<Longrightarrow> rs \<in> valid_vm_rights
theory ArchCSpaceInvPre_AI

lemma acap_rights_update_idem [simp]:
  "acap_rights_update R (acap_rights_update R' cap) = acap_rights_update R cap" by (simp add: acap_rights_update_def split: arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. acap_rights_update R (acap_rights_update R' cap) = acap_rights_update R cap
theory ArchCSpaceInvPre_AI

lemma acap_rights_update_id [intro!, simp]:
  "valid_arch_cap ac s \<Longrightarrow> acap_rights_update (acap_rights ac) ac = ac" unfolding acap_rights_update_def acap_rights_def valid_arch_cap_def by (cases ac; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_cap ac s \<Longrightarrow> acap_rights_update (acap_rights ac) ac = ac proof (prove)
goal (1 subgoal):
 1. case ac of ASIDPoolCap r as \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ASIDControlCap \<Rightarrow> True | PageCap dev r rghts sz mapdata \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned ref sz \<and> ref < kernel_base) | PageTableCap r mapdata \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | PageDirectoryCap r mapdata \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) \<Longrightarrow> (case ac of PageCap dev x rs' sz as \<Rightarrow> PageCap dev x (validate_vm_rights (rec_arch_cap undefined undefined (\<lambda>dev x rs sz as. rs) undefined undefined ac)) sz as | _ \<Rightarrow> ac) = ac
theory ArchCSpaceInvPre_AI

lemma obj_ref_none_no_asid:
  "{} = obj_refs new_cap \<longrightarrow> None = table_cap_ref new_cap"
  "obj_refs new_cap = {} \<longrightarrow> table_cap_ref new_cap = None" by (simp add: table_cap_ref_def split: cap.split arch_cap.split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {} = obj_refs new_cap \<longrightarrow> None = table_cap_ref new_cap &&& obj_refs new_cap = {} \<longrightarrow> table_cap_ref new_cap = None
theory ArchCSpaceInvPre_AI

lemma is_valid_vtable_root_is_arch_cap:
  "is_valid_vtable_root cap \<Longrightarrow> is_arch_cap cap" by (clarsimp simp: is_valid_vtable_root_def is_arch_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_valid_vtable_root cap \<Longrightarrow> is_arch_cap cap
theory CSpaceInv_AI

lemma is_valid_vtable_root_simps[simp]:
  "\<not> is_valid_vtable_root (UntypedCap a b c d)"
  "\<not> is_valid_vtable_root (ThreadCap tcb_ref)"
  "\<not> is_valid_vtable_root (CNodeCap cnode_ref sz guard)"
  "\<not> is_valid_vtable_root (EndpointCap ep_ref badge R)"
  "\<not> is_valid_vtable_root (NotificationCap ep_ref badge R)"
  "\<not> is_valid_vtable_root (ReplyCap tcb_ref master R)"
  "\<not> is_valid_vtable_root (Zombie e f g)"
  "\<not> is_valid_vtable_root (NullCap)"
  "\<not> is_valid_vtable_root (DomainCap)" by (fastforce dest: is_valid_vtable_root_is_arch_cap simp: is_cap_simps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<not> is_valid_vtable_root (UntypedCap a b c d) &&& \<not> is_valid_vtable_root (ThreadCap tcb_ref)) &&& \<not> is_valid_vtable_root (CNodeCap cnode_ref sz guard) &&& \<not> is_valid_vtable_root (EndpointCap ep_ref badge R)) &&& (\<not> is_valid_vtable_root (NotificationCap ep_ref badge R) &&& \<not> is_valid_vtable_root (ReplyCap tcb_ref master R)) &&& \<not> is_valid_vtable_root (Zombie e f g) &&& \<not> is_valid_vtable_root NullCap &&& \<not> is_valid_vtable_root DomainCap