kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchAcc_AI

lemma is_aligned_lookup_pt_slot_no_fail:
  "\<lbrakk>is_aligned vptr 16; is_aligned pt 6\<rbrakk>
   \<Longrightarrow> is_aligned (lookup_pt_slot_no_fail pt vptr) 6" apply (clarsimp simp: lookup_pt_slot_no_fail_def) apply (erule aligned_add_aligned) apply (rule is_aligned_shiftl) apply (rule is_aligned_andI1) apply (rule is_aligned_shiftr) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned vptr 16; is_aligned pt 6\<rbrakk> \<Longrightarrow> is_aligned (lookup_pt_slot_no_fail pt vptr) 6 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned vptr 16; is_aligned pt 6\<rbrakk> \<Longrightarrow> is_aligned (pt + ((vptr >> 12) && 0xFF << 2)) 6 proof (prove)
goal (2 subgoals):
 1. is_aligned vptr 16 \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) 6
 2. is_aligned vptr 16 \<Longrightarrow> 6 \<le> 6 proof (prove)
goal (2 subgoals):
 1. is_aligned vptr 16 \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF) (6 - 2)
 2. is_aligned vptr 16 \<Longrightarrow> 6 \<le> 6 proof (prove)
goal (2 subgoals):
 1. is_aligned vptr 16 \<Longrightarrow> is_aligned (vptr >> 12) (6 - 2)
 2. is_aligned vptr 16 \<Longrightarrow> 6 \<le> 6 proof (prove)
goal (2 subgoals):
 1. is_aligned vptr 16 \<Longrightarrow> is_aligned vptr (6 - 2 + 12)
 2. is_aligned vptr 16 \<Longrightarrow> 6 \<le> 6 proof (prove)
goal (1 subgoal):
 1. is_aligned vptr 16 \<Longrightarrow> 6 \<le> 6 proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma pd_bits: "pd_bits = 14" by (simp add: pd_bits_def pageBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pd_bits = 14
theory ArchAcc_AI

lemma word_shift_by_n:
  "x * (2^n) = (x::'a::len word) << n" by (simp add: shiftl_t2n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x * 2 ^ n = x << n
theory ArchAcc_AI

lemma vs_lookup_arch_update:
  "arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s) \<Longrightarrow>
  vs_lookup (arch_state_update f s) = vs_lookup s" apply (rule order_antisym) apply (rule vs_lookup_sub) apply (clarsimp simp: obj_at_def) apply simp apply (rule vs_lookup_sub) apply (clarsimp simp: obj_at_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> vs_lookup (arch_state_update f s) = vs_lookup s proof (prove)
goal (2 subgoals):
 1. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> vs_lookup (arch_state_update f s) \<subseteq> vs_lookup s
 2. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> vs_lookup s \<subseteq> vs_lookup (arch_state_update f s) proof (prove)
goal (3 subgoals):
 1. \<And>ko p. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; ko_at ko p (arch_state_update f s)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s
 2. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> graph_of (asid_table (arch_state_update f s)) \<subseteq> graph_of (asid_table s)
 3. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> vs_lookup s \<subseteq> vs_lookup (arch_state_update f s) proof (prove)
goal (2 subgoals):
 1. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> graph_of (asid_table (arch_state_update f s)) \<subseteq> graph_of (asid_table s)
 2. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> vs_lookup s \<subseteq> vs_lookup (arch_state_update f s) proof (prove)
goal (1 subgoal):
 1. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> vs_lookup s \<subseteq> vs_lookup (arch_state_update f s) proof (prove)
goal (2 subgoals):
 1. \<And>ko p. \<lbrakk>arm_asid_table (f (arch_state s)) = asid_table s; ko_at ko p s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p (arch_state_update f s)
 2. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (arch_state_update f s)) proof (prove)
goal (1 subgoal):
 1. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (arch_state_update f s)) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma vs_lookup_pages_arch_update:
  "arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s) \<Longrightarrow>
  vs_lookup_pages (arch_state_update f s) = vs_lookup_pages s" apply (rule order_antisym) apply (rule vs_lookup_pages_sub) apply (clarsimp simp: obj_at_def) apply simp apply (rule vs_lookup_pages_sub) apply (clarsimp simp: obj_at_def) apply simp done

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

lemma vs_lookup_hwasid_table [iff]:
  "vs_lookup (s\<lparr>arch_state := arm_hwasid_table_update f (arch_state s)\<rparr>) = vs_lookup s" by (simp add: vs_lookup_arch_update)

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

