kings-crown/FVELER_Isabelle huggingface dataset:
theory VSpace_C

lemma wordFromMessageInfo_spec:
  defines "mil s \<equiv> seL4_MessageInfo_lift \<^bsup>s\<^esup>mi"
  shows "\<forall>s. \<Gamma> \<turnstile> {s} Call wordFromMessageInfo_'proc
                  \<lbrace>\<acute>ret__unsigned_long = (label_CL (mil s) << 12)
                                      || (capsUnwrapped_CL (mil s) << 9)
                                      || (extraCaps_CL (mil s) << 7)
                                      || length_CL (mil s)\<rbrace>" unfolding mil_def apply vcg apply (simp add: seL4_MessageInfo_lift_def mask_shift_simps word_sless_def word_sle_def) apply word_bitwise done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call wordFromMessageInfo_'proc \<lbrace>\<acute>ret__unsigned_long = (label_CL (mil s) << 12) || (capsUnwrapped_CL (mil s) << 9) || (extraCaps_CL (mil s) << 7) || length_CL (mil s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call wordFromMessageInfo_'proc \<lbrace>\<acute>ret__unsigned_long = (label_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi) << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi) << 9) || (extraCaps_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi) << 7) || length_CL (seL4_MessageInfo_lift \<^bsup>s\<^esup>mi)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>mi. 0 <s 1 \<and> 0 \<le>s 0 \<and> UCAST(32 \<rightarrow> 32) (seL4_MessageInfo_C.words_C mi.[unat 0]) = (label_CL (seL4_MessageInfo_lift mi) << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift mi) << 9) || (extraCaps_CL (seL4_MessageInfo_lift mi) << 7) || length_CL (seL4_MessageInfo_lift mi) proof (prove)
