theory RPCTo

lemma echo_char_internal_wp[wp_unsafe]:
  notes seL4_GetMR_wp[wp] seL4_SetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s52'. globals_frame_intact s52' \<and>
           ipc_buffer_valid s52' \<and>
           tls_valid s52' \<and>
           thread_index_C (tls s52') \<in> {1..thread_count} \<and>
           is_valid_w8 s52' (Ptr (symbol_table ''echo_char_i_1'')) \<and>
           is_valid_w8 s52' (Ptr (symbol_table ''echo_char_i_2'')) \<and>
           (\<forall>x r53' i_in_value .
           \<forall> i_symbol \<in> {''echo_char_i_1'', ''echo_char_i_2''}.
           P54' x
           (setMR (update_global_w8 i_symbol i_in_value s52') 0 r53')
           )\<rbrace>
    echo_char_internal'
   \<lbrace>P54'\<rbrace>!" apply (simp add:echo_char_internal'_def) apply wp apply (wp RPCTo_echo_char_wp)+ apply (wp get_echo_char_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_w8_def) apply force? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s52'. globals_frame_intact s52' \<and> ipc_buffer_valid s52' \<and> tls_valid s52' \<and> thread_index_C (tls s52') \<in> {1..thread_count} \<and> is_valid_w8 s52' (PTR(8 word) (symbol_table ''echo_char_i_1'')) \<and> is_valid_w8 s52' (PTR(8 word) (symbol_table ''echo_char_i_2'')) \<and> (\<forall>x r53' i_in_value. \<forall>i_symbol\<in>{''echo_char_i_1'', ''echo_char_i_2''}. P54' x (setMR (update_global_w8 i_symbol i_in_value s52') 0 r53'))\<rbrace> echo_char_internal' \<lbrace>P54'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s52'. globals_frame_intact s52' \<and> ipc_buffer_valid s52' \<and> tls_valid s52' \<and> 1 \<le> thread_index_C (tls s52') \<and> thread_index_C (tls s52') \<le> thread_count \<and> is_valid_w8 s52' (PTR(8 word) (symbol_table ''echo_char_i_1'')) \<and> is_valid_w8 s52' (PTR(8 word) (symbol_table ''echo_char_i_2'')) \<and> (\<forall>x r53' i_in_value. P54' x (setMR (update_global_w8 ''echo_char_i_1'' i_in_value s52') 0 r53') \<and> P54' x (setMR (update_global_w8 ''echo_char_i_2'' i_in_value s52') 0 r53'))\<rbrace> do ret' <- get_echo_char_i';
ret'a <- seL4_GetMR' 1;
y <- guard (\<lambda>s. is_valid_w8 s ret');
y <- modify (heap_w8_update (\<lambda>a. a(ret' := UCAST(32 \<rightarrow> 8) ret'a)));
i___char'param <- gets (\<lambda>s. heap_w8 s ret');
ret' <- RPCTo_echo_char' i___char'param;
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 (word_of_int ret'));
return 1
od \<lbrace>P54'\<rbrace>! proof (prove)
goal (7 subgoals):
 1. \<And>ret' ret'a y ya i___char'param. \<lbrace>?B14 ret' ret'a y ya i___char'param\<rbrace> RPCTo_echo_char' i___char'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. P54' 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. heap_w8 s ret') \<lbrace>?B14 ret' ret'a y ya\<rbrace>!
 3. \<And>ret' ret'a y. \<lbrace>?B12 ret' ret'a y\<rbrace> modify (heap_w8_update (\<lambda>a. a(ret' := UCAST(32 \<rightarrow> 8) 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_w8 s 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_char_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_w8 s (PTR(8 word) (symbol_table ''echo_char_i_1'')) \<and> is_valid_w8 s (PTR(8 word) (symbol_table ''echo_char_i_2'')) \<and> (\<forall>x r53' i_in_value. P54' x (setMR (update_global_w8 ''echo_char_i_1'' i_in_value s) 0 r53') \<and> P54' x (setMR (update_global_w8 ''echo_char_i_2'' i_in_value s) 0 r53')) \<Longrightarrow> ?Q9 s proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>?P36 x\<rbrace> get_echo_char_i' \<lbrace>\<lambda>rv s. 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>r10'. globals_frame_intact (heap_w8_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 8) x)) s) \<and> ipc_buffer_valid (heap_w8_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 8) x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. P54' 1 (setMR (heap_w8_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 8) x)) s) (nat 0) (word_of_int r10')))) \<and> is_valid_w8 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_w8 s (PTR(8 word) (symbol_table ''echo_char_i_1'')) \<and> is_valid_w8 s (PTR(8 word) (symbol_table ''echo_char_i_2'')) \<and> (\<forall>x r53' i_in_value. P54' x (setMR (update_global_w8 ''echo_char_i_1'' i_in_value s) 0 r53') \<and> P54' x (setMR (update_global_w8 ''echo_char_i_2'' i_in_value s) 0 r53')) \<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_w8 s (PTR(8 word) (symbol_table ''echo_char_i_1'')) \<and> is_valid_w8 s (PTR(8 word) (symbol_table ''echo_char_i_2'')) \<and> (\<forall>x r53' i_in_value. P54' x (setMR (update_global_w8 ''echo_char_i_1'' i_in_value s) 0 r53') \<and> P54' x (setMR (update_global_w8 ''echo_char_i_2'' i_in_value s) 0 r53')) \<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_w8 s (PTR(8 word) (symbol_table ''echo_char_i_1'')) \<and> is_valid_w8 s (PTR(8 word) (symbol_table ''echo_char_i_2'')) \<and> (\<forall>rv. (rv = PTR(8 word) (symbol_table ''echo_char_i_1'') \<longrightarrow> 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>r10'. globals_frame_intact (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''echo_char_i_1'') := UCAST(32 \<rightarrow> 8) x)) s) \<and> ipc_buffer_valid (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''echo_char_i_1'') := UCAST(32 \<rightarrow> 8) x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. P54' 1 (setMR (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''echo_char_i_1'') := UCAST(32 \<rightarrow> 8) x)) s) (nat 0) (word_of_int r10')))) \<and> is_valid_w8 s (PTR(8 word) (symbol_table ''echo_char_i_1''))) \<and> (rv = PTR(8 word) (symbol_table ''echo_char_i_2'') \<longrightarrow> 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>r10'. globals_frame_intact (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''echo_char_i_2'') := UCAST(32 \<rightarrow> 8) x)) s) \<and> ipc_buffer_valid (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''echo_char_i_2'') := UCAST(32 \<rightarrow> 8) x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. P54' 1 (setMR (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''echo_char_i_2'') := UCAST(32 \<rightarrow> 8) x)) s) (nat 0) (word_of_int r10')))) \<and> is_valid_w8 s (PTR(8 word) (symbol_table ''echo_char_i_2'')))) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!