kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchAcc_AI

lemma set_pt_valid_global:
  "\<lbrace>\<lambda>s. valid_global_refs s\<rbrace>
  set_pt p pt
  \<lbrace>\<lambda>_ s. valid_global_refs s\<rbrace>" by (wp valid_global_refs_cte_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_global_refs\<rbrace>
theory ArchAcc_AI

lemma set_pt_valid_arch_state[wp]:
  "\<lbrace>\<lambda>s. valid_arch_state s\<rbrace>
  set_pt p pt
  \<lbrace>\<lambda>_ s. valid_arch_state s\<rbrace>" by (wp valid_arch_state_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_arch_state\<rbrace>
theory ArchAcc_AI

lemma set_pt_cur:
  "\<lbrace>\<lambda>s. cur_tcb s\<rbrace>
  set_pt p pt
  \<lbrace>\<lambda>_ s. cur_tcb s\<rbrace>" unfolding set_pt_def cur_tcb_def including unfold_objects by (wpsimp wp: set_object_wp_strong simp: a_type_def is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb\<rbrace> set_pt p pt \<lbrace>\<lambda>_. cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at (cur_thread s) s\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_ s. tcb_at (cur_thread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at (cur_thread s) s\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_ s. tcb_at (cur_thread s) s\<rbrace>
theory ArchAcc_AI

lemma set_pt_aligned [wp]:
  "\<lbrace>pspace_aligned\<rbrace> set_pt p pt \<lbrace>\<lambda>_. pspace_aligned\<rbrace>" unfolding set_pt_def including unfold_objects by (wpsimp wp: set_object_aligned[THEN hoare_set_object_weaken_pre])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> set_pt p pt \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_. pspace_aligned\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_. pspace_aligned\<rbrace>
theory ArchAcc_AI

