theory Fastpath_C

lemma thread_state_ptr_set_tsType_np_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> (tsType_' s = scast ThreadState_Running \<or> tsType_' s = scast ThreadState_Restart
                          \<or> tsType_' s = scast ThreadState_BlockedOnReply)\<rbrace>
              Call thread_state_ptr_set_tsType_np_'proc
       {t. (\<exists>thread_state.
               tsType_CL (thread_state_lift thread_state) = tsType_' 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 (clarsimp simp: h_t_valid_clift_Some_iff) apply (frule h_t_valid_c_guard_cparent[OF h_t_valid_clift], simp+,
         simp add: typ_uinfo_t_def) apply (frule clift_subtype, simp+) apply (clarsimp simp: typ_heap_simps' word_sle_def word_sless_def) apply (subst parent_update_child, erule typ_heap_simps', simp+) apply (clarsimp simp: typ_heap_simps') apply (rule exI, rule conjI[OF _ conjI [OF _ refl]]) apply (simp_all add: thread_state_lift_def) apply (auto simp: "StrictC'_thread_state_defs" mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c ptr s \<and> (\<^bsup>s\<^esup>tsType = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> \<^bsup>s\<^esup>tsType = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<^bsup>s\<^esup>tsType = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply)\<rbrace> Call thread_state_ptr_set_tsType_np_'proc \<lbrace>\<exists>thread_state. tsType_CL (thread_state_lift thread_state) = \<^bsup>s\<^esup>tsType \<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> (\<^bsup>s\<^esup>tsType = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> \<^bsup>s\<^esup>tsType = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> \<^bsup>s\<^esup>tsType = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply)\<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> 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) (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'']; tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c ts_ptr_' x \<and> (\<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' 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 (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. \<lbrakk>tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply; cslift x (cparent (ts_ptr_' x) [''tcbState_C'']) = Some v\<rbrakk> \<Longrightarrow> (\<exists>v. cslift x (ts_ptr_' x) = Some v) \<and> (\<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' 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 (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>tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply; cslift x (cparent (ts_ptr_' x) [''tcbState_C'']) = Some v; x \<Turnstile>\<^sub>c ts_ptr_' x\<rbrakk> \<Longrightarrow> (\<exists>v. cslift x (ts_ptr_' x) = Some v) \<and> (\<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' 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 (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>tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply; cslift x (cparent (ts_ptr_' x) [''tcbState_C'']) = Some v; x \<Turnstile>\<^sub>c ts_ptr_' x; cslift x (ts_ptr_' x) = Some (tcbState_C v)\<rbrakk> \<Longrightarrow> \<exists>thread_state. tsType_CL (thread_state_lift thread_state) = tsType_' 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 (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>tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply; 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> 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 (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>tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply; 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> 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 (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>tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply; 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> 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 (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 (2 subgoals):
 1. \<And>x v. \<lbrakk>tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply; 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 (tsType_' x)) (tcbState_C v))) = tsType_' x
 2. \<And>x v. \<lbrakk>tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply; 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 (tsType_' x)) (tcbState_C v))) = tcbQueued_CL (thread_state_lift (tcbState_C v)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<or> tsType_' x = SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReply; cslift x (cparent (ts_ptr_' x) [''tcbState_C'']) = Some v; cslift x (ts_ptr_' x) = Some (tcbState_C v)\<rbrakk> \<Longrightarrow> tsType_' x && mask 4 = tsType_' x proof (prove)
goal:
No subgoals!