theory VSpace_R

lemma clear_page_table_corres:
  "corres dc (pspace_aligned and page_table_at p and valid_etcbs)
             (pspace_aligned' and pspace_distinct')
    (mapM_x (swp store_pte ARM_A.InvalidPTE)
       [p , p + 4 .e. p + 2 ^ ptBits - 1])
    (mapM_x (swp storePTE ARM_H.InvalidPTE)
       [p , p + 4 .e. p + 2 ^ ptBits - 1])" apply (rule_tac F="is_aligned p ptBits" in corres_req) apply (clarsimp simp: obj_at_def a_type_def) apply (clarsimp split: Structures_A.kernel_object.split_asm if_split_asm
                          arch_kernel_obj.split_asm) apply (drule(1) pspace_alignedD) apply (simp add: ptBits_def pageBits_def pteBits_def) apply (simp add: upto_enum_step_subtract[where x=p and y="p + 4"]
                   is_aligned_no_overflow pt_bits_stuff
                   upto_enum_step_red[where us=2, simplified]
                   mapM_x_mapM liftM_def[symmetric]) apply (rule corres_guard_imp,
         rule_tac r'=dc and S="(=)"
               and Q="\<lambda>xs s. \<forall>x \<in> set xs. pte_at x s \<and> pspace_aligned s \<and> valid_etcbs s"
               and Q'="\<lambda>xs. pspace_aligned' and pspace_distinct'"
                in corres_mapM_list_all2, simp_all) apply (rule corres_guard_imp, rule storePTE_corres') apply (simp add:pte_relation_aligned_def)+ apply (wp hoare_vcg_const_Ball_lift | simp)+ apply (simp add: list_all2_refl) apply (clarsimp simp: upto_enum_step_def) apply (erule page_table_pte_atI[simplified shiftl_t2n mult.commute, simplified]) apply (simp add: ptBits_def pageBits_def pt_bits_def word_less_nat_alt word_le_nat_alt unat_of_nat
                    pteBits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (pspace_aligned and typ_at (AArch APageTable) p and valid_etcbs) (pspace_aligned' and pspace_distinct') (mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) (mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> state_relation; (pspace_aligned and typ_at (AArch APageTable) p and valid_etcbs) s; (pspace_aligned' and pspace_distinct') s'\<rbrakk> \<Longrightarrow> is_aligned p ptBits
 2. is_aligned p ptBits \<Longrightarrow> corres dc (pspace_aligned and typ_at (AArch APageTable) p and valid_etcbs) (pspace_aligned' and pspace_distinct') (mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) (mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) proof (prove)
goal (2 subgoals):
 1. \<And>s s' ko. \<lbrakk>(s, s') \<in> state_relation; pspace_aligned s; pspace_aligned' s'; pspace_distinct' s'; valid_etcbs s; kheap s p = Some ko; (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 arch_kernel_obj.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 APageTable\<rbrakk> \<Longrightarrow> is_aligned p ptBits
 2. is_aligned p ptBits \<Longrightarrow> corres dc (pspace_aligned and typ_at (AArch APageTable) p and valid_etcbs) (pspace_aligned' and pspace_distinct') (mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) (mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) proof (prove)
goal (2 subgoals):
 1. \<And>s s' x2. \<lbrakk>(s, s') \<in> state_relation; pspace_aligned s; pspace_aligned' s'; pspace_distinct' s'; valid_etcbs s; kheap s p = Some (ArchObj (PageTable x2))\<rbrakk> \<Longrightarrow> is_aligned p ptBits
 2. is_aligned p ptBits \<Longrightarrow> corres dc (pspace_aligned and typ_at (AArch APageTable) p and valid_etcbs) (pspace_aligned' and pspace_distinct') (mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) (mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) proof (prove)
goal (2 subgoals):
 1. \<And>s s' x2. \<lbrakk>(s, s') \<in> state_relation; pspace_aligned s; pspace_aligned' s'; pspace_distinct' s'; valid_etcbs s; is_aligned p (obj_bits (ArchObj (PageTable x2)))\<rbrakk> \<Longrightarrow> is_aligned p ptBits
 2. is_aligned p ptBits \<Longrightarrow> corres dc (pspace_aligned and typ_at (AArch APageTable) p and valid_etcbs) (pspace_aligned' and pspace_distinct') (mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) (mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) proof (prove)
goal (1 subgoal):
 1. is_aligned p ptBits \<Longrightarrow> corres dc (pspace_aligned and typ_at (AArch APageTable) p and valid_etcbs) (pspace_aligned' and pspace_distinct') (mapM_x (swp store_pte ARM_A.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) (mapM_x (swp storePTE ARM_H.InvalidPTE) [p , p + 4 .e. p + 2 ^ ptBits - 1]) proof (prove)
goal (1 subgoal):
 1. is_aligned p ptBits \<Longrightarrow> corres dc (pspace_aligned and typ_at (AArch APageTable) p and valid_etcbs) (pspace_aligned' and pspace_distinct') (mapM (swp store_pte ARM_A.InvalidPTE) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1])) (mapM (swp storePTE ARM_H.InvalidPTE) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1])) proof (prove)
