theory RPCTo

lemma increment_char_internal_wp[wp_unsafe]:
  notes seL4_GetMR_wp[wp] seL4_SetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s55'. globals_frame_intact s55' \<and>
           ipc_buffer_valid s55' \<and>
           tls_valid s55' \<and>
           thread_index_C (tls s55') \<in> {1..thread_count} \<and>
           is_valid_w8 s55' (Ptr (symbol_table ''increment_char_x_1'')) \<and>
           is_valid_w8 s55' (Ptr (symbol_table ''increment_char_x_2'')) \<and>
           (\<forall>x x_in_value x_out_value .
           \<forall> x_symbol \<in> {''increment_char_x_1'',
           ''increment_char_x_2''}.
           P57' x
           (setMR (update_global_w8 x_symbol x_in_value s55') 0 x_out_value)
           )\<rbrace>
    increment_char_internal'
   \<lbrace>P57'\<rbrace>!" apply (simp add:increment_char_internal'_def) apply wp apply (wp RPCTo_increment_char_wp)+ apply (wp get_increment_char_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_w8_def) apply force? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s55'. globals_frame_intact s55' \<and> ipc_buffer_valid s55' \<and> tls_valid s55' \<and> thread_index_C (tls s55') \<in> {1..thread_count} \<and> is_valid_w8 s55' (PTR(8 word) (symbol_table ''increment_char_x_1'')) \<and> is_valid_w8 s55' (PTR(8 word) (symbol_table ''increment_char_x_2'')) \<and> (\<forall>x x_in_value x_out_value. \<forall>x_symbol\<in>{''increment_char_x_1'', ''increment_char_x_2''}. P57' x (setMR (update_global_w8 x_symbol x_in_value s55') 0 x_out_value))\<rbrace> increment_char_internal' \<lbrace>P57'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s55'. globals_frame_intact s55' \<and> ipc_buffer_valid s55' \<and> tls_valid s55' \<and> 1 \<le> thread_index_C (tls s55') \<and> thread_index_C (tls s55') \<le> thread_count \<and> is_valid_w8 s55' (PTR(8 word) (symbol_table ''increment_char_x_1'')) \<and> is_valid_w8 s55' (PTR(8 word) (symbol_table ''increment_char_x_2'')) \<and> (\<forall>x x_in_value x_out_value. P57' x (setMR (update_global_w8 ''increment_char_x_1'' x_in_value s55') 0 x_out_value) \<and> P57' x (setMR (update_global_w8 ''increment_char_x_2'' x_in_value s55') 0 x_out_value))\<rbrace> do ret' <- get_increment_char_x';
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)));
y <- RPCTo_increment_char' ret';
y <- guard (\<lambda>s. is_valid_w8 s ret');
mr___unsigned'param <- gets (\<lambda>s. UCAST(8 \<rightarrow> 32) (heap_w8 s ret'));
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 mr___unsigned'param);
return 1
od \<lbrace>P57'\<rbrace>! proof (prove)
goal (6 subgoals):
 1. \<And>ret' ret'a y ya. \<lbrace>?B13 ret' ret'a y ya\<rbrace> RPCTo_increment_char' ret' \<lbrace>\<lambda>yb s. (globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>x. P57' 1 (setMR s (nat 0) (UCAST(8 \<rightarrow> 32) (heap_w8 s ret'))))) \<and> is_valid_w8 s ret'\<rbrace>!
 2. \<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>!
 3. \<And>ret' ret'a. \<lbrace>?B11 ret' ret'a\<rbrace> guard (\<lambda>s. is_valid_w8 s ret') \<lbrace>?B12 ret' ret'a\<rbrace>!
 4. \<And>ret'. \<lbrace>?B10 ret'\<rbrace> seL4_GetMR' 1 \<lbrace>?B11 ret'\<rbrace>!
 5. \<lbrace>?Q9\<rbrace> get_increment_char_x' \<lbrace>?B10\<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_w8 s (PTR(8 word) (symbol_table ''increment_char_x_1'')) \<and> is_valid_w8 s (PTR(8 word) (symbol_table ''increment_char_x_2'')) \<and> (\<forall>x x_in_value x_out_value. P57' x (setMR (update_global_w8 ''increment_char_x_1'' x_in_value s) 0 x_out_value) \<and> P57' x (setMR (update_global_w8 ''increment_char_x_2'' x_in_value s) 0 x_out_value)) \<Longrightarrow> ?Q9 s proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>?P36 x\<rbrace> get_increment_char_x' \<lbrace>\<lambda>rv s. 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>r14'. (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. P57' 1 (setMR (heap_w8_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 8) x)) s) (nat 0) (UCAST(8 \<rightarrow> 32) (heap_w8 (heap_w8_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 8) x)) s) rv))))) \<and> is_valid_w8 (heap_w8_update (\<lambda>a. a(rv := UCAST(32 \<rightarrow> 8) x)) s) rv) \<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 ''increment_char_x_1'')) \<and> is_valid_w8 s (PTR(8 word) (symbol_table ''increment_char_x_2'')) \<and> (\<forall>x x_in_value x_out_value. P57' x (setMR (update_global_w8 ''increment_char_x_1'' x_in_value s) 0 x_out_value) \<and> P57' x (setMR (update_global_w8 ''increment_char_x_2'' x_in_value s) 0 x_out_value)) \<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 ''increment_char_x_1'')) \<and> is_valid_w8 s (PTR(8 word) (symbol_table ''increment_char_x_2'')) \<and> (\<forall>x x_in_value x_out_value. P57' x (setMR (update_global_w8 ''increment_char_x_1'' x_in_value s) 0 x_out_value) \<and> P57' x (setMR (update_global_w8 ''increment_char_x_2'' x_in_value s) 0 x_out_value)) \<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 ''increment_char_x_1'')) \<and> is_valid_w8 s (PTR(8 word) (symbol_table ''increment_char_x_2'')) \<and> (\<forall>rv. (rv = PTR(8 word) (symbol_table ''increment_char_x_1'') \<longrightarrow> 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>r14'. (globals_frame_intact (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''increment_char_x_1'') := UCAST(32 \<rightarrow> 8) x)) s) \<and> ipc_buffer_valid (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''increment_char_x_1'') := UCAST(32 \<rightarrow> 8) x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. P57' 1 (setMR (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''increment_char_x_1'') := UCAST(32 \<rightarrow> 8) x)) s) (nat 0) (UCAST(8 \<rightarrow> 32) (heap_w8 (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''increment_char_x_1'') := UCAST(32 \<rightarrow> 8) x)) s) (PTR(8 word) (symbol_table ''increment_char_x_1''))))))) \<and> is_valid_w8 (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''increment_char_x_1'') := UCAST(32 \<rightarrow> 8) x)) s) (PTR(8 word) (symbol_table ''increment_char_x_1''))) \<and> is_valid_w8 s (PTR(8 word) (symbol_table ''increment_char_x_1''))) \<and> (rv = PTR(8 word) (symbol_table ''increment_char_x_2'') \<longrightarrow> 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>r14'. (globals_frame_intact (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''increment_char_x_2'') := UCAST(32 \<rightarrow> 8) x)) s) \<and> ipc_buffer_valid (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''increment_char_x_2'') := UCAST(32 \<rightarrow> 8) x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. P57' 1 (setMR (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''increment_char_x_2'') := UCAST(32 \<rightarrow> 8) x)) s) (nat 0) (UCAST(8 \<rightarrow> 32) (heap_w8 (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''increment_char_x_2'') := UCAST(32 \<rightarrow> 8) x)) s) (PTR(8 word) (symbol_table ''increment_char_x_2''))))))) \<and> is_valid_w8 (heap_w8_update (\<lambda>a. a(PTR(8 word) (symbol_table ''increment_char_x_2'') := UCAST(32 \<rightarrow> 8) x)) s) (PTR(8 word) (symbol_table ''increment_char_x_2''))) \<and> is_valid_w8 s (PTR(8 word) (symbol_table ''increment_char_x_2'')))) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!