theory RPCFrom

lemma RPCFrom_echo_parameter_nf:
  notes seL4_SetMR_wp[wp] seL4_GetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s1'. globals_frame_intact s1' \<and>
          is_valid_w32 s1' (ptr_coerce pout) \<and>
          ipc_buffer_valid s1'\<rbrace>
   RPCFrom_echo_parameter' pin pout
  \<lbrace>\<lambda>_ s1'. globals_frame_intact s1' \<and>
           is_valid_w32 s1' (ptr_coerce pout) \<and>
           ipc_buffer_valid s1'\<rbrace>!" apply (simp add:RPCFrom_echo_parameter'_def) apply (wp seL4_Call_wp) apply (simp add:seL4_MessageInfo_new'_def) apply wp+ apply (simp add:globals_frame_intact_def ipc_buffer_valid_def
                  setMRs_def setMR_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s1'. globals_frame_intact s1' \<and> is_valid_w32 s1' (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout) \<and> ipc_buffer_valid s1'\<rbrace> RPCFrom_echo_parameter' pin pout \<lbrace>\<lambda>_ s1'. globals_frame_intact s1' \<and> is_valid_w32 s1' (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout) \<and> ipc_buffer_valid s1'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s1'. globals_frame_intact s1' \<and> is_valid_w32 s1' (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout) \<and> ipc_buffer_valid s1'\<rbrace> do y <- exec_concrete lift_global_heap (seL4_SetMR' 0 1);
y <- exec_concrete lift_global_heap (seL4_SetMR' 1 (word_of_int pin));
ret' <- seL4_MessageInfo_new' 0 0 0 2;
ret' <- seL4_Call' 6 ret';
ret' <- seL4_GetMR' 0;
ret'a <- seL4_GetMR' 1;
y <- guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout));
y <- modify (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) pout := ret'a)));
return (sint (UCAST(32 \<rightarrow> 32 signed) ret'))
od \<lbrace>\<lambda>_ s1'. globals_frame_intact s1' \<and> is_valid_w32 s1' (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout) \<and> ipc_buffer_valid s1'\<rbrace>! proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrace>?B5 x y\<rbrace> seL4_MessageInfo_new' 0 0 0 2 \<lbrace>\<lambda>ret' s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x v0 v1 v2 v3 xa. 0 \<le> 0 \<and> 0 < 120 \<and> globals_frame_intact (setMRs s v0 v1 v2 v3) \<and> ipc_buffer_valid (setMRs s v0 v1 v2 v3) \<and> (\<forall>x. 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact (setMRs s v0 v1 v2 v3) \<and> ipc_buffer_valid (setMRs s v0 v1 v2 v3) \<and> (globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) pout := x)) (setMRs s v0 v1 v2 v3)) \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) pout := x)) (setMRs s v0 v1 v2 v3)) (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) pout := x)) (setMRs s v0 v1 v2 v3))) \<and> is_valid_w32 (setMRs s v0 v1 v2 v3) (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout)))\<rbrace>!
 2. \<And>x. \<lbrace>?B4 x\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 1 (word_of_int pin)) \<lbrace>?B5 x\<rbrace>!
 3. \<lbrace>?Q3\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 0 1) \<lbrace>?B4\<rbrace>!
 4. \<And>s. globals_frame_intact s \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout) \<and> ipc_buffer_valid s \<Longrightarrow> ?Q3 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?B5 () ()\<rbrace> do seL4_MessageInfo___struct_seL4_MessageInfo_C <- unknown;
return (seL4_MessageInfo_C.words_C_update (\<lambda>x. Arrays.update (seL4_MessageInfo_C.words_C seL4_MessageInfo___struct_seL4_MessageInfo_C) 0 2) seL4_MessageInfo___struct_seL4_MessageInfo_C)
od \<lbrace>\<lambda>ret' s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>v0 v1 v2 v3. globals_frame_intact (setMRs s v0 v1 v2 v3) \<and> ipc_buffer_valid (setMRs s v0 v1 v2 v3) \<and> globals_frame_intact (setMRs s v0 v1 v2 v3) \<and> ipc_buffer_valid (setMRs s v0 v1 v2 v3) \<and> (\<forall>x. globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) pout := x)) (setMRs s v0 v1 v2 v3)) \<and> is_valid_w32 (setMRs s v0 v1 v2 v3) (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) pout := x)) (setMRs s v0 v1 v2 v3)) \<and> is_valid_w32 (setMRs s v0 v1 v2 v3) (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout)))\<rbrace>!
 2. \<And>x. \<lbrace>?B4 x\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 1 (word_of_int pin)) \<lbrace>?B5 x\<rbrace>!
 3. \<lbrace>?Q3\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 0 1) \<lbrace>?B4\<rbrace>!
 4. \<And>s. globals_frame_intact s \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout) \<and> ipc_buffer_valid s \<Longrightarrow> ?Q3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_frame_intact s \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout) \<and> ipc_buffer_valid s \<Longrightarrow> globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>x. globals_frame_intact (setMR s (nat 0) 1) \<and> ipc_buffer_valid (setMR s (nat 0) 1) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>x xa. globals_frame_intact (setMR (setMR s (nat 0) 1) (nat 1) (word_of_int pin)) \<and> ipc_buffer_valid (setMR (setMR s (nat 0) 1) (nat 1) (word_of_int pin)) \<and> (\<forall>v0 v1 v2 v3. globals_frame_intact (setMRs (setMR (setMR s (nat 0) 1) (nat 1) (word_of_int pin)) v0 v1 v2 v3) \<and> ipc_buffer_valid (setMRs (setMR (setMR s (nat 0) 1) (nat 1) (word_of_int pin)) v0 v1 v2 v3) \<and> globals_frame_intact (setMRs (setMR (setMR s (nat 0) 1) (nat 1) (word_of_int pin)) v0 v1 v2 v3) \<and> ipc_buffer_valid (setMRs (setMR (setMR s (nat 0) 1) (nat 1) (word_of_int pin)) v0 v1 v2 v3) \<and> (\<forall>x. globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) pout := x)) (setMRs (setMR (setMR s (nat 0) 1) (nat 1) (word_of_int pin)) v0 v1 v2 v3)) \<and> is_valid_w32 (setMRs (setMR (setMR s (nat 0) 1) (nat 1) (word_of_int pin)) v0 v1 v2 v3) (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) pout := x)) (setMRs (setMR (setMR s (nat 0) 1) (nat 1) (word_of_int pin)) v0 v1 v2 v3)) \<and> is_valid_w32 (setMRs (setMR (setMR s (nat 0) 1) (nat 1) (word_of_int pin)) v0 v1 v2 v3) (PTR_COERCE(32 signed word \<rightarrow> 32 word) pout))))) proof (prove)
goal:
No subgoals!