theory VSpace_C

lemma lookupPDSlot_spec:
  "\<forall>s. \<Gamma> \<turnstile>  \<lbrace>s. array_assertion (pd_' s) (2 ^ pageBits) (hrs_htd (\<acute>t_hrs))\<rbrace>
  Call lookupPDSlot_'proc
  \<lbrace>  \<acute>ret__ptr_to_struct_pde_C =  Ptr (lookupPDSlot (ptr_val (pd_' s))  (vptr_' s)) \<rbrace>" apply vcg apply (clarsimp simp: lookupPDSlot_def) apply (simp add: ARM_A.lookup_pd_slot_def) apply (subst array_assertion_shrink_right, assumption) apply (rule unat_le_helper, simp) apply (rule order_less_imp_le, rule vptr_shiftr_le_2p) apply (simp add: Let_def word_sle_def) apply (case_tac pd) apply (simp add: word_shift_by_2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. array_assertion \<^bsup>s\<^esup>pd (2 ^ pageBits) (hrs_htd \<acute>t_hrs)\<rbrace> Call lookupPDSlot_'proc \<lbrace>\<acute>ret__ptr_to_struct_pde_C = pde_Ptr (lookupPDSlot (ptr_val \<^bsup>s\<^esup>pd) \<^bsup>s\<^esup>vptr)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t_hrs vptr pd. array_assertion pd (2 ^ pageBits) (hrs_htd t_hrs) \<Longrightarrow> 0 \<le>s 0xC + 8 \<and> 0xC + 8 <s 0x20 \<and> - 2147483648 \<le> sint 0xC + sint 8 \<and> sint 0xC + sint 8 \<le> 2147483647 \<and> ptr_add_assertion' pd (uint (UCAST(32 \<rightarrow> 32) (vptr >> unat (0xC + 8)))) False (hrs_htd t_hrs) \<and> pd +\<^sub>p uint (UCAST(32 \<rightarrow> 32) (vptr >> unat (0xC + 8))) = pde_Ptr (lookupPDSlot (ptr_val pd) vptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b vptr pd. array_assertion pd (2 ^ pageBits) (hrs_htd (a, b)) \<Longrightarrow> (vptr >> 20 = 0 \<or> array_assertion pd (unat (vptr >> 20)) (hrs_htd (a, b))) \<and> pd +\<^sub>p uint (vptr >> 20) = pde_Ptr (lookup_pd_slot (ptr_val pd) vptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b vptr pd. array_assertion pd (2 ^ pageBits) (hrs_htd (a, b)) \<Longrightarrow> (vptr >> 20 = 0 \<or> array_assertion pd (unat (vptr >> 20)) (hrs_htd (a, b))) \<and> pd +\<^sub>p uint (vptr >> 20) = pde_Ptr (ptr_val pd + (vptr >> 20 << 2)) proof (prove)
goal (2 subgoals):
 1. \<And>a b vptr pd. array_assertion pd (2 ^ pageBits) (hrs_htd (a, b)) \<Longrightarrow> unat (vptr >> 20) \<le> 2 ^ pageBits
 2. \<And>a b vptr pd. array_assertion pd (2 ^ pageBits) (hrs_htd (a, b)) \<Longrightarrow> (vptr >> 20 = 0 \<or> True) \<and> pd +\<^sub>p uint (vptr >> 20) = pde_Ptr (ptr_val pd + (vptr >> 20 << 2)) proof (prove)
goal (2 subgoals):
 1. \<And>a b vptr pd. array_assertion pd (2 ^ pageBits) (hrs_htd (a, b)) \<Longrightarrow> vptr >> 20 \<le> 2 ^ pageBits
 2. \<And>a b vptr pd. array_assertion pd (2 ^ pageBits) (hrs_htd (a, b)) \<Longrightarrow> (vptr >> 20 = 0 \<or> True) \<and> pd +\<^sub>p uint (vptr >> 20) = pde_Ptr (ptr_val pd + (vptr >> 20 << 2)) proof (prove)
goal (1 subgoal):
 1. \<And>a b vptr pd. array_assertion pd (2 ^ pageBits) (hrs_htd (a, b)) \<Longrightarrow> (vptr >> 20 = 0 \<or> True) \<and> pd +\<^sub>p uint (vptr >> 20) = pde_Ptr (ptr_val pd + (vptr >> 20 << 2)) proof (prove)
goal (1 subgoal):
 1. \<And>a b vptr pd. array_assertion pd (2 ^ pageBits) (hrs_htd (a, b)) \<Longrightarrow> pd +\<^sub>p uint (vptr >> 20) = pde_Ptr (ptr_val pd + (vptr >> 20 << 2)) proof (prove)
goal (1 subgoal):
 1. \<And>a b vptr pd x. \<lbrakk>array_assertion pd (2 ^ pageBits) (hrs_htd (a, b)); pd = pde_Ptr x\<rbrakk> \<Longrightarrow> pd +\<^sub>p uint (vptr >> 20) = pde_Ptr (ptr_val pd + (vptr >> 20 << 2)) proof (prove)
goal:
No subgoals!