kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchRetype_AI

lemma unique_table_caps_null:
  "unique_table_caps (null_filter s)
       = unique_table_caps s" apply (simp add: unique_table_caps_def) apply (intro iff_allI) apply (clarsimp simp: null_filter_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unique_table_caps (null_filter s) = unique_table_caps s proof (prove)
goal (1 subgoal):
 1. (\<forall>p p' cap. null_filter s p = Some cap \<longrightarrow> (\<forall>cap'. null_filter s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p))) = (\<forall>p p' cap. s p = Some cap \<longrightarrow> (\<forall>cap'. s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p))) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap. (null_filter s p = Some cap \<longrightarrow> (\<forall>cap'. null_filter s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p))) = (s p = Some cap \<longrightarrow> (\<forall>cap'. s p' = Some cap' \<longrightarrow> cap_asid cap = None \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> (is_pd_cap cap \<longrightarrow> is_pd_cap cap' \<longrightarrow> p' = p) \<and> (is_pt_cap cap \<longrightarrow> is_pt_cap cap' \<longrightarrow> p' = p))) proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma unique_table_refs_null:
  "unique_table_refs (null_filter s)
       = unique_table_refs s" apply (simp only: unique_table_refs_def) apply (intro iff_allI) apply (clarsimp simp: null_filter_def) apply (auto dest!: obj_ref_none_no_asid[rule_format]
               simp: table_cap_ref_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unique_table_refs (null_filter s) = unique_table_refs s proof (prove)
