theory Fastpath_C

lemma thread_state_ptr_mset_blockingObject_tsType_spec:
  defines "ptr s \<equiv> cparent \<^bsup>s\<^esup>ts_ptr [''tcbState_C''] :: tcb_C ptr"
  shows
  "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. hrs_htd \<^bsup>s\<^esup>t_hrs \<Turnstile>\<^sub>t ptr s \<and> is_aligned (ep_ref_' s) 4
                         \<and> tsType_' s && mask 4 = tsType_' s\<rbrace>
              Call thread_state_ptr_mset_blockingObject_tsType_'proc
       {t. (\<exists>thread_state.
               tsType_CL (thread_state_lift thread_state) = tsType_' s
             \<and> blockingObject_CL (thread_state_lift thread_state) = ep_ref_' s
             \<and> tcbQueued_CL (thread_state_lift thread_state)
                  = tcbQueued_CL (thread_state_lift (tcbState_C (the (cslift s (ptr s)))))
             \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ptr s)
                          (the (cslift s (ptr s))\<lparr>tcbState_C := thread_state\<rparr>))
                  (t_hrs_' (globals s))
           )}" apply (intro allI, rule conseqPre, vcg) apply (clarsimp simp: ptr_def) apply (frule h_t_valid_c_guard_cparent, simp+) apply (simp add: typ_uinfo_t_def) apply (clarsimp simp: h_t_valid_clift_Some_iff) apply (frule clift_subtype, simp+) apply (clarsimp simp: typ_heap_simps') apply (subst parent_update_child, erule typ_heap_simps', simp+) apply (clarsimp simp: typ_heap_simps' word_sless_def word_sle_def) apply (rule exI, intro conjI[rotated], rule refl) apply (simp_all add: thread_state_lift_def word_ao_dist
                         is_aligned_mask mask_def mask_eq_0_eq_x,
           simp_all add: mask_eq_x_eq_0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c ptr s \<and> is_aligned \<^bsup>s\<^esup>ep_ref 4 \<and> \<^bsup>s\<^esup>tsType && mask 4 = \<^bsup>s\<^esup>tsType\<rbrace> Call thread_state_ptr_mset_blockingObject_tsType_'proc \<lbrace>\<exists>thread_state. tsType_CL (thread_state_lift thread_state) = \<^bsup>s\<^esup>tsType \<and> blockingObject_CL (thread_state_lift thread_state) = \<^bsup>s\<^esup>ep_ref \<and> tcbQueued_CL (thread_state_lift thread_state) = tcbQueued_CL (thread_state_lift (tcbState_C (the (cslift s (ptr s))))) \<and> \<acute>t_hrs = hrs_mem_update (heap_update (ptr s) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift s (ptr s))))) \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c ptr s \<and> is_aligned \<^bsup>s\<^esup>ep_ref 4 \<and> \<^bsup>s\<^esup>tsType && mask 4 = \<^bsup>s\<^esup>tsType\<rbrace> \<subseteq> {sa. 0 <s 3 \<and> 0 \<le>s 0 \<and> sa \<Turnstile>\<^sub>c ts_ptr_' sa \<and> (\<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' s \<and> blockingObject_CL (thread_state_lift thread_state) = ep_ref_' s \<and> tcbQueued_CL (thread_state_lift thread_state) = tcbQueued_CL (thread_state_lift (tcbState_C (the (cslift s (ptr s))))) \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(ts_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(ts_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (UCAST(32 \<rightarrow> 32) (ep_ref_' sa || tsType_' sa)))) (t_hrs_' (globals sa)) = hrs_mem_update (heap_update (ptr s) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift s (ptr s))))) (t_hrs_' (globals s)))} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (ts_ptr_' x) [''tcbState_C'']; is_aligned (ep_ref_' x) 4; tsType_' x && mask 4 = tsType_' x\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ts_ptr_' x \<and> (\<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' x \<and> blockingObject_CL (thread_state_lift thread_state) = ep_ref_' x \<and> tcbQueued_CL (thread_state_lift thread_state) = tcbQueued_CL (thread_state_lift (tcbState_C (the (cslift x (cparent (ts_ptr_' x) [''tcbState_C'']))))) \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(ts_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(ts_ptr_' x\<rightarrow>[''words_C'']))) 0 (ep_ref_' x || tsType_' x))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (ts_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (ts_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (ts_ptr_' x) [''tcbState_C'']; is_aligned (ep_ref_' x) 4; tsType_' x && mask 4 = tsType_' x\<rbrakk> \<Longrightarrow> export_uinfo (typ_info_t TYPE(thread_state_C)) = typ_uinfo_t TYPE(thread_state_C)
 2. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (ts_ptr_' x) [''tcbState_C'']; is_aligned (ep_ref_' x) 4; tsType_' x && mask 4 = tsType_' x; x \<Turnstile>\<^sub>c ts_ptr_' x\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ts_ptr_' x \<and> (\<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' x \<and> blockingObject_CL (thread_state_lift thread_state) = ep_ref_' x \<and> tcbQueued_CL (thread_state_lift thread_state) = tcbQueued_CL (thread_state_lift (tcbState_C (the (cslift x (cparent (ts_ptr_' x) [''tcbState_C'']))))) \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(ts_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(ts_ptr_' x\<rightarrow>[''words_C'']))) 0 (ep_ref_' x || tsType_' x))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (ts_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (ts_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (ts_ptr_' x) [''tcbState_C'']; is_aligned (ep_ref_' x) 4; tsType_' x && mask 4 = tsType_' x; x \<Turnstile>\<^sub>c ts_ptr_' x\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ts_ptr_' x \<and> (\<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' x \<and> blockingObject_CL (thread_state_lift thread_state) = ep_ref_' x \<and> tcbQueued_CL (thread_state_lift thread_state) = tcbQueued_CL (thread_state_lift (tcbState_C (the (cslift x (cparent (ts_ptr_' x) [''tcbState_C'']))))) \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(ts_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(ts_ptr_' x\<rightarrow>[''words_C'']))) 0 (ep_ref_' x || tsType_' x))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (ts_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (ts_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x v va. \<lbrakk>is_aligned (ep_ref_' x) 4; tsType_' x && mask 4 = tsType_' x; cslift x (cparent (ts_ptr_' x) [''tcbState_C'']) = Some v; cslift x (ts_ptr_' x) = Some va\<rbrakk> \<Longrightarrow> \<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' x \<and> blockingObject_CL (thread_state_lift thread_state) = ep_ref_' x \<and> tcbQueued_CL (thread_state_lift thread_state) = tcbQueued_CL (thread_state_lift (tcbState_C v)) \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(ts_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(ts_ptr_' x\<rightarrow>[''words_C'']))) 0 (ep_ref_' x || tsType_' x))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (ts_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) v)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v va. \<lbrakk>is_aligned (ep_ref_' x) 4; tsType_' x && mask 4 = tsType_' x; cslift x (cparent (ts_ptr_' x) [''tcbState_C'']) = Some v; tcbState_C v = va; cslift x (ts_ptr_' x) = Some va\<rbrakk> \<Longrightarrow> \<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' x \<and> blockingObject_CL (thread_state_lift thread_state) = ep_ref_' x \<and> tcbQueued_CL (thread_state_lift thread_state) = tcbQueued_CL (thread_state_lift va) \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(ts_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(ts_ptr_' x\<rightarrow>[''words_C'']))) 0 (ep_ref_' x || tsType_' x))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (ts_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) v)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (ep_ref_' x) 4; tsType_' x && mask 4 = tsType_' x; cslift x (cparent (ts_ptr_' x) [''tcbState_C'']) = Some v; cslift x (ts_ptr_' x) = Some (tcbState_C v)\<rbrakk> \<Longrightarrow> \<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' x \<and> blockingObject_CL (thread_state_lift thread_state) = ep_ref_' x \<and> tcbQueued_CL (thread_state_lift thread_state) = tcbQueued_CL (thread_state_lift (tcbState_C v)) \<and> hrs_mem_update (heap_update (ts_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C v)) 0 (ep_ref_' x || tsType_' x)) (tcbState_C v))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (ts_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) v)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (ep_ref_' x) 4; tsType_' x && mask 4 = tsType_' x; cslift x (cparent (ts_ptr_' x) [''tcbState_C'']) = Some v; cslift x (ts_ptr_' x) = Some (tcbState_C v)\<rbrakk> \<Longrightarrow> \<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' x \<and> blockingObject_CL (thread_state_lift thread_state) = ep_ref_' x \<and> tcbQueued_CL (thread_state_lift thread_state) = tcbQueued_CL (thread_state_lift (tcbState_C v)) \<and> hrs_mem_update (heap_update (cparent (ts_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C v)) 0 (ep_ref_' x || tsType_' x)) (tcbState_C v)) (h_val (hrs_mem (t_hrs_' (globals x))) (cparent (ts_ptr_' x) [''tcbState_C''])))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (ts_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) v)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (ep_ref_' x) 4; tsType_' x && mask 4 = tsType_' x; cslift x (cparent (ts_ptr_' x) [''tcbState_C'']) = Some v; cslift x (ts_ptr_' x) = Some (tcbState_C v)\<rbrakk> \<Longrightarrow> \<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' x \<and> blockingObject_CL (thread_state_lift thread_state) = ep_ref_' x \<and> tcbQueued_CL (thread_state_lift thread_state) = tcbQueued_CL (thread_state_lift (tcbState_C v)) \<and> hrs_mem_update (heap_update (cparent (ts_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C v)) 0 (ep_ref_' x || tsType_' x)) (tcbState_C v)) v)) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (ts_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) v)) (t_hrs_' (globals x)) proof (prove)