goal (1 subgoal):
 1. \<And>mi. seL4_MessageInfo_C.words_C mi.[0] = seL4_MessageInfo_C.words_C mi.[0] && 0xFFFFF000 || seL4_MessageInfo_C.words_C mi.[0] && 0xE00 || seL4_MessageInfo_C.words_C mi.[0] && 0x180 || seL4_MessageInfo_C.words_C mi.[0] && 0x7F proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma invalidateTranslationSingleLocal_ccorres:
  "ccorres dc xfdc \<top> (\<lbrace>\<acute>vptr = w\<rbrace>) []
           (doMachineOp (invalidateLocalTLB_VAASID w))
           (Call invalidateTranslationSingleLocal_'proc)" apply cinit' apply (ctac (no_vcg) add: invalidateLocalTLB_VAASID_ccorres) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>vptr = w\<rbrace> [] (doMachineOp (invalidateLocalTLB_VAASID w)) (Call invalidateTranslationSingleLocal_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q5 ?Q'5 [SKIP] (doMachineOp (invalidateLocalTLB_VAASID w)) (CALL invalidateLocalTLB_VAASID_'proc(\<acute>vptr))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>vptr = w\<rbrace>\<rbrakk> \<Longrightarrow> ?Q5 s \<and> s' \<in> ?Q'5 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>vptr = w\<rbrace>\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. mva_plus_asid_'_update (\<lambda>_. vptr_' s) s \<in> \<lbrace>\<acute>mva_plus_asid = w\<rbrace>} proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma invalidateTranslationSingle_ccorres:
  "ccorres dc xfdc \<top> (\<lbrace>\<acute>vptr = w\<rbrace>) []
           (doMachineOp (invalidateLocalTLB_VAASID w))
           (Call invalidateTranslationSingle_'proc)" apply cinit' apply (ctac (no_vcg) add: invalidateTranslationSingleLocal_ccorres) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>vptr = w\<rbrace> [] (doMachineOp (invalidateLocalTLB_VAASID w)) (Call invalidateTranslationSingle_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q43 ?Q'43 [SKIP] (doMachineOp (invalidateLocalTLB_VAASID w)) (CALL invalidateTranslationSingleLocal_'proc(\<acute>vptr))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>vptr = w\<rbrace>\<rbrakk> \<Longrightarrow> ?Q43 s \<and> s' \<in> ?Q'43 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>vptr = w\<rbrace>\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. vptr_'_update (\<lambda>_. vptr_' s) s \<in> \<lbrace>\<acute>vptr = w\<rbrace>} proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma ccorres_return_void_C':
  "ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc (\<lambda>_. True) UNIV (SKIP # hs) (return (Inl rv)) return_void_C" apply (rule ccorres_from_vcg_throws) apply (simp add: return_def) apply (rule allI, rule conseqPre, vcg) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc (\<lambda>_. True) UNIV (SKIP # hs) (return (Inl rv)) return_void_C proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_void_C {},{s. \<exists>(rv, \<sigma>')\<in>fst (return (Inl rv) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inl_rrel dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr} return_void_C {},{s. (\<sigma>, s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. (\<sigma>, s\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr} proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma is_aligned_cache_preconds:
  "\<lbrakk>is_aligned rva n; n \<ge> 6\<rbrakk> \<Longrightarrow> rva \<le> rva + 0x3F \<and>
          addrFromPPtr rva \<le> addrFromPPtr rva + 0x3F \<and> rva && mask 5 = addrFromPPtr rva && mask 5" supply if_cong[cong] apply (drule is_aligned_weaken, simp) apply (rule conjI) apply (drule is_aligned_no_overflow, simp, unat_arith)[1] apply (rule conjI) apply (drule is_aligned_addrFromPPtr_n, simp) apply (drule is_aligned_no_overflow, unat_arith) apply (frule is_aligned_addrFromPPtr_n, simp) apply (drule_tac x=6 and y=5 in is_aligned_weaken, simp)+ apply (simp add: is_aligned_mask) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned rva n; 6 \<le> n\<rbrakk> \<Longrightarrow> rva \<le> rva + 0x3F \<and> addrFromPPtr rva \<le> addrFromPPtr rva + 0x3F \<and> rva && mask 5 = addrFromPPtr rva && mask 5 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned rva n; 6 \<le> n\<rbrakk> \<Longrightarrow> rva \<le> rva + 0x3F \<and> addrFromPPtr rva \<le> addrFromPPtr rva + 0x3F \<and> rva && mask 5 = addrFromPPtr rva && mask 5 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>6 \<le> n; is_aligned rva 6\<rbrakk> \<Longrightarrow> rva \<le> rva + 0x3F \<and> addrFromPPtr rva \<le> addrFromPPtr rva + 0x3F \<and> rva && mask 5 = addrFromPPtr rva && mask 5 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>6 \<le> n; is_aligned rva 6\<rbrakk> \<Longrightarrow> rva \<le> rva + 0x3F
 2. \<lbrakk>6 \<le> n; is_aligned rva 6\<rbrakk> \<Longrightarrow> addrFromPPtr rva \<le> addrFromPPtr rva + 0x3F \<and> rva && mask 5 = addrFromPPtr rva && mask 5 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>6 \<le> n; is_aligned rva 6\<rbrakk> \<Longrightarrow> addrFromPPtr rva \<le> addrFromPPtr rva + 0x3F \<and> rva && mask 5 = addrFromPPtr rva && mask 5 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>6 \<le> n; is_aligned rva 6\<rbrakk> \<Longrightarrow> addrFromPPtr rva \<le> addrFromPPtr rva + 0x3F
 2. \<lbrakk>6 \<le> n; is_aligned rva 6\<rbrakk> \<Longrightarrow> rva && mask 5 = addrFromPPtr rva && mask 5 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>6 \<le> n; is_aligned (addrFromPPtr rva) 6\<rbrakk> \<Longrightarrow> addrFromPPtr rva \<le> addrFromPPtr rva + 0x3F
 2. \<lbrakk>6 \<le> n; is_aligned rva 6\<rbrakk> \<Longrightarrow> rva && mask 5 = addrFromPPtr rva && mask 5 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>6 \<le> n; is_aligned rva 6\<rbrakk> \<Longrightarrow> rva && mask 5 = addrFromPPtr rva && mask 5 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>6 \<le> n; is_aligned rva 6; is_aligned (addrFromPPtr rva) 6\<rbrakk> \<Longrightarrow> rva && mask 5 = addrFromPPtr rva && mask 5 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>6 \<le> n; is_aligned rva 5; is_aligned (addrFromPPtr rva) 5\<rbrakk> \<Longrightarrow> rva && mask 5 = addrFromPPtr rva && mask 5 proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma pte_pte_invalid_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_pte_C :== PROC pte_pte_invalid_new()
       \<lbrace> pte_lift \<acute>ret__struct_pte_C = Some (Pte_pte_large
          \<lparr> pte_pte_large_CL.address_CL = 0,
             XN_CL = 0,
             TEX_CL = 0,
              nG_CL = 0,
              S_CL = 0,
              APX_CL = 0,
              AP_CL = 0,
              C_CL = 0,
              B_CL = 0,
              reserved_CL = 0
          \<rparr>)\<rbrace>" apply vcg apply (clarsimp simp: pte_lift_def pte_get_tag_def pte_pte_large_def fupdate_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call pte_pte_invalid_new_'proc \<lbrace>pte_lift \<acute>ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = 0, XN_CL = 0, TEX_CL = 0, nG_CL = 0, S_CL = 0, APX_CL = 0, AP_CL = 0, C_CL = 0, B_CL = 0, reserved_CL = 0\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. pte_lift (pte_C.words_C_update (fupdate 0 (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0)) (pte_C.pte_C (ARRAY _. 0))) = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = 0, XN_CL = 0, TEX_CL = 0, nG_CL = 0, S_CL = 0, APX_CL = 0, AP_CL = 0, C_CL = 0, B_CL = 0, reserved_CL = 0\<rparr>) proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma ccorres_name_pre_C:
  "(\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g)
  \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs f g" apply (rule ccorres_guard_imp) apply (rule_tac xf'=id in ccorres_abstract, rule ceqv_refl) apply (rule_tac P="rv' \<in> P'" in ccorres_gen_asm2) apply assumption apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g) \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs f g proof (prove)
goal (3 subgoals):
 1. (\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g) \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' hs f g
 2. \<And>s. \<lbrakk>\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g; P s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. \<And>rv'. (\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g) \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q (?G'4 rv') hs f g
 2. \<And>s. \<lbrakk>\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g; P s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s. s \<in> ?G'4 (id s)} proof (prove)
goal (3 subgoals):
 1. \<And>rv'. \<lbrakk>\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g; rv' \<in> P'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf ?Q (?G'7 rv') hs f g
 2. \<And>s. \<lbrakk>\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g; P s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s. s \<in> ?G'7 (id s) \<inter> \<lbrace>id s \<in> P'\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g; P s\<rbrakk> \<Longrightarrow> P s
 2. \<And>s. \<lbrakk>\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s. s \<in> {id s} \<inter> \<lbrace>id s \<in> P'\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g; s \<in> P'\<rbrakk> \<Longrightarrow> s \<in> {s. s \<in> {id s} \<inter> \<lbrace>id s \<in> P'\<rbrace>} proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma large_ptSlot_array_constraint:
  "is_aligned (ptSlot :: word32) 6 \<Longrightarrow> n \<le> limit - 240 \<and> 240 \<le> limit
    \<Longrightarrow> \<exists>i. ptSlot = (ptSlot && ~~ mask ptBits) + of_nat i * 4 \<and> i + n \<le> limit" apply (rule_tac x="unat ((ptSlot && mask ptBits) >> 2)" in exI) apply (simp add: shiftl_t2n[where n=2, symmetric, THEN trans[rotated],
                   OF mult.commute, simplified]) apply (simp add: shiftr_shiftl1) apply (rule conjI, rule trans,
         rule word_plus_and_or_coroll2[symmetric, where w="mask ptBits"]) apply (simp, rule is_aligned_neg_mask_eq[THEN sym], rule is_aligned_andI1,
          erule is_aligned_weaken, simp) apply (clarsimp simp add: le_diff_conv2) apply (erule order_trans[rotated], simp) apply (rule unat_le_helper) apply (simp add: is_aligned_mask mask_def ptBits_def pageBits_def) apply (word_bitwise, simp add: pteBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptSlot 6; n \<le> limit - 240 \<and> 240 \<le> limit\<rbrakk> \<Longrightarrow> \<exists>i. ptSlot = (ptSlot && ~~ mask ptBits) + word_of_nat i * 4 \<and> i + n \<le> limit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptSlot 6; n \<le> limit - 240 \<and> 240 \<le> limit\<rbrakk> \<Longrightarrow> ptSlot = (ptSlot && ~~ mask ptBits) + word_of_nat (unat (ptSlot && mask ptBits >> 2)) * 4 \<and> unat (ptSlot && mask ptBits >> 2) + n \<le> limit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptSlot 6; n \<le> limit - 240 \<and> 240 \<le> limit\<rbrakk> \<Longrightarrow> ptSlot = (ptSlot && ~~ mask ptBits) + (ptSlot && mask ptBits >> 2 << 2) \<and> unat (ptSlot && mask ptBits >> 2) + n \<le> limit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptSlot 6; n \<le> limit - 240 \<and> 240 \<le> limit\<rbrakk> \<Longrightarrow> ptSlot = (ptSlot && ~~ mask ptBits) + ((ptSlot && mask ptBits) && ~~ mask 2) \<and> unat (ptSlot && mask ptBits >> 2) + n \<le> limit proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptSlot 6; n \<le> limit - 240 \<and> 240 \<le> limit\<rbrakk> \<Longrightarrow> (ptSlot && mask ptBits) + (ptSlot && ~~ mask ptBits) = (ptSlot && ~~ mask ptBits) + ((ptSlot && mask ptBits) && ~~ mask 2)
 2. \<lbrakk>is_aligned ptSlot 6; n \<le> limit - 240 \<and> 240 \<le> limit\<rbrakk> \<Longrightarrow> unat (ptSlot && mask ptBits >> 2) + n \<le> limit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptSlot 6; n \<le> limit - 240 \<and> 240 \<le> limit\<rbrakk> \<Longrightarrow> unat (ptSlot && mask ptBits >> 2) + n \<le> limit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptSlot 6; n + 240 \<le> limit\<rbrakk> \<Longrightarrow> unat (ptSlot && mask ptBits >> 2) + n \<le> limit proof (prove)
goal (1 subgoal):
 1. is_aligned ptSlot 6 \<Longrightarrow> unat (ptSlot && mask ptBits >> 2) \<le> 240 proof (prove)
goal (1 subgoal):
 1. is_aligned ptSlot 6 \<Longrightarrow> ptSlot && mask ptBits >> 2 \<le> word_of_nat 240 proof (prove)
goal (1 subgoal):
 1. ptSlot && 0x3F = 0 \<Longrightarrow> ptSlot && 2 ^ (8 + pteBits) - 1 >> 2 \<le> 0xF0 proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma large_pdSlot_array_constraint:
  "is_aligned pd pdBits \<Longrightarrow> vmsz_aligned vptr ARMSuperSection \<Longrightarrow> n \<le> limit - 4080 \<and> 4080 \<le> limit
    \<Longrightarrow> \<exists>i. lookup_pd_slot pd vptr = pd + of_nat i * 4 \<and> i + n \<le> limit" apply (rule_tac x="unat (vptr >> 20)" in exI) apply (rule conjI) apply (simp add: lookup_pd_slot_def shiftl_t2n) apply (clarsimp simp add: le_diff_conv2) apply (erule order_trans[rotated], simp) apply (rule unat_le_helper) apply (simp add: is_aligned_mask mask_def pdBits_def pageBits_def
                   vmsz_aligned_def) apply (word_bitwise, simp?) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pdBits; vmsz_aligned vptr Wellformed_C.ARMSuperSection; n \<le> limit - 4080 \<and> 4080 \<le> limit\<rbrakk> \<Longrightarrow> \<exists>i. lookup_pd_slot pd vptr = pd + word_of_nat i * 4 \<and> i + n \<le> limit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pdBits; vmsz_aligned vptr Wellformed_C.ARMSuperSection; n \<le> limit - 4080 \<and> 4080 \<le> limit\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr = pd + word_of_nat (unat (vptr >> 20)) * 4 \<and> unat (vptr >> 20) + n \<le> limit proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd pdBits; vmsz_aligned vptr Wellformed_C.ARMSuperSection; n \<le> limit - 4080 \<and> 4080 \<le> limit\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr = pd + word_of_nat (unat (vptr >> 20)) * 4
 2. \<lbrakk>is_aligned pd pdBits; vmsz_aligned vptr Wellformed_C.ARMSuperSection; n \<le> limit - 4080 \<and> 4080 \<le> limit\<rbrakk> \<Longrightarrow> unat (vptr >> 20) + n \<le> limit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pdBits; vmsz_aligned vptr Wellformed_C.ARMSuperSection; n \<le> limit - 4080 \<and> 4080 \<le> limit\<rbrakk> \<Longrightarrow> unat (vptr >> 20) + n \<le> limit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pdBits; vmsz_aligned vptr Wellformed_C.ARMSuperSection; n + 4080 \<le> limit\<rbrakk> \<Longrightarrow> unat (vptr >> 20) + n \<le> limit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pdBits; vmsz_aligned vptr Wellformed_C.ARMSuperSection\<rbrakk> \<Longrightarrow> unat (vptr >> 20) \<le> 4080 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pdBits; vmsz_aligned vptr Wellformed_C.ARMSuperSection\<rbrakk> \<Longrightarrow> vptr >> 20 \<le> word_of_nat 4080 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd && 2 ^ (12 + pdeBits) - 1 = 0; vptr && 0xFFFFFF = 0\<rbrakk> \<Longrightarrow> vptr >> 20 \<le> 0xFF0 proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma findPDForASID_page_directory_at'_simple[wp]:
  notes checkPDAt_inv[wp del]
  shows "\<lbrace>\<top>\<rbrace> findPDForASID asiv
    \<lbrace>\<lambda>rv s. page_directory_at' rv s\<rbrace>,-" apply (simp add:findPDForASID_def) apply (wp getASID_wp|simp add:checkPDAt_def | wpc)+ apply auto? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> findPDForASID asiv \<lbrace>page_directory_at'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE y <- assertE (0 < asiv);