lemma set_pt_vspace_objs [wp]:
  "\<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageTable pt) s)\<rbrace>
  set_pt p pt
  \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" unfolding set_pt_def including unfold_objects apply (wpsimp wp: set_object_vspace_objs[THEN hoare_set_object_weaken_pre]
              simp: a_type_def) by (simp add: vs_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageTable pt) s)\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageTable pt) s)\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> valid_vspace_obj (PageTable pt) s)\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x2 a b. \<lbrakk>valid_vspace_objs s; (\<exists>ref. (ref \<rhd> p) s) \<longrightarrow> (\<forall>x. valid_pte (pt x) s); kheap s p = Some (ArchObj (PageTable x2)); (a, b) \<in> vs_refs (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (a, b) \<in> vs_refs (ArchObj (PageTable x2))
theory ArchAcc_AI

lemma store_pte_vs_lookup [wp]:
  "\<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> store_pte x pte \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>" unfolding store_pte_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> store_pte x pte \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> do base <- return (x && ~~ mask pt_bits);
offset <- return (x && mask pt_bits >> 2);
pt <- get_pt base;
(return $ pt(UCAST(32 \<rightarrow> 8) offset := pte)) >>= set_pt base
od \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>
theory ArchAcc_AI

lemma unique_table_caps_ptD:
  "\<lbrakk> cs p = Some cap; cap_asid cap = None;
     cs p' = Some cap'; is_pt_cap cap; is_pt_cap cap';
     obj_refs cap' = obj_refs cap;
     unique_table_caps cs\<rbrakk>
  \<Longrightarrow> p = p'" by (fastforce simp add: unique_table_caps_def)

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

lemma unique_table_caps_pdD:
  "\<lbrakk> cs p = Some cap; cap_asid cap = None;
     cs p' = Some cap'; is_pd_cap cap; is_pd_cap cap';
     obj_refs cap' = obj_refs cap;
     unique_table_caps cs\<rbrakk>
  \<Longrightarrow> p = p'" by (fastforce simp add: unique_table_caps_def)

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

lemma valid_objs_caps:
  "valid_objs s \<Longrightarrow> valid_caps (caps_of_state s) s" apply (clarsimp simp: valid_caps_def) apply (erule (1) caps_of_state_valid_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_objs s \<Longrightarrow> valid_caps (caps_of_state s) s proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>valid_objs s; caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> s \<turnstile> cap proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma valid_set_ptI:
  "(!!s opt. \<lbrakk>P s; kheap s p = Some (ArchObj (PageTable opt))\<rbrakk>
         \<Longrightarrow> Q () (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>))
   \<Longrightarrow> \<lbrace>P\<rbrace> set_pt p pt \<lbrace>Q\<rbrace>" by (rule validI) (clarsimp simp: simpler_set_pt_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s opt. \<lbrakk>P s; kheap s p = Some (ArchObj (PageTable opt))\<rbrakk> \<Longrightarrow> Q () (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) \<Longrightarrow> \<lbrace>P\<rbrace> set_pt p pt \<lbrace>Q\<rbrace>
theory ArchAcc_AI

lemma set_object_caps_of_state:
  "\<lbrace>(\<lambda>s. \<not>(tcb_at p s) \<and> \<not>(\<exists>n. cap_table_at n p s)) and
    K ((\<forall>x y. obj \<noteq> CNode x y) \<and> (\<forall>x. obj \<noteq> TCB x)) and
    (\<lambda>s. P (caps_of_state s))\<rbrace>
   set_object p obj
   \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" apply (wpsimp wp: set_object_wp_strong) apply (erule rsubst[where P=P]) apply (rule ext) apply (simp add: caps_of_state_cte_wp_at obj_at_def is_cap_table_def
                   is_tcb_def) apply (auto simp: cte_wp_at_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<not> tcb_at p s \<and> (\<nexists>n. cap_table_at n p s)) and K ((\<forall>x y. obj \<noteq> CNode x y) \<and> (\<forall>x. obj \<noteq> TCB x)) and (\<lambda>s. P (caps_of_state s))\<rbrace> set_object p obj \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>\<not> tcb_at p s; \<forall>n. \<not> cap_table_at n p s; \<forall>x y. obj \<noteq> CNode x y; \<forall>x. obj \<noteq> TCB x; P (caps_of_state s); ko_at ko p s; a_type obj = a_type ko\<rbrakk> \<Longrightarrow> P (caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>\<not> tcb_at p s; \<forall>n. \<not> cap_table_at n p s; \<forall>x y. obj \<noteq> CNode x y; \<forall>x. obj \<noteq> TCB x; ko_at ko p s; a_type obj = a_type ko\<rbrakk> \<Longrightarrow> caps_of_state s = caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko x. \<lbrakk>\<not> tcb_at p s; \<forall>n. \<not> cap_table_at n p s; \<forall>x y. obj \<noteq> CNode x y; \<forall>x. obj \<noteq> TCB x; ko_at ko p s; a_type obj = a_type ko\<rbrakk> \<Longrightarrow> caps_of_state s x = caps_of_state (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>) x proof (prove)
goal (1 subgoal):
 1. \<And>s ko x. \<lbrakk>\<not> (case ko of TCB t \<Rightarrow> True | _ \<Rightarrow> False); \<forall>n. \<not> (case ko of CNode sz cs \<Rightarrow> n = sz \<and> well_formed_cnode_n n cs | _ \<Rightarrow> False); \<forall>x y. obj \<noteq> CNode x y; \<forall>x. obj \<noteq> TCB x; kheap s p = Some ko; a_type obj = a_type ko\<rbrakk> \<Longrightarrow> ((\<exists>cap. cte_wp_at ((=) cap) x s) \<longrightarrow> ((\<exists>cap. cte_wp_at ((=) cap) x (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>)) \<longrightarrow> (THE cap. cte_wp_at ((=) cap) x s) = (THE cap. cte_wp_at ((=) cap) x (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>))) \<and> (\<exists>cap. cte_wp_at ((=) cap) x (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>))) \<and> ((\<forall>cap. \<not> cte_wp_at ((=) cap) x s) \<longrightarrow> (\<forall>cap. \<not> cte_wp_at ((=) cap) x (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>))) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma valid_global_refsD2:
  "\<lbrakk> caps_of_state s ptr = Some cap; valid_global_refs s \<rbrakk>
      \<Longrightarrow> global_refs s \<inter> cap_range cap = {}" by (cases ptr,
      simp add: valid_global_refs_def valid_refs_def
                cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s ptr = Some cap; valid_global_refs s\<rbrakk> \<Longrightarrow> global_refs s \<inter> cap_range cap = {}
theory ArchAcc_AI

lemma set_pt_global_objs [wp]:
  "\<lbrace>valid_global_objs and valid_arch_state and
    (\<lambda>s. p \<in> set (arm_global_pts (arch_state s)) \<longrightarrow>
         (\<forall>x. aligned_pte (pt x)))\<rbrace>
   set_pt p pt
   \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>" apply (rule valid_set_ptI) apply (clarsimp simp: valid_global_objs_def valid_arch_state_def valid_vspace_obj_def
                        valid_vso_at_def obj_at_def empty_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_objs and valid_arch_state and (\<lambda>s. p \<in> set (arm_global_pts (arch_state s)) \<longrightarrow> (\<forall>x. aligned_pte (pt x)))\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. valid_global_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s opt. \<lbrakk>(valid_global_objs and valid_arch_state and (\<lambda>s. p \<in> set (arm_global_pts (arch_state s)) \<longrightarrow> (\<forall>x. aligned_pte (pt x)))) s; kheap s p = Some (ArchObj (PageTable opt))\<rbrakk> \<Longrightarrow> valid_global_objs (s\<lparr>kheap := (kheap s)(p \<mapsto> ArchObj (PageTable pt))\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pt_asid_map [wp]:
  "\<lbrace>valid_asid_map\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" apply (simp add: valid_asid_map_def vspace_at_asid_def) apply (rule hoare_lift_Pf2 [where f="arch_state"]) apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<noteq> 0)\<rbrace> set_pt p pt \<lbrace>\<lambda>_ s. dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<noteq> 0)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. dom (arm_asid_map x) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map x). case x of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<noteq> 0)\<rbrace> set_pt p pt \<lbrace>\<lambda>_ a. dom (arm_asid_map x) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map x). case x of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) a \<and> asid \<noteq> 0)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> set_pt p pt \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma set_pt_only_idle [wp]:
  "\<lbrace>only_idle\<rbrace> set_pt p pt \<lbrace>\<lambda>_. only_idle\<rbrace>" by (wp only_idle_lift)

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

