kings-crown/FVELER_Isabelle huggingface dataset:
theory Untyped_AI

lemma invoked_untyp_tcb[wp]:
  "\<lbrace>invs and st_tcb_at active tptr
        and valid_untyped_inv ui and ct_active\<rbrace>
     invoke_untyped ui \<lbrace>\<lambda>rv. \<lambda>s :: 'state_ext state. tcb_at tptr s\<rbrace>" apply (simp add: tcb_at_st_tcb_at) apply (rule hoare_pre, wp invoke_untyped_st_tcb_at) apply (clarsimp elim!: pred_tcb_weakenE) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and st_tcb_at active tptr and valid_untyped_inv ui and ct_active\<rbrace> invoke_untyped ui \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and st_tcb_at active tptr and valid_untyped_inv ui and ct_active\<rbrace> invoke_untyped ui \<lbrace>\<lambda>rv. st_tcb_at (\<lambda>_. True) tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and st_tcb_at active tptr and valid_untyped_inv ui and ct_active) s \<Longrightarrow> (invs and st_tcb_at ((\<lambda>_. True) and Not \<circ> inactive and Not \<circ> idle) tptr and ct_active and valid_untyped_inv ui) s proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>invs s; active (itcb_state tcb); valid_untyped_inv ui s; ct_active s\<rbrakk> \<Longrightarrow> itcb_state tcb \<noteq> Inactive \<and> itcb_state tcb \<noteq> IdleThreadState proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma sts_mdb[wp]:
  "\<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>" by (simp add: set_thread_state_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>
theory Untyped_AI

lemma update_untyped_cap_valid_objs:
  "\<lbrace> valid_objs and valid_cap cap
      and cte_wp_at (is_untyped_cap) p and K (is_untyped_cap cap)\<rbrace>
    set_cap cap p \<lbrace> \<lambda>rv. valid_objs \<rbrace>" apply (wp set_cap_valid_objs) apply (clarsimp simp: is_cap_simps cte_wp_at_caps_of_state) apply (drule tcb_cap_valid_caps_of_stateD, simp+) apply (simp add: tcb_cap_valid_untyped_to_thread) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap cap and cte_wp_at is_untyped_cap p and K (is_untyped_cap cap)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs and valid_cap cap and cte_wp_at is_untyped_cap p and K (is_untyped_cap cap)) s \<Longrightarrow> (valid_objs and valid_cap cap and tcb_cap_valid cap p) s proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f deva ra bitsa fa. \<lbrakk>valid_objs s; s \<turnstile> UntypedCap dev r bits f; cap = UntypedCap dev r bits f; caps_of_state s p = Some (UntypedCap deva ra bitsa fa)\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) p s proof (prove)
goal (1 subgoal):
 1. \<And>s dev r bits f deva ra bitsa fa. \<lbrakk>valid_objs s; s \<turnstile> UntypedCap dev r bits f; cap = UntypedCap dev r bits f; tcb_cap_valid (UntypedCap deva ra bitsa fa) p s\<rbrakk> \<Longrightarrow> tcb_cap_valid (UntypedCap dev r bits f) p s proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma valid_untyped_pspace_no_overlap:
  "pspace_no_overlap {ptr .. ptr + 2 ^ sz - 1} s
    \<Longrightarrow> valid_untyped (UntypedCap dev ptr sz idx) s" apply (clarsimp simp: valid_untyped_def split del: if_split) apply (drule(1) pspace_no_overlap_obj_range) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_no_overlap {ptr..ptr + 2 ^ sz - 1} s \<Longrightarrow> valid_untyped (UntypedCap dev ptr sz idx) s proof (prove)
goal (1 subgoal):
 1. \<And>p obj. \<lbrakk>pspace_no_overlap {ptr..ptr + 2 ^ sz - 1} s; kheap s p = Some obj; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {} proof (prove)
goal (1 subgoal):
 1. \<And>p obj. \<lbrakk>kheap s p = Some obj; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<inter> {ptr..ptr + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> obj_range p obj \<subseteq> {ptr..ptr + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {ptr + word_of_nat idx..ptr + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {} proof (prove)
goal:
No subgoals!
theory Untyped_AI

lemma snd_set_zip_in_set:
  "x\<in> snd ` set (zip a b) \<Longrightarrow> x\<in> set b" apply (clarsimp) apply (erule in_set_zipE) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> snd ` set (zip a b) \<Longrightarrow> x \<in> set b proof (prove)
goal (1 subgoal):
 1. \<And>aa. (aa, x) \<in> set (zip a b) \<Longrightarrow> x \<in> set b proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>aa \<in> set a; x \<in> set b\<rbrakk> \<Longrightarrow> x \<in> set b proof (prove)
goal:
No subgoals!
theory ArchUntyped_AI

lemma of_bl_nat_to_cref[Untyped_AI_assms]:
    "\<lbrakk> x < 2 ^ bits; bits < word_bits \<rbrakk>
      \<Longrightarrow> (of_bl (nat_to_cref bits x) :: machine_word) = of_nat x" apply (clarsimp intro!: less_mask_eq
                  simp: nat_to_cref_def of_drop_to_bl
                        word_size word_less_nat_alt word_bits_def) by (metis add_lessD1 le_unat_uoi nat_le_iff_add nat_le_linear)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ bits; bits < word_bits\<rbrakk> \<Longrightarrow> of_bl (nat_to_cref bits x) = word_of_nat x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ bits; bits < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat x) < 2 ^ bits
theory ArchUntyped_AI

lemma data_to_obj_type_sp[Untyped_AI_assms]:
  "\<lbrace>P\<rbrace> data_to_obj_type x \<lbrace>\<lambda>ts (s::'state_ext::state_ext state). ts \<noteq> ArchObject ASIDPoolObj \<and> P s\<rbrace>, -" unfolding data_to_obj_type_def apply (rule hoare_pre) apply (wp|wpc)+ apply clarsimp apply (simp add: arch_data_to_obj_type_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> data_to_obj_type x \<lbrace>\<lambda>ts s. ts \<noteq> ArchObject ASIDPoolObj \<and> P s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE n <- returnOk $ data_to_nat x;
if n = 0 then returnOk $ Untyped else if n = 1 then returnOk $ TCBObject else if n = 2 then returnOk $ EndpointObject else if n = 3 then returnOk $ NotificationObject else if n = 4 then returnOk $ CapTableObject else case arch_data_to_obj_type (n - 5) of None \<Rightarrow> throwError (InvalidArgument 0) | Some tp \<Rightarrow> returnOk (ArchObject tp)
odE \<lbrace>\<lambda>ts s. ts \<noteq> ArchObject ASIDPoolObj \<and> P s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE n <- returnOk $ data_to_nat x;
if n = 0 then returnOk $ Untyped else if n = 1 then returnOk $ TCBObject else if n = 2 then returnOk $ EndpointObject else if n = 3 then returnOk $ NotificationObject else if n = 4 then returnOk $ CapTableObject else case arch_data_to_obj_type (n - 5) of None \<Rightarrow> throwError (InvalidArgument 0) | Some tp \<Rightarrow> returnOk (ArchObject tp)
odE \<lbrace>\<lambda>ts s. ts \<noteq> ArchObject ASIDPoolObj \<and> P s\<rbrace>, -
 2. \<And>s. P s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> True \<and> (data_to_nat x = 0 \<longrightarrow> Untyped \<noteq> ArchObject ASIDPoolObj \<and> P s) \<and> (data_to_nat x \<noteq> 0 \<longrightarrow> (data_to_nat x = 1 \<longrightarrow> TCBObject \<noteq> ArchObject ASIDPoolObj \<and> P s) \<and> (data_to_nat x \<noteq> 1 \<longrightarrow> (data_to_nat x = 2 \<longrightarrow> EndpointObject \<noteq> ArchObject ASIDPoolObj \<and> P s) \<and> (data_to_nat x \<noteq> 2 \<longrightarrow> (data_to_nat x = 3 \<longrightarrow> NotificationObject \<noteq> ArchObject ASIDPoolObj \<and> P s) \<and> (data_to_nat x \<noteq> 3 \<longrightarrow> (data_to_nat x = 4 \<longrightarrow> CapTableObject \<noteq> ArchObject ASIDPoolObj \<and> P s) \<and> (data_to_nat x \<noteq> 4 \<longrightarrow> (arch_data_to_obj_type (data_to_nat x - 5) = None \<longrightarrow> True) \<and> (\<forall>xa. arch_data_to_obj_type (data_to_nat x - 5) = Some xa \<longrightarrow> ArchObject xa \<noteq> ArchObject ASIDPoolObj \<and> P s)))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; 0 < unat x; unat x \<noteq> Suc 0; unat x \<noteq> 2; unat x \<noteq> 3; unat x \<noteq> 4; arch_data_to_obj_type (unat x - 5) = Some ASIDPoolObj\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchUntyped_AI

lemma asid_bits_ge_0:
  "(0::word32) < 2 ^ asid_bits" by (simp add: asid_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < 2 ^ local.asid_bits
theory ArchUntyped_AI

lemma copy_global_mappings_hoare_lift:(*FIXME: arch_split  \<rightarrow> these do not seem to be used globally *)
  assumes wp: "\<And>ptr val. \<lbrace>Q\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv. Q\<rbrace>"
  shows       "\<lbrace>Q\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>rv. Q\<rbrace>" apply (simp add: copy_global_mappings_def) apply (wp mapM_x_wp' wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> do global_pd <- gets (arm_global_pd \<circ> arch_state);
mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (pd + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]
od \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchUntyped_AI

lemma init_arch_objects_hoare_lift:
  assumes wp: "\<And>oper. \<lbrace>(P::'state_ext::state_ext state\<Rightarrow>bool)\<rbrace> do_machine_op oper \<lbrace>\<lambda>rv :: unit. Q\<rbrace>"
              "\<And>ptr val. \<lbrace>P\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv. P\<rbrace>"
  shows       "\<lbrace>P and Q\<rbrace> init_arch_objects tp ptr sz us adds \<lbrace>\<lambda>rv. Q\<rbrace>" proof - have pres: "\<And>oper. \<lbrace>P and Q\<rbrace> do_machine_op oper \<lbrace>\<lambda>rv :: unit. Q\<rbrace>"
             "\<lbrace>P and Q\<rbrace> return () \<lbrace>\<lambda>rv. Q\<rbrace>" by (wp wp | simp)+ show ?thesis apply (simp add: init_arch_objects_def
                  pres reserve_region_def unless_def when_def
           split: Structures_A.apiobject_type.split
                  aobject_type.split) apply clarsimp apply (rule hoare_pre) apply (wp mapM_x_wp' copy_global_mappings_hoare_lift wp) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and Q\<rbrace> init_arch_objects tp ptr sz us adds \<lbrace>\<lambda>rv. Q\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>P and Q\<rbrace> init_arch_objects tp ptr sz us adds \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>oper. \<lbrace>P and Q\<rbrace> do_machine_op oper \<lbrace>\<lambda>rv. Q\<rbrace>) &&& \<lbrace>P and Q\<rbrace> return () \<lbrace>\<lambda>rv. Q\<rbrace> proof (state)
this:
\<lbrace>P and Q\<rbrace> do_machine_op ?oper \<lbrace>\<lambda>rv. Q\<rbrace>
\<lbrace>P and Q\<rbrace> return () \<lbrace>\<lambda>rv. Q\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P and Q\<rbrace> init_arch_objects tp ptr sz us adds \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and Q\<rbrace> init_arch_objects tp ptr sz us adds \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. tp = ArchObject PageDirectoryObj \<longrightarrow> \<lbrace>P and Q\<rbrace> do y <- mapM_x copy_global_mappings adds;
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) adds)
od \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. tp = ArchObject PageDirectoryObj \<Longrightarrow> \<lbrace>P and Q\<rbrace> do y <- mapM_x copy_global_mappings adds;
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) adds)
od \<lbrace>\<lambda>rv. Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. tp = ArchObject PageDirectoryObj \<Longrightarrow> \<lbrace>?Q5\<rbrace> do y <- mapM_x copy_global_mappings adds;
do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU x (x + 2 ^ pd_bits - 1) (addrFromPPtr x)) adds)
od \<lbrace>\<lambda>rv. Q\<rbrace>
 2. \<And>s. \<lbrakk>tp = ArchObject PageDirectoryObj; (P and Q) s\<rbrakk> \<Longrightarrow> ?Q5 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>tp = ArchObject PageDirectoryObj; (P and Q) s\<rbrakk> \<Longrightarrow> P s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>P and Q\<rbrace> init_arch_objects tp ptr sz us adds \<lbrace>\<lambda>rv. Q\<rbrace>

goal:
No subgoals!
theory ArchUntyped_AI

lemma cap_refs_in_kernel_windowD2:
  "\<lbrakk> cte_wp_at P p (s::'state_ext::state_ext state); cap_refs_in_kernel_window s \<rbrakk>
       \<Longrightarrow> \<exists>cap. P cap \<and> region_in_kernel_window (cap_range cap) s" apply (clarsimp simp: cte_wp_at_caps_of_state region_in_kernel_window_def) apply (drule(1) cap_refs_in_kernel_windowD) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P p s; cap_refs_in_kernel_window s\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> region_in_kernel_window (cap_range cap) s proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_refs_in_kernel_window s; caps_of_state s p = Some cap; P cap\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> (\<forall>x\<in>cap_range cap. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) proof (prove)
goal (1 subgoal):
 1. \<And>cap. \<lbrakk>cap_refs_in_kernel_window s; P cap; \<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> \<exists>cap. P cap \<and> (\<forall>x\<in>cap_range cap. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow) proof (prove)
goal:
No subgoals!
theory ArchUntyped_AI

lemma init_arch_objects_caps_overlap_reserved[wp,Untyped_AI_assms]:
  "\<lbrace>\<lambda>(s::'state_ext::state_ext state). caps_overlap_reserved S s\<rbrace>
   init_arch_objects ty ptr n us y
   \<lbrace>\<lambda>rv s. caps_overlap_reserved S s\<rbrace>" apply (simp add:caps_overlap_reserved_def) apply (rule hoare_pre) apply (wp retype_region_mdb init_arch_objects_hoare_lift) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>caps_overlap_reserved S\<rbrace> init_arch_objects ty ptr n us y \<lbrace>\<lambda>rv. caps_overlap_reserved S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}\<rbrace> init_arch_objects ty ptr n us y \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> init_arch_objects ty ptr n us y \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}\<rbrace>
 2. \<And>s. \<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {} \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {} \<Longrightarrow> ((\<lambda>a. \<forall>cap\<in>ran (caps_of_state a). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}) and (\<lambda>s. \<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {})) s proof (prove)
goal:
No subgoals!
theory ArchUntyped_AI

lemma pbfs_atleast_pageBits':
  "pageBits \<le> pageBitsForSize sz" by (cases sz, simp_all add: pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pageBits \<le> pageBitsForSize sz
theory ArchUntyped_AI

lemma pbfs_less_wb':
  "pageBitsForSize sz < word_bits" by (cases sz, simp_all add: word_bits_conv pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pageBitsForSize sz < word_bits
theory ArchUntyped_AI

lemma reachable_pg_cap_exst_update[simp]:
  "reachable_pg_cap x (trans_state f (s::'state_ext::state_ext state)) = reachable_pg_cap x s" by (simp add: reachable_pg_cap_def vs_lookup_pages_def
                vs_lookup_pages1_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reachable_pg_cap x (trans_state f s) = reachable_pg_cap x s
theory ArchUntyped_AI

lemma create_cap_cap_refs_in_kernel_window[wp, Untyped_AI_assms]:
  "\<lbrace>cap_refs_in_kernel_window and cte_wp_at (\<lambda>c. cap_range (default_cap tp oref sz dev) \<subseteq> cap_range c) p\<rbrace>
     create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" apply (simp add: create_cap_def) apply (wp | simp)+ apply (clarsimp simp: cte_wp_at_caps_of_state) apply (drule(1) cap_refs_in_kernel_windowD) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window and cte_wp_at (\<lambda>c. cap_range (default_cap tp oref sz dev) \<subseteq> cap_range c) p\<rbrace> create_cap tp sz p dev (cref, oref) \<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 (default_cap tp oref sz dev) \<subseteq> cap_range c) p\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
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 (default_cap tp oref sz dev) \<subseteq> cap_range c) p s \<Longrightarrow> \<forall>ref\<in>cap_range (default_cap tp oref sz dev). arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>s ref cap. \<lbrakk>ref \<in> cap_range (default_cap tp oref sz dev); cap_refs_in_kernel_window s; caps_of_state s p = Some cap; cap_range (default_cap tp oref sz dev) \<subseteq> cap_range cap\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>s ref cap. \<lbrakk>ref \<in> cap_range (default_cap tp oref sz dev); cap_refs_in_kernel_window s; cap_range (default_cap tp oref sz dev) \<subseteq> cap_range cap; \<forall>ref\<in>cap_range cap. arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow proof (prove)
goal:
No subgoals!
theory ArchUntyped_AI

lemma valid_arch_state_global_pd:
  "\<lbrakk> valid_arch_state s; pspace_aligned s \<rbrakk>
    \<Longrightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd)) (arm_global_pd (arch_state s)) s
           \<and> is_aligned (arm_global_pd (arch_state s)) pd_bits" apply (clarsimp simp: valid_arch_state_def a_type_def
                        pd_aligned pd_bits_def pageBits_def
                 elim!: obj_at_weakenE) apply (clarsimp split: Structures_A.kernel_object.split_asm
                         arch_kernel_obj.split_asm if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_state s; pspace_aligned s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd)) (arm_global_pd (arch_state s)) s \<and> is_aligned (arm_global_pd (arch_state s)) pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>pspace_aligned s; valid_asid_table (asid_table s) s; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory; valid_global_pts s; is_inv (arm_hwasid_table (arch_state s)) (map_option fst \<circ> arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> \<exists>pd. ko = ArchObj (PageDirectory pd) proof (prove)
goal:
No subgoals!
theory ArchUntyped_AI

lemma mapM_copy_global_mappings_nonempty_table[wp]:
  "\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
        \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and
    K (\<forall>pd\<in>set pds. is_aligned pd pd_bits)\<rbrace>
   mapM_x copy_global_mappings pds
   \<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_strengthen_post) apply (rule mapM_x_wp', rule copy_global_mappings_nonempty_table) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and K (\<forall>pd\<in>set pds. is_aligned pd pd_bits)\<rbrace> mapM_x copy_global_mappings pds \<lbrace>\<lambda>rv s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>pd\<in>set pds. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace> mapM_x copy_global_mappings pds \<lbrace>\<lambda>rv s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<forall>pd\<in>set pds. is_aligned pd pd_bits \<Longrightarrow> \<lbrace>\<lambda>s. \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace> mapM_x copy_global_mappings pds \<lbrace>?Q2\<rbrace>
 2. \<And>rv s. \<lbrakk>\<forall>pd\<in>set pds. is_aligned pd pd_bits; ?Q2 rv s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<forall>pd\<in>set pds. is_aligned pd pd_bits; x \<in> set pds\<rbrakk> \<Longrightarrow> is_aligned x pd_bits
 2. \<And>rv s. \<lbrakk>\<forall>pd\<in>set pds. is_aligned pd pd_bits; \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrakk> \<Longrightarrow> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s proof (prove)
goal:
No subgoals!
theory ArchUntyped_AI

lemma nonempty_table_caps_of[Untyped_AI_assms]:
  "nonempty_table S ko \<Longrightarrow> caps_of ko = {}" by (auto simp: caps_of_def cap_of_def nonempty_table_def a_type_def
          split: Structures_A.kernel_object.split if_split_asm)

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