kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchRetype_AI

lemma get_pde_valid[wp]:
  "\<lbrace>valid_vspace_objs
    and \<exists>\<rhd> (x && ~~mask pd_bits)
    and K (ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)\<rbrace>
   get_pde x
   \<lbrace>valid_pde\<rbrace>" apply (simp add: get_pde_def) apply wp apply clarsimp apply (drule (2) valid_vspace_objsD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)\<rbrace> get_pde x \<lbrace>valid_pde\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)\<rbrace> do pd <- get_pd (x && ~~ mask pd_bits);
return (pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2)))
od \<lbrace>valid_pde\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (x && ~~ mask pd_bits) s \<longrightarrow> valid_pde (pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2))) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd ref. \<lbrakk>valid_vspace_objs s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (ref \<rhd> (x && ~~ mask pd_bits)) s; ako_at (PageDirectory pd) (x && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> valid_pde (pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2))) s proof (prove)
goal (1 subgoal):
 1. \<And>s pd ref. \<lbrakk>valid_vspace_objs s; UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots; ako_at (PageDirectory pd) (x && ~~ mask pd_bits) s; valid_vspace_obj (PageDirectory pd) s\<rbrakk> \<Longrightarrow> valid_pde (pd (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2))) s proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma set_pd_arch_state[wp]:
  "\<lbrace>valid_arch_state\<rbrace> set_pd ptr val \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>" by (rule set_pd_valid_arch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> set_pd ptr val \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>
theory ArchRetype_AI

lemma equal_kernel_mappings_specific_def:
  "ko_at (ArchObj (PageDirectory pd)) p s
    \<Longrightarrow> equal_kernel_mappings s
          = (\<forall>p' pd'. ko_at (ArchObj (PageDirectory pd')) p' s
                        \<longrightarrow> (\<forall>w \<in> kernel_mapping_slots. pd' w = pd w))" apply (rule iffI) apply (clarsimp simp: equal_kernel_mappings_def) apply (clarsimp simp: equal_kernel_mappings_def) apply (subgoal_tac "pda w = pd w \<and> pd' w = pd w") apply (erule conjE, erule(1) trans[OF _ sym]) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ako_at (PageDirectory pd) p s \<Longrightarrow> equal_kernel_mappings s = (\<forall>p' pd'. ako_at (PageDirectory pd') p' s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pd w)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ako_at (PageDirectory pd) p s; equal_kernel_mappings s\<rbrakk> \<Longrightarrow> \<forall>p' pd'. ako_at (PageDirectory pd') p' s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pd w)
 2. \<lbrakk>ako_at (PageDirectory pd) p s; \<forall>p' pd'. ako_at (PageDirectory pd') p' s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pd w)\<rbrakk> \<Longrightarrow> equal_kernel_mappings s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ako_at (PageDirectory pd) p s; \<forall>p' pd'. ako_at (PageDirectory pd') p' s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pd w)\<rbrakk> \<Longrightarrow> equal_kernel_mappings s proof (prove)
goal (1 subgoal):
 1. \<And>x y pda pd' w. \<lbrakk>ako_at (PageDirectory pd) p s; \<forall>p' pd'. ako_at (PageDirectory pd') p' s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pd w); w \<in> kernel_mapping_slots; ako_at (PageDirectory pda) x s; ako_at (PageDirectory pd') y s\<rbrakk> \<Longrightarrow> pda w = pd' w proof (prove)
goal (2 subgoals):
 1. \<And>x y pda pd' w. \<lbrakk>ako_at (PageDirectory pd) p s; \<forall>p' pd'. ako_at (PageDirectory pd') p' s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pd w); w \<in> kernel_mapping_slots; ako_at (PageDirectory pda) x s; ako_at (PageDirectory pd') y s; pda w = pd w \<and> pd' w = pd w\<rbrakk> \<Longrightarrow> pda w = pd' w
 2. \<And>x y pda pd' w. \<lbrakk>ako_at (PageDirectory pd) p s; \<forall>p' pd'. ako_at (PageDirectory pd') p' s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pd w); w \<in> kernel_mapping_slots; ako_at (PageDirectory pda) x s; ako_at (PageDirectory pd') y s\<rbrakk> \<Longrightarrow> pda w = pd w \<and> pd' w = pd w proof (prove)