lemma vs_lookup_pages_asid_map[iff]:
  "vs_lookup_pages (s\<lparr>arch_state := arm_asid_map_update f (arch_state s)\<rparr>) =
   vs_lookup_pages s" by (simp add: vs_lookup_pages_arch_update)

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

lemma vs_lookup_pages_hwasid_table[iff]:
  "vs_lookup_pages (s\<lparr>arch_state := arm_hwasid_table_update f (arch_state s)\<rparr>) =
   vs_lookup_pages s" by (simp add: vs_lookup_pages_arch_update)

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

lemma vs_lookup_pages_next_asid[iff]:
  "vs_lookup_pages (s\<lparr>arch_state := arm_next_asid_update f (arch_state s)\<rparr>) =
   vs_lookup_pages s" by (simp add: vs_lookup_pages_arch_update)

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

lemma store_pte_valid_vspace_objs[wp]:
  "\<lbrace>valid_vspace_objs and valid_pte pte\<rbrace>
    store_pte p pte
  \<lbrace>\<lambda>_. (valid_vspace_objs)\<rbrace>" unfolding store_pte_def apply wp apply clarsimp apply (unfold valid_vspace_objs_def) apply (erule_tac x="p && ~~ mask pt_bits" in allE) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and valid_pte pte\<rbrace> store_pte p pte \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and valid_pte pte\<rbrace> do base <- return (p && ~~ mask pt_bits);
