theory structures_proofs

lemma (in kernel_all_substitute) pde_pde_section_new_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s}
       \<acute>ret__struct_pde_C :== PROC pde_pde_section_new(\<acute>address, \<acute>size, \<acute>nG, \<acute>S, \<acute>APX, \<acute>TEX, \<acute>AP, \<acute>P, \<acute>Domain, \<acute>XN, \<acute>C, \<acute>B)
       \<lbrace>pde_pde_section_lift \<acute>ret__struct_pde_C = \<lparr>
          pde_pde_section_CL.address_CL = (\<^bsup>s\<^esup>address___unsigned AND NOT (mask 20)),
          pde_pde_section_CL.size_CL = (\<^bsup>s\<^esup>size___unsigned AND mask 1),
          pde_pde_section_CL.nG_CL = (\<^bsup>s\<^esup>nG___unsigned AND mask 1),
          pde_pde_section_CL.S_CL = (\<^bsup>s\<^esup>S___unsigned AND mask 1),
          pde_pde_section_CL.APX_CL = (\<^bsup>s\<^esup>APX___unsigned AND mask 1),
          pde_pde_section_CL.TEX_CL = (\<^bsup>s\<^esup>TEX___unsigned AND mask 3),
          pde_pde_section_CL.AP_CL = (\<^bsup>s\<^esup>AP___unsigned AND mask 2),
          pde_pde_section_CL.P_CL = (\<^bsup>s\<^esup>P___unsigned AND mask 1),
          pde_pde_section_CL.Domain_CL = (\<^bsup>s\<^esup>Domain___unsigned AND mask 4),
          pde_pde_section_CL.XN_CL = (\<^bsup>s\<^esup>XN___unsigned AND mask 1),
          pde_pde_section_CL.C_CL = (\<^bsup>s\<^esup>C___unsigned AND mask 1),
          pde_pde_section_CL.B_CL = (\<^bsup>s\<^esup>B___unsigned AND mask 1) \<rparr> \<and>
        pde_get_tag \<acute>ret__struct_pde_C = scast pde_pde_section\<rbrace>" apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps o_def mask_def shift_over_ao_dists) apply (rule context_conjI[THEN iffD1[OF conj_commute]],
         fastforce simp: pde_get_tag_eq_x pde_pde_section_def
                         mask_def shift_over_ao_dists word_bw_assocs word_ao_dist) apply (simp add: pde_pde_section_lift_def) apply (erule pde_lift_pde_section[THEN subst[OF sym]]; simp?) apply ((intro conjI sign_extend_eq)?;
         (simp add: mask_def shift_over_ao_dists multi_shift_simps word_size
                    word_ao_dist word_bw_assocs word_and_max_simps pde_pde_section_def))? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call pde_pde_section_new_'proc \<lbrace>pde_pde_section_lift \<acute>ret__struct_pde_C = \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>address && ~~ mask 20, size_CL = \<^bsup>s\<^esup>size && mask 1, nG_CL = \<^bsup>s\<^esup>nG && mask 1, S_CL = \<^bsup>s\<^esup>S && mask 1, APX_CL = \<^bsup>s\<^esup>APX && mask 1, TEX_CL = \<^bsup>s\<^esup>TEX && mask 3, AP_CL = \<^bsup>s\<^esup>AP && mask 2, P_CL = \<^bsup>s\<^esup>P && mask 1, Domain_CL = \<^bsup>s\<^esup>Domain && mask 4, XN_CL = \<^bsup>s\<^esup>XN && mask 1, C_CL = \<^bsup>s\<^esup>C && mask 1, B_CL = \<^bsup>s\<^esup>B && mask 1\<rparr> \<and> pde_get_tag \<acute>ret__struct_pde_C = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v. 0 <s 1 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 \<le>s 2 \<and> 2 <s 0x20 \<and> 0 \<le>s 3 \<and> 3 <s 0x20 \<and> 0 \<le>s 4 \<and> 4 <s 0x20 \<and> 0 \<le>s 5 \<and> 5 <s 0x20 \<and> 0 \<le>s 9 \<and> 9 <s 0x20 \<and> 0 \<le>s 0xA \<and> 0xA <s 0x20 \<and> 0 \<le>s 0xC \<and> 0xC <s 0x20 \<and> 0 \<le>s 0xF \<and> 0xF <s 0x20 \<and> 0 \<le>s 0x10 \<and> 0x10 <s 0x20 \<and> 0 \<le>s 0x11 \<and> 0x11 <s 0x20 \<and> 0 \<le>s 0x12 \<and> 0x12 <s 0x20 \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> pde_pde_section_lift (pde_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (((((((((((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>address && 0xFFF00000 >> unat 0)) || (\<acute>size && 1 << unat 0x12)) || (\<acute>nG && 1 << unat 0x11)) || (\<acute>S && 1 << unat 0x10)) || (\<acute>APX && 1 << unat 0xF)) || (\<acute>TEX && 7 << unat 0xC)) || (\<acute>AP && 3 << unat 0xA)) || (\<acute>P && 1 << unat 9)) || (\<acute>Domain && 0xF << unat 5)) || (\<acute>XN && 1 << unat 4)) || (\<acute>C && 1 << unat 3)) || (\<acute>B && 1 << unat 2)) || (SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 << unat 0))) v) = \<lparr>pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>address && ~~ mask 20, size_CL = \<^bsup>s\<^esup>size && mask 1, nG_CL = \<^bsup>s\<^esup>nG && mask 1, S_CL = \<^bsup>s\<^esup>S && mask 1, APX_CL = \<^bsup>s\<^esup>APX && mask 1, TEX_CL = \<^bsup>s\<^esup>TEX && mask 3, AP_CL = \<^bsup>s\<^esup>AP && mask 2, P_CL = \<^bsup>s\<^esup>P && mask 1, Domain_CL = \<^bsup>s\<^esup>Domain && mask 4, XN_CL = \<^bsup>s\<^esup>XN && mask 1, C_CL = \<^bsup>s\<^esup>C && mask 1, B_CL = \<^bsup>s\<^esup>B && mask 1\<rparr> \<and> pde_get_tag (pde_C.words_C_update (\<lambda>v. Arrays.update v (unat 0) (((((((((((((SCAST(32 signed \<rightarrow> 32) 0 || (\<acute>address && 0xFFF00000 >> unat 0)) || (\<acute>size && 1 << unat 0x12)) || (\<acute>nG && 1 << unat 0x11)) || (\<acute>S && 1 << unat 0x10)) || (\<acute>APX && 1 << unat 0xF)) || (\<acute>TEX && 7 << unat 0xC)) || (\<acute>AP && 3 << unat 0xA)) || (\<acute>P && 1 << unat 9)) || (\<acute>Domain && 0xF << unat 5)) || (\<acute>XN && 1 << unat 4)) || (\<acute>C && 1 << unat 3)) || (\<acute>B && 1 << unat 2)) || (SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 << unat 0))) v) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s v. pde_pde_section_lift (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3)) v) = \<lparr>pde_pde_section_CL.address_CL = address_' s && 0xFFF00000, size_CL = size_' s && 1, nG_CL = nG_' s && 1, S_CL = S_' s && 1, APX_CL = APX_' s && 1, TEX_CL = TEX_' s && 7, AP_CL = AP_' s && 3, P_CL = P_' s && 1, Domain_CL = Domain_' s && 0xF, XN_CL = XN_' s && 1, C_CL = C_' s && 1, B_CL = B_' s && 1\<rparr> \<and> pde_get_tag (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3)) v) = SCAST(32 signed \<rightarrow> 32) pde_pde_section proof (prove)