lemma set_pt_equal_mappings [wp]:
  "\<lbrace>equal_kernel_mappings\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>" by (simp add: set_pt_def | wp set_object_equal_mappings get_object_wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equal_kernel_mappings\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>
theory ArchAcc_AI

lemma set_pt_valid_global_vspace_mappings:
  "\<lbrace>\<lambda>s. valid_global_vspace_mappings s \<and> valid_global_objs s \<and> p \<notin> global_refs s\<rbrace>
      set_pt p pt
   \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>" unfolding set_pt_def including unfold_objects by (wpsimp wp: set_object_global_vspace_mappings)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_global_vspace_mappings s \<and> valid_global_objs s \<and> p \<notin> global_refs s\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_global_vspace_mappings s \<and> valid_global_objs s \<and> p \<notin> global_refs s\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_global_vspace_mappings s \<and> valid_global_objs s \<and> p \<notin> global_refs s\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>
theory ArchAcc_AI

lemma set_pt_kernel_window[wp]:
  "\<lbrace>pspace_in_kernel_window\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>" unfolding set_pt_def including unfold_objects by (wpsimp wp: set_object_pspace_in_kernel_window[THEN hoare_set_object_weaken_pre])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>
theory ArchAcc_AI

lemma set_pt_respects_device_region[wp]:
  "\<lbrace>pspace_respects_device_region\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace>" unfolding set_pt_def including unfold_objects by (wpsimp wp: set_object_pspace_respects_device_region[THEN hoare_set_object_weaken_pre])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_respects_device_region\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace>
theory ArchAcc_AI

lemma set_pt_caps_in_kernel_window[wp]:
  "\<lbrace>cap_refs_in_kernel_window\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" unfolding set_pt_def including unfold_objects by (wpsimp wp: set_object_cap_refs_in_kernel_window[THEN hoare_set_object_weaken_pre]
           simp: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_in_kernel_window\<rbrace> set_pt p pt \<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 (PageTable pt)) \<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 (PageTable pt)) \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>
theory ArchAcc_AI

lemma set_pt_caps_respects_device_region[wp]:
  "\<lbrace>cap_refs_respects_device_region\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" unfolding set_pt_def including unfold_objects by (wpsimp wp: set_object_cap_refs_respects_device_region[THEN hoare_set_object_weaken_pre]
           simp: a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region\<rbrace> set_pt p pt \<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 (PageTable pt)) \<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 (PageTable pt)) \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>
theory ArchAcc_AI

lemma set_pt_valid_ioc[wp]:
  "\<lbrace>valid_ioc\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_ioc\<rbrace>" unfolding set_pt_def including unfold_objects by (wpsimp wp: set_object_valid_ioc_no_caps[THEN hoare_set_object_weaken_pre]
           simp: is_tcb is_cap_table)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ioc\<rbrace> set_object p (ArchObj (PageTable pt)) \<lbrace>\<lambda>_. valid_ioc\<rbrace>