goal (1 subgoal):
 1. \<And>x y pda pd' w. \<lbrakk>ako_at (PageDirectory pd) p s; \<forall>p' pd'. ako_at (PageDirectory pd') p' s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd' w = pd w); w \<in> kernel_mapping_slots; ako_at (PageDirectory pda) x s; ako_at (PageDirectory pd') y s\<rbrakk> \<Longrightarrow> pda w = pd w \<and> pd' w = pd w proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma store_pde_valid_global_pd_mappings[wp]:
  "\<lbrace>valid_global_objs and valid_global_vspace_mappings
          and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s)\<rbrace>
     store_pde p pde
   \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>" apply (simp add: store_pde_def set_pd_def) apply (wp set_object_global_vspace_mappings get_object_wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs and valid_global_vspace_mappings and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s)\<rbrace> store_pde p pde \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs and valid_global_vspace_mappings and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s)\<rbrace> do pd <- get_pd (p && ~~ mask pd_bits);
set_object (p && ~~ mask pd_bits) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))
od \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_global_objs and valid_global_vspace_mappings and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s)) s \<Longrightarrow> \<forall>pd. ako_at (PageDirectory pd) (p && ~~ mask pd_bits) s \<longrightarrow> (valid_global_vspace_mappings and (\<lambda>s. typ_at (AArch APageDirectory) (p && ~~ mask pd_bits) s \<or> typ_at (AArch APageTable) (p && ~~ mask pd_bits) s \<longrightarrow> valid_global_objs s \<and> p && ~~ mask pd_bits \<notin> global_refs s)) s proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma store_pde_valid_ioc[wp]:
 "\<lbrace>valid_ioc\<rbrace> store_pde ptr pde \<lbrace>\<lambda>_. valid_ioc\<rbrace>" by (simp add: store_pde_def, wp) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> store_pde ptr pde \<lbrace>\<lambda>_. valid_ioc\<rbrace>
theory ArchRetype_AI

lemma store_pde_vms[wp]:
 "\<lbrace>valid_machine_state\<rbrace> store_pde ptr pde \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" by (simp add: store_pde_def, wp) clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> store_pde ptr pde \<lbrace>\<lambda>_. valid_machine_state\<rbrace>
theory ArchRetype_AI

