theory Retype_R

lemma createObjects'_pde_mappings'[wp]:
  "\<lbrace>\<lambda>s. valid_pde_mappings' s \<and> range_cover ptr sz (objBitsKO val + gbits) n  \<and> n \<noteq> 0
            \<and> pspace_aligned' s \<and> pspace_distinct' s
            \<and> pspace_no_overlap' ptr sz s
            \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = InvalidPDE)\<rbrace>
       createObjects' ptr n val gbits
   \<lbrace>\<lambda>_. valid_pde_mappings'\<rbrace>" apply (simp only: valid_pde_mappings'_def3 all_simps(1)[symmetric]) apply (rule hoare_vcg_all_lift) apply (wp createObjects_orig_obj_at2') apply (clarsimp simp: projectKO_opt_pde o_def
                 split: Structures_H.kernel_object.split_asm
                        arch_kernel_object.split_asm) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pde_mappings' s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>_. valid_pde_mappings'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x. \<not> obj_at' (Not \<circ> valid_pde_mapping' (x && mask pdBits)) x s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>_ s. \<forall>x. \<not> obj_at' (Not \<circ> valid_pde_mapping' (x && mask pdBits)) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. \<not> obj_at' (Not \<circ> valid_pde_mapping' (x && mask pdBits)) x s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE)\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv s. \<not> obj_at' (Not \<circ> valid_pde_mapping' (x && mask pdBits)) x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x s. \<not> obj_at' (Not \<circ> valid_pde_mapping' (x && mask pdBits)) x s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>pde. projectKO_opt val = Some pde \<longrightarrow> pde = ARM_H.InvalidPDE) \<Longrightarrow> n \<noteq> 0 \<and> range_cover ptr (?sz4 x) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> obj_at' (Not \<circ> valid_pde_mapping' (x && mask pdBits)) x s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> (Not \<circ> valid_pde_mapping' (x && mask pdBits)) a) \<and> pspace_no_overlap' ptr (?sz4 x) s proof (prove)
goal (10 subgoals):
 1. \<And>x s x1. \<lbrakk>val = KOEndpoint x1; \<not> obj_at' (\<lambda>xa. \<not> valid_pde_mapping' (x && mask pdBits) xa) x s; range_cover ptr sz (objBitsKO (KOEndpoint x1) + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz4 x) (objBitsKO (KOEndpoint x1) + gbits) n \<and> pspace_no_overlap' ptr (?sz4 x) s
 2. \<And>x s x2. \<lbrakk>val = KONotification x2; \<not> obj_at' (\<lambda>xa. \<not> valid_pde_mapping' (x && mask pdBits) xa) x s; range_cover ptr sz (objBitsKO (KONotification x2) + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz4 x) (objBitsKO (KONotification x2) + gbits) n \<and> pspace_no_overlap' ptr (?sz4 x) s
 3. \<And>x s. \<lbrakk>val = KOKernelData; \<not> obj_at' (\<lambda>xa. \<not> valid_pde_mapping' (x && mask pdBits) xa) x s; range_cover ptr sz (objBitsKO KOKernelData + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz4 x) (objBitsKO KOKernelData + gbits) n \<and> pspace_no_overlap' ptr (?sz4 x) s
 4. \<And>x s. \<lbrakk>val = KOUserData; \<not> obj_at' (\<lambda>xa. \<not> valid_pde_mapping' (x && mask pdBits) xa) x s; range_cover ptr sz (objBitsKO KOUserData + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz4 x) (objBitsKO KOUserData + gbits) n \<and> pspace_no_overlap' ptr (?sz4 x) s
 5. \<And>x s. \<lbrakk>val = KOUserDataDevice; \<not> obj_at' (\<lambda>xa. \<not> valid_pde_mapping' (x && mask pdBits) xa) x s; range_cover ptr sz (objBitsKO KOUserDataDevice + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz4 x) (objBitsKO KOUserDataDevice + gbits) n \<and> pspace_no_overlap' ptr (?sz4 x) s
 6. \<And>x s x6. \<lbrakk>val = KOTCB x6; \<not> obj_at' (\<lambda>xa. \<not> valid_pde_mapping' (x && mask pdBits) xa) x s; range_cover ptr sz (objBitsKO (KOTCB x6) + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz4 x) (objBitsKO (KOTCB x6) + gbits) n \<and> pspace_no_overlap' ptr (?sz4 x) s
 7. \<And>x s x7. \<lbrakk>val = KOCTE x7; \<not> obj_at' (\<lambda>xa. \<not> valid_pde_mapping' (x && mask pdBits) xa) x s; range_cover ptr sz (objBitsKO (KOCTE x7) + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz4 x) (objBitsKO (KOCTE x7) + gbits) n \<and> pspace_no_overlap' ptr (?sz4 x) s
 8. \<And>x s x1. \<lbrakk>val = KOArch (KOASIDPool x1); \<not> obj_at' (\<lambda>xa. \<not> valid_pde_mapping' (x && mask pdBits) xa) x s; range_cover ptr sz (objBitsKO (KOArch (KOASIDPool x1)) + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz4 x) (objBitsKO (KOArch (KOASIDPool x1)) + gbits) n \<and> pspace_no_overlap' ptr (?sz4 x) s
 9. \<And>x s x2. \<lbrakk>val = KOArch (KOPTE x2); \<not> obj_at' (\<lambda>xa. \<not> valid_pde_mapping' (x && mask pdBits) xa) x s; range_cover ptr sz (objBitsKO (KOArch (KOPTE x2)) + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz4 x) (objBitsKO (KOArch (KOPTE x2)) + gbits) n \<and> pspace_no_overlap' ptr (?sz4 x) s
 10. \<And>x s. \<lbrakk>val = KOArch (KOPDE ARM_H.InvalidPDE); \<not> obj_at' (\<lambda>xa. \<not> valid_pde_mapping' (x && mask pdBits) xa) x s; range_cover ptr sz (objBitsKO (KOArch (KOPDE ARM_H.InvalidPDE)) + gbits) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz4 x) (objBitsKO (KOArch (KOPDE ARM_H.InvalidPDE)) + gbits) n \<and> pspace_no_overlap' ptr (?sz4 x) s proof (prove)
goal:
No subgoals!