goal (1 subgoal):
 1. (\<forall>p p' cap cap'. null_filter s p = Some cap \<longrightarrow> null_filter s p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) = (\<forall>p p' cap cap'. s p = Some cap \<longrightarrow> s p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap'. (null_filter s p = Some cap \<longrightarrow> null_filter s p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) = (s p = Some cap \<longrightarrow> s p' = Some cap' \<longrightarrow> obj_refs cap' = obj_refs cap \<longrightarrow> table_cap_ref cap' = table_cap_ref cap) proof (prove)
goal (1 subgoal):
 1. \<And>p p' cap cap'. (s p' = Some NullCap \<longrightarrow> s p \<noteq> Some NullCap \<longrightarrow> s p = Some cap \<longrightarrow> NullCap = cap' \<longrightarrow> {} = obj_refs cap \<longrightarrow> table_cap_ref NullCap = table_cap_ref cap) \<and> (s p' \<noteq> Some NullCap \<longrightarrow> s p = Some NullCap \<longrightarrow> NullCap = cap \<longrightarrow> s p' = Some cap' \<longrightarrow> obj_refs cap' = {} \<longrightarrow> table_cap_ref cap' = table_cap_ref NullCap) proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma default_obj_dev:
  "\<lbrakk>ty \<noteq> Untyped;default_object ty dev us = ArchObj (DataPage dev' sz)\<rbrakk> \<Longrightarrow> dev = dev'" by (clarsimp simp: default_object_def default_arch_object_def
              split: apiobject_type.split_asm aobject_type.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ty \<noteq> Untyped; default_object ty dev us = ArchObj (DataPage dev' sz)\<rbrakk> \<Longrightarrow> dev = dev'
theory ArchRetype_AI

lemma cap_range_respects_device_region_cong[cong]:
  "device_state (machine_state s) = device_state (machine_state s')
  \<Longrightarrow> cap_range_respects_device_region cap s = cap_range_respects_device_region cap s'" by (clarsimp simp: cap_range_respects_device_region_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. device_state (machine_state s) = device_state (machine_state s') \<Longrightarrow> cap_range_respects_device_region cap s = cap_range_respects_device_region cap s'
theory ArchRetype_AI

lemma valid_table_caps:
  "valid_table_caps s \<Longrightarrow> valid_table_caps s'" apply (simp add: valid_table_caps_def
              del: imp_disjL) apply (elim allEI, intro impI, simp) apply (frule caps_retype[rotated]) apply clarsimp apply (rule obj_at_pres) apply simp done

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

lemma valid_kernel_mappings:
  "valid_kernel_mappings s \<Longrightarrow> valid_kernel_mappings s'" apply (simp add: valid_kernel_mappings_def s'_def
                   ball_ran_eq ps_def) apply (simp add: default_object_def valid_kernel_mappings_if_pd_def
                   tyunt default_arch_object_def pde_ref_def
            split: Structures_A.apiobject_type.split
                   aobject_type.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_kernel_mappings s \<Longrightarrow> valid_kernel_mappings s' proof (prove)
goal (1 subgoal):
 1. \<forall>x y. kheap s x = Some y \<longrightarrow> valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) y \<Longrightarrow> (\<exists>x. x \<in> set (retype_addrs ptr ty n us)) \<longrightarrow> valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) (default_object ty dev us) proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma valid_global_vspace_mappings:
  "valid_global_vspace_mappings s
         \<Longrightarrow> valid_global_vspace_mappings s'" apply (erule valid_global_vspace_mappings_pres) apply (simp | erule obj_at_pres)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_global_vspace_mappings s \<Longrightarrow> valid_global_vspace_mappings s' proof (prove)
goal (4 subgoals):
 1. \<And>pd. ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s \<Longrightarrow> ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s'
 2. \<And>pt p. \<lbrakk>ako_at (PageTable pt) p s; valid_global_objs s \<Longrightarrow> p \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> ako_at (PageTable pt) p s'
 3. arm_global_pd (arch_state s') = arm_global_pd (arch_state s)
 4. arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s) proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma pspace_in_kernel_window:
  "\<lbrakk> pspace_in_kernel_window (s :: 'state_ext state);
     region_in_kernel_window {ptr .. (ptr &&~~ mask sz) + 2 ^ sz - 1} s \<rbrakk>
          \<Longrightarrow> pspace_in_kernel_window s'" apply (simp add: pspace_in_kernel_window_def s'_def ps_def) apply (clarsimp simp: region_in_kernel_window_def
                   del: ballI) apply (drule retype_addrs_mem_subset_ptr_bits[OF cover tyunt]) apply (fastforce simp: field_simps obj_bits_dev_irr tyunt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_in_kernel_window s; region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s\<rbrakk> \<Longrightarrow> pspace_in_kernel_window s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x ko. kheap s x = Some ko \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits ko - 1}. arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow); region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s\<rbrakk> \<Longrightarrow> \<forall>x. x \<in> set (retype_addrs ptr ty n us) \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits (default_object ty dev us) - 1}. arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x ko. kheap s x = Some ko \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits ko - 1}. arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow); \<forall>x\<in>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow; x \<in> set (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> \<forall>y\<in>{x..x + 2 ^ obj_bits (default_object ty dev us) - 1}. arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x ko. kheap s x = Some ko \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits ko - 1}. arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow); \<forall>x\<in>{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow; {x..x + (2 ^ obj_bits_api ty us - 1)} \<subseteq> up_aligned_area ptr sz\<rbrakk> \<Longrightarrow> \<forall>y\<in>{x..x + 2 ^ obj_bits (default_object ty dev us) - 1}. arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma cap_refs_respects_device_region:
  assumes psp_resp_dev: "pspace_respects_device_region s"
      and cap_refs_resp_dev: "cap_refs_respects_device_region s"
  shows "cap_refs_respects_device_region s'" using cap_refs_resp_dev apply (clarsimp simp: cap_refs_respects_device_region_def
              simp del: split_paired_All split_paired_Ex) apply (drule_tac x = "(a,b)" in spec) apply (erule notE) apply (subst(asm) cte_retype) apply (simp add: cap_range_respects_device_region_def cap_range_def) apply (clarsimp simp: cte_wp_at_caps_of_state s'_def dom_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_refs_respects_device_region s' proof (prove)
using this:
cap_refs_respects_device_region s

goal (1 subgoal):
 1. cap_refs_respects_device_region s' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>cref. \<not> cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s) cref s; cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s') (a, b) s'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s') (a, b) s'; \<not> cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s') (a, b) s' \<Longrightarrow> cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s) (a, b) s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<not> \<not> cap_range_respects_device_region NullCap s'
 2. \<And>a b. cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s') (a, b) s \<Longrightarrow> cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s') (a, b) s \<Longrightarrow> cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s) (a, b) s proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma vms:
  "valid_machine_state s \<Longrightarrow> valid_machine_state s'" apply (simp add: s'_def ps_def valid_machine_state_def in_user_frame_def) apply (rule allI, erule_tac x=p in allE, clarsimp) apply (rule_tac x=sz in exI, clarsimp simp: obj_at_def orthr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_machine_state s \<Longrightarrow> valid_machine_state s' proof (prove)
goal (1 subgoal):
 1. \<forall>p. (\<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s) \<or> underlying_memory (machine_state s) p = 0 \<Longrightarrow> \<forall>p. (\<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) (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>)) \<or> underlying_memory (machine_state s) p = 0 proof (prove)
goal (1 subgoal):
 1. \<And>p sz. \<lbrakk>underlying_memory (machine_state s) p \<noteq> 0; typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) s\<rbrakk> \<Longrightarrow> \<exists>sz. typ_at (AArch (AUserData sz)) (p && ~~ mask (pageBitsForSize sz)) (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>) proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma post_retype_invs:
  "\<lbrakk> invs s; region_in_kernel_window {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} s \<rbrakk>
        \<Longrightarrow> post_retype_invs ty (retype_addrs ptr ty n us) s'" using equal_kernel_mappings by (clarsimp simp: invs_def post_retype_invs_def valid_state_def
                     unsafe_rep2 null_filter valid_idle
                     valid_reply_caps valid_reply_masters
                     valid_global_refs valid_arch_state
                     valid_irq_node_def obj_at_pres
                     valid_arch_caps valid_global_objs
                     valid_vspace_objs' valid_irq_handlers
                     valid_mdb_rep2 mdb_and_revokable
                     valid_pspace cur_tcb only_idle
                     valid_kernel_mappings valid_asid_map
                     valid_global_vspace_mappings valid_ioc vms
                     pspace_in_kernel_window pspace_respects_device_region
                     cap_refs_respects_device_region
                     cap_refs_in_kernel_window valid_irq_states
              split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s\<rbrakk> \<Longrightarrow> post_retype_invs ty (retype_addrs ptr ty n us) s' proof (prove)
