theory structures_proofs

lemma (in kernel_all_substitute) cap_untyped_cap_ptr_set_capFreeIndex_spec:
    defines "ptrval s \<equiv> cslift s (cparent \<^bsup>s\<^esup>cap_ptr [''cap_C''] :: cte_C ptr)"
    shows "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c (cparent \<^bsup>s\<^esup>cap_ptr [''cap_C''] :: cte_C ptr) \<and> cap_get_tag (cte_C.cap_C (the (ptrval s))) = scast cap_untyped_cap\<rbrace>
            PROC cap_untyped_cap_ptr_set_capFreeIndex(\<acute>cap_ptr, \<acute>v32)
            {t. \<exists>cap. cap_untyped_cap_lift cap =
                                    cap_untyped_cap_lift (cte_C.cap_C (the (ptrval s))) \<lparr> cap_untyped_cap_CL.capFreeIndex_CL := (\<^bsup>s\<^esup>v32 AND mask 26) \<rparr> \<and>
                                    cap_get_tag cap = scast cap_untyped_cap \<and>
                                    t_hrs_' (globals t) = hrs_mem_update (heap_update
                                            ((cparent \<^bsup>s\<^esup>cap_ptr [''cap_C''] :: cte_C ptr))
                                            (cte_C.cap_C_update (\<lambda>_. cap)(the (ptrval s))))
                                        (t_hrs_' (globals s))
                                    } " unfolding ptrval_def apply (rule allI, rule conseqPre, vcg) apply (clarsimp) apply (frule h_t_valid_c_guard_cparent, simp, simp add: typ_uinfo_t_def) apply (drule h_t_valid_clift_Some_iff[THEN iffD1], erule exE) apply (frule clift_subtype, simp, simp) apply (clarsimp simp: typ_heap_simps c_guard_clift
                        packed_heap_update_collapse_hrs) apply (simp add: guard_simps mask_shift_simps
                   cap_tag_defs[THEN tag_eq_to_tag_masked_eq])? apply (simp add: parent_update_child[OF c_guard_clift]
                   typ_heap_simps c_guard_clift) apply (simp add: o_def cap_untyped_cap_lift_def) apply (simp only: cap_lift_untyped_cap cong: rev_conj_cong) apply (rule exI, rule conjI[rotated], rule conjI[OF _ refl]) apply (simp_all add: cap_get_tag_eq_x cap_tag_defs mask_shift_simps) apply (intro conjI sign_extend_eq; simp add: mask_def word_ao_dist word_bw_assocs)? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c cparent \<^bsup>s\<^esup>cap_ptr [''cap_C''] \<and> cap_get_tag (cte_C.cap_C (the (ptrval s))) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap\<rbrace> Call cap_untyped_cap_ptr_set_capFreeIndex_'proc \<lbrace>\<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (ptrval s)))\<lparr>capFreeIndex_CL := \<^bsup>s\<^esup>v32 && mask 26\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> \<acute>t_hrs = hrs_mem_update (heap_update (cparent \<^bsup>s\<^esup>cap_ptr [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap) (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>cap_ptr [''cap_C''] \<and> cap_get_tag (cte_C.cap_C (the (cslift s (cparent \<^bsup>s\<^esup>cap_ptr [''cap_C''])))) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap\<rbrace> Call cap_untyped_cap_ptr_set_capFreeIndex_'proc \<lbrace>\<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cparent \<^bsup>s\<^esup>cap_ptr [''cap_C'']))))\<lparr>capFreeIndex_CL := \<^bsup>s\<^esup>v32 && mask 26\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> \<acute>t_hrs = hrs_mem_update (heap_update (cparent \<^bsup>s\<^esup>cap_ptr [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cparent \<^bsup>s\<^esup>cap_ptr [''cap_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>cap_ptr [''cap_C''] \<and> cap_get_tag (cte_C.cap_C (the (cslift s (cparent \<^bsup>s\<^esup>cap_ptr [''cap_C''])))) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap\<rbrace> \<subseteq> {sa. 1 <s 2 \<and> 0 \<le>s 1 \<and> sa \<Turnstile>\<^sub>c cap_ptr_' sa \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> sa \<Turnstile>\<^sub>c cap_ptr_' sa \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFC0))) (t_hrs_' (globals sa))) \<Turnstile>\<^sub>t cap_ptr_' sa \<and> 0 \<le>s 6 \<and> 6 <s 0x20 \<and> 1 <s 2 \<and> 0 \<le>s 1 \<and> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFC0))) (t_hrs_' (globals sa))) \<Turnstile>\<^sub>t cap_ptr_' sa \<and> (\<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift s (cparent (cap_ptr_' s) [''cap_C'']))))\<lparr>capFreeIndex_CL := v32_' s && mask 26\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFC0))) (t_hrs_' (globals sa)))) (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFC0))) (t_hrs_' (globals sa)))) (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] || (v32_' sa << unat 6) && 0xFFFFFFC0))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(cap_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFC0))) (t_hrs_' (globals sa))) = hrs_mem_update (heap_update (cparent (cap_ptr_' s) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift s (cparent (cap_ptr_' s) [''cap_C'']))))) (t_hrs_' (globals s)))} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (cap_ptr_' x) [''cap_C'']; cap_get_tag (cte_C.cap_C (the (cslift x (cparent (cap_ptr_' x) [''cap_C''])))) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c cap_ptr_' x \<and> (\<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift x (cparent (cap_ptr_' x) [''cap_C'']))))\<lparr>capFreeIndex_CL := v32_' x && mask 26\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0x3F))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0x3F))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] || (v32_' x << 6) && 0xFFFFFFC0))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0x3F))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (cap_ptr_' x) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift x (cparent (cap_ptr_' x) [''cap_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (cap_ptr_' x) [''cap_C'']; cap_get_tag (cte_C.cap_C (the (cslift x (cparent (cap_ptr_' x) [''cap_C''])))) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; x \<Turnstile>\<^sub>c cap_ptr_' x\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c cap_ptr_' x \<and> (\<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift x (cparent (cap_ptr_' x) [''cap_C'']))))\<lparr>capFreeIndex_CL := v32_' x && mask 26\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0x3F))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0x3F))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] || (v32_' x << 6) && 0xFFFFFFC0))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0x3F))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (cap_ptr_' x) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift x (cparent (cap_ptr_' x) [''cap_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cap_get_tag (cte_C.cap_C (the (cslift x (cparent (cap_ptr_' x) [''cap_C''])))) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; x \<Turnstile>\<^sub>c cap_ptr_' x; cslift x (cparent (cap_ptr_' x) [''cap_C'']) = Some v\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c cap_ptr_' x \<and> (\<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift x (cparent (cap_ptr_' x) [''cap_C'']))))\<lparr>capFreeIndex_CL := v32_' x && mask 26\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0x3F))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0x3F))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] || (v32_' x << 6) && 0xFFFFFFC0))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0x3F))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (cap_ptr_' x) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift x (cparent (cap_ptr_' x) [''cap_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cap_get_tag (cte_C.cap_C (the (cslift x (cparent (cap_ptr_' x) [''cap_C''])))) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; x \<Turnstile>\<^sub>c cap_ptr_' x; cslift x (cparent (cap_ptr_' x) [''cap_C'']) = Some v; cslift x (cap_ptr_' x) = Some (from_bytes (access_ti\<^sub>0 (adjust_ti (typ_info_t TYPE(cap_C)) cte_C.cap_C (cte_C.cap_C_update \<circ> (\<lambda>x _. x))) v))\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c cap_ptr_' x \<and> (\<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C (the (cslift x (cparent (cap_ptr_' x) [''cap_C'']))))\<lparr>capFreeIndex_CL := v32_' x && mask 26\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0x3F))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0x3F))) (t_hrs_' (globals x)))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] || (v32_' x << 6) && 0xFFFFFFC0))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(cap_ptr_' x\<rightarrow>[''words_C''])).[Suc 0] && 0x3F))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (cparent (cap_ptr_' x) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap) (the (cslift x (cparent (cap_ptr_' x) [''cap_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cslift x (cparent (cap_ptr_' x) [''cap_C'']) = Some v; cslift x (cap_ptr_' x) = Some (cte_C.cap_C v)\<rbrakk> \<Longrightarrow> \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C v)\<lparr>capFreeIndex_CL := v32_' x && mask 26\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> hrs_mem_update (heap_update (cap_ptr_' x) (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C v)) (Suc 0) (cap_C.words_C (cte_C.cap_C v).[Suc 0] && 0x3F || (v32_' x << 6) && 0xFFFFFFC0)) (cte_C.cap_C v))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (cap_ptr_' x) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap) v)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cslift x (cparent (cap_ptr_' x) [''cap_C'']) = Some v; cslift x (cap_ptr_' x) = Some (cte_C.cap_C v)\<rbrakk> \<Longrightarrow> \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C v)\<lparr>capFreeIndex_CL := v32_' x && 0x3FFFFFF\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> hrs_mem_update (heap_update (cap_ptr_' x) (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C v)) (Suc 0) (cap_C.words_C (cte_C.cap_C v).[Suc 0] && 0x3F || (v32_' x << 6) && 0xFFFFFFC0)) (cte_C.cap_C v))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (cap_ptr_' x) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap) v)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cslift x (cparent (cap_ptr_' x) [''cap_C'']) = Some v; cslift x (cap_ptr_' x) = Some (cte_C.cap_C v)\<rbrakk> \<Longrightarrow> \<exists>cap. cap_untyped_cap_lift cap = cap_untyped_cap_lift (cte_C.cap_C v)\<lparr>capFreeIndex_CL := v32_' x && 0x3FFFFFF\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> hrs_mem_update (heap_update (cparent (cap_ptr_' x) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C v)) (Suc 0) (cap_C.words_C (cte_C.cap_C v).[Suc 0] && 0x3F || (v32_' x << 6) && 0xFFFFFFC0)) (cte_C.cap_C v)) v)) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (cap_ptr_' x) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap) v)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cslift x (cparent (cap_ptr_' x) [''cap_C'']) = Some v; cslift x (cap_ptr_' x) = Some (cte_C.cap_C v)\<rbrakk> \<Longrightarrow> \<exists>cap. (case cap_lift cap of Some (Cap_untyped_cap rec) \<Rightarrow> rec) = (case cap_lift (cte_C.cap_C v) of Some (Cap_untyped_cap rec) \<Rightarrow> rec)\<lparr>capFreeIndex_CL := v32_' x && 0x3FFFFFF\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> hrs_mem_update (heap_update (cparent (cap_ptr_' x) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C v)) (Suc 0) (cap_C.words_C (cte_C.cap_C v).[Suc 0] && 0x3F || (v32_' x << 6) && 0xFFFFFFC0)) (cte_C.cap_C v)) v)) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (cap_ptr_' x) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap) v)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cslift x (cparent (cap_ptr_' x) [''cap_C'']) = Some v; cslift x (cap_ptr_' x) = Some (cte_C.cap_C v)\<rbrakk> \<Longrightarrow> \<exists>cap. (case Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C cap.[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C cap.[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C cap.[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C cap.[0] << 0) && ~~ mask 4\<rparr>) of Some (Cap_untyped_cap rec) \<Rightarrow> rec) = (case Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C (cte_C.cap_C v).[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C (cte_C.cap_C v).[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C (cte_C.cap_C v).[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C (cte_C.cap_C v).[0] << 0) && ~~ mask 4\<rparr>) of Some (Cap_untyped_cap rec) \<Rightarrow> rec)\<lparr>capFreeIndex_CL := v32_' x && 0x3FFFFFF\<rparr> \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<and> hrs_mem_update (heap_update (cparent (cap_ptr_' x) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C v)) (Suc 0) (cap_C.words_C (cte_C.cap_C v).[Suc 0] && 0x3F || (v32_' x << 6) && 0xFFFFFFC0)) (cte_C.cap_C v)) v)) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (cap_ptr_' x) [''cap_C'']) (cte_C.cap_C_update (\<lambda>_. cap) v)) (t_hrs_' (globals x)) proof (prove)
