theory VSpace_C

lemma makeUserPTE_spec:
  "\<forall>s. \<Gamma> \<turnstile>
  \<lbrace>s. (\<acute>page_size = scast Kernel_C.ARMSmallPage \<or> \<acute>page_size = scast Kernel_C.ARMLargePage) \<and>
      \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size)  \<and>
      \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace>
  Call makeUserPTE_'proc
  \<lbrace> pte_lift \<acute>ret__struct_pte_C = Some (if \<^bsup>s\<^esup>page_size = scast Kernel_C.ARMSmallPage
    then Pte_pte_small
     \<lparr> pte_pte_small_CL.address_CL = \<^bsup>s\<^esup>paddr,
       nG_CL = 1,
       S_CL = shared_bit_from_cacheable \<^bsup>s\<^esup>cacheable,
       APX_CL = 0,
       TEX_CL = tex_bits_from_cacheable \<^bsup>s\<^esup>cacheable,
       AP_CL = ap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights),
       C_CL = 0,
       B_CL = iwb_from_cacheable  \<^bsup>s\<^esup>cacheable,
       XN_CL = \<^bsup>s\<^esup>nonexecutable
     \<rparr>
    else Pte_pte_large
     \<lparr> pte_pte_large_CL.address_CL =  \<^bsup>s\<^esup>paddr,
       XN_CL = \<^bsup>s\<^esup>nonexecutable,
       TEX_CL = tex_bits_from_cacheable \<^bsup>s\<^esup>cacheable,
       nG_CL = 1,
       S_CL = shared_bit_from_cacheable \<^bsup>s\<^esup>cacheable,
       APX_CL = 0,
       AP_CL = ap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights),
       C_CL = 0,
       B_CL =  iwb_from_cacheable  \<^bsup>s\<^esup>cacheable,
       reserved_CL = 1
     \<rparr>)\<rbrace>" apply vcg apply (clarsimp simp:vmsz_aligned'_def) apply (intro conjI) apply (rule impI) apply (drule is_aligned_weaken[where y = 12]) apply (clarsimp simp:gen_framesize_to_H_def pageBitsForSize_def split:if_splits) apply (clarsimp dest:is_aligned_neg_mask_eq) apply (intro conjI impI allI) apply (fold_subgoals (prefix))[2] subgoal premises prems using prems by ((clarsimp simp add: pte_lift_def pte_pte_small_lift_def pte_tag_defs
                  mask_def ap_from_vm_rights_mask addrFromPPtr_def
                  shared_bit_from_cacheable_def tex_bits_from_cacheable_def
                  iwb_from_cacheable_def dest!:mask_eq1_nochoice)+) apply (clarsimp) apply (drule is_aligned_weaken[where y = 16]) apply (clarsimp simp:gen_framesize_to_H_def pageBitsForSize_def split:if_splits) apply (intro conjI impI allI) apply ((clarsimp simp add: pte_lift_def pte_pte_large_lift_def pte_tag_defs
   mask_def ap_from_vm_rights_mask addrFromPPtr_def
   shared_bit_from_cacheable_def tex_bits_from_cacheable_def
   iwb_from_cacheable_def dest!:mask_eq1_nochoice is_aligned_neg_mask_eq)+)[2] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> Call makeUserPTE_'proc \<lbrace>pte_lift \<acute>ret__struct_pte_C = Some (if \<^bsup>s\<^esup>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage then Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = \<^bsup>s\<^esup>paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable \<^bsup>s\<^esup>cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable \<^bsup>s\<^esup>cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights), C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable, XN_CL = \<^bsup>s\<^esup>nonexecutable\<rparr> else Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = \<^bsup>s\<^esup>paddr, XN_CL = \<^bsup>s\<^esup>nonexecutable, TEX_CL = tex_bits_from_cacheable \<^bsup>s\<^esup>cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable \<^bsup>s\<^esup>cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights), C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable, reserved_CL = 1\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; vmsz_aligned' paddr (gen_framesize_to_H page_size); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable\<rbrakk> \<Longrightarrow> vm_rights < 4 \<and> (\<forall>ret__unsigned_long. ret__unsigned_long = ap_from_vm_rights (vmrights_to_H vm_rights) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = UCAST(32 \<rightarrow> 32) paddr && ~~ mask 12, nG_CL = SCAST(32 signed \<rightarrow> 32) 1 && mask 1, S_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, APX_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, TEX_CL = SCAST(32 signed \<rightarrow> 32) 5 && mask 3, AP_CL = UCAST(32 \<rightarrow> 32) (ap_from_vm_rights (vmrights_to_H vm_rights)) && mask 2, C_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, B_CL = SCAST(32 signed \<rightarrow> 32) 1 && mask 1, XN_CL = UCAST(32 \<rightarrow> 32) nonexecutable && mask 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (if page_size = page_size then Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, XN_CL = nonexecutable\<rparr> else Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = UCAST(32 \<rightarrow> 32) paddr && ~~ mask 12, nG_CL = SCAST(32 signed \<rightarrow> 32) 1 && mask 1, S_CL = SCAST(32 signed \<rightarrow> 32) 1 && mask 1, APX_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, TEX_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 3, AP_CL = UCAST(32 \<rightarrow> 32) (ap_from_vm_rights (vmrights_to_H vm_rights)) && mask 2, C_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, B_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, XN_CL = UCAST(32 \<rightarrow> 32) nonexecutable && mask 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (if page_size = page_size then Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, XN_CL = nonexecutable\<rparr> else Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<noteq> page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = UCAST(32 \<rightarrow> 32) paddr && ~~ mask 16, XN_CL = UCAST(32 \<rightarrow> 32) nonexecutable && mask 1, TEX_CL = SCAST(32 signed \<rightarrow> 32) 5 && mask 3, nG_CL = SCAST(32 signed \<rightarrow> 32) 1 && mask 1, S_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, APX_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, AP_CL = UCAST(32 \<rightarrow> 32) (ap_from_vm_rights (vmrights_to_H vm_rights)) && mask 2, C_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, B_CL = SCAST(32 signed \<rightarrow> 32) 1 && mask 1, reserved_CL = SCAST(32 signed \<rightarrow> 32) 1 && mask 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (if page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage then Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, XN_CL = nonexecutable\<rparr> else Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = UCAST(32 \<rightarrow> 32) paddr && ~~ mask 16, XN_CL = UCAST(32 \<rightarrow> 32) nonexecutable && mask 1, TEX_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 3, nG_CL = SCAST(32 signed \<rightarrow> 32) 1 && mask 1, S_CL = SCAST(32 signed \<rightarrow> 32) 1 && mask 1, APX_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, AP_CL = UCAST(32 \<rightarrow> 32) (ap_from_vm_rights (vmrights_to_H vm_rights)) && mask 2, C_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, B_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, reserved_CL = SCAST(32 signed \<rightarrow> 32) 1 && mask 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (if page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage then Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, XN_CL = nonexecutable\<rparr> else Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size)) proof (prove)
goal (1 subgoal):
 1. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; is_aligned paddr (pageBitsForSize (gen_framesize_to_H page_size)); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable\<rbrakk> \<Longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr && ~~ mask 12, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, XN_CL = nonexecutable\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr && ~~ mask 12, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, TEX_CL = tex_bits_from_cacheable 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, XN_CL = nonexecutable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<noteq> page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size) proof (prove)
goal (2 subgoals):
 1. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; is_aligned paddr (pageBitsForSize (gen_framesize_to_H page_size)); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable\<rbrakk> \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr && ~~ mask 12, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, XN_CL = nonexecutable\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr && ~~ mask 12, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, TEX_CL = tex_bits_from_cacheable 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, XN_CL = nonexecutable\<rparr>)))
 2. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; is_aligned paddr (pageBitsForSize (gen_framesize_to_H page_size)); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable\<rbrakk> \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<noteq> page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size proof (prove)
