theory CNode_DR

lemma copy_global_mappings_dwp:
  "is_aligned word pd_bits\<Longrightarrow> \<lbrace>\<lambda>ps. valid_idle (ps :: det_state) \<and> transform ps = cs\<rbrace> copy_global_mappings word \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" apply (simp add:copy_global_mappings_def) apply wp apply (rule_tac Q = "\<lambda>r s. valid_idle s \<and> transform s = cs" in hoare_strengthen_post) apply (rule mapM_x_wp') apply wp apply (rule_tac Q="\<lambda>s. valid_idle s \<and> transform s = cs" in hoare_vcg_precond_imp) apply (rule dcorres_to_wp) apply (rule corres_guard_imp[OF store_pde_set_cap_corres]) apply (clarsimp simp:kernel_mapping_slots_def) apply (simp add: kernel_base_def pd_bits_def pageBits_def) apply (simp add: mask_add_aligned) apply (subst less_mask_eq,simp) apply (simp add:shiftl_t2n) apply (subst mult.commute) apply (rule div_lt_mult,simp+,unat_arith,simp+) apply (simp add:shiftl_shiftr1 word_size) apply (subst less_mask_eq,simp) apply unat_arith apply (subst ucast_le_migrate[symmetric]) apply (simp add:word_size,unat_arith) apply (simp add:word_size)+ apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned word pd_bits \<Longrightarrow> \<lbrace>\<lambda>ps. valid_idle ps \<and> transform ps = cs\<rbrace> copy_global_mappings word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned word pd_bits \<Longrightarrow> \<lbrace>\<lambda>ps. valid_idle ps \<and> transform ps = cs\<rbrace> do global_pd <- gets (arm_global_pd \<circ> arch_state);
mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (word + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]
od \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>global_pd. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?B1 global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (word + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
 2. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?B1\<rbrace>
 3. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>global_pd. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?B1 global_pd\<rbrace> mapM_x (\<lambda>index. get_pde (global_pd + (index << 2)) >>= store_pde (word + (index << 2))) [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1] \<lbrace>\<lambda>r s. valid_idle s \<and> transform s = cs\<rbrace>
 2. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 3. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?B1\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> transform s = cs\<rbrace> get_pde (global_pd + (x << 2)) >>= store_pde (word + (x << 2)) \<lbrace>\<lambda>r s. valid_idle s \<and> transform s = cs\<rbrace>
 2. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 3. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 4. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>global_pd x xa. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?P'9 global_pd x xa\<rbrace> store_pde (word + (x << 2)) xa \<lbrace>\<lambda>rv s. transform s = cs\<rbrace>
 2. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 3. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 4. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 5. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 6. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>global_pd x xa. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. valid_idle s \<and> transform s = cs\<rbrace> store_pde (word + (x << 2)) xa \<lbrace>\<lambda>rv s. transform s = cs\<rbrace>
 2. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 3. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 4. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 5. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 6. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 7. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>global_pd x xa. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) valid_idle (return (?x13 global_pd x xa)) (store_pde (word + (x << 2)) xa)
 2. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 3. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 4. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 5. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 6. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 7. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>global_pd x xa. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (word + (x << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots
 2. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 3. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 5. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 6. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 7. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 8. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 9. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>x. \<lbrakk>is_aligned word pd_bits; kernel_base >> 20 \<le> x; x \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> UCAST(32 \<rightarrow> 12) (word + (x << 2) && mask pd_bits >> 2)
 2. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 3. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 5. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 6. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 7. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 8. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 9. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> 0xE00 \<le> UCAST(32 \<rightarrow> 12) (word + (x << 2) && mask 14 >> 2)
 2. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 3. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 5. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 6. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 7. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 8. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 9. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> 0xE00 \<le> UCAST(32 \<rightarrow> 12) ((x << 2) && mask 14 >> 2)
 2. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 3. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 5. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 6. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 7. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 8. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 9. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (10 subgoals):
 1. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> x << 2 < 0x4000
 2. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> 0xE00 \<le> UCAST(32 \<rightarrow> 12) (x << 2 >> 2)
 3. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 5. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 6. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 7. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 8. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 9. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 10. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (10 subgoals):
 1. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> 4 * x < 0x4000
 2. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> 0xE00 \<le> UCAST(32 \<rightarrow> 12) (x << 2 >> 2)
 3. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 5. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 6. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 7. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 8. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 9. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 10. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (10 subgoals):
 1. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> x * 4 < 0x4000
 2. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> 0xE00 \<le> UCAST(32 \<rightarrow> 12) (x << 2 >> 2)
 3. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 5. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 6. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 7. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 8. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 9. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 10. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> 0xE00 \<le> UCAST(32 \<rightarrow> 12) (x << 2 >> 2)
 2. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 3. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 5. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 6. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 7. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 8. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 9. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> 0xE00 \<le> UCAST(32 \<rightarrow> 12) (x && mask 30)
 2. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 3. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 5. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 6. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 7. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 8. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 9. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (10 subgoals):
 1. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> x < 0x40000000
 2. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> 0xE00 \<le> UCAST(32 \<rightarrow> 12) x
 3. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 5. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 6. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 7. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 8. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 9. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 10. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> 0xE00 \<le> UCAST(32 \<rightarrow> 12) x
 2. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 3. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 5. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 6. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 7. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 8. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 9. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (11 subgoals):
 1. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> x < 2 ^ size 0xE00
 2. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> size 0xE00 < size x
 3. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) 0xE00 \<le> x
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 5. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 6. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 7. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 8. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 9. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 10. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> size 0xE00 < size x
 2. \<And>x. \<lbrakk>is_aligned word 14; 0xE00 \<le> x; x \<le> 0xFFF\<rbrakk> \<Longrightarrow> UCAST(12 \<rightarrow> 32) 0xE00 \<le> x
 3. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; True\<rbrakk> \<Longrightarrow> True
 4. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s\<rbrakk> \<Longrightarrow> valid_idle s
 5. \<And>global_pd x xa s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; ?P'9 global_pd x xa s\<rbrakk> \<Longrightarrow> valid_idle s \<and> transform s = cs
 6. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> ?P'9 global_pd x xa s\<rbrace>
 7. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 8. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 9. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 10. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>global_pd x. \<lbrakk>is_aligned word pd_bits; kernel_base >> 20 \<le> x \<and> x \<le> 2 ^ (pd_bits - 2) - 1\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 global_pd x\<rbrace> get_pde (global_pd + (x << 2)) \<lbrace>\<lambda>xa s. valid_idle s \<and> transform s = cs\<rbrace>
 2. \<And>global_pd x s. \<lbrakk>is_aligned word pd_bits; x \<in> set [kernel_base >> 20 .e. 2 ^ (pd_bits - 2) - 1]; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q7 global_pd x s
 3. \<And>global_pd rv s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> transform s = cs
 4. is_aligned word pd_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd s. valid_idle s \<and> transform s = cs\<rbrace>
 5. \<And>s. \<lbrakk>is_aligned word pd_bits; valid_idle s \<and> transform s = cs\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!