goal (2 subgoals):
 1. \<And>x v. \<lbrakk>cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cslift x (cparent (cap_ptr_' x) [''cap_C'']) = Some v; cslift x (cap_ptr_' x) = Some (cte_C.cap_C v)\<rbrakk> \<Longrightarrow> cap_get_tag (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C v)) (Suc 0) (cap_C.words_C (cte_C.cap_C v).[Suc 0] && 0x3F || (v32_' x << 6) && 0xFFFFFFC0)) (cte_C.cap_C v)) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap
 2. \<And>x v. \<lbrakk>cap_get_tag (cte_C.cap_C v) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap; cslift x (cparent (cap_ptr_' x) [''cap_C'']) = Some v; cslift x (cap_ptr_' x) = Some (cte_C.cap_C v)\<rbrakk> \<Longrightarrow> (case Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C v)) (Suc 0) (cap_C.words_C (cte_C.cap_C v).[Suc 0] && 0x3F || (v32_' x << 6) && 0xFFFFFFC0)) (cte_C.cap_C v)).[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C v)) (Suc 0) (cap_C.words_C (cte_C.cap_C v).[Suc 0] && 0x3F || (v32_' x << 6) && 0xFFFFFFC0)) (cte_C.cap_C v)).[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C v)) (Suc 0) (cap_C.words_C (cte_C.cap_C v).[Suc 0] && 0x3F || (v32_' x << 6) && 0xFFFFFFC0)) (cte_C.cap_C v)).[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C (cap_C.words_C_update (\<lambda>_. Arrays.update (cap_C.words_C (cte_C.cap_C v)) (Suc 0) (cap_C.words_C (cte_C.cap_C v).[Suc 0] && 0x3F || (v32_' x << 6) && 0xFFFFFFC0)) (cte_C.cap_C v)).[0] << 0) && ~~ mask 4\<rparr>) of Some (Cap_untyped_cap rec) \<Rightarrow> rec) = (case Some (Cap_untyped_cap \<lparr>capFreeIndex_CL = (cap_C.words_C (cte_C.cap_C v).[1] >> 6) && mask 26, capIsDevice_CL = (cap_C.words_C (cte_C.cap_C v).[1] >> 5) && mask 1, capBlockSize_CL = (cap_C.words_C (cte_C.cap_C v).[1] >> 0) && mask 5, capPtr_CL = (cap_C.words_C (cte_C.cap_C v).[0] << 0) && ~~ mask 4\<rparr>) of Some (Cap_untyped_cap rec) \<Rightarrow> rec)\<lparr>capFreeIndex_CL := v32_' x && 0x3FFFFFF\<rparr> proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!