goal (1 subgoal):
 1. \<And>s v. pde_get_tag (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3)) v) = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<Longrightarrow> pde_pde_section_lift (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3)) v) = \<lparr>pde_pde_section_CL.address_CL = address_' s && 0xFFF00000, size_CL = size_' s && 1, nG_CL = nG_' s && 1, S_CL = S_' s && 1, APX_CL = APX_' s && 1, TEX_CL = TEX_' s && 7, AP_CL = AP_' s && 3, P_CL = P_' s && 1, Domain_CL = Domain_' s && 0xF, XN_CL = XN_' s && 1, C_CL = C_' s && 1, B_CL = B_' s && 1\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s v. pde_get_tag (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3)) v) = SCAST(32 signed \<rightarrow> 32) pde_pde_section \<Longrightarrow> (case pde_lift (pde_C.words_C_update (\<lambda>v. Arrays.update v 0 ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3)) v) of Some (Pde_pde_section rec) \<Rightarrow> rec) = \<lparr>pde_pde_section_CL.address_CL = address_' s && 0xFFF00000, size_CL = size_' s && 1, nG_CL = nG_' s && 1, S_CL = S_' s && 1, APX_CL = APX_' s && 1, TEX_CL = TEX_' s && 7, AP_CL = AP_' s && 3, P_CL = P_' s && 1, Domain_CL = Domain_' s && 0xF, XN_CL = XN_' s && 1, C_CL = C_' s && 1, B_CL = B_' s && 1\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3) && ~~ mask 20 = address_' s && 0xFFF00000 \<and> ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 >> 18) && 1 = size_' s && 1 \<and> ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 >> 17) && 1 = nG_' s && 1 \<and> ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 >> 16) && 1 = S_' s && 1 \<and> ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 >> 15) && 1 = APX_' s && 1 \<and> ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 >> 12) && mask 3 = TEX_' s && 7 \<and> ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 >> 10) && mask 2 = AP_' s && 3 \<and> ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 >> 9) && 1 = P_' s && 1 \<and> ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 >> 5) && mask 4 = Domain_' s && 0xF \<and> ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 >> 4) && 1 = XN_' s && 1 \<and> ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 >> 3) && 1 = C_' s && 1 \<and> ((((((((((((address_' s && 0xFFF00000 || (size_' s << 18) && 0x40000) || (nG_' s << 17) && 0x20000) || (S_' s << 16) && 0x10000) || (APX_' s << 15) && 0x8000) || (TEX_' s << 12) && 0x7000) || (AP_' s << 10) && 0xC00) || (P_' s << 9) && 0x200) || (Domain_' s << 5) && 0x1E0) || (XN_' s << 4) && 0x10) || (C_' s << 3) && 8) || (B_' s << 2) && 4) || SCAST(32 signed \<rightarrow> 32) pde_pde_section && 3 >> 2) && 1 = B_' s && 1 proof (prove)
goal:
No subgoals!