theory Fastpath_C

lemma endpoint_ptr_set_epQueue_head_np_spec:
  "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. hrs_htd \<^bsup>s\<^esup>t_hrs \<Turnstile>\<^sub>t ep_ptr_' s \<and> is_aligned (epQueue_head_' s) 4\<rbrace>
              Call endpoint_ptr_set_epQueue_head_np_'proc
       {t. (\<exists>endpoint.
               endpoint_lift endpoint = endpoint_lift (the (cslift s (ep_ptr_' s)))
                           \<lparr> epQueue_head_CL := epQueue_head_' s \<rparr>
               \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ep_ptr_' s)
                          endpoint)
                  (t_hrs_' (globals s))
           )}" apply (intro allI, rule conseqPre, vcg) apply (clarsimp simp: h_t_valid_clift_Some_iff typ_heap_simps'
                        word_sless_def word_sle_def) apply (rule exI, rule conjI[OF _ refl]) apply (simp add: endpoint_lift_def word_ao_dist
                   mask_def) apply (simp add: limited_and_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>ep_ptr \<and> is_aligned \<^bsup>s\<^esup>epQueue_head 4\<rbrace> Call endpoint_ptr_set_epQueue_head_np_'proc \<lbrace>\<exists>endpoint. endpoint_lift endpoint = endpoint_lift (the (cslift s \<^bsup>s\<^esup>ep_ptr))\<lparr>epQueue_head_CL := \<^bsup>s\<^esup>epQueue_head\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update \<^bsup>s\<^esup>ep_ptr endpoint) \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>ep_ptr \<and> is_aligned \<^bsup>s\<^esup>epQueue_head 4\<rbrace> \<subseteq> {sa. 1 <s 4 \<and> 0 \<le>s 1 \<and> sa \<Turnstile>\<^sub>c ep_ptr_' sa \<and> (\<exists>endpoint. endpoint_lift endpoint = endpoint_lift (the (cslift s (ep_ptr_' s)))\<lparr>epQueue_head_CL := epQueue_head_' s\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[4]) &(ep_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[4]) &(ep_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (UCAST(32 \<rightarrow> 32) (epQueue_head_' sa)))) (t_hrs_' (globals sa)) = hrs_mem_update (heap_update (ep_ptr_' s) endpoint) (t_hrs_' (globals s)))} proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (epQueue_head_' x) 4; cslift x (ep_ptr_' x) = Some v\<rbrakk> \<Longrightarrow> \<exists>endpoint. endpoint_lift endpoint = endpoint_lift v\<lparr>epQueue_head_CL := epQueue_head_' x\<rparr> \<and> hrs_mem_update (heap_update (ep_ptr_' x) (endpoint_C.words_C_update (\<lambda>_. Arrays.update (endpoint_C.words_C v) (Suc 0) (epQueue_head_' x)) v)) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (ep_ptr_' x) endpoint) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (epQueue_head_' x) 4; cslift x (ep_ptr_' x) = Some v\<rbrakk> \<Longrightarrow> endpoint_lift (endpoint_C.words_C_update (\<lambda>_. Arrays.update (endpoint_C.words_C v) (Suc 0) (epQueue_head_' x)) v) = endpoint_lift v\<lparr>epQueue_head_CL := epQueue_head_' x\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (epQueue_head_' x) 4; cslift x (ep_ptr_' x) = Some v\<rbrakk> \<Longrightarrow> epQueue_head_' x && 0xFFFFFFF0 = epQueue_head_' x proof (prove)
goal:
No subgoals!