theory ArchKHeap_AI

lemma pspace_in_kernel_window_atyp_lift_strong:
  assumes atyp_inv: "\<And>P p T. \<lbrace> \<lambda>s. P (typ_at T p s) \<rbrace> f \<lbrace> \<lambda>rv s. P (typ_at T p s) \<rbrace>"
  assumes arch_inv: "\<And>P. \<lbrace>\<lambda>s. P (arm_kernel_vspace (arch_state s))\<rbrace> f \<lbrace>\<lambda>r s. P (arm_kernel_vspace (arch_state s))\<rbrace>"
  shows      "\<lbrace>\<lambda>s. pspace_in_kernel_window s\<rbrace> f \<lbrace>\<lambda>rv s. pspace_in_kernel_window s\<rbrace>" apply (simp add: pspace_in_kernel_window_def) apply (rule hoare_lift_Pf[where f="\<lambda>s. arm_kernel_vspace (arch_state s)", OF _ arch_inv]) apply (rule hoare_vcg_all_lift) apply (simp add: obj_bits_T) apply (simp add: valid_def) apply clarsimp subgoal for _ x s _ _ ko apply (cases "kheap s x") apply (frule use_valid[OF _ atyp_inv, where P1= "\<lambda>x. \<not> x" and T1="a_type ko" and p1=x];
          simp add: obj_at_def a_type_def) subgoal for ko' apply (drule spec[of _ ko']) apply (simp add: obj_bits_T) apply (frule use_valid[OF _ atyp_inv, where P1= "\<lambda>x. x" and T1="a_type ko'" and p1=x]) by (simp add: obj_at_def a_type_def)+ done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_in_kernel_window\<rbrace> f \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x ko. kheap s x = Some ko \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits ko - 1}. arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow)\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x ko. kheap s x = Some ko \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits ko - 1}. arm_kernel_vspace (arch_state s) y = ArmVSpaceKernelWindow)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. \<forall>xa ko. kheap s xa = Some ko \<longrightarrow> (\<forall>y\<in>{xa..xa + 2 ^ obj_bits ko - 1}. x y = ArmVSpaceKernelWindow)\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>xa ko. kheap a xa = Some ko \<longrightarrow> (\<forall>y\<in>{xa..xa + 2 ^ obj_bits ko - 1}. x y = ArmVSpaceKernelWindow)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrace>\<lambda>s. \<forall>ko. kheap s xa = Some ko \<longrightarrow> (\<forall>y\<in>{xa..xa + 2 ^ obj_bits ko - 1}. x y = ArmVSpaceKernelWindow)\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>ko. kheap s xa = Some ko \<longrightarrow> (\<forall>y\<in>{xa..xa + 2 ^ obj_bits ko - 1}. x y = ArmVSpaceKernelWindow)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrace>\<lambda>s. \<forall>ko. kheap s xa = Some ko \<longrightarrow> (\<forall>y\<in>{xa..xa + 2 ^ obj_bits_type (a_type ko) - 1}. x y = ArmVSpaceKernelWindow)\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>ko. kheap s xa = Some ko \<longrightarrow> (\<forall>y\<in>{xa..xa + 2 ^ obj_bits_type (a_type ko) - 1}. x y = ArmVSpaceKernelWindow)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<forall>s. (\<forall>ko. kheap s xa = Some ko \<longrightarrow> (\<forall>y\<in>{xa..xa + 2 ^ obj_bits_type (a_type ko) - 1}. x y = ArmVSpaceKernelWindow)) \<longrightarrow> (\<forall>xb\<in>fst (f s). case xb of (r, s') \<Rightarrow> \<forall>ko. kheap s' xa = Some ko \<longrightarrow> (\<forall>y\<in>{xa..xa + 2 ^ obj_bits_type (a_type ko) - 1}. x y = ArmVSpaceKernelWindow)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa s a b ko y. \<lbrakk>\<forall>ko. kheap s xa = Some ko \<longrightarrow> (\<forall>y\<in>{xa..xa + 2 ^ obj_bits_type (a_type ko) - 1}. x y = ArmVSpaceKernelWindow); (a, b) \<in> fst (f s); kheap b xa = Some ko; xa \<le> y; y \<le> xa + 2 ^ obj_bits_type (a_type ko) - 1\<rbrakk> \<Longrightarrow> x y = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ko. kheap s x = Some ko \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits_type (a_type ko) - 1}. x_ y = ArmVSpaceKernelWindow); (a_, b_) \<in> fst (f s); kheap b_ x = Some ko; x \<le> y_; y_ \<le> x + 2 ^ obj_bits_type (a_type ko) - 1\<rbrakk> \<Longrightarrow> x_ y_ = ArmVSpaceKernelWindow proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>ko. kheap s x = Some ko \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits_type (a_type ko) - 1}. x_ y = ArmVSpaceKernelWindow); (a_, b_) \<in> fst (f s); kheap b_ x = Some ko; x \<le> y_; y_ \<le> x + 2 ^ obj_bits_type (a_type ko) - 1; kheap s x = None\<rbrakk> \<Longrightarrow> x_ y_ = ArmVSpaceKernelWindow
 2. \<And>aa. \<lbrakk>\<forall>ko. kheap s x = Some ko \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits_type (a_type ko) - 1}. x_ y = ArmVSpaceKernelWindow); (a_, b_) \<in> fst (f s); kheap b_ x = Some ko; x \<le> y_; y_ \<le> x + 2 ^ obj_bits_type (a_type ko) - 1; kheap s x = Some aa\<rbrakk> \<Longrightarrow> x_ y_ = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>\<forall>ko. kheap s x = Some ko \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits_type (a_type ko) - 1}. x_ y = ArmVSpaceKernelWindow); (a_, b_) \<in> fst (f s); kheap b_ x = Some ko; x \<le> y_; y_ \<le> x + 2 ^ obj_bits_type (a_type ko) - 1; kheap s x = Some aa\<rbrakk> \<Longrightarrow> x_ y_ = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ko. kheap s x = Some ko \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits_type (a_type ko) - 1}. x_ y = ArmVSpaceKernelWindow); (a_, b_) \<in> fst (f s); kheap b_ x = Some ko; x \<le> y_; y_ \<le> x + 2 ^ obj_bits_type (a_type ko) - 1; kheap s x = Some ko'\<rbrakk> \<Longrightarrow> x_ y_ = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a_, b_) \<in> fst (f s); kheap b_ x = Some ko; x \<le> y_; y_ \<le> x + 2 ^ obj_bits_type (a_type ko) - 1; kheap s x = Some ko'; kheap s x = Some ko' \<longrightarrow> (\<forall>y\<in>{x..x + 2 ^ obj_bits_type (a_type ko') - 1}. x_ y = ArmVSpaceKernelWindow)\<rbrakk> \<Longrightarrow> x_ y_ = ArmVSpaceKernelWindow proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a_, b_) \<in> fst (f s); kheap b_ x = Some ko; x \<le> y_; y_ \<le> x + 2 ^ obj_bits_type (a_type ko) - 1; kheap s x = Some ko'; \<forall>y\<in>{x..x + 2 ^ obj_bits_type (a_type ko') - 1}. x_ y = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> x_ y_ = ArmVSpaceKernelWindow proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(a_, b_) \<in> fst (f s); kheap b_ x = Some ko; x \<le> y_; y_ \<le> x + 2 ^ obj_bits_type (a_type ko) - 1; kheap s x = Some ko'; \<forall>y\<in>{x..x + 2 ^ obj_bits_type (a_type ko') - 1}. x_ y = ArmVSpaceKernelWindow\<rbrakk> \<Longrightarrow> typ_at (a_type ko') x s
 2. \<lbrakk>(a_, b_) \<in> fst (f s); kheap b_ x = Some ko; x \<le> y_; y_ \<le> x + 2 ^ obj_bits_type (a_type ko) - 1; kheap s x = Some ko'; \<forall>y\<in>{x..x + 2 ^ obj_bits_type (a_type ko') - 1}. x_ y = ArmVSpaceKernelWindow; typ_at (a_type ko') x b_\<rbrakk> \<Longrightarrow> x_ y_ = ArmVSpaceKernelWindow proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!