theory ArchKHeap_AI

lemma valid_kernel_mappings_lift:
  "\<lbrace>valid_kernel_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>" apply (simp add: valid_kernel_mappings_def) apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch]) apply (simp add: valid_kernel_mappings_if_pd_def ran_def
              del: valid_kernel_mappings_if_pd_arch_def) apply (rule hoare_vcg_all_lift) apply (case_tac "\<exists>ao. xa = ArchObj ao") apply (rule hoare_convert_imp) apply clarsimp apply (rule hoare_vcg_all_lift) subgoal for ao a by (rule aobj_at[where P=Not and P'="\<lambda>x. x = ArchObj ao", simplified obj_at_def, simplified]) apply clarsimp apply (case_tac ao; simp add: hoare_vcg_prop) apply (clarsimp simp del: valid_kernel_mappings_if_pd_arch_def) apply (case_tac xa; simp add: hoare_vcg_prop) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_kernel_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ko\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) ko\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>ko\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts (arch_state s))) ko\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. \<forall>ko\<in>ran (kheap s). valid_kernel_mappings_if_pd (set (arm_global_pts x)) ko\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>ko\<in>ran (kheap a). valid_kernel_mappings_if_pd (set (arm_global_pts x)) ko\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. \<forall>xa. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>xa. (\<exists>aa. kheap a aa = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrace>\<lambda>s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<exists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace>
 2. \<And>x xa. \<nexists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<exists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. \<nexists>a. kheap s a = Some xa\<rbrace> f \<lbrace>\<lambda>rv s. \<nexists>a. kheap s a = Some xa\<rbrace>
 2. \<And>x xa. \<exists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace>
 3. \<And>x xa. \<nexists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ao. \<lbrace>\<lambda>s. \<forall>a. kheap s a \<noteq> Some (ArchObj ao)\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>a. kheap s a \<noteq> Some (ArchObj ao)\<rbrace>
 2. \<And>x xa. \<exists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace>
 3. \<And>x xa. \<nexists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ao a. \<lbrace>\<lambda>s. kheap s a \<noteq> Some (ArchObj ao)\<rbrace> f \<lbrace>\<lambda>rv s. kheap s a \<noteq> Some (ArchObj ao)\<rbrace>
 2. \<And>x xa. \<exists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace>
 3. \<And>x xa. \<nexists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. kheap s a \<noteq> Some (ArchObj ao)\<rbrace> f \<lbrace>\<lambda>rv s. kheap s a \<noteq> Some (ArchObj ao)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<exists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace>
 2. \<And>x xa. \<nexists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x ao. \<lbrace>\<lambda>s. case ao of PageDirectory pd \<Rightarrow> \<forall>xa r. pde_ref (pd xa) = Some r \<longrightarrow> (r \<in> set (arm_global_pts x)) = (xa \<in> kernel_mapping_slots) | _ \<Rightarrow> True\<rbrace> f \<lbrace>\<lambda>rv s. case ao of PageDirectory pd \<Rightarrow> \<forall>xa r. pde_ref (pd xa) = Some r \<longrightarrow> (r \<in> set (arm_global_pts x)) = (xa \<in> kernel_mapping_slots) | _ \<Rightarrow> True\<rbrace>
 2. \<And>x xa. \<nexists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<nexists>ao. xa = ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> f \<lbrace>\<lambda>rv s. (\<exists>a. kheap s a = Some xa) \<longrightarrow> arch_obj_fun_lift (valid_kernel_mappings_if_pd_arch (set (arm_global_pts x))) True xa\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<forall>ao. xa \<noteq> ArchObj ao \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> f \<lbrace>\<lambda>rv s. True\<rbrace> proof (prove)
goal:
No subgoals!