theory structures_proofs

lemma (in kernel_all_substitute) thread_state_ptr_set_blockingObject_spec:
           defines "ptrval s \<equiv> cslift s (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C''] :: tcb_C ptr)"
           shows "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C''] :: tcb_C ptr)\<rbrace>
            PROC thread_state_ptr_set_blockingObject(\<acute>thread_state_ptr, \<acute>v32)
            {t. \<exists>thread_state.
                              thread_state_lift thread_state =
                              thread_state_lift ((tcb_C.tcbState_C (the (ptrval s)))) \<lparr> thread_state_CL.blockingObject_CL := (\<^bsup>s\<^esup>v32 AND NOT (mask 4)) \<rparr> \<and>
                              t_hrs_' (globals t) = hrs_mem_update (heap_update
                                      ((cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C''] :: tcb_C ptr))
                                      (tcb_C.tcbState_C_update (\<lambda>_. thread_state)(the (ptrval s))))
                                  (t_hrs_' (globals s))
                              } "  
  (* Invoke vcg *)
   unfolding ptrval_def apply (rule allI, rule conseqPre, vcg) apply (clarsimp) 

  (* Infer h_t_valid for all three levels of indirection *)
   apply (frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def) apply (frule h_t_valid_c_guard_field[where f="[''words_C'']"],
                                       simp, simp add: typ_uinfo_t_def) 

  (* Discharge guards, including c_guard for pointers *)
   apply (simp add: h_t_valid_c_guard guard_simps) 

  (* Lift field updates to bitfield struct updates *)
   apply (simp add: heap_update_field_hrs h_t_valid_c_guard typ_heap_simps) 

  (* Collapse multiple updates *)
   apply (simp add: packed_heap_update_collapse_hrs) 

  (* Instantiate the toplevel object *)
   apply (frule iffD1[OF h_t_valid_clift_Some_iff], rule exE, assumption, simp) 

  (* Instantiate the next-level object in terms of the last *)
   apply (frule clift_subtype, simp+) 

  (* Resolve pointer accesses *)
   apply (simp add: h_val_field_clift') 

  (* Rewrite bitfield struct updates as enclosing struct updates *)
   apply (frule h_t_valid_c_guard) apply (simp add: parent_update_child) 

  (* Equate the updated values *)
   apply (rule exI, rule conjI[rotated], simp add: h_val_clift') 

  (* Rewrite struct updates *)
   apply (simp add: o_def thread_state_lift_def) 

  (* Solve bitwise arithmetic *)
   apply ((intro conjI sign_extend_eq)?;
         (simp add: mask_def shift_over_ao_dists multi_shift_simps word_size
                    word_ao_dist word_bw_assocs word_and_max_simps))? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C'']\<rbrace> Call thread_state_ptr_set_blockingObject_'proc \<lbrace>\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (ptrval s)))\<lparr>blockingObject_CL := \<^bsup>s\<^esup>v32 && ~~ mask 4\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (ptrval s)))) \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C'']\<rbrace> Call thread_state_ptr_set_blockingObject_'proc \<lbrace>\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (ptrval s)))\<lparr>blockingObject_CL := \<^bsup>s\<^esup>v32 && ~~ mask 4\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (ptrval s)))) \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C'']\<rbrace> Call thread_state_ptr_set_blockingObject_'proc \<lbrace>\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift s (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C'']))))\<lparr>blockingObject_CL := \<^bsup>s\<^esup>v32 && ~~ mask 4\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift s (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C'']))))) \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C'']\<rbrace> \<subseteq> {sa. 0 <s 3 \<and> 0 \<le>s 0 \<and> sa \<Turnstile>\<^sub>c thread_state_ptr_' sa \<and> 0 <s 3 \<and> 0 \<le>s 0 \<and> sa \<Turnstile>\<^sub>c thread_state_ptr_' sa \<and> 0 <s 3 \<and> 0 \<le>s 0 \<and> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xFFFFFFF0))) (t_hrs_' (globals sa))) \<Turnstile>\<^sub>t thread_state_ptr_' sa \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 3 \<and> 0 \<le>s 0 \<and> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xFFFFFFF0))) (t_hrs_' (globals sa))) \<Turnstile>\<^sub>t thread_state_ptr_' sa \<and> (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift s (cparent (thread_state_ptr_' s) [''tcbState_C'']))))\<lparr>blockingObject_CL := v32_' s && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xFFFFFFF0))) (t_hrs_' (globals sa)))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xFFFFFFF0))) (t_hrs_' (globals sa)))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] || (v32_' sa >> unat 0) && 0xFFFFFFF0))) (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[3]) &(thread_state_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xFFFFFFF0))) (t_hrs_' (globals sa))) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' s) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift s (cparent (thread_state_ptr_' s) [''tcbState_C'']))))) (t_hrs_' (globals s)))} proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C''] \<Longrightarrow> x \<Turnstile>\<^sub>c thread_state_ptr_' x \<and> (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] || v32_' x && 0xFFFFFFF0))) (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C''] \<Longrightarrow> x \<Turnstile>\<^sub>c thread_state_ptr_' x \<and> (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] || v32_' x && 0xFFFFFFF0))) (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c thread_state_ptr_' x \<and> (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] || v32_' x && 0xFFFFFFF0))) (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; x \<Turnstile>\<^sub>c PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c thread_state_ptr_' x \<and> (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] || v32_' x && 0xFFFFFFF0))) (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; x \<Turnstile>\<^sub>c PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c thread_state_ptr_' x \<and> (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] || v32_' x && 0xFFFFFFF0))) (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; x \<Turnstile>\<^sub>c PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] || v32_' x && 0xFFFFFFF0))) (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; x \<Turnstile>\<^sub>c PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] || v32_' x && 0xFFFFFFF0))) (hrs_mem_update (heap_update (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']))))) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C xa)\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C xa)\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa)\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C xa)\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa)\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C xa)\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[3]) &(thread_state_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa)\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C xa)\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C xa)) 0 (thread_state_C.words_C (tcbState_C xa).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa)\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C xa)\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C xa)) 0 (thread_state_C.words_C (tcbState_C xa).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa); c_guard (cparent (thread_state_ptr_' x) [''tcbState_C''])\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C xa)\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (thread_state_ptr_' x) (thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C xa)) 0 (thread_state_C.words_C (tcbState_C xa).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa); c_guard (cparent (thread_state_ptr_' x) [''tcbState_C''])\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C xa)\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C xa)) 0 (thread_state_C.words_C (tcbState_C xa).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x))) (h_val (hrs_mem (t_hrs_' (globals x))) (cparent (thread_state_ptr_' x) [''tcbState_C''])))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa); c_guard (cparent (thread_state_ptr_' x) [''tcbState_C''])\<rbrakk> \<Longrightarrow> \<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C xa)\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C xa)) 0 (thread_state_C.words_C (tcbState_C xa).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (thread_state_ptr_' x))) (h_val (hrs_mem (t_hrs_' (globals x))) (cparent (thread_state_ptr_' x) [''tcbState_C''])))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (thread_state_ptr_' x) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa); c_guard (cparent (thread_state_ptr_' x) [''tcbState_C''])\<rbrakk> \<Longrightarrow> thread_state_lift (thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C xa)) 0 (thread_state_C.words_C (tcbState_C xa).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (tcbState_C xa)) = thread_state_lift (tcbState_C xa)\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa); c_guard (cparent (thread_state_ptr_' x) [''tcbState_C''])\<rbrakk> \<Longrightarrow> thread_state_lift (thread_state_C.words_C_update (\<lambda>_. Arrays.update (thread_state_C.words_C (tcbState_C xa)) 0 (thread_state_C.words_C (tcbState_C xa).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (tcbState_C xa)) = thread_state_lift (tcbState_C xa)\<lparr>blockingObject_CL := v32_' x && ~~ mask 4\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa); c_guard (cparent (thread_state_ptr_' x) [''tcbState_C''])\<rbrakk> \<Longrightarrow> (thread_state_C.words_C (tcbState_C xa).[0] && 0xF || v32_' x && 0xFFFFFFF0) && ~~ mask 4 = v32_' x && ~~ mask 4 \<and> (thread_state_C.words_C (tcbState_C xa).[0] && 0xF || v32_' x && 0xFFFFFFF0) && mask 4 = thread_state_C.words_C (tcbState_C xa).[0] && mask 4 proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (thread_state_ptr_' x) [''tcbState_C'']; x \<Turnstile>\<^sub>c thread_state_ptr_' x; cslift x (cparent (thread_state_ptr_' x) [''tcbState_C'']) = Some xa; cslift x (thread_state_ptr_' x) = Some (tcbState_C xa); c_guard (cparent (thread_state_ptr_' x) [''tcbState_C''])\<rbrakk> \<Longrightarrow> (thread_state_C.words_C (tcbState_C xa).[0] && 0xF || v32_' x && 0xFFFFFFF0) && ~~ mask 4 = v32_' x && ~~ mask 4 \<and> (thread_state_C.words_C (tcbState_C xa).[0] && 0xF || v32_' x && 0xFFFFFFF0) && mask 4 = thread_state_C.words_C (tcbState_C xa).[0] && mask 4 proof (prove)
goal:
No subgoals!