theory structures_proofs

lemma (in kernel_all_substitute) mdb_node_ptr_set_mdbRevocable_spec:
           defines "ptrval s \<equiv> cslift s (cparent \<^bsup>s\<^esup>mdb_node_ptr [''cteMDBNode_C''] :: cte_C ptr)"
           shows "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c (cparent \<^bsup>s\<^esup>mdb_node_ptr [''cteMDBNode_C''] :: cte_C ptr)\<rbrace>
            PROC mdb_node_ptr_set_mdbRevocable(\<acute>mdb_node_ptr, \<acute>v32)
            {t. \<exists>mdb_node.
                              mdb_node_lift mdb_node =
                              mdb_node_lift ((cte_C.cteMDBNode_C (the (ptrval s)))) \<lparr> mdb_node_CL.mdbRevocable_CL := (\<^bsup>s\<^esup>v32 AND mask 1) \<rparr> \<and>
                              t_hrs_' (globals t) = hrs_mem_update (heap_update
                                      ((cparent \<^bsup>s\<^esup>mdb_node_ptr [''cteMDBNode_C''] :: cte_C ptr))
                                      (cte_C.cteMDBNode_C_update (\<lambda>_. mdb_node)(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 mdb_node_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>mdb_node_ptr [''cteMDBNode_C'']\<rbrace> Call mdb_node_ptr_set_mdbRevocable_'proc \<lbrace>\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (ptrval s)))\<lparr>mdbRevocable_CL := \<^bsup>s\<^esup>v32 && mask 1\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update (cparent \<^bsup>s\<^esup>mdb_node_ptr [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (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>mdb_node_ptr [''cteMDBNode_C'']\<rbrace> Call mdb_node_ptr_set_mdbRevocable_'proc \<lbrace>\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (ptrval s)))\<lparr>mdbRevocable_CL := \<^bsup>s\<^esup>v32 && mask 1\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update (cparent \<^bsup>s\<^esup>mdb_node_ptr [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (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>mdb_node_ptr [''cteMDBNode_C'']\<rbrace> Call mdb_node_ptr_set_mdbRevocable_'proc \<lbrace>\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s (cparent \<^bsup>s\<^esup>mdb_node_ptr [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := \<^bsup>s\<^esup>v32 && mask 1\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update (cparent \<^bsup>s\<^esup>mdb_node_ptr [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s (cparent \<^bsup>s\<^esup>mdb_node_ptr [''cteMDBNode_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>mdb_node_ptr [''cteMDBNode_C'']\<rbrace> \<subseteq> {sa. 1 <s 2 \<and> 0 \<le>s 1 \<and> sa \<Turnstile>\<^sub>c mdb_node_ptr_' sa \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> sa \<Turnstile>\<^sub>c mdb_node_ptr_' sa \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 2))) (t_hrs_' (globals sa))) \<Turnstile>\<^sub>t mdb_node_ptr_' sa \<and> 0 \<le>s 1 \<and> 1 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 2))) (t_hrs_' (globals sa))) \<Turnstile>\<^sub>t mdb_node_ptr_' sa \<and> (\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s (cparent (mdb_node_ptr_' s) [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := v32_' s && mask 1\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 2))) (t_hrs_' (globals sa)))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 2))) (t_hrs_' (globals sa)))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] || (v32_' sa << unat 1) && SCAST(32 signed \<rightarrow> 32) 2))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 2))) (t_hrs_' (globals sa))) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' s) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s (cparent (mdb_node_ptr_' s) [''cteMDBNode_C'']))))) (t_hrs_' (globals s)))} proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C''] \<Longrightarrow> x \<Turnstile>\<^sub>c mdb_node_ptr_' x \<and> (\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] || (v32_' x << Suc 0) && 2))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C''] \<Longrightarrow> x \<Turnstile>\<^sub>c mdb_node_ptr_' x \<and> (\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] || (v32_' x << Suc 0) && 2))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c mdb_node_ptr_' x \<and> (\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] || (v32_' x << Suc 0) && 2))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; x \<Turnstile>\<^sub>c PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c mdb_node_ptr_' x \<and> (\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] || (v32_' x << Suc 0) && 2))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; x \<Turnstile>\<^sub>c PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c mdb_node_ptr_' x \<and> (\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] || (v32_' x << Suc 0) && 2))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; x \<Turnstile>\<^sub>c PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] || (v32_' x << Suc 0) && 2))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; x \<Turnstile>\<^sub>c PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] || (v32_' x << Suc 0) && 2))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']))))) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C xa)\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C xa)\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa; cslift x (mdb_node_ptr_' x) = Some (cteMDBNode_C xa)\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C xa)\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa; cslift x (mdb_node_ptr_' x) = Some (cteMDBNode_C xa)\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C xa)\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(mdb_node_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa; cslift x (mdb_node_ptr_' x) = Some (cteMDBNode_C xa)\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C xa)\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (mdb_node_C.words_C (cteMDBNode_C xa)) (Suc 0) (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa; cslift x (mdb_node_ptr_' x) = Some (cteMDBNode_C xa)\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C xa)\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (mdb_node_C.words_C (cteMDBNode_C xa)) (Suc 0) (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa; cslift x (mdb_node_ptr_' x) = Some (cteMDBNode_C xa); c_guard (cparent (mdb_node_ptr_' x) [''cteMDBNode_C''])\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C xa)\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (mdb_node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (mdb_node_C.words_C (cteMDBNode_C xa)) (Suc 0) (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa; cslift x (mdb_node_ptr_' x) = Some (cteMDBNode_C xa); c_guard (cparent (mdb_node_ptr_' x) [''cteMDBNode_C''])\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C xa)\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node_C.words_C_update (\<lambda>_. Arrays.update (mdb_node_C.words_C (cteMDBNode_C xa)) (Suc 0) (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x))) (h_val (hrs_mem (t_hrs_' (globals x))) (cparent (mdb_node_ptr_' x) [''cteMDBNode_C''])))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa; cslift x (mdb_node_ptr_' x) = Some (cteMDBNode_C xa); c_guard (cparent (mdb_node_ptr_' x) [''cteMDBNode_C''])\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C xa)\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> \<and> hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node_C.words_C_update (\<lambda>_. Arrays.update (mdb_node_C.words_C (cteMDBNode_C xa)) (Suc 0) (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (h_val (hrs_mem (t_hrs_' (globals x))) (mdb_node_ptr_' x))) (h_val (hrs_mem (t_hrs_' (globals x))) (cparent (mdb_node_ptr_' x) [''cteMDBNode_C''])))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) xa)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa; cslift x (mdb_node_ptr_' x) = Some (cteMDBNode_C xa); c_guard (cparent (mdb_node_ptr_' x) [''cteMDBNode_C''])\<rbrakk> \<Longrightarrow> mdb_node_lift (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (mdb_node_C.words_C (cteMDBNode_C xa)) (Suc 0) (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (cteMDBNode_C xa)) = mdb_node_lift (cteMDBNode_C xa)\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa; cslift x (mdb_node_ptr_' x) = Some (cteMDBNode_C xa); c_guard (cparent (mdb_node_ptr_' x) [''cteMDBNode_C''])\<rbrakk> \<Longrightarrow> mdb_node_lift (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (mdb_node_C.words_C (cteMDBNode_C xa)) (Suc 0) (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2)) (cteMDBNode_C xa)) = mdb_node_lift (cteMDBNode_C xa)\<lparr>mdbRevocable_CL := v32_' x && 1\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa; cslift x (mdb_node_ptr_' x) = Some (cteMDBNode_C xa); c_guard (cparent (mdb_node_ptr_' x) [''cteMDBNode_C''])\<rbrakk> \<Longrightarrow> (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2) && ~~ mask 3 = mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && ~~ mask 3 \<and> (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2 >> Suc 0) && 1 = v32_' x && 1 \<and> (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2) && 1 = mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 1 proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<Turnstile>\<^sub>c cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']; x \<Turnstile>\<^sub>c mdb_node_ptr_' x; cslift x (cparent (mdb_node_ptr_' x) [''cteMDBNode_C'']) = Some xa; cslift x (mdb_node_ptr_' x) = Some (cteMDBNode_C xa); c_guard (cparent (mdb_node_ptr_' x) [''cteMDBNode_C''])\<rbrakk> \<Longrightarrow> (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2) && ~~ mask 3 = mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && ~~ mask 3 \<and> (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2 >> Suc 0) && 1 = v32_' x && 1 \<and> (mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 0xFFFFFFFD || (v32_' x << Suc 0) && 2) && 1 = mdb_node_C.words_C (cteMDBNode_C xa).[Suc 0] && 1 proof (prove)
goal:
No subgoals!