goal (2 subgoals):
 1. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; is_aligned paddr (pageBitsForSize (gen_framesize_to_H page_size)); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage = page_size\<rbrakk> \<Longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr && ~~ mask 12, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, XN_CL = nonexecutable\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr && ~~ mask 12, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, TEX_CL = tex_bits_from_cacheable 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, XN_CL = nonexecutable\<rparr>)))
 2. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; is_aligned paddr (pageBitsForSize (gen_framesize_to_H page_size)); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable\<rbrakk> \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<noteq> page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size proof (prove)
goal (3 subgoals):
 1. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage = page_size\<rbrakk> \<Longrightarrow> 12 \<le> pageBitsForSize (gen_framesize_to_H page_size)
 2. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage = page_size; is_aligned paddr 12\<rbrakk> \<Longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr && ~~ mask 12, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, XN_CL = nonexecutable\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr && ~~ mask 12, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, TEX_CL = tex_bits_from_cacheable 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, XN_CL = nonexecutable\<rparr>)))
 3. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; is_aligned paddr (pageBitsForSize (gen_framesize_to_H page_size)); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable\<rbrakk> \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<noteq> page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size proof (prove)
goal (2 subgoals):
 1. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage = page_size; is_aligned paddr 12\<rbrakk> \<Longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr && ~~ mask 12, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, XN_CL = nonexecutable\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr && ~~ mask 12, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, TEX_CL = tex_bits_from_cacheable 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, XN_CL = nonexecutable\<rparr>)))
 2. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; is_aligned paddr (pageBitsForSize (gen_framesize_to_H page_size)); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable\<rbrakk> \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<noteq> page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size proof (prove)
