theory RPCTo

lemma echo_parameter_internal_wp[wp_unsafe]:
  notes seL4_GetMR_wp[wp] seL4_SetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s49'. globals_frame_intact s49' \<and>
           ipc_buffer_valid s49' \<and>
           tls_valid s49' \<and>
           thread_index_C (tls s49') \<in> {1..thread_count} \<and>
           is_valid_w32 s49' (Ptr (symbol_table ''echo_parameter_pin_1'')) \<and>
           is_valid_w32 s49' (Ptr (symbol_table ''echo_parameter_pin_2'')) \<and>
           is_valid_w32 s49' (Ptr (symbol_table ''echo_parameter_pout_1'')) \<and>
           is_valid_w32 s49' (Ptr (symbol_table ''echo_parameter_pout_2'')) \<and>
           (\<forall>x r50' pin_in_value pout_out_value .
           \<forall> pin_symbol \<in> {''echo_parameter_pin_1'',
           ''echo_parameter_pin_2''}.
           \<forall> pout_symbol \<in> {''echo_parameter_pout_1'',
           ''echo_parameter_pout_2''}.
           P51' x
           (setMR (setMR (update_global_w32 pin_symbol pin_in_value s49') 0
           r50') 1 pout_out_value))\<rbrace>
    echo_parameter_internal'
   \<lbrace>P51'\<rbrace>!" apply (simp add:echo_parameter_internal'_def) apply wp apply (wp RPCTo_echo_parameter_wp)+ apply (wp get_echo_parameter_pout_wp) apply (wp get_echo_parameter_pin_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_w32_def) apply force? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s49'. globals_frame_intact s49' \<and> ipc_buffer_valid s49' \<and> tls_valid s49' \<and> thread_index_C (tls s49') \<in> {1..thread_count} \<and> is_valid_w32 s49' (PTR(32 word) (symbol_table ''echo_parameter_pin_1'')) \<and> is_valid_w32 s49' (PTR(32 word) (symbol_table ''echo_parameter_pin_2'')) \<and> is_valid_w32 s49' (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) \<and> is_valid_w32 s49' (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) \<and> (\<forall>x r50' pin_in_value pout_out_value. \<forall>pin_symbol\<in>{''echo_parameter_pin_1'', ''echo_parameter_pin_2''}. \<forall>pout_symbol\<in>{''echo_parameter_pout_1'', ''echo_parameter_pout_2''}. P51' x (setMR (setMR (update_global_w32 pin_symbol pin_in_value s49') 0 r50') 1 pout_out_value))\<rbrace> echo_parameter_internal' \<lbrace>P51'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s49'. globals_frame_intact s49' \<and> ipc_buffer_valid s49' \<and> tls_valid s49' \<and> 1 \<le> thread_index_C (tls s49') \<and> thread_index_C (tls s49') \<le> thread_count \<and> is_valid_w32 s49' (PTR(32 word) (symbol_table ''echo_parameter_pin_1'')) \<and> is_valid_w32 s49' (PTR(32 word) (symbol_table ''echo_parameter_pin_2'')) \<and> is_valid_w32 s49' (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) \<and> is_valid_w32 s49' (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) \<and> ((\<exists>pout_symbol. pout_symbol = ''echo_parameter_pout_1'' \<or> pout_symbol = ''echo_parameter_pout_2'') \<longrightarrow> (\<forall>x r50' pin_in_value pout_out_value. P51' x (setMR (setMR (update_global_w32 ''echo_parameter_pin_1'' pin_in_value s49') 0 r50') (Suc 0) pout_out_value) \<and> P51' x (setMR (setMR (update_global_w32 ''echo_parameter_pin_2'' pin_in_value s49') 0 r50') (Suc 0) pout_out_value)))\<rbrace> do ret' <- get_echo_parameter_pin';
ret'a <- seL4_GetMR' 1;
y <- guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret'));
y <- modify (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) ret' := ret'a)));
ret'a <- get_echo_parameter_pout';
y <- guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret'));
pin___int'param <- gets (\<lambda>s. sint (ucast_32_to_s32 (heap_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret'))));
ret' <- RPCTo_echo_parameter' pin___int'param ret'a;
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 (word_of_int ret'));
y <- guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret'a));
mr___unsigned'param <- gets (\<lambda>s. heap_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret'a));
y <- exec_concrete lift_global_heap (seL4_SetMR' 1 mr___unsigned'param);
return 2
od \<lbrace>P51'\<rbrace>! proof (prove)
goal (9 subgoals):
 1. \<And>ret' ret'a y ya ret'b yb pin___int'param. \<lbrace>?B30 ret' ret'a y ya ret'b yb pin___int'param\<rbrace> RPCTo_echo_parameter' pin___int'param ret'b \<lbrace>\<lambda>ret'c s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>x. (globals_frame_intact (setMR s (nat 0) (word_of_int ret'c)) \<and> ipc_buffer_valid (setMR s (nat 0) (word_of_int ret'c)) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>x. P51' 2 (setMR (setMR s (nat 0) (word_of_int ret'c)) (nat 1) (heap_w32 (setMR s (nat 0) (word_of_int ret'c)) (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret'b))))) \<and> is_valid_w32 (setMR s (nat 0) (word_of_int ret'c)) (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret'b))\<rbrace>!
 2. \<And>ret' ret'a y ya ret'b yb. \<lbrace>?B29 ret' ret'a y ya ret'b yb\<rbrace> gets (\<lambda>s. sint (ucast_32_to_s32 (heap_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret')))) \<lbrace>?B30 ret' ret'a y ya ret'b yb\<rbrace>!
 3. \<And>ret' ret'a y ya ret'b. \<lbrace>?B28 ret' ret'a y ya ret'b\<rbrace> guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret')) \<lbrace>?B29 ret' ret'a y ya ret'b\<rbrace>!
 4. \<And>ret' ret'a y ya. \<lbrace>?B27 ret' ret'a y ya\<rbrace> get_echo_parameter_pout' \<lbrace>?B28 ret' ret'a y ya\<rbrace>!
 5. \<And>ret' ret'a y. \<lbrace>?B26 ret' ret'a y\<rbrace> modify (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) ret' := ret'a))) \<lbrace>?B27 ret' ret'a y\<rbrace>!
 6. \<And>ret' ret'a. \<lbrace>?B25 ret' ret'a\<rbrace> guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret')) \<lbrace>?B26 ret' ret'a\<rbrace>!
 7. \<And>ret'. \<lbrace>?B24 ret'\<rbrace> seL4_GetMR' 1 \<lbrace>?B25 ret'\<rbrace>!
 8. \<lbrace>?Q23\<rbrace> get_echo_parameter_pin' \<lbrace>?B24\<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_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pin_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pin_2'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) \<and> ((\<exists>pout_symbol. pout_symbol = ''echo_parameter_pout_1'' \<or> pout_symbol = ''echo_parameter_pout_2'') \<longrightarrow> (\<forall>x r50' pin_in_value pout_out_value. P51' x (setMR (setMR (update_global_w32 ''echo_parameter_pin_1'' pin_in_value s) 0 r50') (Suc 0) pout_out_value) \<and> P51' x (setMR (setMR (update_global_w32 ''echo_parameter_pin_2'' pin_in_value s) 0 r50') (Suc 0) pout_out_value))) \<Longrightarrow> ?Q23 s proof (prove)
goal (6 subgoals):
 1. \<And>ret' ret'a y ya. \<lbrace>?B27 ret' ret'a y ya\<rbrace> get_echo_parameter_pout' \<lbrace>\<lambda>ret'b s. (\<forall>r5'. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>x. (globals_frame_intact (setMR s (nat 0) (word_of_int r5')) \<and> ipc_buffer_valid (setMR s (nat 0) (word_of_int r5')) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>x. P51' 2 (setMR (setMR s (nat 0) (word_of_int r5')) (nat 1) (heap_w32 (setMR s (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret'b))))) \<and> is_valid_w32 (setMR s (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret'b))) \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret')\<rbrace>!
 2. \<And>ret' ret'a y. \<lbrace>?B26 ret' ret'a y\<rbrace> modify (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) ret' := ret'a))) \<lbrace>?B27 ret' ret'a y\<rbrace>!
 3. \<And>ret' ret'a. \<lbrace>?B25 ret' ret'a\<rbrace> guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret')) \<lbrace>?B26 ret' ret'a\<rbrace>!
 4. \<And>ret'. \<lbrace>?B24 ret'\<rbrace> seL4_GetMR' 1 \<lbrace>?B25 ret'\<rbrace>!
 5. \<lbrace>?Q23\<rbrace> get_echo_parameter_pin' \<lbrace>?B24\<rbrace>!
 6. \<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_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pin_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pin_2'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) \<and> ((\<exists>pout_symbol. pout_symbol = ''echo_parameter_pout_1'' \<or> pout_symbol = ''echo_parameter_pout_2'') \<longrightarrow> (\<forall>x r50' pin_in_value pout_out_value. P51' x (setMR (setMR (update_global_w32 ''echo_parameter_pin_1'' pin_in_value s) 0 r50') (Suc 0) pout_out_value) \<and> P51' x (setMR (setMR (update_global_w32 ''echo_parameter_pin_2'' pin_in_value s) 0 r50') (Suc 0) pout_out_value))) \<Longrightarrow> ?Q23 s proof (prove)
