theory structures_proofs

lemma (in kernel_all_substitute) pde_pde_section_ptr_get_address_spec:
    defines "ptrval s \<equiv> cslift s \<^bsup>s\<^esup>pde_ptr"
    shows "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>pde_ptr \<and> pde_get_tag (the (ptrval s)) = scast pde_pde_section\<rbrace>
            \<acute>ret__unsigned :== PROC pde_pde_section_ptr_get_address(\<acute>pde_ptr)
            \<lbrace>\<acute>ret__unsigned = pde_pde_section_CL.address_CL (pde_pde_section_lift (the (ptrval s)))\<rbrace> " unfolding ptrval_def apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff guard_simps
                        mask_shift_simps sign_extend_def' nth_is_and_neq_0
                        pde_lift_pde_section pde_pde_section_lift_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>pde_ptr \<and> pde_get_tag (the (ptrval s)) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrace> Call pde_pde_section_ptr_get_address_'proc \<lbrace>\<acute>ret__unsigned = pde_pde_section_CL.address_CL (pde_pde_section_lift (the (ptrval s)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>pde_ptr \<and> pde_get_tag (the (cslift s \<^bsup>s\<^esup>pde_ptr)) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrace> Call pde_pde_section_ptr_get_address_'proc \<lbrace>\<acute>ret__unsigned = pde_pde_section_CL.address_CL (pde_pde_section_lift (the (cslift s \<^bsup>s\<^esup>pde_ptr)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>pde_ptr \<and> pde_get_tag (the (cslift s \<^bsup>s\<^esup>pde_ptr)) = SCAST(32 signed \<rightarrow> 32) pde_pde_section\<rbrace> \<subseteq> {sa. \<forall>v. 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 1 \<and> 0 \<le>s 0 \<and> sa \<Turnstile>\<^sub>c pde_ptr_' sa \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[1]) &(pde_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 0xFFF00000 << unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[1]) &(pde_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 0xFFF00000 << unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = pde_pde_section_CL.address_CL (pde_pde_section_lift (the (cslift s (pde_ptr_' s))))) \<and> ((if (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[1]) &(pde_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 0xFFF00000 << unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[1]) &(pde_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 0xFFF00000 << unat 0 = pde_pde_section_CL.address_CL (pde_pde_section_lift (the (cslift s (pde_ptr_' s)))))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[1]) &(pde_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && 0xFFF00000 << unat 0 = pde_pde_section_CL.address_CL (pde_pde_section_lift (the (cslift s (pde_ptr_' s)))))} proof (prove)
goal:
No subgoals!