theory Fastpath_C

lemma mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_spec:
  defines "ptr s \<equiv> cparent \<^bsup>s\<^esup>node_ptr [''cteMDBNode_C''] :: cte_C ptr"
  shows
  "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. hrs_htd \<^bsup>s\<^esup>t_hrs \<Turnstile>\<^sub>t ptr s \<and> is_aligned (mdbNext___unsigned_long_' s) 4
                         \<and> mdbRevocable___unsigned_long_' s && mask 1 = mdbRevocable___unsigned_long_' s
                         \<and> mdbFirstBadged___unsigned_long_' s && mask 1 = mdbFirstBadged___unsigned_long_' s\<rbrace>
              Call mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_'proc
       {t. (\<exists>mdb_node.
               mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s (ptr s))))
                           \<lparr> mdbNext_CL := mdbNext___unsigned_long_' s, mdbRevocable_CL := mdbRevocable___unsigned_long_' s,
                             mdbFirstBadged_CL := mdbFirstBadged___unsigned_long_' s \<rparr>
               \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (ptr s)
                          (the (cslift s (ptr s)) \<lparr> cteMDBNode_C := mdb_node \<rparr>))
                  (t_hrs_' (globals s))
           )}" supply shiftl_of_Suc[simp del] apply (intro allI, rule conseqPre, vcg) apply (clarsimp simp: ptr_def) apply (clarsimp simp: h_t_valid_clift_Some_iff) apply (frule h_t_valid_c_guard_cparent[OF h_t_valid_clift], simp+,
         simp add: typ_uinfo_t_def) apply (frule clift_subtype, simp+) apply (clarsimp simp: typ_heap_simps' word_sle_def word_sless_def) apply (subst parent_update_child, erule typ_heap_simps', simp+) apply (clarsimp simp: typ_heap_simps') apply (rule exI, rule conjI[OF _ refl]) apply (simp add: mdb_node_lift_def word_ao_dist shiftr_over_or_dist) apply (fold limited_and_def) apply (simp add: limited_and_simps mask_def and_mask2 word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c ptr s \<and> is_aligned \<^bsup>s\<^esup>mdbNext___unsigned_long 4 \<and> \<^bsup>s\<^esup>mdbRevocable___unsigned_long && mask 1 = \<^bsup>s\<^esup>mdbRevocable___unsigned_long \<and> \<^bsup>s\<^esup>mdbFirstBadged___unsigned_long && mask 1 = \<^bsup>s\<^esup>mdbFirstBadged___unsigned_long\<rbrace> Call mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_'proc \<lbrace>\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s (ptr s))))\<lparr>mdbNext_CL := \<^bsup>s\<^esup>mdbNext___unsigned_long, mdbRevocable_CL := \<^bsup>s\<^esup>mdbRevocable___unsigned_long, mdbFirstBadged_CL := \<^bsup>s\<^esup>mdbFirstBadged___unsigned_long\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update (ptr s) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s (ptr s))))) \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c ptr s \<and> is_aligned \<^bsup>s\<^esup>mdbNext___unsigned_long 4 \<and> \<^bsup>s\<^esup>mdbRevocable___unsigned_long && mask 1 = \<^bsup>s\<^esup>mdbRevocable___unsigned_long \<and> \<^bsup>s\<^esup>mdbFirstBadged___unsigned_long && mask 1 = \<^bsup>s\<^esup>mdbFirstBadged___unsigned_long\<rbrace> Call mdb_node_ptr_mset_mdbNext_mdbRevocable_mdbFirstBadged_'proc \<lbrace>\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s (ptr s))))\<lparr>mdbNext_CL := \<^bsup>s\<^esup>mdbNext___unsigned_long, mdbRevocable_CL := \<^bsup>s\<^esup>mdbRevocable___unsigned_long, mdbFirstBadged_CL := \<^bsup>s\<^esup>mdbFirstBadged___unsigned_long\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update (ptr s) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s (ptr s))))) \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c ptr s \<and> is_aligned \<^bsup>s\<^esup>mdbNext___unsigned_long 4 \<and> \<^bsup>s\<^esup>mdbRevocable___unsigned_long && mask 1 = \<^bsup>s\<^esup>mdbRevocable___unsigned_long \<and> \<^bsup>s\<^esup>mdbFirstBadged___unsigned_long && mask 1 = \<^bsup>s\<^esup>mdbFirstBadged___unsigned_long\<rbrace> \<subseteq> {sa. 1 <s 2 \<and> 0 \<le>s 1 \<and> sa \<Turnstile>\<^sub>c node_ptr_' sa \<and> 0 \<le>s 1 \<and> 1 <s 0x20 \<and> (\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s (ptr s))))\<lparr>mdbNext_CL := mdbNext___unsigned_long_' s, mdbRevocable_CL := mdbRevocable___unsigned_long_' s, mdbFirstBadged_CL := mdbFirstBadged___unsigned_long_' s\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (UCAST(32 \<rightarrow> 32) ((mdbNext___unsigned_long_' sa || (mdbRevocable___unsigned_long_' sa << unat 1)) || mdbFirstBadged___unsigned_long_' sa)))) (t_hrs_' (globals sa)) = hrs_mem_update (heap_update (ptr s) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift s (ptr s))))) (t_hrs_' (globals s)))} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<Turnstile>\<^sub>c cparent (node_ptr_' x) [''cteMDBNode_C'']; is_aligned (mdbNext___unsigned_long_' x) 4; mdbRevocable___unsigned_long_' x && 1 = mdbRevocable___unsigned_long_' x; mdbFirstBadged___unsigned_long_' x && 1 = mdbFirstBadged___unsigned_long_' x\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c node_ptr_' x \<and> (\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift x (cparent (node_ptr_' x) [''cteMDBNode_C'']))))\<lparr>mdbNext_CL := mdbNext___unsigned_long_' x, mdbRevocable_CL := mdbRevocable___unsigned_long_' x, mdbFirstBadged_CL := mdbFirstBadged___unsigned_long_' x\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) ((mdbNext___unsigned_long_' x || (mdbRevocable___unsigned_long_' x << Suc 0)) || mdbFirstBadged___unsigned_long_' x))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) (the (cslift x (cparent (node_ptr_' x) [''cteMDBNode_C'']))))) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (mdbNext___unsigned_long_' x) 4; mdbRevocable___unsigned_long_' x && 1 = mdbRevocable___unsigned_long_' x; mdbFirstBadged___unsigned_long_' x && 1 = mdbFirstBadged___unsigned_long_' x; cslift x (cparent (node_ptr_' x) [''cteMDBNode_C'']) = Some v\<rbrakk> \<Longrightarrow> (\<exists>v. cslift x (node_ptr_' x) = Some v) \<and> (\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C v)\<lparr>mdbNext_CL := mdbNext___unsigned_long_' x, mdbRevocable_CL := mdbRevocable___unsigned_long_' x, mdbFirstBadged_CL := mdbFirstBadged___unsigned_long_' x\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) ((mdbNext___unsigned_long_' x || (mdbRevocable___unsigned_long_' x << Suc 0)) || mdbFirstBadged___unsigned_long_' x))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) v)) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (mdbNext___unsigned_long_' x) 4; mdbRevocable___unsigned_long_' x && 1 = mdbRevocable___unsigned_long_' x; mdbFirstBadged___unsigned_long_' x && 1 = mdbFirstBadged___unsigned_long_' x; cslift x (cparent (node_ptr_' x) [''cteMDBNode_C'']) = Some v; x \<Turnstile>\<^sub>c node_ptr_' x\<rbrakk> \<Longrightarrow> (\<exists>v. cslift x (node_ptr_' x) = Some v) \<and> (\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C v)\<lparr>mdbNext_CL := mdbNext___unsigned_long_' x, mdbRevocable_CL := mdbRevocable___unsigned_long_' x, mdbFirstBadged_CL := mdbFirstBadged___unsigned_long_' x\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) ((mdbNext___unsigned_long_' x || (mdbRevocable___unsigned_long_' x << Suc 0)) || mdbFirstBadged___unsigned_long_' x))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) v)) (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (mdbNext___unsigned_long_' x) 4; mdbRevocable___unsigned_long_' x && 1 = mdbRevocable___unsigned_long_' x; mdbFirstBadged___unsigned_long_' x && 1 = mdbFirstBadged___unsigned_long_' x; cslift x (cparent (node_ptr_' x) [''cteMDBNode_C'']) = Some v; x \<Turnstile>\<^sub>c node_ptr_' x; cslift x (node_ptr_' x) = Some (cteMDBNode_C v)\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C v)\<lparr>mdbNext_CL := mdbNext___unsigned_long_' x, mdbRevocable_CL := mdbRevocable___unsigned_long_' x, mdbFirstBadged_CL := mdbFirstBadged___unsigned_long_' x\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[2]) &(node_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[2]) &(node_ptr_' x\<rightarrow>[''words_C'']))) (Suc 0) ((mdbNext___unsigned_long_' x || (mdbRevocable___unsigned_long_' x << Suc 0)) || mdbFirstBadged___unsigned_long_' x))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) v)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (mdbNext___unsigned_long_' x) 4; mdbRevocable___unsigned_long_' x && 1 = mdbRevocable___unsigned_long_' x; mdbFirstBadged___unsigned_long_' x && 1 = mdbFirstBadged___unsigned_long_' x; cslift x (cparent (node_ptr_' x) [''cteMDBNode_C'']) = Some v; cslift x (node_ptr_' x) = Some (cteMDBNode_C v)\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C v)\<lparr>mdbNext_CL := mdbNext___unsigned_long_' x, mdbRevocable_CL := mdbRevocable___unsigned_long_' x, mdbFirstBadged_CL := mdbFirstBadged___unsigned_long_' x\<rparr> \<and> hrs_mem_update (heap_update (node_ptr_' x) (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (mdb_node_C.words_C (cteMDBNode_C v)) (Suc 0) ((mdbNext___unsigned_long_' x || (mdbRevocable___unsigned_long_' x << Suc 0)) || mdbFirstBadged___unsigned_long_' x)) (cteMDBNode_C v))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) v)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (mdbNext___unsigned_long_' x) 4; mdbRevocable___unsigned_long_' x && 1 = mdbRevocable___unsigned_long_' x; mdbFirstBadged___unsigned_long_' x && 1 = mdbFirstBadged___unsigned_long_' x; cslift x (cparent (node_ptr_' x) [''cteMDBNode_C'']) = Some v; cslift x (node_ptr_' x) = Some (cteMDBNode_C v)\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C v)\<lparr>mdbNext_CL := mdbNext___unsigned_long_' x, mdbRevocable_CL := mdbRevocable___unsigned_long_' x, mdbFirstBadged_CL := mdbFirstBadged___unsigned_long_' x\<rparr> \<and> hrs_mem_update (heap_update (cparent (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 v)) (Suc 0) ((mdbNext___unsigned_long_' x || (mdbRevocable___unsigned_long_' x << Suc 0)) || mdbFirstBadged___unsigned_long_' x)) (cteMDBNode_C v)) (h_val (hrs_mem (t_hrs_' (globals x))) (cparent (node_ptr_' x) [''cteMDBNode_C''])))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) v)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (mdbNext___unsigned_long_' x) 4; mdbRevocable___unsigned_long_' x && 1 = mdbRevocable___unsigned_long_' x; mdbFirstBadged___unsigned_long_' x && 1 = mdbFirstBadged___unsigned_long_' x; cslift x (cparent (node_ptr_' x) [''cteMDBNode_C'']) = Some v; cslift x (node_ptr_' x) = Some (cteMDBNode_C v)\<rbrakk> \<Longrightarrow> \<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C v)\<lparr>mdbNext_CL := mdbNext___unsigned_long_' x, mdbRevocable_CL := mdbRevocable___unsigned_long_' x, mdbFirstBadged_CL := mdbFirstBadged___unsigned_long_' x\<rparr> \<and> hrs_mem_update (heap_update (cparent (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 v)) (Suc 0) ((mdbNext___unsigned_long_' x || (mdbRevocable___unsigned_long_' x << Suc 0)) || mdbFirstBadged___unsigned_long_' x)) (cteMDBNode_C v)) v)) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (cparent (node_ptr_' x) [''cteMDBNode_C'']) (cteMDBNode_C_update (\<lambda>_. mdb_node) v)) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (mdbNext___unsigned_long_' x) 4; mdbRevocable___unsigned_long_' x && 1 = mdbRevocable___unsigned_long_' x; mdbFirstBadged___unsigned_long_' x && 1 = mdbFirstBadged___unsigned_long_' x; cslift x (cparent (node_ptr_' x) [''cteMDBNode_C'']) = Some v; cslift x (node_ptr_' x) = Some (cteMDBNode_C v)\<rbrakk> \<Longrightarrow> mdb_node_lift (mdb_node_C.words_C_update (\<lambda>_. Arrays.update (mdb_node_C.words_C (cteMDBNode_C v)) (Suc 0) ((mdbNext___unsigned_long_' x || (mdbRevocable___unsigned_long_' x << Suc 0)) || mdbFirstBadged___unsigned_long_' x)) (cteMDBNode_C v)) = mdb_node_lift (cteMDBNode_C v)\<lparr>mdbNext_CL := mdbNext___unsigned_long_' x, mdbRevocable_CL := mdbRevocable___unsigned_long_' x, mdbFirstBadged_CL := mdbFirstBadged___unsigned_long_' x\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (mdbNext___unsigned_long_' x) 4; mdbRevocable___unsigned_long_' x && 1 = mdbRevocable___unsigned_long_' x; mdbFirstBadged___unsigned_long_' x && 1 = mdbFirstBadged___unsigned_long_' x; cslift x (cparent (node_ptr_' x) [''cteMDBNode_C'']) = Some v; cslift x (node_ptr_' x) = Some (cteMDBNode_C v)\<rbrakk> \<Longrightarrow> (mdbNext___unsigned_long_' x || (mdbRevocable___unsigned_long_' x << Suc 0) && ~~ mask 3) || mdbFirstBadged___unsigned_long_' x && ~~ mask 3 = mdbNext___unsigned_long_' x \<and> ((mdbNext___unsigned_long_' x >> Suc 0) && 1 || (mdbRevocable___unsigned_long_' x << Suc 0 >> Suc 0) && 1) || (mdbFirstBadged___unsigned_long_' x >> Suc 0) && 1 = mdbRevocable___unsigned_long_' x \<and> (mdbNext___unsigned_long_' x && 1 || (mdbRevocable___unsigned_long_' x << Suc 0) && 1) || mdbFirstBadged___unsigned_long_' x = mdbFirstBadged___unsigned_long_' x proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>is_aligned (mdbNext___unsigned_long_' x) 4; limited_and (mdbRevocable___unsigned_long_' x) 1; limited_and (mdbFirstBadged___unsigned_long_' x) 1; cslift x (cparent (node_ptr_' x) [''cteMDBNode_C'']) = Some v; cslift x (node_ptr_' x) = Some (cteMDBNode_C v)\<rbrakk> \<Longrightarrow> (mdbNext___unsigned_long_' x || (mdbRevocable___unsigned_long_' x << Suc 0) && ~~ mask 3) || mdbFirstBadged___unsigned_long_' x && ~~ mask 3 = mdbNext___unsigned_long_' x \<and> ((mdbNext___unsigned_long_' x >> Suc 0) && 1 || (mdbRevocable___unsigned_long_' x << Suc 0 >> Suc 0) && 1) || (mdbFirstBadged___unsigned_long_' x >> Suc 0) && 1 = mdbRevocable___unsigned_long_' x \<and> (mdbNext___unsigned_long_' x && 1 || (mdbRevocable___unsigned_long_' x << Suc 0) && 1) || mdbFirstBadged___unsigned_long_' x = mdbFirstBadged___unsigned_long_' x proof (prove)
goal:
No subgoals!