theory VSpace_C

lemma makeUserPDE_spec:
  "\<forall>s. \<Gamma> \<turnstile>
  \<lbrace>s. (\<acute>page_size = scast Kernel_C.ARMSection \<or> \<acute>page_size = scast Kernel_C.ARMSuperSection) \<and>
      \<acute>vm_rights < 4 \<and> vmsz_aligned' (\<acute>paddr) (gen_framesize_to_H \<acute>page_size)  \<and>
      \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and>
      \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace>
  Call makeUserPDE_'proc
  \<lbrace> pde_lift \<acute>ret__struct_pde_C = Some (Pde_pde_section \<lparr>
       pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr,
       size_CL = if \<^bsup>s\<^esup>page_size = scast Kernel_C.ARMSection then 0 else 1,
       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),
       P_CL = \<^bsup>s\<^esup>parity,
       Domain_CL = \<^bsup>s\<^esup>domain,
       XN_CL = \<^bsup>s\<^esup>nonexecutable,
       C_CL = 0,
       B_CL = iwb_from_cacheable  \<^bsup>s\<^esup>cacheable
    \<rparr>) \<rbrace>" supply if_cong[cong] apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp:ap_from_vm_rights_mask split:if_splits) apply (intro conjI impI allI | clarsimp )+ apply (simp only:pde_pde_section_lift pde_pde_section_lift_def) apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def ap_from_vm_rights_mask) apply (clarsimp simp: Kernel_C.ARMSection_def Kernel_C.ARMSmallPage_def
       Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq ) apply (clarsimp simp:mask_def ap_from_vm_rights_mask
      shared_bit_from_cacheable_def tex_bits_from_cacheable_def
      iwb_from_cacheable_def
      split:if_splits dest!:mask_eq1_nochoice) apply (simp only:pde_pde_section_lift pde_pde_section_lift_def) apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def ap_from_vm_rights_mask) apply (clarsimp simp: Kernel_C.ARMSection_def Kernel_C.ARMSmallPage_def
       Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq) apply (clarsimp simp:ap_from_vm_rights_mask mask_def
     shared_bit_from_cacheable_def tex_bits_from_cacheable_def
     iwb_from_cacheable_def
     split:if_splits dest!:mask_eq1_nochoice) apply (clarsimp) apply (intro conjI impI allI) apply (simp add:pde_pde_section_lift pde_pde_section_lift_def) apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def ap_from_vm_rights_mask) apply (drule is_aligned_weaken[where y = 20]) apply (clarsimp simp: Kernel_C.ARMSuperSection_def Kernel_C.ARMSmallPage_def
       Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq)+ apply (clarsimp simp:mask_def ap_from_vm_rights_mask
     shared_bit_from_cacheable_def tex_bits_from_cacheable_def
     iwb_from_cacheable_def
     split:if_splits dest!:mask_eq1_nochoice) apply (simp add:pde_pde_section_lift pde_pde_section_lift_def) apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def ap_from_vm_rights_mask) apply (drule is_aligned_weaken[where y = 20]) apply (clarsimp simp: Kernel_C.ARMSuperSection_def Kernel_C.ARMSmallPage_def
       Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq)+ apply (clarsimp simp:mask_def ap_from_vm_rights_mask
     shared_bit_from_cacheable_def tex_bits_from_cacheable_def
     iwb_from_cacheable_def
     split:if_splits dest!:mask_eq1_nochoice) 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.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> Call makeUserPDE_'proc \<lbrace>pde_lift \<acute>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = if \<^bsup>s\<^esup>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then 0 else 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> Call makeUserPDE_'proc \<lbrace>pde_lift \<acute>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = if \<^bsup>s\<^esup>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then 0 else 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> \<subseteq> \<lbrace>\<forall>v va. \<acute>vm_rights < 4 \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = UCAST(32 \<rightarrow> 32) \<acute>paddr && ~~ mask 20, size_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) 0) && mask 1, 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 \<acute>vm_rights)) && mask 2, P_CL = UCAST(32 \<rightarrow> 32) \<acute>parity && mask 1, Domain_CL = UCAST(32 \<rightarrow> 32) \<acute>domain && mask 4, XN_CL = UCAST(32 \<rightarrow> 32) \<acute>nonexecutable && mask 1, C_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, B_CL = SCAST(32 signed \<rightarrow> 32) 1 && mask 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = if \<^bsup>s\<^esup>page_size = \<acute>page_size then 0 else 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = UCAST(32 \<rightarrow> 32) \<acute>paddr && ~~ mask 20, size_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) 0) && mask 1, 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 \<acute>vm_rights)) && mask 2, P_CL = UCAST(32 \<rightarrow> 32) \<acute>parity && mask 1, Domain_CL = UCAST(32 \<rightarrow> 32) \<acute>domain && mask 4, XN_CL = UCAST(32 \<rightarrow> 32) \<acute>nonexecutable && mask 1, C_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, B_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = if \<^bsup>s\<^esup>page_size = \<acute>page_size then 0 else 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = UCAST(32 \<rightarrow> 32) \<acute>paddr && ~~ mask 20, size_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) 1) && mask 1, 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 \<acute>vm_rights)) && mask 2, P_CL = UCAST(32 \<rightarrow> 32) \<acute>parity && mask 1, Domain_CL = UCAST(32 \<rightarrow> 32) \<acute>domain && mask 4, XN_CL = UCAST(32 \<rightarrow> 32) \<acute>nonexecutable && mask 1, C_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, B_CL = SCAST(32 signed \<rightarrow> 32) 1 && mask 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = if \<^bsup>s\<^esup>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then 0 else 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = UCAST(32 \<rightarrow> 32) \<acute>paddr && ~~ mask 20, size_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) 1) && mask 1, 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 \<acute>vm_rights)) && mask 2, P_CL = UCAST(32 \<rightarrow> 32) \<acute>parity && mask 1, Domain_CL = UCAST(32 \<rightarrow> 32) \<acute>domain && mask 4, XN_CL = UCAST(32 \<rightarrow> 32) \<acute>nonexecutable && mask 1, C_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1, B_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = if \<^bsup>s\<^esup>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection then 0 else 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (page_size_' s = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<longrightarrow> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> \<subseteq> \<lbrace>\<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size))\<rbrace>) \<and> (page_size_' s \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<longrightarrow> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> \<subseteq> \<lbrace>(\<^bsup>s\<^esup>page_size = \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<forall>t. pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size))) \<and> (\<^bsup>s\<^esup>page_size \<noteq> \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size)))\<rbrace>) proof (prove)