offset <- return (p && mask pt_bits >> 2);
pt <- get_pt base;
(return $ pt(UCAST(32 \<rightarrow> 8) offset := pte)) >>= set_pt base
od \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vspace_objs and valid_pte pte) s \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> valid_vspace_objs s \<and> ((\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> (\<forall>x. valid_pte ((pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte)) x) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s pt ref x. \<lbrakk>valid_vspace_objs s; valid_pte pte s; ako_at (PageTable pt) (p && ~~ mask pt_bits) s; (ref \<rhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> valid_pte (pt x) s proof (prove)
goal (1 subgoal):
 1. \<And>s pt ref x. \<lbrakk>\<forall>p rs ao. (rs \<rhd> p) s \<longrightarrow> ako_at ao p s \<longrightarrow> valid_vspace_obj ao s; valid_pte pte s; ako_at (PageTable pt) (p && ~~ mask pt_bits) s; (ref \<rhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)\<rbrakk> \<Longrightarrow> valid_pte (pt x) s proof (prove)
goal (1 subgoal):
 1. \<And>s pt ref x. \<lbrakk>valid_pte pte s; ako_at (PageTable pt) (p && ~~ mask pt_bits) s; (ref \<rhd> (p && ~~ mask pt_bits)) s; x \<noteq> UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2); \<forall>rs ao. (rs \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> ako_at ao (p && ~~ mask pt_bits) s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> valid_pte (pt x) s proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma unique_table_caps_pdE:
  "\<lbrakk> unique_table_caps cs; cs p = Some cap; cap_asid cap = None;
     cs p' = Some cap'; cap_asid cap' = Some v; is_pd_cap cap;
     is_pd_cap cap'; obj_refs cap' = obj_refs cap \<rbrakk>
       \<Longrightarrow> P" apply (frule(6) unique_table_caps_pdD[where cs=cs]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unique_table_caps cs; cs p = Some cap; cap_asid cap = None; cs p' = Some cap'; cap_asid cap' = Some v; is_pd_cap cap; is_pd_cap cap'; obj_refs cap' = obj_refs cap\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unique_table_caps cs; cs p = Some cap; cap_asid cap = None; cs p' = Some cap'; cap_asid cap' = Some v; is_pd_cap cap; is_pd_cap cap'; obj_refs cap' = obj_refs cap; p = p'\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma eq_ucast_word12[simp]:
  "((ucast (x :: 12 word) :: word32) = ucast y) = (x = y)" apply safe apply (drule_tac f="ucast :: (word32 \<Rightarrow> 12 word)" in arg_cong) apply (simp add: ucast_up_ucast_id is_up_def
                   source_size_def target_size_def word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (UCAST(12 \<rightarrow> 32) x = UCAST(12 \<rightarrow> 32) y) = (x = y) proof (prove)
goal (1 subgoal):
 1. UCAST(12 \<rightarrow> 32) x = UCAST(12 \<rightarrow> 32) y \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) x) = UCAST(32 \<rightarrow> 12) (UCAST(12 \<rightarrow> 32) y) \<Longrightarrow> x = y proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_only_idle [wp]:
  "\<lbrace>only_idle\<rbrace> set_pd p pd \<lbrace>\<lambda>_. only_idle\<rbrace>" by (wp only_idle_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>only_idle\<rbrace> set_pd p pd \<lbrace>\<lambda>_. only_idle\<rbrace>
theory ArchAcc_AI

lemma set_pd_equal_kernel_mappings_triv:
  "\<lbrace>obj_at (\<lambda>ko. \<exists>pd'. ko = (ArchObj (PageDirectory pd'))
                       \<and> (\<forall>x \<in> kernel_mapping_slots. pd x = pd' x)) p
          and equal_kernel_mappings\<rbrace>
     set_pd p pd
   \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>" apply (simp add: set_pd_def) apply (wp set_object_equal_mappings get_object_wp) apply (clarsimp simp: obj_at_def) apply (simp add: equal_kernel_mappings_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and equal_kernel_mappings\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and equal_kernel_mappings\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and equal_kernel_mappings) s \<Longrightarrow> equal_kernel_mappings s \<and> (\<forall>pda. ArchObj (PageDirectory pd) = ArchObj (PageDirectory pda) \<longrightarrow> (\<forall>x pd'. ako_at (PageDirectory pd') x s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pda w = pd' w))) proof (prove)
goal (1 subgoal):
 1. \<And>s x pd' pd'a w. \<lbrakk>equal_kernel_mappings s; kheap s p = Some (ArchObj (PageDirectory pd'a)); \<forall>x\<in>kernel_mapping_slots. pd x = pd'a x; kheap s x = Some (ArchObj (PageDirectory pd')); w \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> pd'a w = pd' w proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_kernel_window[wp]:
  "\<lbrace>pspace_in_kernel_window\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>" apply (simp add: set_pd_def) including unfold_objects apply (wpsimp wp: set_object_pspace_in_kernel_window[THEN hoare_set_object_weaken_pre]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_device_region[wp]:
  "\<lbrace>pspace_respects_device_region\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace>" apply (simp add: set_pd_def) including unfold_objects apply (wpsimp wp: set_object_pspace_respects_device_region[THEN hoare_set_object_weaken_pre]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_caps_kernel_window[wp]:
  "\<lbrace>cap_refs_in_kernel_window\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" apply (simp add: set_pd_def) including unfold_objects apply (wpsimp wp: set_object_cap_refs_in_kernel_window[THEN hoare_set_object_weaken_pre]
              simp: a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_caps_respects_device_region[wp]:
  "\<lbrace>cap_refs_respects_device_region\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" apply (simp add: set_pd_def) including unfold_objects apply (wpsimp wp: set_object_cap_refs_respects_device_region[THEN hoare_set_object_weaken_pre]
              simp: a_type_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region\<rbrace> set_object p (ArchObj (PageDirectory pd)) \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_valid_ioc[wp]:
  "\<lbrace>valid_ioc\<rbrace> set_pd p pt \<lbrace>\<lambda>_. valid_ioc\<rbrace>" apply (simp add: set_pd_def) including unfold_objects apply (wpsimp wp: set_object_valid_ioc_no_caps[THEN hoare_set_object_weaken_pre]
              simp: a_type_def is_tcb is_cap_table) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> set_pd p pt \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> set_object p (ArchObj (PageDirectory pt)) \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> set_object p (ArchObj (PageDirectory pt)) \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pd_vms[wp]:
  "\<lbrace>valid_machine_state\<rbrace> set_pd p pt \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" apply (simp add: set_pd_def) apply (wp set_object_wp_strong) apply clarify apply (erule valid_machine_state_heap_updI) apply (fastforce simp: a_type_def obj_at_def
           split: Structures_A.kernel_object.splits arch_kernel_obj.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> set_pd p pt \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> set_object p (ArchObj (PageDirectory pt)) \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_machine_state s \<Longrightarrow> \<forall>ko. ko_at ko p s \<longrightarrow> a_type (ArchObj (PageDirectory pt)) = a_type ko \<longrightarrow> valid_machine_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pt))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_machine_state s; ko_at ko p s; a_type (ArchObj (PageDirectory pt)) = a_type ko\<rbrakk> \<Longrightarrow> valid_machine_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageDirectory pt))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>ko_at ko p s; a_type (ArchObj (PageDirectory pt)) = a_type ko\<rbrakk> \<Longrightarrow> typ_at (?type5 s ko) p s
 2. \<And>s ko. \<lbrakk>ko_at ko p s; a_type (ArchObj (PageDirectory pt)) = a_type ko\<rbrakk> \<Longrightarrow> a_type (ArchObj (PageDirectory pt)) = ?type5 s ko proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma store_pde_state_refs_of:
  "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv s. P (state_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_refs_of_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_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_refs_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (state_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_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_refs_of s x = state_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!