goal (5 subgoals):
 1. \<And>ret' ret'a y. \<lbrace>?B26 ret' ret'a y\<rbrace> modify (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) ret' := ret'a))) \<lbrace>\<lambda>ya 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_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) \<and> (\<forall>rv. (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pout_1'') \<longrightarrow> (\<forall>r5'. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>x. (globals_frame_intact (setMR s (nat 0) (word_of_int r5')) \<and> ipc_buffer_valid (setMR s (nat 0) (word_of_int r5')) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>x. P51' 2 (setMR (setMR s (nat 0) (word_of_int r5')) (nat 1) (heap_w32 (setMR s (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pout_1''))))))) \<and> is_valid_w32 (setMR s (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pout_1''))))) \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret')) \<and> (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pout_2'') \<longrightarrow> (\<forall>r5'. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>x. (globals_frame_intact (setMR s (nat 0) (word_of_int r5')) \<and> ipc_buffer_valid (setMR s (nat 0) (word_of_int r5')) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>x. P51' 2 (setMR (setMR s (nat 0) (word_of_int r5')) (nat 1) (heap_w32 (setMR s (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pout_2''))))))) \<and> is_valid_w32 (setMR s (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pout_2''))))) \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret')))\<rbrace>!
 2. \<And>ret' ret'a. \<lbrace>?B25 ret' ret'a\<rbrace> guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret')) \<lbrace>?B26 ret' ret'a\<rbrace>!
 3. \<And>ret'. \<lbrace>?B24 ret'\<rbrace> seL4_GetMR' 1 \<lbrace>?B25 ret'\<rbrace>!
 4. \<lbrace>?Q23\<rbrace> get_echo_parameter_pin' \<lbrace>?B24\<rbrace>!
 5. \<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_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pin_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pin_2'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) \<and> ((\<exists>pout_symbol. pout_symbol = ''echo_parameter_pout_1'' \<or> pout_symbol = ''echo_parameter_pout_2'') \<longrightarrow> (\<forall>x r50' pin_in_value pout_out_value. P51' x (setMR (setMR (update_global_w32 ''echo_parameter_pin_1'' pin_in_value s) 0 r50') (Suc 0) pout_out_value) \<and> P51' x (setMR (setMR (update_global_w32 ''echo_parameter_pin_2'' pin_in_value s) 0 r50') (Suc 0) pout_out_value))) \<Longrightarrow> ?Q23 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_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pin_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pin_2'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) \<and> ((\<exists>pout_symbol. pout_symbol = ''echo_parameter_pout_1'' \<or> pout_symbol = ''echo_parameter_pout_2'') \<longrightarrow> (\<forall>x r50' pin_in_value pout_out_value. P51' x (setMR (setMR (update_global_w32 ''echo_parameter_pin_1'' pin_in_value s) 0 r50') (Suc 0) pout_out_value) \<and> P51' x (setMR (setMR (update_global_w32 ''echo_parameter_pin_2'' pin_in_value s) 0 r50') (Suc 0) pout_out_value))) \<Longrightarrow> 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_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pin_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pin_2'')) \<and> (\<forall>rv. (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'') \<longrightarrow> (\<forall>x. 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) \<and> tls_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) \<and> 1 \<le> thread_index_C (tls (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s)) \<and> thread_index_C (tls (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s)) \<le> thread_count \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) \<and> (\<forall>rv. (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pout_1'') \<longrightarrow> (\<forall>r5'. globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. (globals_frame_intact (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (nat 0) (word_of_int r5')) \<and> ipc_buffer_valid (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (nat 0) (word_of_int r5')) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xa. P51' 2 (setMR (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (nat 0) (word_of_int r5')) (nat 1) (heap_w32 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pout_1''))))))) \<and> is_valid_w32 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pout_1''))))) \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')))) \<and> (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pout_2'') \<longrightarrow> (\<forall>r5'. globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. (globals_frame_intact (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (nat 0) (word_of_int r5')) \<and> ipc_buffer_valid (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (nat 0) (word_of_int r5')) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xa. P51' 2 (setMR (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (nat 0) (word_of_int r5')) (nat 1) (heap_w32 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pout_2''))))))) \<and> is_valid_w32 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pout_2''))))) \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')) := x)) s) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'')))))) \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_1''))))) \<and> (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'') \<longrightarrow> (\<forall>x. 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) \<and> tls_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) \<and> 1 \<le> thread_index_C (tls (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s)) \<and> thread_index_C (tls (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s)) \<le> thread_count \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) \<and> (\<forall>rv. (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pout_1'') \<longrightarrow> (\<forall>r5'. globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. (globals_frame_intact (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (nat 0) (word_of_int r5')) \<and> ipc_buffer_valid (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (nat 0) (word_of_int r5')) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xa. P51' 2 (setMR (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (nat 0) (word_of_int r5')) (nat 1) (heap_w32 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pout_1''))))))) \<and> is_valid_w32 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pout_1''))))) \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')))) \<and> (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pout_2'') \<longrightarrow> (\<forall>r5'. globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. (globals_frame_intact (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (nat 0) (word_of_int r5')) \<and> ipc_buffer_valid (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (nat 0) (word_of_int r5')) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xa. P51' 2 (setMR (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (nat 0) (word_of_int r5')) (nat 1) (heap_w32 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pout_2''))))))) \<and> is_valid_w32 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (nat 0) (word_of_int r5')) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pout_2''))))) \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')) := x)) s) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')))))) \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'')))))) proof (prove)