y <- assertE (asiv \<le> snd asidRange);
asidTable <- liftE (gets (armKSASIDTable \<circ> ksArchState));
pool <- liftME (inv asidpool.ASIDPool) (case asidTable (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asiv)) of None \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> withoutFailure $ getObject ptr);
case pool (asiv && mask local.asid_low_bits) of None \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | Some ptr \<Rightarrow> doE haskell_assertE (ptr \<noteq> 0) [];
withoutFailure $ checkPDAt ptr;
returnOk ptr
odE
odE \<lbrace>page_directory_at'\<rbrace>, - proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma array_assertion_abs_pte_16:
  "\<forall>s s'. (s, s') \<in> rf_sr \<and> (page_table_at' (ptr_val ptPtr && ~~ mask ptBits) s
        \<and> is_aligned (ptr_val ptPtr) 6) \<and> (n s' \<le> 16 \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
    \<longrightarrow> (x s' = 0 \<or> array_assertion (ptPtr :: pte_C ptr) (n s') (hrs_htd (t_hrs_' (globals s'))))" apply (intro allI impI disjCI2, clarsimp) apply (drule(1) page_table_at_rf_sr, clarsimp) apply (cases ptPtr, simp) apply (erule clift_array_assertion_imp, simp_all) apply (rule large_ptSlot_array_constraint, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> (page_table_at' (ptr_val ptPtr && ~~ mask ptBits) s \<and> is_aligned (ptr_val ptPtr) 6) \<and> n s' \<le> 16 \<and> (x s' \<noteq> (0::'a) \<longrightarrow> n s' \<noteq> 0) \<longrightarrow> x s' = (0::'a) \<or> array_assertion ptPtr (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; page_table_at' (ptr_val ptPtr && ~~ mask ptBits) s; is_aligned (ptr_val ptPtr) 6; n s' \<le> 16; 0 < n s'\<rbrakk> \<Longrightarrow> array_assertion ptPtr (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' y. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; is_aligned (ptr_val ptPtr) 6; n s' \<le> 16; 0 < n s'; cslift s' (pt_Ptr (ptr_val ptPtr && ~~ mask ptBits)) = Some y\<rbrakk> \<Longrightarrow> array_assertion ptPtr (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' y xa. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; is_aligned xa 6; n s' \<le> 16; 0 < n s'; cslift s' (pt_Ptr (xa && ~~ mask ptBits)) = Some y; ptPtr = pte_Ptr xa\<rbrakk> \<Longrightarrow> array_assertion (pte_Ptr xa) (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' xa. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; is_aligned xa 6; n s' \<le> 16; 0 < n s'; ptPtr = pte_Ptr xa\<rbrakk> \<Longrightarrow> \<exists>i. xa = (xa && ~~ mask ptBits) + word_of_nat i * 4 \<and> i + n s' \<le> 256 proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma array_assertion_abs_pde_16:
  "\<forall>s s'. (s, s') \<in> rf_sr \<and> (page_directory_at' pd s
        \<and> vmsz_aligned vptr ARMSuperSection) \<and> (n s' \<le> 16 \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
    \<longrightarrow> (x s' = 0 \<or> array_assertion (pde_Ptr (lookup_pd_slot pd vptr)) (n s') (hrs_htd (t_hrs_' (globals s'))))" apply (intro allI impI disjCI2, clarsimp) apply (frule(1) page_directory_at_rf_sr, clarsimp) apply (erule clift_array_assertion_imp, simp_all) apply (rule large_pdSlot_array_constraint, simp_all add: page_directory_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> (page_directory_at' pd s \<and> vmsz_aligned vptr Wellformed_C.ARMSuperSection) \<and> n s' \<le> 16 \<and> (x s' \<noteq> (0::'a) \<longrightarrow> n s' \<noteq> 0) \<longrightarrow> x s' = (0::'a) \<or> array_assertion (pde_Ptr (lookup_pd_slot pd vptr)) (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; page_directory_at' pd s; vmsz_aligned vptr Wellformed_C.ARMSuperSection; n s' \<le> 16; 0 < n s'\<rbrakk> \<Longrightarrow> array_assertion (pde_Ptr (lookup_pd_slot pd vptr)) (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' y. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; page_directory_at' pd s; vmsz_aligned vptr Wellformed_C.ARMSuperSection; n s' \<le> 16; 0 < n s'; cslift s' (pd_Ptr pd) = Some y\<rbrakk> \<Longrightarrow> array_assertion (pde_Ptr (lookup_pd_slot pd vptr)) (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; page_directory_at' pd s; vmsz_aligned vptr Wellformed_C.ARMSuperSection; n s' \<le> 16; 0 < n s'\<rbrakk> \<Longrightarrow> \<exists>i. lookup_pd_slot pd vptr = pd + word_of_nat i * 4 \<and> i + n s' \<le> 4096 proof (prove)
goal:
No subgoals!