theory RPCTo

lemma get_echo_parameter_pout_nf:
  "\<forall>s31'.
    \<lbrace>\<lambda>s32'. globals_frame_intact s32' \<and>
            ipc_buffer_valid s32' \<and>
            tls_valid s32' \<and>
            thread_index_C (tls s32') \<in> {1..thread_count} \<and>
            is_valid_w32 s32' (Ptr (symbol_table ''echo_parameter_pout_1'')) \<and>
            is_valid_w32 s32' (Ptr (symbol_table ''echo_parameter_pout_2'')) \<and>
            s32' = s31'\<rbrace>
     get_echo_parameter_pout'
    \<lbrace>\<lambda>r33' s32'. r33' \<in> {Ptr (symbol_table
      ''echo_parameter_pout_1''), Ptr (symbol_table ''echo_parameter_pout_2'')
      } \<and>
      s32' = s31'\<rbrace>!" apply (rule allI) apply (simp add:get_echo_parameter_pout'_def) apply (wp seL4_GetIPCBuffer_wp) apply (clarsimp simp:thread_count_def tls_valid_def tls_def) apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s31'. \<lbrace>\<lambda>s32'. globals_frame_intact s32' \<and> ipc_buffer_valid s32' \<and> tls_valid s32' \<and> thread_index_C (tls s32') \<in> {1..thread_count} \<and> is_valid_w32 s32' (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) \<and> is_valid_w32 s32' (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) \<and> s32' = s31'\<rbrace> get_echo_parameter_pout' \<lbrace>\<lambda>r33' s32'. r33' \<in> {PTR(32 signed word) (symbol_table ''echo_parameter_pout_1''), PTR(32 signed word) (symbol_table ''echo_parameter_pout_2'')} \<and> s32' = s31'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s31'. \<lbrace>\<lambda>s32'. globals_frame_intact s32' \<and> ipc_buffer_valid s32' \<and> tls_valid s32' \<and> thread_index_C (tls s32') \<in> {1..thread_count} \<and> is_valid_w32 s32' (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) \<and> is_valid_w32 s32' (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) \<and> s32' = s31'\<rbrace> get_echo_parameter_pout' \<lbrace>\<lambda>r33' s32'. r33' \<in> {PTR(32 signed word) (symbol_table ''echo_parameter_pout_1''), PTR(32 signed word) (symbol_table ''echo_parameter_pout_2'')} \<and> s32' = s31'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s31'. \<lbrace>\<lambda>s32'. globals_frame_intact s32' \<and> ipc_buffer_valid s32' \<and> tls_valid s32' \<and> 1 \<le> thread_index_C (tls s32') \<and> thread_index_C (tls s32') \<le> thread_count \<and> is_valid_w32 s32' (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) \<and> is_valid_w32 s32' (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) \<and> s32' = s31'\<rbrace> do ret' <- camkes_get_tls';
y <- guard (\<lambda>s. is_valid_camkes_tls_t_C s ret');
condition (\<lambda>s. thread_index_C (heap_camkes_tls_t_C s ret') = 1)
  (do y <- guard (\<lambda>s. is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')));
return (PTR(32 signed word) (symbol_table ''echo_parameter_pout_1''))
od)
  condition (\<lambda>s. thread_index_C (heap_camkes_tls_t_C s ret') = 2)
  (do y <- guard (\<lambda>s. is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')));
return (PTR(32 signed word) (symbol_table ''echo_parameter_pout_2''))
od)
  (do y <- abort';
fail
od)
od \<lbrace>\<lambda>r33' s32'. (r33' = PTR(32 signed word) (symbol_table ''echo_parameter_pout_1'') \<or> r33' = PTR(32 signed word) (symbol_table ''echo_parameter_pout_2'')) \<and> s32' = s31'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s31' 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> s = s31' \<Longrightarrow> tls_valid s \<and> globals_frame_intact s \<and> (if thread_index_C (heap_camkes_tls_t_C s (tls_ptr s)) = 1 then ((PTR(32 signed word) (symbol_table ''echo_parameter_pout_1'') = PTR(32 signed word) (symbol_table ''echo_parameter_pout_1'') \<or> PTR(32 signed word) (symbol_table ''echo_parameter_pout_1'') = PTR(32 signed word) (symbol_table ''echo_parameter_pout_2'')) \<and> s = s31') \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')) else if thread_index_C (heap_camkes_tls_t_C s (tls_ptr s)) = 2 then ((PTR(32 signed word) (symbol_table ''echo_parameter_pout_2'') = PTR(32 signed word) (symbol_table ''echo_parameter_pout_1'') \<or> PTR(32 signed word) (symbol_table ''echo_parameter_pout_2'') = PTR(32 signed word) (symbol_table ''echo_parameter_pout_2'')) \<and> s = s31') \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')) else False) \<and> is_valid_camkes_tls_t_C s (tls_ptr s) proof (prove)
goal (1 subgoal):
 1. \<And>s31'. \<lbrakk>globals_frame_intact s31'; ipc_buffer_valid s31'; is_valid_camkes_tls_t_C s31' (tls_ptr s31'); 1 \<le> thread_index_C (heap_camkes_tls_t_C s31' (tls_ptr s31')); thread_index_C (heap_camkes_tls_t_C s31' (tls_ptr s31')) \<le> 2; is_valid_w32 s31' (PTR(32 word) (symbol_table ''echo_parameter_pout_1'')); is_valid_w32 s31' (PTR(32 word) (symbol_table ''echo_parameter_pout_2'')); thread_index_C (heap_camkes_tls_t_C s31' (tls_ptr s31')) \<noteq> 2\<rbrakk> \<Longrightarrow> thread_index_C (heap_camkes_tls_t_C s31' (tls_ptr s31')) = 1 proof (prove)
goal:
No subgoals!