theory Retype_R

lemma createObjects_valid_arch:
  "\<lbrace>\<lambda>s. valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and>
        pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<rbrace>
      createObjects ptr n val gbits
   \<lbrace>\<lambda>rv s. valid_arch_state' s\<rbrace>" apply (simp add: valid_arch_state'_def valid_asid_table'_def
                   page_directory_at'_def valid_global_pts'_def
                   page_table_at'_def) apply (rule hoare_pre) apply (rule hoare_use_eq [where f=ksArchState, OF createObjects_ksArch]) apply (simp add: createObjects_def) apply (wp createObjects'_typ_at hoare_vcg_all_lift hoare_vcg_const_imp_lift
              hoare_vcg_const_Ball_lift) apply (simp add: o_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. pte_at' (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. pte_at' (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q8\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. pte_at' (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s))\<rbrace>
 2. \<And>s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. pte_at' (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<Longrightarrow> ?Q8 s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P11 f\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv s. dom (armKSASIDTable f) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable f) \<and> is_aligned (armKSGlobalPD f) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD f + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs f). is_aligned p ptBits \<and> (\<forall>y<0x100. pte_at' (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable f) (map_option fst \<circ> armKSASIDMap f) \<and> valid_asid_map' (armKSASIDMap f)\<rbrace>
 2. \<And>s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. pte_at' (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<Longrightarrow> ?P11 (ksArchState s) s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P11 f\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>rv s. dom (armKSASIDTable f) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable f) \<and> is_aligned (armKSGlobalPD f) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD f + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs f). is_aligned p ptBits \<and> (\<forall>y<0x100. pte_at' (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable f) (\<lambda>a. map_option fst (armKSASIDMap f a)) \<and> valid_asid_map' (armKSASIDMap f)\<rbrace>
 2. \<And>s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. pte_at' (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<Longrightarrow> ?P11 (ksArchState s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. pte_at' (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<Longrightarrow> dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>x<0x1000. n \<noteq> 0 \<and> range_cover ptr (?sz40 (ksArchState s) x) (objBitsKO val + gbits) n \<and> pde_at' (armKSGlobalPD (ksArchState s) + (x << 2)) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz40 (ksArchState s) x) s) \<and> (\<forall>x\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned x ptBits \<and> (\<forall>xa<0x100. n \<noteq> 0 \<and> range_cover ptr (?sz47 (ksArchState s) x xa) (objBitsKO val + gbits) n \<and> pte_at' (x + (xa << 2)) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz47 (ksArchState s) x xa) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (\<lambda>a. map_option fst (armKSASIDMap (ksArchState s) a)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. pte_at' (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (\<lambda>x. map_option fst (armKSASIDMap (ksArchState s) x)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<Longrightarrow> (\<forall>x<0x1000. range_cover ptr (?sz40 (ksArchState s) x) (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr (?sz40 (ksArchState s) x) s) \<and> (\<forall>x\<in>set (armKSGlobalPTs (ksArchState s)). \<forall>xa<0x100. range_cover ptr (?sz47 (ksArchState s) x xa) (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr (?sz47 (ksArchState s) x xa) s) proof (prove)
goal:
No subgoals!