lemma copy_global_mappings_valid_ioc[wp]:
 "\<lbrace>valid_ioc\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>_. valid_ioc\<rbrace>" by (wpsimp wp: mapM_x_wp[of UNIV] simp: copy_global_mappings_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>_. valid_ioc\<rbrace>
theory ArchRetype_AI

lemma copy_global_mappings_vms[wp]:
 "\<lbrace>valid_machine_state\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" by (wpsimp wp: mapM_x_wp[of UNIV] simp: copy_global_mappings_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>_. valid_machine_state\<rbrace>
theory ArchRetype_AI

lemma dmo_eq_kernel_restricted [wp, Retype_AI_assms]:
  "\<lbrace>\<lambda>s. equal_kernel_mappings (kheap_update (f (kheap s)) s)\<rbrace>
       do_machine_op m
   \<lbrace>\<lambda>rv s. equal_kernel_mappings (kheap_update (f (kheap s)) s)\<rbrace>" apply (simp add: do_machine_op_def split_def) apply wp apply (simp add: equal_kernel_mappings_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. equal_kernel_mappings (kheap_update (f (kheap s)) s)\<rbrace> do_machine_op m \<lbrace>\<lambda>rv s. equal_kernel_mappings (kheap_update (f (kheap s)) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. equal_kernel_mappings (kheap_update (f (kheap s)) s)\<rbrace> do ms <- gets machine_state;
p <- select_f (m ms);
y <- modify (machine_state_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>rv s. equal_kernel_mappings (kheap_update (f (kheap s)) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. equal_kernel_mappings (kheap_update (f (kheap s)) s) \<Longrightarrow> \<forall>x\<in>fst (m (machine_state s)). equal_kernel_mappings (kheap_update (f (kheap (s\<lparr>machine_state := snd x\<rparr>))) (s\<lparr>machine_state := snd x\<rparr>)) proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma dmo_mapM_x_ccr_invs[wp]:
  "\<lbrace>invs\<rbrace>
   do_machine_op (mapM_x (\<lambda>ptr. cleanCacheRange_PoU ptr (w ptr) (addrFromPPtr ptr)) xs)
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (clarsimp simp: mapM_x_mapM do_machine_op_return_foo) apply (rule hoare_pre) apply (subst dom_mapM) apply ((simp add: clearMemory_def
      | wp empty_fail_cleanCacheRange_PoU ef_storeWord
      empty_fail_mapM_x empty_fail_bind)+)[1] apply (wp mapM_wp' | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op (mapM_x (\<lambda>ptr. cleanCacheRange_PoU ptr (w ptr) (addrFromPPtr ptr)) xs) \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do y <- do_machine_op (mapM (\<lambda>ptr. cleanCacheRange_PoU ptr (w ptr) (addrFromPPtr ptr)) xs);
return ()
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- do_machine_op (mapM (\<lambda>ptr. cleanCacheRange_PoU ptr (w ptr) (addrFromPPtr ptr)) xs);
return ()
od \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. empty_fail (cleanCacheRange_PoU x (w x) (addrFromPPtr x))
 2. \<lbrace>?Q\<rbrace> do y <- mapM (do_machine_op \<circ> (\<lambda>ptr. cleanCacheRange_PoU ptr (w ptr) (addrFromPPtr ptr))) xs;
return ()
od \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- mapM (do_machine_op \<circ> (\<lambda>ptr. cleanCacheRange_PoU ptr (w ptr) (addrFromPPtr ptr))) xs;
return ()
od \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma obj_bits_api_neq_0 [Retype_AI_assms]:
  "ty \<noteq> Untyped \<Longrightarrow> 0 < obj_bits_api ty us" unfolding obj_bits_api_def by (clarsimp simp: slot_bits_def default_arch_object_def pageBits_def
               split: Structures_A.apiobject_type.splits aobject_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ty \<noteq> Untyped \<Longrightarrow> 0 < obj_bits_api ty us proof (prove)
goal (1 subgoal):
 1. ty \<noteq> Untyped \<Longrightarrow> 0 < (case ty of Untyped \<Rightarrow> us | TCBObject \<Rightarrow> obj_bits (TCB default_tcb) | EndpointObject \<Rightarrow> obj_bits (Endpoint undefined) | NotificationObject \<Rightarrow> obj_bits (Notification undefined) | CapTableObject \<Rightarrow> us + slot_bits | ArchObject aobj \<Rightarrow> obj_bits $ ArchObj $ default_arch_object aobj False us)
theory ArchRetype_AI

lemma vs_lookup_sub2:
  assumes ko: "\<And>ko p. \<lbrakk> ko_at ko p s; vs_refs ko \<noteq> {} \<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'"
  assumes table: "graph_of (arm_asid_table (arch_state s)) \<subseteq> graph_of (arm_asid_table (arch_state s'))"
  shows "vs_lookup s \<subseteq> vs_lookup s'" unfolding vs_lookup_def apply (rule Image_mono) apply (rule vs_lookup_trans_sub2) apply (erule (1) ko) apply (unfold vs_asid_refs_def) apply (rule image_mono) apply (rule table) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup s \<subseteq> vs_lookup s' proof (prove)
goal (1 subgoal):
 1. (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<subseteq> (vs_lookup1 s')\<^sup>* `` vs_asid_refs (asid_table s') proof (prove)
goal (2 subgoals):
 1. (vs_lookup1 s)\<^sup>* \<subseteq> (vs_lookup1 s')\<^sup>*
 2. vs_asid_refs (asid_table s) \<subseteq> vs_asid_refs (asid_table s') proof (prove)
goal (2 subgoals):
 1. \<And>ko p. \<lbrakk>ko_at ko p s; vs_refs ko \<noteq> {}\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'
 2. vs_asid_refs (asid_table s) \<subseteq> vs_asid_refs (asid_table s') proof (prove)
goal (1 subgoal):
 1. vs_asid_refs (asid_table s) \<subseteq> vs_asid_refs (asid_table s') proof (prove)
goal (1 subgoal):
 1. (\<lambda>(r, p). ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` graph_of (asid_table s) \<subseteq> (\<lambda>(r, p). ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` graph_of (asid_table s') proof (prove)
goal (1 subgoal):
 1. graph_of (asid_table s) \<subseteq> graph_of (asid_table s') proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma vs_lookup_pages_sub2:
  assumes ko: "\<And>ko p. \<lbrakk> ko_at ko p s; vs_refs_pages ko \<noteq> {} \<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'"
  assumes table: "graph_of (arm_asid_table (arch_state s)) \<subseteq> graph_of (arm_asid_table (arch_state s'))"
  shows "vs_lookup_pages s \<subseteq> vs_lookup_pages s'" unfolding vs_lookup_pages_def apply (rule Image_mono) apply (rule vs_lookup_pages_trans_sub2) apply (erule (1) ko) apply (unfold vs_asid_refs_def) apply (rule image_mono) apply (rule table) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages s \<subseteq> vs_lookup_pages s' proof (prove)
goal (1 subgoal):
 1. (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<subseteq> (vs_lookup_pages1 s')\<^sup>* `` vs_asid_refs (asid_table s') proof (prove)
goal (2 subgoals):
 1. (vs_lookup_pages1 s)\<^sup>* \<subseteq> (vs_lookup_pages1 s')\<^sup>*
 2. vs_asid_refs (asid_table s) \<subseteq> vs_asid_refs (asid_table s') proof (prove)
goal (2 subgoals):
 1. \<And>ko p. \<lbrakk>ko_at ko p s; vs_refs_pages ko \<noteq> {}\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'
 2. vs_asid_refs (asid_table s) \<subseteq> vs_asid_refs (asid_table s') proof (prove)
goal (1 subgoal):
 1. vs_asid_refs (asid_table s) \<subseteq> vs_asid_refs (asid_table s') proof (prove)
goal (1 subgoal):
 1. (\<lambda>(r, p). ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` graph_of (asid_table s) \<subseteq> (\<lambda>(r, p). ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` graph_of (asid_table s') proof (prove)
goal (1 subgoal):
 1. graph_of (asid_table s) \<subseteq> graph_of (asid_table s') proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma valid_default_arch_tcb:
  "\<And>s. valid_arch_tcb default_arch_tcb s" by (simp add: default_arch_tcb_def valid_arch_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_arch_tcb default_arch_tcb s
theory ArchRetype_AI

lemma valid_global_refs:
  "valid_global_refs s \<Longrightarrow> valid_global_refs s'" apply (simp add: valid_global_refs_def valid_refs_def global_refs_def idle_s') apply (simp add: cte_retype cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_refs s \<Longrightarrow> valid_global_refs s' proof (prove)
goal (1 subgoal):
 1. \<forall>a b. \<not> cte_wp_at (\<lambda>c. idle_thread s \<in> cap_range c \<or> arm_global_pd (arch_state s) \<in> cap_range c \<or> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range c \<noteq> {}) (a, b) s \<Longrightarrow> \<forall>a b. \<not> cte_wp_at (\<lambda>c. idle_thread s \<in> cap_range c \<or> arm_global_pd (arch_state s) \<in> cap_range c \<or> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range c \<noteq> {}) (a, b) s' proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma valid_arch_state:
  "valid_arch_state s \<Longrightarrow> valid_arch_state s'" by (clarsimp simp: valid_arch_state_def obj_at_pres
                     valid_asid_table_def valid_global_pts_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_state s \<Longrightarrow> valid_arch_state s'
theory ArchRetype_AI

lemma vs_refs_default [simp]:
  "vs_refs (default_object ty dev us) = {}" by (simp add: default_object_def default_arch_object_def tyunt vs_refs_def
                o_def pde_ref_def graph_of_def
           split: Structures_A.apiobject_type.splits aobject_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_refs (default_object ty dev us) = {}
theory ArchRetype_AI

lemma vs_refs_pages_default [simp]:
  "vs_refs_pages (default_object ty dev us) = {}" by (simp add: default_object_def default_arch_object_def tyunt vs_refs_pages_def
                o_def pde_ref_pages_def pte_ref_pages_def graph_of_def
           split: Structures_A.apiobject_type.splits aobject_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_refs_pages (default_object ty dev us) = {}
theory ArchRetype_AI

lemma vs_lookup_pages':
  "vs_lookup_pages s' = vs_lookup_pages s" apply (rule order_antisym) apply (rule vs_lookup_pages_sub2) apply (clarsimp simp: obj_at_def s'_def ps_def split: if_split_asm) apply simp apply (rule vs_lookup_pages_sub) apply (clarsimp simp: obj_at_def s'_def ps_def split: if_split_asm dest!: orthr) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages s' = vs_lookup_pages s proof (prove)
goal (2 subgoals):
 1. vs_lookup_pages s' \<subseteq> vs_lookup_pages s
 2. vs_lookup_pages s \<subseteq> vs_lookup_pages s' proof (prove)
goal (3 subgoals):
 1. \<And>ko p. \<lbrakk>ko_at ko p s'; vs_refs_pages ko \<noteq> {}\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s
 2. graph_of (asid_table s') \<subseteq> graph_of (asid_table s)
 3. vs_lookup_pages s \<subseteq> vs_lookup_pages s' proof (prove)
goal (2 subgoals):
 1. graph_of (asid_table s') \<subseteq> graph_of (asid_table s)
 2. vs_lookup_pages s \<subseteq> vs_lookup_pages s' proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages s \<subseteq> vs_lookup_pages s' proof (prove)
goal (2 subgoals):
 1. \<And>ko p. ko_at ko p s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'
 2. graph_of (asid_table s) \<subseteq> graph_of (asid_table s') proof (prove)
goal (1 subgoal):
 1. graph_of (asid_table s) \<subseteq> graph_of (asid_table s') proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma hyp_refs_eq:
  "ARM.state_hyp_refs_of s' = ARM.state_hyp_refs_of s" unfolding s'_def ps_def apply (rule ext) apply (clarsimp simp: state_hyp_refs_of_def orthr split: option.splits) apply (cases ty; simp add: tyunt default_object_def default_tcb_def hyp_refs_of_def tcb_hyp_refs_def
                             default_arch_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_hyp_refs_of s' = state_hyp_refs_of s proof (prove)
goal (1 subgoal):
 1. state_hyp_refs_of (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) = state_hyp_refs_of s proof (prove)
goal (1 subgoal):
 1. \<And>x. state_hyp_refs_of (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>) x = state_hyp_refs_of s x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kheap s x = None; x \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> hyp_refs_of (default_object ty dev us) = {} proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma valid_vspace_obj_pres:
  "valid_vspace_obj ao s \<Longrightarrow> valid_vspace_obj ao s'" apply (cases ao; simp add: valid_vspace_obj_def obj_at_pres) apply (erule allEI ballEI; rename_tac t i; case_tac "t i"; fastforce simp: data_at_def obj_at_pres)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_obj ao s \<Longrightarrow> valid_vspace_obj ao s' proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>\<forall>x. valid_pte (x2 x) s; ao = PageTable x2\<rbrakk> \<Longrightarrow> \<forall>x. valid_pte (x2 x) s'
 2. \<And>x3. \<lbrakk>\<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s; ao = PageDirectory x3\<rbrakk> \<Longrightarrow> \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s' proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma valid_vs_lookup_def2:
  "valid_vs_lookup s = valid_vs_lookup2 (vs_lookup_pages s) (null_filter (caps_of_state s))" apply (simp add: valid_vs_lookup_def valid_vs_lookup2_def) apply (intro iff_allI imp_cong[OF refl] disj_cong[OF refl]
               iff_exI conj_cong[OF refl]) apply (auto simp: null_filter_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vs_lookup s = valid_vs_lookup2 (vs_lookup_pages s) (null_filter (caps_of_state s)) proof (prove)
goal (1 subgoal):
 1. (\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) = (\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. null_filter (caps_of_state s) (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)) proof (prove)
goal (1 subgoal):
 1. \<And>p ref a b cap. \<lbrakk>(ref \<unrhd> p) s; ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None]\<rbrakk> \<Longrightarrow> (caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) = (null_filter (caps_of_state s) (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal:
No subgoals!