theory ArchUserOp_IF

lemma requiv_ptable_lift_eq:
  "\<lbrakk> reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s;
     invs s'; is_subject aag (cur_thread s); ptable_rights_s s x \<noteq> {} \<rbrakk>
     \<Longrightarrow> ptable_lift_s s x = ptable_lift_s s' x" apply (simp add: ptable_lift_s_def ptable_rights_s_def) apply (case_tac "x \<in> kernel_mappings") apply (clarsimp simp: ptable_lift_def split: option.splits) apply (rule conjI) apply clarsimp apply (frule some_get_page_info_kmapsD) apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
                               vspace_cap_rights_to_auth_def ptable_rights_def)+)[4] apply clarsimp apply (frule some_get_page_info_kmapsD) apply ((fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
                              vspace_cap_rights_to_auth_def ptable_rights_def)+)[4] apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) =
                   arm_global_pd (arch_state s)") apply (frule requiv_pd_of_thread_global_pd) apply (fastforce+)[4] apply (clarsimp simp: ptable_lift_def split: option.splits) apply (rule conjI) apply clarsimp apply (frule get_page_info_gpd_kmaps[rotated, rotated]) apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] apply clarsimp apply (rule conjI) apply (frule get_page_info_gpd_kmaps[rotated, rotated]) apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] apply clarsimp apply (frule get_page_info_gpd_kmaps[rotated, rotated]) apply ((fastforce simp: invs_valid_global_objs invs_arch_state)+)[3] apply (case_tac "get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') =
                   arm_global_pd (arch_state s')") apply (drule reads_equiv_sym) apply (frule requiv_pd_of_thread_global_pd) apply ((fastforce simp: reads_equiv_def)+)[5] apply (simp add: ptable_lift_def) apply (frule requiv_get_pd_of_thread_eq, simp+)[1] apply (frule pd_of_thread_same_agent, simp+)[1] apply (subst requiv_get_page_info_eq, simp+)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights_s s x \<noteq> {}\<rbrakk> \<Longrightarrow> ptable_lift_s s x = ptable_lift_s s' x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None \<longrightarrow> (\<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x \<noteq> Some (a, aa, ab, b))) \<and> (\<forall>a aa. (\<exists>ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)) \<longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac)))
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None \<longrightarrow> (\<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x \<noteq> Some (a, aa, ab, b))
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> \<forall>a aa. (\<exists>ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)) \<longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac))
 3. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (3 subgoals):
 1. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> \<forall>a aa. (\<exists>ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)) \<longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac))
 3. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (6 subgoals):
 1. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> x \<in> kernel_mappings
 2. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> valid_global_vspace_mappings s'
 3. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> equal_kernel_mappings s'
 4. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b); (\<exists>sz. pageBitsForSize sz = aa) \<and> b = {}\<rbrakk> \<Longrightarrow> False
 5. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> \<forall>a aa. (\<exists>ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)) \<longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac))
 6. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> \<forall>a aa. (\<exists>ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)) \<longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac))
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac))
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (5 subgoals):
 1. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> x \<in> kernel_mappings
 2. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> valid_global_vspace_mappings s
 3. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> equal_kernel_mappings s
 4. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<in> kernel_mappings; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x = Some (a, aa, ab, b); (\<exists>sz. pageBitsForSize sz = aa) \<and> b = {}\<rbrakk> \<Longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac))
 5. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (6 subgoals):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> is_subject aag (cur_thread s)
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> invs s
 3. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> pas_refined aag s
 4. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)
 5. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x
 6. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> (get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = None \<longrightarrow> (\<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x \<noteq> Some (a, aa, ab, b))) \<and> (\<forall>a aa. (\<exists>ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)) \<longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac)))
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = None \<longrightarrow> (\<forall>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x \<noteq> Some (a, aa, ab, b))
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> \<forall>a aa. (\<exists>ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)) \<longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac))
 3. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (3 subgoals):
 1. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> \<forall>a aa. (\<exists>ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)) \<longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac))
 3. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (5 subgoals):
 1. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> valid_global_objs s'
 2. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> valid_arch_state s'
 3. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = None; get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b); x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> \<forall>a aa. (\<exists>ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)) \<longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac))
 5. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> \<forall>a aa. (\<exists>ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)) \<longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac))
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> (\<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)) \<and> (\<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac))
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (3 subgoals):
 1. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> \<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)
 2. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> \<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac)
 3. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (5 subgoals):
 1. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> valid_global_objs s
 2. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> \<exists>a aa ab b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (a, aa, ab, b)
 4. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> \<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac)
 5. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b)\<rbrakk> \<Longrightarrow> \<forall>ab ac. (\<exists>a b. get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ab, ac, a, b)) \<longrightarrow> a + (x && mask aa) = ab + (x && mask ac)
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<And>a aa ab b ac ad ae ba. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ac, ad, ae, ba)\<rbrakk> \<Longrightarrow> a + (x && mask aa) = ac + (x && mask ad)
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (4 subgoals):
 1. \<And>a aa ab b ac ad ae ba. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ac, ad, ae, ba)\<rbrakk> \<Longrightarrow> valid_global_objs s
 2. \<And>a aa ab b ac ad ae ba. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ac, ad, ae, ba)\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<And>a aa ab b ac ad ae ba. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (arm_global_pd (arch_state s)) x = Some (a, aa, ab, b); get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (arm_global_pd (arch_state s')) x = Some (ac, ad, ae, ba); x \<in> kernel_mappings\<rbrakk> \<Longrightarrow> a + (x && mask aa) = ac + (x && mask ad)
 4. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); reads_equiv aag s' s\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x
 2. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (6 subgoals):
 1. \<lbrakk>pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); reads_equiv aag s' s\<rbrakk> \<Longrightarrow> is_subject aag (cur_thread s')
 2. \<lbrakk>pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); reads_equiv aag s' s\<rbrakk> \<Longrightarrow> invs s'
 3. \<lbrakk>pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); reads_equiv aag s' s\<rbrakk> \<Longrightarrow> pas_refined aag s'
 4. \<lbrakk>pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); reads_equiv aag s' s\<rbrakk> \<Longrightarrow> get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s')
 5. \<lbrakk>pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') = arm_global_pd (arch_state s'); reads_equiv aag s' s; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = arm_global_pd (arch_state s)\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x
 6. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> ptable_lift (cur_thread s) s x = ptable_lift (cur_thread s') s' x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s')\<rbrakk> \<Longrightarrow> (case get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s) (arch_state s) (cur_thread s)) x of None \<Rightarrow> None | Some (base, bits, rights) \<Rightarrow> Some (base + (x && mask bits))) = (case get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x of None \<Rightarrow> None | Some (base, bits, rights) \<Rightarrow> Some (base + (x && mask bits))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (cur_thread s); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s'); get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')\<rbrakk> \<Longrightarrow> (case get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x of None \<Rightarrow> None | Some (base, bits, rights) \<Rightarrow> Some (base + (x && mask bits))) = (case get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x of None \<Rightarrow> None | Some (base, bits, rights) \<Rightarrow> Some (base + (x && mask bits))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv aag s s'; pas_refined aag s; pas_refined aag s'; invs s; invs s'; is_subject aag (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')); ptable_rights (cur_thread s) s x \<noteq> {}; x \<notin> kernel_mappings; get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s); get_pd_of_thread (kheap s') (arch_state s') (cur_thread s') \<noteq> arm_global_pd (arch_state s'); get_pd_of_thread (kheap s) (arch_state s) (cur_thread s) = get_pd_of_thread (kheap s') (arch_state s') (cur_thread s'); is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (case get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x of None \<Rightarrow> None | Some (base, bits, rights) \<Rightarrow> Some (base + (x && mask bits))) = (case get_page_info (\<lambda>obj. get_arch_obj (kheap s' obj)) (get_pd_of_thread (kheap s') (arch_state s') (cur_thread s')) x of None \<Rightarrow> None | Some (base, bits, rights) \<Rightarrow> Some (base + (x && mask bits))) proof (prove)
goal:
No subgoals!