theory RPCTo

lemma echo_int_internal_wp[wp_unsafe]:
  notes seL4_GetMR_wp[wp] seL4_SetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s46'. globals_frame_intact s46' \<and>
           ipc_buffer_valid s46' \<and>
           tls_valid s46' \<and>
           thread_index_C (tls s46') \<in> {1..thread_count} \<and>
           is_valid_w32 s46' (Ptr (symbol_table ''echo_int_i_1'')) \<and>
           is_valid_w32 s46' (Ptr (symbol_table ''echo_int_i_2'')) \<and>
           (\<forall>x r47' i_in_value .
           \<forall> i_symbol \<in> {''echo_int_i_1'', ''echo_int_i_2''}.
           P48' x
           (setMR (update_global_w32 i_symbol i_in_value s46') 0 r47')
           )\<rbrace>
    echo_int_internal'
   \<lbrace>P48'\<rbrace>!" apply (simp add:echo_int_internal'_def) apply wp apply (wp RPCTo_echo_int_wp)+ apply (wp get_echo_int_i_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>s46'. globals_frame_intact s46' \<and> ipc_buffer_valid s46' \<and> tls_valid s46' \<and> thread_index_C (tls s46') \<in> {1..thread_count} \<and> is_valid_w32 s46' (PTR(32 word) (symbol_table ''echo_int_i_1'')) \<and> is_valid_w32 s46' (PTR(32 word) (symbol_table ''echo_int_i_2'')) \<and> (\<forall>x r47' i_in_value. \<forall>i_symbol\<in>{''echo_int_i_1'', ''echo_int_i_2''}. P48' x (setMR (update_global_w32 i_symbol i_in_value s46') 0 r47'))\<rbrace> echo_int_internal' \<lbrace>P48'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s46'. globals_frame_intact s46' \<and> ipc_buffer_valid s46' \<and> tls_valid s46' \<and> 1 \<le> thread_index_C (tls s46') \<and> thread_index_C (tls s46') \<le> thread_count \<and> is_valid_w32 s46' (PTR(32 word) (symbol_table ''echo_int_i_1'')) \<and> is_valid_w32 s46' (PTR(32 word) (symbol_table ''echo_int_i_2'')) \<and> (\<forall>x r47' i_in_value. P48' x (setMR (update_global_w32 ''echo_int_i_1'' i_in_value s46') 0 r47') \<and> P48' x (setMR (update_global_w32 ''echo_int_i_2'' i_in_value s46') 0 r47'))\<rbrace> do ret' <- get_echo_int_i';
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)));
i___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_int' i___int'param;
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 (word_of_int ret'));
return 1
od \<lbrace>P48'\<rbrace>! proof (prove)
goal (7 subgoals):
 1. \<And>ret' ret'a y ya i___int'param. \<lbrace>?B14 ret' ret'a y ya i___int'param\<rbrace> RPCTo_echo_int' i___int'param \<lbrace>\<lambda>ret'b s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>x. P48' 1 (setMR s (nat 0) (word_of_int ret'b)))\<rbrace>!
 2. \<And>ret' ret'a y ya. \<lbrace>?B13 ret' ret'a y ya\<rbrace> gets (\<lambda>s. sint (ucast_32_to_s32 (heap_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret')))) \<lbrace>?B14 ret' ret'a y ya\<rbrace>!
 3. \<And>ret' ret'a y. \<lbrace>?B12 ret' ret'a y\<rbrace> modify (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) ret' := ret'a))) \<lbrace>?B13 ret' ret'a y\<rbrace>!
 4. \<And>ret' ret'a. \<lbrace>?B11 ret' ret'a\<rbrace> guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret')) \<lbrace>?B12 ret' ret'a\<rbrace>!
 5. \<And>ret'. \<lbrace>?B10 ret'\<rbrace> seL4_GetMR' 1 \<lbrace>?B11 ret'\<rbrace>!
 6. \<lbrace>?Q9\<rbrace> get_echo_int_i' \<lbrace>?B10\<rbrace>!
 7. \<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_int_i_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_int_i_2'')) \<and> (\<forall>x r47' i_in_value. P48' x (setMR (update_global_w32 ''echo_int_i_1'' i_in_value s) 0 r47') \<and> P48' x (setMR (update_global_w32 ''echo_int_i_2'' i_in_value s) 0 r47')) \<Longrightarrow> ?Q9 s proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>?P36 x\<rbrace> get_echo_int_i' \<lbrace>\<lambda>rv s. 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>r1'. globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) rv := x)) s) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) rv := x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. P48' 1 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) rv := x)) s) (nat 0) (word_of_int r1')))) \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) 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_w32 s (PTR(32 word) (symbol_table ''echo_int_i_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_int_i_2'')) \<and> (\<forall>x r47' i_in_value. P48' x (setMR (update_global_w32 ''echo_int_i_1'' i_in_value s) 0 r47') \<and> P48' x (setMR (update_global_w32 ''echo_int_i_2'' i_in_value s) 0 r47')) \<Longrightarrow> \<forall>x. ?P36 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_w32 s (PTR(32 word) (symbol_table ''echo_int_i_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_int_i_2'')) \<and> (\<forall>x r47' i_in_value. P48' x (setMR (update_global_w32 ''echo_int_i_1'' i_in_value s) 0 r47') \<and> P48' x (setMR (update_global_w32 ''echo_int_i_2'' i_in_value s) 0 r47')) \<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_w32 s (PTR(32 word) (symbol_table ''echo_int_i_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_int_i_2'')) \<and> (\<forall>rv. (rv = PTR(32 signed word) (symbol_table ''echo_int_i_1'') \<longrightarrow> 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>r1'. globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_int_i_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_int_i_1'')) := x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. P48' 1 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_int_i_1'')) := x)) s) (nat 0) (word_of_int r1')))) \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_int_i_1'')))) \<and> (rv = PTR(32 signed word) (symbol_table ''echo_int_i_2'') \<longrightarrow> 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>r1'. globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_int_i_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_int_i_2'')) := x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. P48' 1 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_int_i_2'')) := x)) s) (nat 0) (word_of_int r1')))) \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''echo_int_i_2''))))) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!