theory Fastpath_C

lemma endpoint_ptr_mset_epQueue_tail_state_spec:
  "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. hrs_htd \<^bsup>s\<^esup>t_hrs \<Turnstile>\<^sub>t ep_ptr_' s \<and> is_aligned (epQueue_tail_' s) 4
                         \<and> state_' s && mask 2 = state_' s\<rbrace>
              Call endpoint_ptr_mset_epQueue_tail_state_'proc
       {t. (\<exists>endpoint.
               endpoint_lift endpoint = endpoint_lift (the (cslift s (ep_ptr_' s)))
                           \<lparr> endpoint_CL.state_CL := state_' s, epQueue_tail_CL := epQueue_tail_' 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_sle_def word_sless_def) apply (rule exI, rule conjI[OF _ refl]) apply (simp add: endpoint_lift_def word_ao_dist
                   mask_def) apply (fold limited_and_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_tail 4 \<and> \<^bsup>s\<^esup>state && mask 2 = \<^bsup>s\<^esup>state\<rbrace> Call endpoint_ptr_mset_epQueue_tail_state_'proc \<lbrace>\<exists>endpoint. endpoint_lift endpoint = endpoint_lift (the (cslift s \<^bsup>s\<^esup>ep_ptr))\<lparr>endpoint_CL.state_CL := \<^bsup>s\<^esup>state, epQueue_tail_CL := \<^bsup>s\<^esup>epQueue_tail\<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_tail 4 \<and> \<^bsup>s\<^esup>state && mask 2 = \<^bsup>s\<^esup>state\<rbrace> \<subseteq> {sa. 0 <s 4 \<and> 0 \<le>s 0 \<and> sa \<Turnstile>\<^sub>c ep_ptr_' sa \<and> (\<exists>endpoint. endpoint_lift endpoint = endpoint_lift (the (cslift s (ep_ptr_' s)))\<lparr>endpoint_CL.state_CL := state_' s, epQueue_tail_CL := epQueue_tail_' 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 0) (UCAST(32 \<rightarrow> 32) (epQueue_tail_' sa || state_' 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>cslift x (ep_ptr_' x) = Some v; is_aligned (epQueue_tail_' x) 4; state_' x && mask 2 = state_' x\<rbrakk> \<Longrightarrow> \<exists>endpoint. endpoint_lift endpoint = endpoint_lift v\<lparr>endpoint_CL.state_CL := state_' x, epQueue_tail_CL := epQueue_tail_' x\<rparr> \<and> hrs_mem_update (heap_update (ep_ptr_' x) (endpoint_C.words_C_update (\<lambda>_. Arrays.update (endpoint_C.words_C v) 0 (epQueue_tail_' x || state_' 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>cslift x (ep_ptr_' x) = Some v; is_aligned (epQueue_tail_' x) 4; state_' x && mask 2 = state_' x\<rbrakk> \<Longrightarrow> endpoint_lift (endpoint_C.words_C_update (\<lambda>_. Arrays.update (endpoint_C.words_C v) 0 (epQueue_tail_' x || state_' x)) v) = endpoint_lift v\<lparr>endpoint_CL.state_CL := state_' x, epQueue_tail_CL := epQueue_tail_' x\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cslift x (ep_ptr_' x) = Some v; is_aligned (epQueue_tail_' x) 4; state_' x && 3 = state_' x\<rbrakk> \<Longrightarrow> epQueue_tail_' x && 0xFFFFFFF0 || state_' x && 0xFFFFFFF0 = epQueue_tail_' x \<and> epQueue_tail_' x && 3 || state_' x = state_' x proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cslift x (ep_ptr_' x) = Some v; is_aligned (epQueue_tail_' x) 4; limited_and (state_' x) 3\<rbrakk> \<Longrightarrow> epQueue_tail_' x && 0xFFFFFFF0 || state_' x && 0xFFFFFFF0 = epQueue_tail_' x \<and> epQueue_tail_' x && 3 || state_' x = state_' x proof (prove)
goal:
No subgoals!