theory RPCTo

lemma increment_64_internal_wp[wp_unsafe]:
  notes seL4_GetMR_wp[wp] seL4_SetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s61'. globals_frame_intact s61' \<and>
           ipc_buffer_valid s61' \<and>
           tls_valid s61' \<and>
           thread_index_C (tls s61') \<in> {1..thread_count} \<and>
           is_valid_w64 s61' (Ptr (symbol_table ''increment_64_x_1'')) \<and>
           is_valid_w64 s61' (Ptr (symbol_table ''increment_64_x_2'')) \<and>
           (\<forall>x x_in_value x_in_value_high x_out_value x_out_value_high .
           \<forall> x_symbol \<in> {''increment_64_x_1'',
           ''increment_64_x_2''}.
           P63' x
           (setMR (setMR (update_global_w64_high x_symbol x_in_value_high
           (update_global_w64 x_symbol x_in_value s61') ) 0 x_out_value) 1
           x_out_value_high))\<rbrace>
    increment_64_internal'
   \<lbrace>P63'\<rbrace>!" apply (simp add:increment_64_internal'_def) apply wp apply (wp RPCTo_increment_64_wp)+ apply (wp get_increment_64_x_wp)+ apply (clarsimp simp:globals_frame_intact_def ipc_buffer_valid_def
    tls_valid_def tls_def tls_ptr_def thread_count_def setMR_def ucast_id
    update_global_w64_def update_global_w64_high_def) apply force? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s61'. globals_frame_intact s61' \<and> ipc_buffer_valid s61' \<and> tls_valid s61' \<and> thread_index_C (tls s61') \<in> {1..thread_count} \<and> is_valid_w64 s61' (PTR(64 word) (symbol_table ''increment_64_x_1'')) \<and> is_valid_w64 s61' (PTR(64 word) (symbol_table ''increment_64_x_2'')) \<and> (\<forall>x x_in_value x_in_value_high x_out_value x_out_value_high. \<forall>x_symbol\<in>{''increment_64_x_1'', ''increment_64_x_2''}. P63' x (setMR (setMR (update_global_w64_high x_symbol x_in_value_high (update_global_w64 x_symbol x_in_value s61')) 0 x_out_value) 1 x_out_value_high))\<rbrace> increment_64_internal' \<lbrace>P63'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s61'. globals_frame_intact s61' \<and> ipc_buffer_valid s61' \<and> tls_valid s61' \<and> 1 \<le> thread_index_C (tls s61') \<and> thread_index_C (tls s61') \<le> thread_count \<and> is_valid_w64 s61' (PTR(64 word) (symbol_table ''increment_64_x_1'')) \<and> is_valid_w64 s61' (PTR(64 word) (symbol_table ''increment_64_x_2'')) \<and> (\<forall>x x_in_value x_in_value_high x_out_value x_out_value_high. P63' x (setMR (setMR (update_global_w64_high ''increment_64_x_1'' x_in_value_high (update_global_w64 ''increment_64_x_1'' x_in_value s61')) 0 x_out_value) (Suc 0) x_out_value_high) \<and> P63' x (setMR (setMR (update_global_w64_high ''increment_64_x_2'' x_in_value_high (update_global_w64 ''increment_64_x_2'' x_in_value s61')) 0 x_out_value) (Suc 0) x_out_value_high))\<rbrace> do ret' <- get_increment_64_x';
ret'a <- seL4_GetMR' 1;
y <- guard (\<lambda>s. is_valid_w64 s ret');
y <- modify (heap_w64_update (\<lambda>a. a(ret' := UCAST(32 \<rightarrow> 64) ret'a)));
ret'a <- seL4_GetMR' 2;
y <- guard (\<lambda>s. is_valid_w64 s ret');
y <- modify (\<lambda>s. heap_w64_update (\<lambda>a. a(ret' := heap_w64 s ret' || (UCAST(32 \<rightarrow> 64) ret'a << 32))) s);
y <- RPCTo_increment_64' ret';
y <- guard (\<lambda>s. is_valid_w64 s ret');
mr___unsigned'param <- gets (\<lambda>s. UCAST(64 \<rightarrow> 32) (heap_w64 s ret'));
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 mr___unsigned'param);
y <- guard (\<lambda>s. is_valid_w64 s ret');
mr___unsigned'param <- gets (\<lambda>s. UCAST(64 \<rightarrow> 32) (heap_w64 s ret' >> 32));
y <- exec_concrete lift_global_heap (seL4_SetMR' 1 mr___unsigned'param);
return 2
od \<lbrace>P63'\<rbrace>! proof (prove)
goal (9 subgoals):
 1. \<And>x ret' y ya ret'a yb yc. \<lbrace>?B19 x ret' y ya ret'a yb yc\<rbrace> RPCTo_increment_64' x \<lbrace>\<lambda>yd s. (globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. (globals_frame_intact (setMR s (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 s x))) \<and> ipc_buffer_valid (setMR s (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 s x))) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xa. P63' 2 (setMR (setMR s (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 s x))) (nat 1) (UCAST(64 \<rightarrow> 32) (heap_w64 (setMR s (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 s x))) x >> 32))))) \<and> is_valid_w64 (setMR s (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 s x))) x)) \<and> is_valid_w64 s x\<rbrace>!
 2. \<And>x ret' y ya ret'a yb. \<lbrace>?B18 x ret' y ya ret'a yb\<rbrace> modify (\<lambda>s. heap_w64_update (\<lambda>a. a(x := heap_w64 s x || (UCAST(32 \<rightarrow> 64) ret'a << 32))) s) \<lbrace>?B19 x ret' y ya ret'a yb\<rbrace>!
 3. \<And>x ret' y ya ret'a. \<lbrace>?B17 x ret' y ya ret'a\<rbrace> guard (\<lambda>s. is_valid_w64 s x) \<lbrace>?B18 x ret' y ya ret'a\<rbrace>!
 4. \<And>x ret' y ya. \<lbrace>?B16 x ret' y ya\<rbrace> seL4_GetMR' 2 \<lbrace>?B17 x ret' y ya\<rbrace>!
 5. \<And>x ret' y. \<lbrace>?B15 x ret' y\<rbrace> modify (heap_w64_update (\<lambda>a. a(x := UCAST(32 \<rightarrow> 64) ret'))) \<lbrace>?B16 x ret' y\<rbrace>!
 6. \<And>x ret'. \<lbrace>?B14 x ret'\<rbrace> guard (\<lambda>s. is_valid_w64 s x) \<lbrace>?B15 x ret'\<rbrace>!
 7. \<And>x. \<lbrace>?B13 x\<rbrace> seL4_GetMR' 1 \<lbrace>?B14 x\<rbrace>!
 8. \<lbrace>?Q12\<rbrace> get_increment_64_x' \<lbrace>?B13\<rbrace>!
 9. \<And>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> tls_valid s \<and> 1 \<le> thread_index_C (tls s) \<and> thread_index_C (tls s) \<le> thread_count \<and> is_valid_w64 s (PTR(64 word) (symbol_table ''increment_64_x_1'')) \<and> is_valid_w64 s (PTR(64 word) (symbol_table ''increment_64_x_2'')) \<and> (\<forall>x x_in_value x_in_value_high x_out_value x_out_value_high. P63' x (setMR (setMR (update_global_w64_high ''increment_64_x_1'' x_in_value_high (update_global_w64 ''increment_64_x_1'' x_in_value s)) 0 x_out_value) (Suc 0) x_out_value_high) \<and> P63' x (setMR (setMR (update_global_w64_high ''increment_64_x_2'' x_in_value_high (update_global_w64 ''increment_64_x_2'' x_in_value s)) 0 x_out_value) (Suc 0) x_out_value_high)) \<Longrightarrow> ?Q12 s proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>?P58 x\<rbrace> get_increment_64_x' \<lbrace>\<lambda>rv s. 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>xa. 0 \<le> 2 \<and> 2 < 120 \<and> globals_frame_intact (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) \<and> ipc_buffer_valid (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) \<and> (\<forall>r22'. (globals_frame_intact (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) \<and> ipc_buffer_valid (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xb. (globals_frame_intact (setMR (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) rv))) \<and> ipc_buffer_valid (setMR (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) rv))) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xb. P63' 2 (setMR (setMR (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) rv))) (nat 1) (UCAST(64 \<rightarrow> 32) (heap_w64 (setMR (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) rv))) rv >> 32))))) \<and> is_valid_w64 (setMR (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) rv))) rv)) \<and> is_valid_w64 (heap_w64_update (\<lambda>a. a(rv := heap_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s)) rv) \<and> is_valid_w64 (heap_w64_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 64) x)) s) rv) \<and> is_valid_w64 s rv\<rbrace>!
 2. \<And>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> tls_valid s \<and> 1 \<le> thread_index_C (tls s) \<and> thread_index_C (tls s) \<le> thread_count \<and> is_valid_w64 s (PTR(64 word) (symbol_table ''increment_64_x_1'')) \<and> is_valid_w64 s (PTR(64 word) (symbol_table ''increment_64_x_2'')) \<and> (\<forall>x x_in_value x_in_value_high x_out_value x_out_value_high. P63' x (setMR (setMR (update_global_w64_high ''increment_64_x_1'' x_in_value_high (update_global_w64 ''increment_64_x_1'' x_in_value s)) 0 x_out_value) (Suc 0) x_out_value_high) \<and> P63' x (setMR (setMR (update_global_w64_high ''increment_64_x_2'' x_in_value_high (update_global_w64 ''increment_64_x_2'' x_in_value s)) 0 x_out_value) (Suc 0) x_out_value_high)) \<Longrightarrow> \<forall>x. ?P58 x s proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> tls_valid s \<and> 1 \<le> thread_index_C (tls s) \<and> thread_index_C (tls s) \<le> thread_count \<and> is_valid_w64 s (PTR(64 word) (symbol_table ''increment_64_x_1'')) \<and> is_valid_w64 s (PTR(64 word) (symbol_table ''increment_64_x_2'')) \<and> (\<forall>x x_in_value x_in_value_high x_out_value x_out_value_high. P63' x (setMR (setMR (update_global_w64_high ''increment_64_x_1'' x_in_value_high (update_global_w64 ''increment_64_x_1'' x_in_value s)) 0 x_out_value) (Suc 0) x_out_value_high) \<and> P63' x (setMR (setMR (update_global_w64_high ''increment_64_x_2'' x_in_value_high (update_global_w64 ''increment_64_x_2'' x_in_value s)) 0 x_out_value) (Suc 0) x_out_value_high)) \<Longrightarrow> \<forall>x. globals_frame_intact s \<and> ipc_buffer_valid s \<and> tls_valid s \<and> 1 \<le> thread_index_C (tls s) \<and> thread_index_C (tls s) \<le> thread_count \<and> is_valid_w64 s (PTR(64 word) (symbol_table ''increment_64_x_1'')) \<and> is_valid_w64 s (PTR(64 word) (symbol_table ''increment_64_x_2'')) \<and> (\<forall>rv. (rv = PTR(64 word) (symbol_table ''increment_64_x_1'') \<longrightarrow> 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>xa. 0 \<le> 2 \<and> 2 < 120 \<and> globals_frame_intact (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) \<and> ipc_buffer_valid (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) \<and> (\<forall>r22'. (globals_frame_intact (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) \<and> ipc_buffer_valid (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xb. (globals_frame_intact (setMR (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) (PTR(64 word) (symbol_table ''increment_64_x_1''))))) \<and> ipc_buffer_valid (setMR (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) (PTR(64 word) (symbol_table ''increment_64_x_1''))))) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xb. P63' 2 (setMR (setMR (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) (PTR(64 word) (symbol_table ''increment_64_x_1''))))) (nat 1) (UCAST(64 \<rightarrow> 32) (heap_w64 (setMR (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) (PTR(64 word) (symbol_table ''increment_64_x_1''))))) (PTR(64 word) (symbol_table ''increment_64_x_1'')) >> 32))))) \<and> is_valid_w64 (setMR (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) (PTR(64 word) (symbol_table ''increment_64_x_1''))))) (PTR(64 word) (symbol_table ''increment_64_x_1'')))) \<and> is_valid_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s)) (PTR(64 word) (symbol_table ''increment_64_x_1''))) \<and> is_valid_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_1'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_1''))) \<and> is_valid_w64 s (PTR(64 word) (symbol_table ''increment_64_x_1''))) \<and> (rv = PTR(64 word) (symbol_table ''increment_64_x_2'') \<longrightarrow> 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>xa. 0 \<le> 2 \<and> 2 < 120 \<and> globals_frame_intact (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) \<and> ipc_buffer_valid (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) \<and> (\<forall>r22'. (globals_frame_intact (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) \<and> ipc_buffer_valid (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xb. (globals_frame_intact (setMR (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) (PTR(64 word) (symbol_table ''increment_64_x_2''))))) \<and> ipc_buffer_valid (setMR (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) (PTR(64 word) (symbol_table ''increment_64_x_2''))))) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xb. P63' 2 (setMR (setMR (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) (PTR(64 word) (symbol_table ''increment_64_x_2''))))) (nat 1) (UCAST(64 \<rightarrow> 32) (heap_w64 (setMR (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) (PTR(64 word) (symbol_table ''increment_64_x_2''))))) (PTR(64 word) (symbol_table ''increment_64_x_2'')) >> 32))))) \<and> is_valid_w64 (setMR (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) (nat 0) (UCAST(64 \<rightarrow> 32) (heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) (PTR(64 word) (symbol_table ''increment_64_x_2''))))) (PTR(64 word) (symbol_table ''increment_64_x_2'')))) \<and> is_valid_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := heap_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2'')) || (UCAST(32 \<rightarrow> 64) xa << 32))) (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s)) (PTR(64 word) (symbol_table ''increment_64_x_2''))) \<and> is_valid_w64 (heap_w64_update (\<lambda>a. a(PTR(64 word) (symbol_table ''increment_64_x_2'') := UCAST(32 \<rightarrow> 64) x)) s) (PTR(64 word) (symbol_table ''increment_64_x_2''))) \<and> is_valid_w64 s (PTR(64 word) (symbol_table ''increment_64_x_2'')))) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!