theory ArchAcc_AI

lemma in_user_frame_same_type_upd:
  "\<lbrakk>typ_at type p s; type = a_type obj; in_user_frame q s\<rbrakk>
    \<Longrightarrow> in_user_frame q (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>)" apply (clarsimp simp: in_user_frame_def obj_at_def) apply (rule_tac x=sz in exI) apply (auto simp: a_type_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at type p s; type = a_type obj; in_user_frame q s\<rbrakk> \<Longrightarrow> in_user_frame q (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ko sz. \<lbrakk>type = a_type obj; kheap s p = Some ko; a_type ko = a_type obj; kheap s (q && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz))\<rbrakk> \<Longrightarrow> \<exists>sz. (q && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type obj = AArch (AUserData sz)) \<and> (q && ~~ mask (pageBitsForSize sz) \<noteq> p \<longrightarrow> (\<exists>ko. kheap s (q && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz))) proof (prove)
goal (1 subgoal):
 1. \<And>ko sz. \<lbrakk>type = a_type obj; kheap s p = Some ko; a_type ko = a_type obj; kheap s (q && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage False sz))\<rbrakk> \<Longrightarrow> (q && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type obj = AArch (AUserData sz)) \<and> (q && ~~ mask (pageBitsForSize sz) \<noteq> p \<longrightarrow> (\<exists>ko. kheap s (q && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (AUserData sz))) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma in_device_frame_same_type_upd:
  "\<lbrakk>typ_at type p s; type = a_type obj ; in_device_frame q s\<rbrakk>
    \<Longrightarrow> in_device_frame q (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>)" apply (clarsimp simp: in_device_frame_def obj_at_def) apply (rule_tac x=sz in exI) apply (auto simp: a_type_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at type p s; type = a_type obj; in_device_frame q s\<rbrakk> \<Longrightarrow> in_device_frame q (s\<lparr>kheap := (kheap s)(p \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>ko sz. \<lbrakk>type = a_type obj; kheap s p = Some ko; a_type ko = a_type obj; kheap s (q && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage True sz))\<rbrakk> \<Longrightarrow> \<exists>sz. (q && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type obj = AArch (ADeviceData sz)) \<and> (q && ~~ mask (pageBitsForSize sz) \<noteq> p \<longrightarrow> (\<exists>ko. kheap s (q && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz))) proof (prove)
goal (1 subgoal):
 1. \<And>ko sz. \<lbrakk>type = a_type obj; kheap s p = Some ko; a_type ko = a_type obj; kheap s (q && ~~ mask (pageBitsForSize sz)) = Some (ArchObj (DataPage True sz))\<rbrakk> \<Longrightarrow> (q && ~~ mask (pageBitsForSize sz) = p \<longrightarrow> a_type obj = AArch (ADeviceData sz)) \<and> (q && ~~ mask (pageBitsForSize sz) \<noteq> p \<longrightarrow> (\<exists>ko. kheap s (q && ~~ mask (pageBitsForSize sz)) = Some ko \<and> a_type ko = AArch (ADeviceData sz))) proof (prove)
goal:
No subgoals!
theory ArchAcc_AI

lemma store_word_offs_in_user_frame[wp]:
  "\<lbrace>\<lambda>s. in_user_frame p s\<rbrace> store_word_offs a x w \<lbrace>\<lambda>_ s. in_user_frame p s\<rbrace>" unfolding in_user_frame_def by (wp hoare_vcg_ex_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_user_frame p\<rbrace> store_word_offs a x w \<lbrace>\<lambda>_. in_user_frame p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrace> store_word_offs a x w \<lbrace>\<lambda>_ s. \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrace>
theory ArchAcc_AI

lemma store_word_offs_in_device_frame[wp]:
  "\<lbrace>\<lambda>s. in_device_frame p s\<rbrace> store_word_offs a x w \<lbrace>\<lambda>_ s. in_device_frame p s\<rbrace>" unfolding in_device_frame_def by (wp hoare_vcg_ex_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>in_device_frame p\<rbrace> store_word_offs a x w \<lbrace>\<lambda>_. in_device_frame p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>sz. typ_at (AArch (ADeviceData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrace> store_word_offs a x w \<lbrace>\<lambda>_ s. \<exists>sz. typ_at (AArch (ADeviceData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrace>