theory structures_proofs

lemma (in kernel_all_substitute) notification_ptr_set_ntfnQueue_tail_spec:
           defines "ptrval s \<equiv> cslift s \<^bsup>s\<^esup>notification_ptr"
           shows "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>notification_ptr\<rbrace>
            PROC notification_ptr_set_ntfnQueue_tail(\<acute>notification_ptr, \<acute>v32)
            {t. \<exists>notification.
                              notification_lift notification =
                              notification_lift ((the (ptrval s))) \<lparr> notification_CL.ntfnQueue_tail_CL := (\<^bsup>s\<^esup>v32 AND NOT (mask 4)) \<rparr> \<and>
                              t_hrs_' (globals t) = hrs_mem_update (heap_update
                                      (\<^bsup>s\<^esup>notification_ptr)
                                      notification)
                                  (t_hrs_' (globals s))
                              } " unfolding ptrval_def apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: guard_simps) apply (clarsimp simp add: packed_heap_update_collapse_hrs typ_heap_simps)? apply (rule exI, rule conjI[rotated], rule refl) apply (clarsimp simp: h_t_valid_clift_Some_iff notification_lift_def typ_heap_simps) 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 \<^bsup>s\<^esup>notification_ptr\<rbrace> Call notification_ptr_set_ntfnQueue_tail_'proc \<lbrace>\<exists>notification. notification_lift notification = notification_lift (the (ptrval s))\<lparr>ntfnQueue_tail_CL := \<^bsup>s\<^esup>v32 && ~~ mask 4\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update \<^bsup>s\<^esup>notification_ptr notification) \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>notification_ptr\<rbrace> Call notification_ptr_set_ntfnQueue_tail_'proc \<lbrace>\<exists>notification. notification_lift notification = notification_lift (the (cslift s \<^bsup>s\<^esup>notification_ptr))\<lparr>ntfnQueue_tail_CL := \<^bsup>s\<^esup>v32 && ~~ mask 4\<rparr> \<and> \<acute>t_hrs = hrs_mem_update (heap_update \<^bsup>s\<^esup>notification_ptr notification) \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>s. s \<Turnstile>\<^sub>c \<^bsup>s\<^esup>notification_ptr\<rbrace> \<subseteq> {sa. 0 <s 4 \<and> 0 \<le>s 0 \<and> sa \<Turnstile>\<^sub>c notification_ptr_' sa \<and> 0 <s 4 \<and> 0 \<le>s 0 \<and> sa \<Turnstile>\<^sub>c notification_ptr_' sa \<and> 0 <s 4 \<and> 0 \<le>s 0 \<and> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xFFFFFFF0))) (t_hrs_' (globals sa))) \<Turnstile>\<^sub>t notification_ptr_' sa \<and> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 4 \<and> 0 \<le>s 0 \<and> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xFFFFFFF0))) (t_hrs_' (globals sa))) \<Turnstile>\<^sub>t notification_ptr_' sa \<and> (\<exists>notification. notification_lift notification = notification_lift (the (cslift s (notification_ptr_' s)))\<lparr>ntfnQueue_tail_CL := v32_' s && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xFFFFFFF0))) (t_hrs_' (globals sa)))) (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xFFFFFFF0))) (t_hrs_' (globals sa)))) (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] || (v32_' sa >> unat 0) && 0xFFFFFFF0))) (hrs_mem_update (heap_update (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C'']))) (unat 0) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[4]) &(notification_ptr_' sa\<rightarrow>[''words_C''])).[unat 0] && ~~ 0xFFFFFFF0))) (t_hrs_' (globals sa))) = hrs_mem_update (heap_update (notification_ptr_' s) notification) (t_hrs_' (globals s)))} proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<Turnstile>\<^sub>c notification_ptr_' x \<Longrightarrow> \<exists>notification. notification_lift notification = notification_lift (the (cslift x (notification_ptr_' x)))\<lparr>ntfnQueue_tail_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x)))) (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C''])).[0] || v32_' x && 0xFFFFFFF0))) (hrs_mem_update (heap_update (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF))) (t_hrs_' (globals x))) = hrs_mem_update (heap_update (notification_ptr_' x) notification) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<Turnstile>\<^sub>c notification_ptr_' x \<Longrightarrow> \<exists>notification. notification_lift notification = notification_lift (the (cslift x (notification_ptr_' x)))\<lparr>ntfnQueue_tail_CL := v32_' x && ~~ mask 4\<rparr> \<and> hrs_mem_update (heap_update (notification_ptr_' x) (notification_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (notification_ptr_' x)))) (t_hrs_' (globals x)) = hrs_mem_update (heap_update (notification_ptr_' x) notification) (t_hrs_' (globals x)) proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<Turnstile>\<^sub>c notification_ptr_' x \<Longrightarrow> notification_lift (notification_C.words_C_update (\<lambda>_. Arrays.update (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C'']))) 0 (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(32 word[4]) &(notification_ptr_' x\<rightarrow>[''words_C''])).[0] && 0xF || v32_' x && 0xFFFFFFF0)) (h_val (hrs_mem (t_hrs_' (globals x))) (notification_ptr_' x))) = notification_lift (the (cslift x (notification_ptr_' x)))\<lparr>ntfnQueue_tail_CL := v32_' x && ~~ mask 4\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>x v. cslift x (notification_ptr_' x) = Some v \<Longrightarrow> (notification_C.words_C v.[0] && 0xF || v32_' x && 0xFFFFFFF0) && ~~ mask 4 = v32_' x && ~~ mask 4 \<and> (notification_C.words_C v.[0] && 0xF || v32_' x && 0xFFFFFFF0) && mask 2 = notification_C.words_C v.[0] && mask 2 proof (prove)
goal:
No subgoals!