theory RPCTo

lemma increment_parameter_internal_wp[wp_unsafe]:
  notes seL4_GetMR_wp[wp] seL4_SetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s58'. globals_frame_intact s58' \<and>
           ipc_buffer_valid s58' \<and>
           tls_valid s58' \<and>
           thread_index_C (tls s58') \<in> {1..thread_count} \<and>
           is_valid_w32 s58' (Ptr (symbol_table ''increment_parameter_x_1'')) \<and>
           is_valid_w32 s58' (Ptr (symbol_table ''increment_parameter_x_2'')) \<and>
           (\<forall>x x_in_value x_out_value .
           \<forall> x_symbol \<in> {''increment_parameter_x_1'',
           ''increment_parameter_x_2''}.
           P60' x
           (setMR (update_global_w32 x_symbol x_in_value s58') 0 x_out_value)
           )\<rbrace>
    increment_parameter_internal'
   \<lbrace>P60'\<rbrace>!" apply (simp add:increment_parameter_internal'_def) apply wp apply (wp RPCTo_increment_parameter_wp)+ apply (wp get_increment_parameter_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_w32_def) apply force? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s58'. globals_frame_intact s58' \<and> ipc_buffer_valid s58' \<and> tls_valid s58' \<and> thread_index_C (tls s58') \<in> {1..thread_count} \<and> is_valid_w32 s58' (PTR(32 word) (symbol_table ''increment_parameter_x_1'')) \<and> is_valid_w32 s58' (PTR(32 word) (symbol_table ''increment_parameter_x_2'')) \<and> (\<forall>x x_in_value x_out_value. \<forall>x_symbol\<in>{''increment_parameter_x_1'', ''increment_parameter_x_2''}. P60' x (setMR (update_global_w32 x_symbol x_in_value s58') 0 x_out_value))\<rbrace> increment_parameter_internal' \<lbrace>P60'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s58'. globals_frame_intact s58' \<and> ipc_buffer_valid s58' \<and> tls_valid s58' \<and> 1 \<le> thread_index_C (tls s58') \<and> thread_index_C (tls s58') \<le> thread_count \<and> is_valid_w32 s58' (PTR(32 word) (symbol_table ''increment_parameter_x_1'')) \<and> is_valid_w32 s58' (PTR(32 word) (symbol_table ''increment_parameter_x_2'')) \<and> (\<forall>x x_in_value x_out_value. P60' x (setMR (update_global_w32 ''increment_parameter_x_1'' x_in_value s58') 0 x_out_value) \<and> P60' x (setMR (update_global_w32 ''increment_parameter_x_2'' x_in_value s58') 0 x_out_value))\<rbrace> do ret' <- get_increment_parameter_x';
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)));
y <- RPCTo_increment_parameter' ret';
y <- guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret'));
mr___unsigned'param <- gets (\<lambda>s. heap_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret'));
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 mr___unsigned'param);
return 1
od \<lbrace>P60'\<rbrace>! proof (prove)
goal (6 subgoals):
 1. \<And>ret' ret'a y ya. \<lbrace>?B13 ret' ret'a y ya\<rbrace> RPCTo_increment_parameter' ret' \<lbrace>\<lambda>yb s. (globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>x. P60' 1 (setMR s (nat 0) (heap_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret'))))) \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) ret')\<rbrace>!
 2. \<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>!
 3. \<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>!
 4. \<And>ret'. \<lbrace>?B10 ret'\<rbrace> seL4_GetMR' 1 \<lbrace>?B11 ret'\<rbrace>!
 5. \<lbrace>?Q9\<rbrace> get_increment_parameter_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_w32 s (PTR(32 word) (symbol_table ''increment_parameter_x_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''increment_parameter_x_2'')) \<and> (\<forall>x x_in_value x_out_value. P60' x (setMR (update_global_w32 ''increment_parameter_x_1'' x_in_value s) 0 x_out_value) \<and> P60' x (setMR (update_global_w32 ''increment_parameter_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_parameter_x' \<lbrace>\<lambda>rv s. 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>r18'. (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. P60' 1 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) rv := x)) s) (nat 0) (heap_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) rv := x)) s) (PTR_COERCE(32 signed word \<rightarrow> 32 word) rv))))) \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) rv := x)) s) (PTR_COERCE(32 signed word \<rightarrow> 32 word) rv)) \<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 ''increment_parameter_x_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''increment_parameter_x_2'')) \<and> (\<forall>x x_in_value x_out_value. P60' x (setMR (update_global_w32 ''increment_parameter_x_1'' x_in_value s) 0 x_out_value) \<and> P60' x (setMR (update_global_w32 ''increment_parameter_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_w32 s (PTR(32 word) (symbol_table ''increment_parameter_x_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''increment_parameter_x_2'')) \<and> (\<forall>x x_in_value x_out_value. P60' x (setMR (update_global_w32 ''increment_parameter_x_1'' x_in_value s) 0 x_out_value) \<and> P60' x (setMR (update_global_w32 ''increment_parameter_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_w32 s (PTR(32 word) (symbol_table ''increment_parameter_x_1'')) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''increment_parameter_x_2'')) \<and> (\<forall>rv. (rv = PTR(32 signed word) (symbol_table ''increment_parameter_x_1'') \<longrightarrow> 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>r18'. (globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''increment_parameter_x_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 ''increment_parameter_x_1'')) := x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. P60' 1 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''increment_parameter_x_1'')) := x)) s) (nat 0) (heap_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''increment_parameter_x_1'')) := x)) s) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''increment_parameter_x_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 ''increment_parameter_x_1'')) := x)) s) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''increment_parameter_x_1'')))) \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''increment_parameter_x_1'')))) \<and> (rv = PTR(32 signed word) (symbol_table ''increment_parameter_x_2'') \<longrightarrow> 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>r18'. (globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''increment_parameter_x_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 ''increment_parameter_x_2'')) := x)) s) \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. P60' 1 (setMR (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''increment_parameter_x_2'')) := x)) s) (nat 0) (heap_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''increment_parameter_x_2'')) := x)) s) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''increment_parameter_x_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 ''increment_parameter_x_2'')) := x)) s) (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''increment_parameter_x_2'')))) \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) (PTR(32 signed word) (symbol_table ''increment_parameter_x_2''))))) proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!