theory Fastpath_C

lemma mdb_node_ptr_set_mdbPrev_np_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 (mdbPrev___unsigned_long_' s) 4\<rbrace>
              Call mdb_node_ptr_set_mdbPrev_np_'proc
       {t. (\<exists>mdb_node.
               mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s (ptr s))))
                           \<lparr> mdbPrev_CL := mdbPrev___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))
           )}" 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') apply (subst parent_update_child, erule typ_heap_simps', simp+) apply (clarsimp simp: typ_heap_simps' word_sle_def word_sless_def) apply (rule exI, rule conjI [OF _ refl]) apply (simp add: mdb_node_lift_def limited_and_simps mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c ptr s \<and> is_aligned \<^bsup>s\<^esup>mdbPrev___unsigned_long 4\<rbrace> Call mdb_node_ptr_set_mdbPrev_np_'proc \<lbrace>\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s (ptr s))))\<lparr>mdbPrev_CL := \<^bsup>s\<^esup>mdbPrev___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>mdbPrev___unsigned_long 4\<rbrace> \<subseteq> {sa. 0 <s 2 \<and> 0 \<le>s 0 \<and> sa \<Turnstile>\<^sub>c node_ptr_' sa \<and> (\<exists>mdb_node. mdb_node_lift mdb_node = mdb_node_lift (cteMDBNode_C (the (cslift s (ptr s))))\<lparr>mdbPrev_CL := mdbPrev___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 0) (UCAST(32 \<rightarrow> 32) (mdbPrev___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 (mdbPrev___unsigned_long_' x) 4\<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>mdbPrev_CL := mdbPrev___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'']))) 0 (mdbPrev___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 (mdbPrev___unsigned_long_' x) 4; 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>mdbPrev_CL := mdbPrev___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'']))) 0 (mdbPrev___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 (mdbPrev___unsigned_long_' x) 4; 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>mdbPrev_CL := mdbPrev___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'']))) 0 (mdbPrev___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 (mdbPrev___unsigned_long_' x) 4; 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>mdbPrev_CL := mdbPrev___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'']))) 0 (mdbPrev___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 (mdbPrev___unsigned_long_' x) 4; 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>mdbPrev_CL := mdbPrev___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)) 0 (mdbPrev___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 (mdbPrev___unsigned_long_' x) 4; 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>mdbPrev_CL := mdbPrev___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)) 0 (mdbPrev___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 (mdbPrev___unsigned_long_' x) 4; 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>mdbPrev_CL := mdbPrev___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)) 0 (mdbPrev___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 (mdbPrev___unsigned_long_' x) 4; 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)) 0 (mdbPrev___unsigned_long_' x)) (cteMDBNode_C v)) = mdb_node_lift (cteMDBNode_C v)\<lparr>mdbPrev_CL := mdbPrev___unsigned_long_' x\<rparr> proof (prove)
goal:
No subgoals!