theory ArchRetype_IF

lemma copy_global_mappings_reads_respects_g:
  "is_aligned x pd_bits
   \<Longrightarrow> reads_respects_g aag l (\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s)
                                 \<and> pspace_aligned s \<and> valid_arch_state s)
                        (copy_global_mappings x)" unfolding copy_global_mappings_def apply simp apply (rule bind_ev_pre) prefer 3 apply (rule_tac Q="\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and>
                            pspace_aligned s \<and> valid_arch_state s" in hoare_weaken_pre) apply (rule gets_sp) apply (assumption) apply (wp mapM_x_ev store_pde_reads_respects_g get_pde_revg) apply (drule subsetD[OF copy_global_mappings_index_subset]) apply (clarsimp simp: pd_shifting' invs_aligned_pdD) apply (wp get_pde_inv store_pde_aligned store_pde_valid_arch | simp | fastforce)+ apply (fastforce dest: reads_equiv_gD simp: globals_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) (copy_global_mappings x) proof (prove)
goal (1 subgoal):
 1. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) (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) proof (prove)
goal (1 subgoal):
 1. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) (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) proof (prove)
goal (4 subgoals):
 1. \<And>rv. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?Q rv) (mapM_x (\<lambda>index. get_pde (rv + (index << 2)) >>= store_pde (x + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1])
 2. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets (arm_global_pd \<circ> arch_state))
 3. is_aligned x pd_bits \<Longrightarrow> \<lbrace>?P''\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?Q\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned x pd_bits; is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s\<rbrakk> \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (4 subgoals):
 1. is_aligned x pd_bits \<Longrightarrow> \<lbrace>?P''\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?Q\<rbrace>
 2. \<And>rv. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?Q rv) (mapM_x (\<lambda>index. get_pde (rv + (index << 2)) >>= store_pde (x + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1])
 3. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets (arm_global_pd \<circ> arch_state))
 4. \<And>s. \<lbrakk>is_aligned x pd_bits; is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s\<rbrakk> \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (5 subgoals):
 1. is_aligned x pd_bits \<Longrightarrow> \<lbrace>\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?Q\<rbrace>
 2. \<And>s. \<lbrakk>is_aligned x pd_bits; ?P'' s\<rbrakk> \<Longrightarrow> is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s
 3. \<And>rv. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag (?Q rv) (mapM_x (\<lambda>index. get_pde (rv + (index << 2)) >>= store_pde (x + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1])
 4. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets (arm_global_pd \<circ> arch_state))
 5. \<And>s. \<lbrakk>is_aligned x pd_bits; is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s\<rbrakk> \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>is_aligned x pd_bits; ?P'' s\<rbrakk> \<Longrightarrow> is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s
 2. \<And>rv. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = rv)) (mapM_x (\<lambda>index. get_pde (rv + (index << 2)) >>= store_pde (x + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1])
 3. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets (arm_global_pd \<circ> arch_state))
 4. \<And>s. \<lbrakk>is_aligned x pd_bits; is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s\<rbrakk> \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<And>rv. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = rv)) (mapM_x (\<lambda>index. get_pde (rv + (index << 2)) >>= store_pde (x + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1])
 2. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets (arm_global_pd \<circ> arch_state))
 3. \<And>s. \<lbrakk>is_aligned x pd_bits; is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s\<rbrakk> \<Longrightarrow> ?P' s \<and> is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s proof (prove)
goal (4 subgoals):
 1. \<And>rv xa s. \<lbrakk>is_aligned x pd_bits; xa \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ((\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = rv)) s\<rbrakk> \<Longrightarrow> rv + (xa << 2) && ~~ mask pd_bits = arm_global_pd (arch_state s) \<and> is_subject aag (x + (xa << 2) && ~~ mask pd_bits) \<and> x + (xa << 2) && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)
 2. \<And>rv xa. \<lbrakk>is_aligned x pd_bits; xa \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = rv)\<rbrace> get_pde (rv + (xa << 2)) >>= store_pde (x + (xa << 2)) \<lbrace>\<lambda>_. (\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = rv)\<rbrace>
 3. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets (arm_global_pd \<circ> arch_state))
 4. \<And>s. \<lbrakk>is_aligned x pd_bits; is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s\<rbrakk> \<Longrightarrow> ?P' s \<and> is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s proof (prove)
goal (4 subgoals):
 1. \<And>rv xa s. \<lbrakk>is_aligned x pd_bits; ((\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = rv)) s; xa \<in> {x. \<exists>y. x = y >> 20}\<rbrakk> \<Longrightarrow> rv + (xa << 2) && ~~ mask pd_bits = arm_global_pd (arch_state s) \<and> is_subject aag (x + (xa << 2) && ~~ mask pd_bits) \<and> x + (xa << 2) && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)
 2. \<And>rv xa. \<lbrakk>is_aligned x pd_bits; xa \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = rv)\<rbrace> get_pde (rv + (xa << 2)) >>= store_pde (x + (xa << 2)) \<lbrace>\<lambda>_. (\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = rv)\<rbrace>
 3. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets (arm_global_pd \<circ> arch_state))
 4. \<And>s. \<lbrakk>is_aligned x pd_bits; is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s\<rbrakk> \<Longrightarrow> ?P' s \<and> is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s proof (prove)
goal (3 subgoals):
 1. \<And>rv xa. \<lbrakk>is_aligned x pd_bits; xa \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = rv)\<rbrace> get_pde (rv + (xa << 2)) >>= store_pde (x + (xa << 2)) \<lbrace>\<lambda>_. (\<lambda>s. is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s) and (\<lambda>s. (arm_global_pd \<circ> arch_state) s = rv)\<rbrace>
 2. is_aligned x pd_bits \<Longrightarrow> reads_equiv_valid_g_inv (affects_equiv aag l) aag ?P' (gets (arm_global_pd \<circ> arch_state))
 3. \<And>s. \<lbrakk>is_aligned x pd_bits; is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s\<rbrakk> \<Longrightarrow> ?P' s \<and> is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned x pd_bits; is_subject aag x \<and> x \<noteq> arm_global_pd (arch_state s) \<and> pspace_aligned s \<and> valid_arch_state s\<rbrakk> \<Longrightarrow> \<forall>s t. reads_equiv_g aag s t \<and> affects_equiv aag l s t \<longrightarrow> arm_global_pd (arch_state s) = arm_global_pd (arch_state t) proof (prove)
goal:
No subgoals!