theory VSpace_C

lemma lookupPTSlot_nofail_spec:
  "\<forall>s. \<Gamma> \<turnstile>  \<lbrace>s. array_assertion (pt_' s) (2 ^ (ptBits - 2)) (hrs_htd (\<acute>t_hrs))\<rbrace>
  Call lookupPTSlot_nofail_'proc
  \<lbrace>  \<acute>ret__ptr_to_struct_pte_C =  Ptr (lookup_pt_slot_no_fail (ptr_val (pt_' s))  (vptr_' s)) \<rbrace>" apply vcg apply (clarsimp simp: ) apply (simp add: ARM_A.lookup_pt_slot_no_fail_def) apply (subst array_assertion_shrink_right, assumption) apply (rule order_less_imp_le, rule unat_less_helper, simp) apply (rule order_le_less_trans, rule word_and_le1, simp add: ptBits_def pageBits_def) apply (simp add: Let_def word_sle_def pteBits_def) apply (case_tac pt) 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>pt (2 ^ (ptBits - 2)) (hrs_htd \<acute>t_hrs)\<rbrace> Call lookupPTSlot_nofail_'proc \<lbrace>\<acute>ret__ptr_to_struct_pte_C = pte_Ptr (lookup_pt_slot_no_fail (ptr_val \<^bsup>s\<^esup>pt) \<^bsup>s\<^esup>vptr)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t_hrs vptr pt. array_assertion pt (2 ^ (ptBits - 2)) (hrs_htd t_hrs) \<Longrightarrow> 0 \<le>s 8 \<and> 8 <s 0x20 \<and> 0 \<le>s 0xC \<and> 0xC <s 0x20 \<and> ptr_add_assertion' pt (uint (UCAST(32 \<rightarrow> 32) ((vptr >> unat 0xC) && (1 << unat 8) - 1))) False (hrs_htd t_hrs) \<and> pt +\<^sub>p uint (UCAST(32 \<rightarrow> 32) ((vptr >> unat 0xC) && (1 << unat 8) - 1)) = pte_Ptr (lookup_pt_slot_no_fail (ptr_val pt) vptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b vptr pt. array_assertion pt (2 ^ (ptBits - 2)) (hrs_htd (a, b)) \<Longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> array_assertion pt (unat ((vptr >> 12) && 0xFF)) (hrs_htd (a, b))) \<and> pt +\<^sub>p uint ((vptr >> 12) && 0xFF) = pte_Ptr (lookup_pt_slot_no_fail (ptr_val pt) vptr) proof (prove)
goal (1 subgoal):
 1. \<And>a b vptr pt. array_assertion pt (2 ^ (ptBits - 2)) (hrs_htd (a, b)) \<Longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> array_assertion pt (unat ((vptr >> 12) && 0xFF)) (hrs_htd (a, b))) \<and> pt +\<^sub>p uint ((vptr >> 12) && 0xFF) = pte_Ptr (ptr_val pt + ((vptr >> 12) && 0xFF << 2)) proof (prove)
goal (2 subgoals):
 1. \<And>a b vptr pt. array_assertion pt (2 ^ (ptBits - 2)) (hrs_htd (a, b)) \<Longrightarrow> unat ((vptr >> 12) && 0xFF) \<le> 2 ^ (ptBits - 2)
 2. \<And>a b vptr pt. array_assertion pt (2 ^ (ptBits - 2)) (hrs_htd (a, b)) \<Longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> True) \<and> pt +\<^sub>p uint ((vptr >> 12) && 0xFF) = pte_Ptr (ptr_val pt + ((vptr >> 12) && 0xFF << 2)) proof (prove)
goal (2 subgoals):
 1. \<And>a b vptr pt. array_assertion pt (2 ^ (ptBits - 2)) (hrs_htd (a, b)) \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (ptBits - 2)
 2. \<And>a b vptr pt. array_assertion pt (2 ^ (ptBits - 2)) (hrs_htd (a, b)) \<Longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> True) \<and> pt +\<^sub>p uint ((vptr >> 12) && 0xFF) = pte_Ptr (ptr_val pt + ((vptr >> 12) && 0xFF << 2)) proof (prove)
goal (2 subgoals):
 1. \<And>a b pt. array_assertion pt (2 ^ (6 + pteBits)) (hrs_htd (a, b)) \<Longrightarrow> 0xFF < 2 ^ (6 + pteBits)
 2. \<And>a b vptr pt. array_assertion pt (2 ^ (ptBits - 2)) (hrs_htd (a, b)) \<Longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> True) \<and> pt +\<^sub>p uint ((vptr >> 12) && 0xFF) = pte_Ptr (ptr_val pt + ((vptr >> 12) && 0xFF << 2)) proof (prove)
goal (1 subgoal):
 1. \<And>a b vptr pt. array_assertion pt (2 ^ (ptBits - 2)) (hrs_htd (a, b)) \<Longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> True) \<and> pt +\<^sub>p uint ((vptr >> 12) && 0xFF) = pte_Ptr (ptr_val pt + ((vptr >> 12) && 0xFF << 2)) proof (prove)
goal (1 subgoal):
 1. \<And>a b vptr pt x. \<lbrakk>array_assertion pt (2 ^ (ptBits - 2)) (hrs_htd (a, b)); pt = pte_Ptr x\<rbrakk> \<Longrightarrow> ((vptr >> 12) && 0xFF = 0 \<or> True) \<and> pt +\<^sub>p uint ((vptr >> 12) && 0xFF) = pte_Ptr (ptr_val pt + ((vptr >> 12) && 0xFF << 2)) proof (prove)
goal:
No subgoals!