theory VSpace_R

lemma storePDE_pde_mappings'[wp]:
  "\<lbrace>valid_pde_mappings' and K (valid_pde_mapping' (p && mask pdBits) pde)\<rbrace>
      storePDE p pde
   \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>" apply (rule hoare_gen_asm) apply (wp valid_pde_mappings_lift') apply (rule hoare_post_imp) apply (simp only: obj_at'_real_def) apply (simp add: storePDE_def) apply (wp setObject_ko_wp_at) apply simp apply (simp add: objBits_simps archObjSize_def) apply (simp add: pdeBits_def) apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde_mappings' and K (valid_pde_mapping' (p && mask pdBits) pde)\<rbrace> storePDE p pde \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (1 subgoal):
 1. valid_pde_mapping' (p && mask pdBits) pde \<Longrightarrow> \<lbrace>valid_pde_mappings'\<rbrace> storePDE p pde \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. valid_pde_mapping' (p && mask pdBits) pde \<Longrightarrow> \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> storePDE p pde \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace>
 2. \<And>s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; valid_pde_mappings' s\<rbrakk> \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (3 subgoals):
 1. \<And>x rv s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; ?Q6 x rv s\<rbrakk> \<Longrightarrow> obj_at' (valid_pde_mapping' (x && mask pdBits)) x s
 2. \<And>x. valid_pde_mapping' (p && mask pdBits) pde \<Longrightarrow> \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> storePDE p pde \<lbrace>?Q6 x\<rbrace>
 3. \<And>s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; valid_pde_mappings' s\<rbrakk> \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (2 subgoals):
 1. \<And>x. valid_pde_mapping' (p && mask pdBits) pde \<Longrightarrow> \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> storePDE p pde \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> valid_pde_mapping' (x && mask pdBits) obj) x\<rbrace>
 2. \<And>s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; valid_pde_mappings' s\<rbrakk> \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (2 subgoals):
 1. \<And>x. valid_pde_mapping' (p && mask pdBits) pde \<Longrightarrow> \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> setObject p pde \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> valid_pde_mapping' (x && mask pdBits) obj) x\<rbrace>
 2. \<And>s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; valid_pde_mappings' s\<rbrakk> \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (5 subgoals):
 1. \<And>x ko s xa y n. valid_pde_mapping' (p && mask pdBits) pde \<Longrightarrow> updateObject pde ko p y n s = updateObject_default pde ko p y n s
 2. \<And>x v'. valid_pde_mapping' (p && mask pdBits) pde \<Longrightarrow> objBits v' = ?n11 x
 3. \<And>x. valid_pde_mapping' (p && mask pdBits) pde \<Longrightarrow> 1 < 2 ^ ?n11 x
 4. \<And>x s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; obj_at' (valid_pde_mapping' (x && mask pdBits)) x s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. True) p s \<longrightarrow> ko_wp_at' (if p = x then K (\<exists>obj. projectKO_opt (injectKO pde) = Some obj \<and> valid_pde_mapping' (x && mask pdBits) obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> valid_pde_mapping' (x && mask pdBits) obj)) x s
 5. \<And>s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; valid_pde_mappings' s\<rbrakk> \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (4 subgoals):
 1. \<And>x v'. valid_pde_mapping' (p && mask pdBits) pde \<Longrightarrow> objBits v' = ?n11 x
 2. \<And>x. valid_pde_mapping' (p && mask pdBits) pde \<Longrightarrow> 1 < 2 ^ ?n11 x
 3. \<And>x s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; obj_at' (valid_pde_mapping' (x && mask pdBits)) x s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. True) p s \<longrightarrow> ko_wp_at' (if p = x then K (\<exists>obj. projectKO_opt (injectKO pde) = Some obj \<and> valid_pde_mapping' (x && mask pdBits) obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> valid_pde_mapping' (x && mask pdBits) obj)) x s
 4. \<And>s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; valid_pde_mappings' s\<rbrakk> \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (3 subgoals):
 1. \<And>x. valid_pde_mapping' (p && mask pdBits) pde \<Longrightarrow> 1 < 2 ^ pdeBits
 2. \<And>x s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; obj_at' (valid_pde_mapping' (x && mask pdBits)) x s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. True) p s \<longrightarrow> ko_wp_at' (if p = x then K (\<exists>obj. projectKO_opt (injectKO pde) = Some obj \<and> valid_pde_mapping' (x && mask pdBits) obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> valid_pde_mapping' (x && mask pdBits) obj)) x s
 3. \<And>s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; valid_pde_mappings' s\<rbrakk> \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; obj_at' (valid_pde_mapping' (x && mask pdBits)) x s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>x. True) p s \<longrightarrow> ko_wp_at' (if p = x then K (\<exists>obj. projectKO_opt (injectKO pde) = Some obj \<and> valid_pde_mapping' (x && mask pdBits) obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> valid_pde_mapping' (x && mask pdBits) obj)) x s
 2. \<And>s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; valid_pde_mappings' s\<rbrakk> \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pde_mapping' (p && mask pdBits) pde; valid_pde_mappings' s\<rbrakk> \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal:
No subgoals!