using this:
equal_kernel_mappings s \<Longrightarrow> if ty = ArchObject PageDirectoryObj then equal_kernel_mappings (s'\<lparr>kheap := kheap s' |` (- set (retype_addrs ptr ty n us))\<rparr>) else equal_kernel_mappings s'

goal (1 subgoal):
 1. \<lbrakk>invs s; region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s\<rbrakk> \<Longrightarrow> post_retype_invs ty (retype_addrs ptr ty n us) s'
theory ArchRetype_AI

lemma invs_post_retype_invs [Retype_AI_assms']:
  "invs s \<Longrightarrow> post_retype_invs ty refs s" apply (clarsimp simp: post_retype_invs_def invs_def valid_state_def) apply (clarsimp simp: equal_kernel_mappings_def obj_at_def
                        restrict_map_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> post_retype_invs ty refs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ty = ArchObject PageDirectoryObj\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := kheap s |` (- set refs)\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma retype_region_plain_invs:
  "\<lbrace>invs and caps_no_overlap ptr sz and pspace_no_overlap_range_cover ptr sz
      and caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1}
      and region_in_kernel_window {ptr .. (ptr &&~~ mask sz) + 2 ^ sz - 1}
      and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c.  {ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)} \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s)
      and K (ty = Structures_A.CapTableObject \<longrightarrow> 0 < us)
      and K (range_cover ptr sz (obj_bits_api ty us) n)
      and K (ty \<noteq> ArchObject PageDirectoryObj)\<rbrace>
      retype_region ptr n us ty dev\<lbrace>\<lambda>rv. invs\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_strengthen_post[OF retype_region_post_retype_invs]) apply (simp add: post_retype_invs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) and K (ty = CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr sz (obj_bits_api ty us) n) and K (ty \<noteq> ArchObject PageDirectoryObj)\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. ty \<noteq> ArchObject PageDirectoryObj \<Longrightarrow> \<lbrace>invs and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) and K (ty = CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr sz (obj_bits_api ty us) n)\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>ty \<noteq> ArchObject PageDirectoryObj; post_retype_invs ty rv s\<rbrakk> \<Longrightarrow> invs s proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma storeWord_um_eq_0:
  "\<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace>
    storeWord x 0
   \<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace>" by (simp add: storeWord_def word_rsplit_0 word_bits_conv | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace> storeWord x 0 \<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace>
theory ArchRetype_AI

lemma clearMemory_um_eq_0:
  "\<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace>
    clearMemory ptr bits
   \<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace>" apply (clarsimp simp: clearMemory_def) apply (wp mapM_x_wp_inv | simp)+ apply (wp hoare_drop_imps storeWord_um_eq_0) apply (fastforce simp: ignore_failure_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace> clearMemory ptr bits \<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace> do y <- mapM_x (\<lambda>p. storeWord p 0) [ptr , ptr + word_size .e. ptr + word_of_nat bits - 1];
cleanCacheRange_RAM ptr (ptr + word_of_nat bits - 1) (addrFromPPtr ptr)
od \<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>ms. underlying_memory ms p = 0\<rbrace> storeWord x 0 \<lbrace>\<lambda>y ms. underlying_memory ms p = 0\<rbrace>
 2. \<And>s. underlying_memory s p = 0 \<Longrightarrow> underlying_memory s p = 0 proof (prove)
goal (1 subgoal):
 1. \<And>s. underlying_memory s p = 0 \<Longrightarrow> underlying_memory s p = 0 proof (prove)
goal:
No subgoals!
theory ArchRetype_AI

lemma cleanCacheRange_PoU_um_inv[wp]:
  "\<lbrace>\<lambda>m. P (underlying_memory m)\<rbrace>
    cleanCacheRange_PoU ptr w p
   \<lbrace>\<lambda>_ m. P (underlying_memory m)\<rbrace>" by (simp add: cleanCacheRange_PoU_def cleanByVA_PoU_def machine_op_lift_def machine_rest_lift_def
                split_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m. P (underlying_memory m)\<rbrace> cleanCacheRange_PoU ptr w p \<lbrace>\<lambda>_ m. P (underlying_memory m)\<rbrace>
theory ArchRetype_AI

lemma invs_irq_state_independent:
  "invs (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>)
   = invs s" by (clarsimp simp: irq_state_independent_A_def invs_def
      valid_state_def valid_pspace_def valid_mdb_def valid_ioc_def valid_idle_def
      only_idle_def if_unsafe_then_cap_def valid_reply_caps_def
      valid_reply_masters_def valid_global_refs_def valid_arch_state_def
      valid_irq_node_def valid_irq_handlers_def valid_machine_state_def
      valid_arch_caps_def valid_global_objs_def
      valid_kernel_mappings_def equal_kernel_mappings_def
      valid_asid_map_def vspace_at_asid_def
      pspace_in_kernel_window_def cap_refs_in_kernel_window_def
      cur_tcb_def sym_refs_def state_refs_of_def
      swp_def valid_irq_states_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = invs s