goal (2 subgoals):
 1. \<And>nonexecutable vm_rights cacheable paddr. \<lbrakk>vm_rights < 4; cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; is_aligned paddr 12\<rbrakk> \<Longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, XN_CL = nonexecutable\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, TEX_CL = tex_bits_from_cacheable 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, XN_CL = nonexecutable\<rparr>)))
 2. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; is_aligned paddr (pageBitsForSize (gen_framesize_to_H page_size)); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable\<rbrakk> \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<noteq> page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size proof (prove)
goal (3 subgoals):
 1. \<And>nonexecutable vm_rights cacheable paddr ret__struct_pte_C. \<lbrakk>vm_rights < 4; cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; is_aligned paddr 12; cacheable \<noteq> 0; pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small\<rbrakk> \<Longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, XN_CL = nonexecutable\<rparr>)
 2. \<And>nonexecutable vm_rights cacheable paddr ret__struct_pte_C. \<lbrakk>vm_rights < 4; cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; is_aligned paddr 12; cacheable = 0; pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small\<rbrakk> \<Longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, TEX_CL = tex_bits_from_cacheable 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, XN_CL = nonexecutable\<rparr>)
 3. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; is_aligned paddr (pageBitsForSize (gen_framesize_to_H page_size)); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable\<rbrakk> \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<noteq> page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size proof (prove)
goal (2 subgoals):
 1. \<And>nonexecutable vm_rights cacheable paddr ret__struct_pte_C. \<lbrakk>vm_rights < 4; cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; is_aligned paddr 12\<rbrakk> \<Longrightarrow> (\<lbrakk>cacheable \<noteq> 0; pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small\<rbrakk> \<Longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, XN_CL = nonexecutable\<rparr>)) &&& (\<lbrakk>cacheable = 0; pte_pte_small_lift ret__struct_pte_C = \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, XN_CL = nonexecutable\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_small\<rbrakk> \<Longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, TEX_CL = tex_bits_from_cacheable 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, XN_CL = nonexecutable\<rparr>))
 2. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; is_aligned paddr (pageBitsForSize (gen_framesize_to_H page_size)); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable\<rbrakk> \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<noteq> page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>cacheable_ \<noteq> 0; pte_pte_small_lift ret__struct_pte_C_ = \<lparr>pte_pte_small_CL.address_CL = paddr_, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights_) && mask 2, C_CL = 0, B_CL = 1, XN_CL = nonexecutable_\<rparr> \<and> pte_get_tag ret__struct_pte_C_ = SCAST(32 signed \<rightarrow> 32) pte_pte_small\<rbrakk> \<Longrightarrow> pte_lift ret__struct_pte_C_ = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr_, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable_, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable_, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights_), C_CL = 0, B_CL = iwb_from_cacheable cacheable_, XN_CL = nonexecutable_\<rparr>)) &&& (\<lbrakk>cacheable_ = 0; pte_pte_small_lift ret__struct_pte_C_ = \<lparr>pte_pte_small_CL.address_CL = paddr_, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights_) && mask 2, C_CL = 0, B_CL = 0, XN_CL = nonexecutable_\<rparr> \<and> pte_get_tag ret__struct_pte_C_ = SCAST(32 signed \<rightarrow> 32) pte_pte_small\<rbrakk> \<Longrightarrow> pte_lift ret__struct_pte_C_ = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr_, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, TEX_CL = tex_bits_from_cacheable 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights_), C_CL = 0, B_CL = iwb_from_cacheable 0, XN_CL = nonexecutable_\<rparr>)) proof (prove)
using this:
vm_rights_ < 4
cacheable_ && 1 = cacheable_
nonexecutable_ && 1 = nonexecutable_
is_aligned paddr_ 12