goal (3 subgoals):
 1. \<And>x t ta. \<lbrakk>page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x \<noteq> 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr>; pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 0, nG_CL = 1, S_CL = shared_bit_from_cacheable (cacheable_' x), APX_CL = 0, TEX_CL = tex_bits_from_cacheable (cacheable_' x), AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable (cacheable_' x)\<rparr>)
 2. \<And>x t ta. \<lbrakk>page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 0, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>)
 3. \<And>s. page_size_' s \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<Longrightarrow> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> \<subseteq> \<lbrace>(\<^bsup>s\<^esup>page_size = \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<forall>t. pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size))) \<and> (\<^bsup>s\<^esup>page_size \<noteq> \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size)))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x t ta. \<lbrakk>page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x \<noteq> 0; (case Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr>) of Some (Pde_pde_section rec) \<Rightarrow> rec) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr>; pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr>)\<rbrakk> \<Longrightarrow> Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr>) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 0, nG_CL = 1, S_CL = shared_bit_from_cacheable (cacheable_' x), APX_CL = 0, TEX_CL = tex_bits_from_cacheable (cacheable_' x), AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable (cacheable_' x)\<rparr>)
 2. \<And>x t ta. \<lbrakk>page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 0, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>)
 3. \<And>s. page_size_' s \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<Longrightarrow> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> \<subseteq> \<lbrace>(\<^bsup>s\<^esup>page_size = \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<forall>t. pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size))) \<and> (\<^bsup>s\<^esup>page_size \<noteq> \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size)))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x t ta. \<lbrakk>page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection; vm_rights_' x < 4; is_aligned (paddr_' x) (pageBitsForSize (if Kernel_C.ARMSection = Kernel_C.ARMSmallPage then Wellformed_C.ARMSmallPage else if Kernel_C.ARMSection = Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else Wellformed_C.ARMSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x \<noteq> 0; pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr>)\<rbrakk> \<Longrightarrow> paddr_' x && ~~ mask 20 = paddr_' x \<and> shared_bit_from_cacheable (cacheable_' x) = 0 \<and> 5 && mask 3 = tex_bits_from_cacheable (cacheable_' x) \<and> ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2 = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) \<and> domain_' x && mask 4 = domain_' x \<and> iwb_from_cacheable (cacheable_' x) = 1
 2. \<And>x t ta. \<lbrakk>page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 0, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>)
 3. \<And>s. page_size_' s \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<Longrightarrow> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> \<subseteq> \<lbrace>(\<^bsup>s\<^esup>page_size = \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<forall>t. pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size))) \<and> (\<^bsup>s\<^esup>page_size \<noteq> \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size)))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x t ta. \<lbrakk>page_size_' x = 2; vm_rights_' x < 4; is_aligned (paddr_' x) 20; parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x \<noteq> 0; pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 0, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr>)\<rbrakk> \<Longrightarrow> shared_bit_from_cacheable (cacheable_' x) = 0 \<and> 5 && mask 3 = tex_bits_from_cacheable (cacheable_' x) \<and> ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2 = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) \<and> domain_' x && mask 4 = domain_' x \<and> iwb_from_cacheable (cacheable_' x) = 1
 2. \<And>x t ta. \<lbrakk>page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 0, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>)
 3. \<And>s. page_size_' s \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<Longrightarrow> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> \<subseteq> \<lbrace>(\<^bsup>s\<^esup>page_size = \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<forall>t. pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size))) \<and> (\<^bsup>s\<^esup>page_size \<noteq> \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size)))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x t ta. \<lbrakk>page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 0, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>)
 2. \<And>s. page_size_' s \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<Longrightarrow> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> \<subseteq> \<lbrace>(\<^bsup>s\<^esup>page_size = \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<forall>t. pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size))) \<and> (\<^bsup>s\<^esup>page_size \<noteq> \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size)))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x t ta. \<lbrakk>page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; 0 && 1 = 0; nonexecutable_' x && 1 = nonexecutable_' x; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec))\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 0, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>)
 2. \<And>s. page_size_' s \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<Longrightarrow> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> \<subseteq> \<lbrace>(\<^bsup>s\<^esup>page_size = \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<forall>t. pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size))) \<and> (\<^bsup>s\<^esup>page_size \<noteq> \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size)))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x t ta. \<lbrakk>page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection; vm_rights_' x < 4; is_aligned (paddr_' x) (pageBitsForSize (if Kernel_C.ARMSection = Kernel_C.ARMSmallPage then Wellformed_C.ARMSmallPage else if Kernel_C.ARMSection = Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else Wellformed_C.ARMSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; nonexecutable_' x && 1 = nonexecutable_' x; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec))\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 0, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>)
 2. \<And>s. page_size_' s \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<Longrightarrow> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> \<subseteq> \<lbrace>(\<^bsup>s\<^esup>page_size = \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<forall>t. pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size))) \<and> (\<^bsup>s\<^esup>page_size \<noteq> \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size)))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x t ta. \<lbrakk>page_size_' x = 2; vm_rights_' x < 4; is_aligned (paddr_' x) 20; parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; nonexecutable_' x && 1 = nonexecutable_' x; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr>)\<rbrakk> \<Longrightarrow> shared_bit_from_cacheable 0 = 1 \<and> tex_bits_from_cacheable 0 = 0 \<and> ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2 = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) \<and> domain_' x && mask 4 = domain_' x \<and> iwb_from_cacheable 0 = 0
 2. \<And>s. page_size_' s \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<Longrightarrow> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> \<subseteq> \<lbrace>(\<^bsup>s\<^esup>page_size = \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<forall>t. pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size))) \<and> (\<^bsup>s\<^esup>page_size \<noteq> \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. page_size_' s \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<Longrightarrow> \<lbrace>s. (\<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<or> \<acute>page_size = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection) \<and> \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> \<acute>parity && 1 = \<acute>parity \<and> \<acute>domain && 0xF = \<acute>domain \<and> \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> \<subseteq> \<lbrace>(\<^bsup>s\<^esup>page_size = \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<forall>t. pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 0, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size))) \<and> (\<^bsup>s\<^esup>page_size \<noteq> \<acute>page_size \<longrightarrow> \<acute>vm_rights < 4 \<and> ((\<exists>t. \<^bsup>t\<^esup>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights)) \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 0, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> \<acute>page_size \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size \<longrightarrow> (\<acute>cacheable \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 0, APX_CL = 0, TEX_CL = 5 && mask 3, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>))) \<and> (\<acute>cacheable = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift \<^bsup>t\<^esup>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<acute>paddr && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H \<acute>vm_rights) && mask 2, P_CL = \<acute>parity && 1, Domain_CL = \<acute>domain && mask 4, XN_CL = \<acute>nonexecutable && 1, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag \<^bsup>t\<^esup>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift \<^bsup>t\<^esup>ret__struct_pde_C = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, size_CL = 1, 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), P_CL = \<^bsup>s\<^esup>parity, Domain_CL = \<^bsup>s\<^esup>domain, XN_CL = \<^bsup>s\<^esup>nonexecutable, C_CL = 0, B_CL = iwb_from_cacheable \<^bsup>s\<^esup>cacheable\<rparr>)))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = \<acute>page_size)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x))\<rbrakk> \<Longrightarrow> (cacheable_' x \<noteq> 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift (ret__struct_pde_C_' t) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift (ret__struct_pde_C_' t) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, nG_CL = 1, S_CL = shared_bit_from_cacheable (cacheable_' x), APX_CL = 0, TEX_CL = tex_bits_from_cacheable (cacheable_' x), AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable (cacheable_' x)\<rparr>))) \<and> (cacheable_' x = 0 \<longrightarrow> (\<forall>t. pde_pde_section_lift (ret__struct_pde_C_' t) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' t) = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<longrightarrow> pde_lift (ret__struct_pde_C_' t) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x \<noteq> 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, nG_CL = 1, S_CL = shared_bit_from_cacheable (cacheable_' x), APX_CL = 0, TEX_CL = tex_bits_from_cacheable (cacheable_' x), AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable (cacheable_' x)\<rparr>)
 2. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x \<noteq> 0; (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr> \<and> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec))\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, nG_CL = 1, S_CL = shared_bit_from_cacheable (cacheable_' x), APX_CL = 0, TEX_CL = tex_bits_from_cacheable (cacheable_' x), AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable (cacheable_' x)\<rparr>)
 2. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; is_aligned (paddr_' x) (pageBitsForSize (if Kernel_C.ARMSuperSection = Kernel_C.ARMSmallPage then Wellformed_C.ARMSmallPage else if Kernel_C.ARMSuperSection = Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else Wellformed_C.ARMSuperSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x \<noteq> 0; (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr> \<and> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec))\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, nG_CL = 1, S_CL = shared_bit_from_cacheable (cacheable_' x), APX_CL = 0, TEX_CL = tex_bits_from_cacheable (cacheable_' x), AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable (cacheable_' x)\<rparr>)
 2. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x \<noteq> 0; (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr> \<and> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec))\<rbrakk> \<Longrightarrow> 20 \<le> pageBitsForSize (if Kernel_C.ARMSuperSection = Kernel_C.ARMSmallPage then Wellformed_C.ARMSmallPage else if Kernel_C.ARMSuperSection = Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else Wellformed_C.ARMSuperSection)
 2. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x \<noteq> 0; (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr> \<and> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec)); is_aligned (paddr_' x) 20\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, nG_CL = 1, S_CL = shared_bit_from_cacheable (cacheable_' x), APX_CL = 0, TEX_CL = tex_bits_from_cacheable (cacheable_' x), AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable (cacheable_' x)\<rparr>)
 3. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x t ta. \<lbrakk>Kernel_C.ARMSection \<noteq> 3; vm_rights_' x < 4; parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = 3; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x \<noteq> 0; is_aligned (paddr_' x) 20; pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, 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_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 1\<rparr>)\<rbrakk> \<Longrightarrow> shared_bit_from_cacheable (cacheable_' x) = 0 \<and> 5 && mask 3 = tex_bits_from_cacheable (cacheable_' x) \<and> ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2 = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) \<and> domain_' x && mask 4 = domain_' x \<and> iwb_from_cacheable (cacheable_' x) = 1
 2. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; cacheable_' x && 1 = cacheable_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; pde_pde_section_lift (ret__struct_pde_C_' ta) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_get_tag (ret__struct_pde_C_' ta) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; vmsz_aligned' (paddr_' x) (gen_framesize_to_H (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec))\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; is_aligned (paddr_' x) (pageBitsForSize (if Kernel_C.ARMSuperSection = Kernel_C.ARMSmallPage then Wellformed_C.ARMSmallPage else if Kernel_C.ARMSuperSection = Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else Wellformed_C.ARMSuperSection)); parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec))\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec))\<rbrakk> \<Longrightarrow> 20 \<le> pageBitsForSize (if Kernel_C.ARMSuperSection = Kernel_C.ARMSmallPage then Wellformed_C.ARMSmallPage else if Kernel_C.ARMSuperSection = Kernel_C.ARMLargePage then Wellformed_C.ARMLargePage else Wellformed_C.ARMSuperSection)
 2. \<And>x t ta. \<lbrakk>Kernel_C.ARMSuperSection \<noteq> Kernel_C.ARMSection; vm_rights_' x < 4; parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec) = \<lparr>pde_pde_section_CL.address_CL = paddr_' x && ~~ mask 20, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr> \<and> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section (case pde_lift (ret__struct_pde_C_' ta) of Some (Pde_pde_section rec) \<Rightarrow> rec)); is_aligned (paddr_' x) 20\<rbrakk> \<Longrightarrow> pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, 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_' x)), P_CL = parity_' x, Domain_CL = domain_' x, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = iwb_from_cacheable 0\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x t ta. \<lbrakk>Kernel_C.ARMSection \<noteq> 3; vm_rights_' x < 4; parity_' x && 1 = parity_' x; domain_' x && 0xF = domain_' x; nonexecutable_' x && 1 = nonexecutable_' x; page_size_' x = 3; ret__unsigned_long_' t = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)); cacheable_' x = 0; is_aligned (paddr_' x) 20; pde_lift (ret__struct_pde_C_' ta) = Some (Pde_pde_section \<lparr>pde_pde_section_CL.address_CL = paddr_' x, size_CL = 1, nG_CL = 1, S_CL = 1, APX_CL = 0, TEX_CL = 0, AP_CL = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2, P_CL = parity_' x, Domain_CL = domain_' x && mask 4, XN_CL = nonexecutable_' x, C_CL = 0, B_CL = 0\<rparr>)\<rbrakk> \<Longrightarrow> shared_bit_from_cacheable 0 = 1 \<and> tex_bits_from_cacheable 0 = 0 \<and> ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) && mask 2 = ap_from_vm_rights (vmrights_to_H (vm_rights_' x)) \<and> domain_' x && mask 4 = domain_' x \<and> iwb_from_cacheable 0 = 0 proof (prove)
goal:
No subgoals!