goal (1 subgoal):
 1. \<And>s rv. \<lbrakk>is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)); is_valid_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame))); is_valid_camkes_tls_t_C s (PTR(camkes_tls_t_C) (ptr_val (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame))) && 0xFFFFF000)); 1 \<le> thread_index_C (heap_camkes_tls_t_C s (PTR(camkes_tls_t_C) (ptr_val (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame))) && 0xFFFFF000))); thread_index_C (heap_camkes_tls_t_C s (PTR(camkes_tls_t_C) (ptr_val (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame))) && 0xFFFFF000))) \<le> 2; is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pin_1'')); is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pin_2'')); is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')); is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')); (\<exists>pout_symbol. pout_symbol = ''echo_parameter_pout_1'' \<or> pout_symbol = ''echo_parameter_pout_2'') \<longrightarrow> (\<forall>x r50' pin_in_value pout_out_value. P51' x (heap_w32_update (\<lambda>c. c(PTR(32 word) (symbol_table ''echo_parameter_pin_1'') := pin_in_value)) s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a (Suc 0) pout_out_value) (((heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a 0 r50') (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))) (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))\<rparr>) \<and> P51' x (heap_w32_update (\<lambda>c. c(PTR(32 word) (symbol_table ''echo_parameter_pin_2'') := pin_in_value)) s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a (Suc 0) pout_out_value) (((heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a 0 r50') (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))) (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))\<rparr>))\<rbrakk> \<Longrightarrow> (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pin_1'') \<longrightarrow> (\<forall>x rv. (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pout_1'') \<longrightarrow> (\<forall>r5'. P51' 2 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''echo_parameter_pin_1'') := x)) s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a (Suc 0) (((heap_w32 s)(PTR(32 word) (symbol_table ''echo_parameter_pin_1'') := x)) (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')))) (((heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a 0 (word_of_int r5')) (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))) (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))\<rparr>))) \<and> (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pout_2'') \<longrightarrow> (\<forall>r5'. P51' 2 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''echo_parameter_pin_1'') := x)) s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a (Suc 0) (((heap_w32 s)(PTR(32 word) (symbol_table ''echo_parameter_pin_1'') := x)) (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')))) (((heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a 0 (word_of_int r5')) (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))) (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))\<rparr>))))) \<and> (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pin_2'') \<longrightarrow> (\<forall>x rv. (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pout_1'') \<longrightarrow> (\<forall>r5'. P51' 2 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''echo_parameter_pin_2'') := x)) s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a (Suc 0) (((heap_w32 s)(PTR(32 word) (symbol_table ''echo_parameter_pin_2'') := x)) (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')))) (((heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a 0 (word_of_int r5')) (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))) (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))\<rparr>))) \<and> (rv = PTR(32 signed word) (symbol_table ''echo_parameter_pout_2'') \<longrightarrow> (\<forall>r5'. P51' 2 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''echo_parameter_pin_2'') := x)) s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a (Suc 0) (((heap_w32 s)(PTR(32 word) (symbol_table ''echo_parameter_pin_2'') := x)) (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')))) (((heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a 0 (word_of_int r5')) (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))) (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))\<rparr>))))) proof (prove)
goal:
No subgoals!