goal (1 subgoal):
 1. (\<lbrakk>cacheable_ \<noteq> 0; pte_pte_small_lift ret__struct_pte_C_ = \<lparr>pte_pte_small_CL.address_CL = paddr_, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights_) && mask 2, C_CL = 0, B_CL = 1, XN_CL = nonexecutable_\<rparr> \<and> pte_get_tag ret__struct_pte_C_ = SCAST(32 signed \<rightarrow> 32) pte_pte_small\<rbrakk> \<Longrightarrow> pte_lift ret__struct_pte_C_ = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr_, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable_, APX_CL = 0, TEX_CL = tex_bits_from_cacheable cacheable_, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights_), C_CL = 0, B_CL = iwb_from_cacheable cacheable_, XN_CL = nonexecutable_\<rparr>)) &&& (\<lbrakk>cacheable_ = 0; pte_pte_small_lift ret__struct_pte_C_ = \<lparr>pte_pte_small_CL.address_CL = paddr_, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights_) && mask 2, C_CL = 0, B_CL = 0, XN_CL = nonexecutable_\<rparr> \<and> pte_get_tag ret__struct_pte_C_ = SCAST(32 signed \<rightarrow> 32) pte_pte_small\<rbrakk> \<Longrightarrow> pte_lift ret__struct_pte_C_ = Some (Pte_pte_small \<lparr>pte_pte_small_CL.address_CL = paddr_, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, TEX_CL = tex_bits_from_cacheable 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights_), C_CL = 0, B_CL = iwb_from_cacheable 0, XN_CL = nonexecutable_\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>nonexecutable vm_rights page_size cacheable paddr. \<lbrakk>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<or> page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage; vm_rights < 4; is_aligned paddr (pageBitsForSize (gen_framesize_to_H page_size)); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable\<rbrakk> \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<noteq> page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size \<longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = page_size proof (prove)
goal (1 subgoal):
 1. \<And>nonexecutable vm_rights cacheable paddr. \<lbrakk>vm_rights < 4; is_aligned paddr (pageBitsForSize (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage))); cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; Kernel_C.ARMSmallPage \<noteq> Kernel_C.ARMLargePage\<rbrakk> \<Longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>nonexecutable vm_rights cacheable paddr. \<lbrakk>vm_rights < 4; cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; Kernel_C.ARMSmallPage \<noteq> Kernel_C.ARMLargePage\<rbrakk> \<Longrightarrow> 16 \<le> pageBitsForSize (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage))
 2. \<And>nonexecutable vm_rights cacheable paddr. \<lbrakk>vm_rights < 4; cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; Kernel_C.ARMSmallPage \<noteq> Kernel_C.ARMLargePage; is_aligned paddr 16\<rbrakk> \<Longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>nonexecutable vm_rights cacheable paddr. \<lbrakk>vm_rights < 4; cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; Kernel_C.ARMSmallPage \<noteq> Kernel_C.ARMLargePage; is_aligned paddr 16\<rbrakk> \<Longrightarrow> (cacheable \<noteq> 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>))) \<and> (cacheable = 0 \<longrightarrow> (\<forall>ret__struct_pte_C. pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>nonexecutable vm_rights cacheable paddr ret__struct_pte_C. \<lbrakk>vm_rights < 4; cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; Kernel_C.ARMSmallPage \<noteq> Kernel_C.ARMLargePage; is_aligned paddr 16; cacheable \<noteq> 0; pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 5 && mask 3, nG_CL = 1, S_CL = 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 1, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large\<rbrakk> \<Longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable cacheable, nG_CL = 1, S_CL = shared_bit_from_cacheable cacheable, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable cacheable, reserved_CL = 1\<rparr>)
 2. \<And>nonexecutable vm_rights cacheable paddr ret__struct_pte_C. \<lbrakk>vm_rights < 4; cacheable && 1 = cacheable; nonexecutable && 1 = nonexecutable; Kernel_C.ARMSmallPage \<noteq> Kernel_C.ARMLargePage; is_aligned paddr 16; cacheable = 0; pte_pte_large_lift ret__struct_pte_C = \<lparr>pte_pte_large_CL.address_CL = paddr && ~~ mask 16, XN_CL = nonexecutable, TEX_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights) && mask 2, C_CL = 0, B_CL = 0, reserved_CL = 1\<rparr> \<and> pte_get_tag ret__struct_pte_C = SCAST(32 signed \<rightarrow> 32) pte_pte_large\<rbrakk> \<Longrightarrow> pte_lift ret__struct_pte_C = Some (Pte_pte_large \<lparr>pte_pte_large_CL.address_CL = paddr, XN_CL = nonexecutable, TEX_CL = tex_bits_from_cacheable 0, nG_CL = 1, S_CL = shared_bit_from_cacheable 0, APX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H vm_rights), C_CL = 0, B_CL = iwb_from_cacheable 0, reserved_CL = 1\<rparr>) proof (prove)
goal:
No subgoals!