goal (3 subgoals):
 1. \<And>x v. \<lbrakk>is_aligned (ep_ref_' x) 4; tsType_' x && mask 4 = tsType_' x; cslift x (cparent (ts_ptr_' x) [''tcbState_C'']) = Some v; cslift x (ts_ptr_' x) = Some (tcbState_C v)\<rbrakk> \<Longrightarrow> tcbQueued_CL (thread_state_lift (thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C v)) 0 (ep_ref_' x || tsType_' x)) (tcbState_C v))) = tcbQueued_CL (thread_state_lift (tcbState_C v))
 2. \<And>x v. \<lbrakk>is_aligned (ep_ref_' x) 4; tsType_' x && mask 4 = tsType_' x; cslift x (cparent (ts_ptr_' x) [''tcbState_C'']) = Some v; cslift x (ts_ptr_' x) = Some (tcbState_C v)\<rbrakk> \<Longrightarrow> blockingObject_CL (thread_state_lift (thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C v)) 0 (ep_ref_' x || tsType_' x)) (tcbState_C v))) = ep_ref_' x
 3. \<And>x v. \<lbrakk>is_aligned (ep_ref_' x) 4; tsType_' x && mask 4 = tsType_' x; cslift x (cparent (ts_ptr_' x) [''tcbState_C'']) = Some v; cslift x (ts_ptr_' x) = Some (tcbState_C v)\<rbrakk> \<Longrightarrow> tsType_CL (thread_state_lift (thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C v)) 0 (ep_ref_' x || tsType_' x)) (tcbState_C v))) = tsType_' x proof (prove)
goal:
No subgoals!