theory ArchRetype_IF

lemma copy_global_mappings_globals_equiv:
  "\<lbrace>globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace>
   copy_global_mappings x
   \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding copy_global_mappings_def including no_pre apply simp apply wp apply (rule_tac Q="\<lambda>_. globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and>
                                                   is_aligned x pd_bits)" in hoare_strengthen_post) apply (wp mapM_x_wp[OF _ subset_refl] store_pde_globals_equiv) apply (fastforce dest: subsetD[OF copy_global_mappings_index_subset] simp: pd_shifting') apply (simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace> copy_global_mappings x \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace> do global_pd <- gets (arm_global_pd \<circ> arch_state);
pde_bits <- return 2;
pd_size <- return (1 << pd_bits - pde_bits);
mapM_x (\<lambda>index. do offset <- return (index << pde_bits);
get_pde (global_pd + offset) >>= store_pde (x + offset)
od) [kernel_base >> 20 .e. pd_size - 1]
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace> do global_pd <- gets (arm_global_pd \<circ> arch_state);
pde_bits <- return 2;
pd_size <- return (1 << pd_bits - pde_bits);
mapM_x (\<lambda>index. do offset <- return (index << pde_bits);
get_pde (global_pd + offset) >>= store_pde (x + offset)
od) [kernel_base >> 20 .e. pd_size - 1]
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace> do global_pd <- gets (arm_global_pd \<circ> arch_state);
mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (x + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>global_pd. \<lbrace>?B global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (x + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<lbrace>globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>global_pd. \<lbrace>?B global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (x + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>\<lambda>_. globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace>
 2. \<And>global_pd rv sa. (globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)) sa \<Longrightarrow> globals_equiv s sa
 3. \<lbrace>globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?B\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>global_pd xa sa. \<lbrakk>xa \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; (globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)) sa\<rbrakk> \<Longrightarrow> (globals_equiv s and (\<lambda>s. x + (xa << 2) && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s))) sa \<and> x \<noteq> arm_global_pd (arch_state sa) \<and> is_aligned x pd_bits
 2. \<And>global_pd rv sa. (globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)) sa \<Longrightarrow> globals_equiv s sa
 3. \<lbrace>globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>global_pd rv sa. (globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)) sa \<Longrightarrow> globals_equiv s sa
 2. \<lbrace>globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd. globals_equiv s and (\<lambda>s. x \<noteq> arm_global_pd (arch_state s) \<and> is_aligned x pd_bits)\<rbrace> proof (prove)
goal:
No subgoals!