goal (5 subgoals):
 1. \<And>x xs y ys. \<lbrakk>is_aligned p ptBits; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. pte_at y s \<and> pspace_aligned s \<and> valid_etcbs s \<and> (\<forall>x\<in>set xs. pte_at x s \<and> pspace_aligned s \<and> valid_etcbs s)) (pspace_aligned' and pspace_distinct') (store_pte y ARM_A.InvalidPTE) (storePTE y ARM_H.InvalidPTE)
 2. \<And>x xs y. \<lbrakk>is_aligned p ptBits; x = y; suffix (y # xs) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pte_at y s \<and> pspace_aligned s \<and> valid_etcbs s \<and> (\<forall>x\<in>set xs. pte_at x s \<and> pspace_aligned s \<and> valid_etcbs s)\<rbrace> store_pte y ARM_A.InvalidPTE \<lbrace>\<lambda>r s. \<forall>x\<in>set xs. pte_at x s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace>
 3. \<And>x y ys. \<lbrakk>is_aligned p ptBits; x = y; suffix (y # ys) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> storePTE y ARM_H.InvalidPTE \<lbrace>\<lambda>r. pspace_aligned' and pspace_distinct'\<rbrace>
 4. is_aligned p ptBits \<Longrightarrow> list_all2 (=) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1]) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1])
 5. \<And>s. \<lbrakk>is_aligned p ptBits; pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [0 , 4 .e. 2 ^ ptBits - 1]. pte_at (p + x) s proof (prove)
goal (7 subgoals):
 1. \<And>x xs y ys. \<lbrakk>is_aligned p ptBits; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> pte_relation_aligned (y >> 2) ARM_A.InvalidPTE ARM_H.InvalidPTE
 2. \<And>x xs y ys s. \<lbrakk>is_aligned p ptBits; x = y; list_all2 (=) xs ys; pte_at y s \<and> pspace_aligned s \<and> valid_etcbs s \<and> (\<forall>x\<in>set xs. pte_at x s \<and> pspace_aligned s \<and> valid_etcbs s)\<rbrakk> \<Longrightarrow> (pte_at y and pspace_aligned and valid_etcbs) s
 3. \<And>x xs y ys s. \<lbrakk>is_aligned p ptBits; x = y; list_all2 (=) xs ys; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct') s
 4. \<And>x xs y. \<lbrakk>is_aligned p ptBits; x = y; suffix (y # xs) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pte_at y s \<and> pspace_aligned s \<and> valid_etcbs s \<and> (\<forall>x\<in>set xs. pte_at x s \<and> pspace_aligned s \<and> valid_etcbs s)\<rbrace> store_pte y ARM_A.InvalidPTE \<lbrace>\<lambda>r s. \<forall>x\<in>set xs. pte_at x s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace>
 5. \<And>x y ys. \<lbrakk>is_aligned p ptBits; x = y; suffix (y # ys) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> storePTE y ARM_H.InvalidPTE \<lbrace>\<lambda>r. pspace_aligned' and pspace_distinct'\<rbrace>
 6. is_aligned p ptBits \<Longrightarrow> list_all2 (=) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1]) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1])
 7. \<And>s. \<lbrakk>is_aligned p ptBits; pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [0 , 4 .e. 2 ^ ptBits - 1]. pte_at (p + x) s proof (prove)
goal (4 subgoals):
 1. \<And>x xs y. \<lbrakk>is_aligned p ptBits; x = y; suffix (y # xs) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pte_at y s \<and> pspace_aligned s \<and> valid_etcbs s \<and> (\<forall>x\<in>set xs. pte_at x s \<and> pspace_aligned s \<and> valid_etcbs s)\<rbrace> store_pte y ARM_A.InvalidPTE \<lbrace>\<lambda>r s. \<forall>x\<in>set xs. pte_at x s \<and> pspace_aligned s \<and> valid_etcbs s\<rbrace>
 2. \<And>x y ys. \<lbrakk>is_aligned p ptBits; x = y; suffix (y # ys) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1])\<rbrakk> \<Longrightarrow> \<lbrace>pspace_aligned' and pspace_distinct'\<rbrace> storePTE y ARM_H.InvalidPTE \<lbrace>\<lambda>r. pspace_aligned' and pspace_distinct'\<rbrace>
 3. is_aligned p ptBits \<Longrightarrow> list_all2 (=) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1]) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1])
 4. \<And>s. \<lbrakk>is_aligned p ptBits; pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [0 , 4 .e. 2 ^ ptBits - 1]. pte_at (p + x) s proof (prove)
goal (2 subgoals):
 1. is_aligned p ptBits \<Longrightarrow> list_all2 (=) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1]) (map ((+) p) [0 , 4 .e. 2 ^ ptBits - 1])
 2. \<And>s. \<lbrakk>is_aligned p ptBits; pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [0 , 4 .e. 2 ^ ptBits - 1]. pte_at (p + x) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned p ptBits; pspace_aligned s \<and> typ_at (AArch APageTable) p s \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [0 , 4 .e. 2 ^ ptBits - 1]. pte_at (p + x) s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>is_aligned p ptBits; pspace_aligned s; typ_at (AArch APageTable) p s; valid_etcbs s; x \<le> (2 ^ ptBits - 1) div 4\<rbrakk> \<Longrightarrow> pte_at (p + x * 4) s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned p ptBits; pspace_aligned s; valid_etcbs s; x \<le> (2 ^ ptBits - 1) div 4\<rbrakk> \<Longrightarrow> x < 2 ^ (pt_bits - 2)
 2. \<And>s x. \<lbrakk>is_aligned p ptBits; pspace_aligned s; valid_etcbs s; x \<le> (2 ^ ptBits - 1) div 4\<rbrakk> \<Longrightarrow> pspace_aligned s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>is_aligned p ptBits; pspace_aligned s; valid_etcbs s; x \<le> (2 ^ ptBits - 1) div 4\<rbrakk> \<Longrightarrow> pspace_aligned s proof (prove)
goal:
No subgoals!