theory RPCFrom

lemma RPCFrom_echo_int_nf:
  notes seL4_SetMR_wp[wp] seL4_GetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s0'. globals_frame_intact s0' \<and>
          ipc_buffer_valid s0'\<rbrace>
   RPCFrom_echo_int' i
  \<lbrace>\<lambda>_ s0'. globals_frame_intact s0' \<and>
           ipc_buffer_valid s0'\<rbrace>!" apply (simp add:RPCFrom_echo_int'_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>s0'. globals_frame_intact s0' \<and> ipc_buffer_valid s0'\<rbrace> RPCFrom_echo_int' i \<lbrace>\<lambda>_ s0'. globals_frame_intact s0' \<and> ipc_buffer_valid s0'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0'. globals_frame_intact s0' \<and> ipc_buffer_valid s0'\<rbrace> do y <- exec_concrete lift_global_heap (seL4_SetMR' 0 0);
y <- exec_concrete lift_global_heap (seL4_SetMR' 1 (word_of_int i));
ret' <- seL4_MessageInfo_new' 0 0 0 2;
ret' <- seL4_Call' 6 ret';
ret' <- seL4_GetMR' 0;
return (sint (UCAST(32 \<rightarrow> 32 signed) ret'))
od \<lbrace>\<lambda>_ s0'. globals_frame_intact s0' \<and> ipc_buffer_valid s0'\<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> globals_frame_intact (setMRs s v0 v1 v2 v3) \<and> ipc_buffer_valid (setMRs s v0 v1 v2 v3))\<rbrace>!
 2. \<And>x. \<lbrace>?B4 x\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 1 (word_of_int i)) \<lbrace>?B5 x\<rbrace>!
 3. \<lbrace>?Q3\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 0 0) \<lbrace>?B4\<rbrace>!
 4. \<And>s. globals_frame_intact s \<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))\<rbrace>!
 2. \<And>x. \<lbrace>?B4 x\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 1 (word_of_int i)) \<lbrace>?B5 x\<rbrace>!
 3. \<lbrace>?Q3\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 0 0) \<lbrace>?B4\<rbrace>!
 4. \<And>s. globals_frame_intact s \<and> ipc_buffer_valid s \<Longrightarrow> ?Q3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_frame_intact s \<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) 0) \<and> ipc_buffer_valid (setMR s (nat 0) 0) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>x xa. globals_frame_intact (setMR (setMR s (nat 0) 0) (nat 1) (word_of_int i)) \<and> ipc_buffer_valid (setMR (setMR s (nat 0) 0) (nat 1) (word_of_int i)) \<and> (\<forall>v0 v1 v2 v3. globals_frame_intact (setMRs (setMR (setMR s (nat 0) 0) (nat 1) (word_of_int i)) v0 v1 v2 v3) \<and> ipc_buffer_valid (setMRs (setMR (setMR s (nat 0) 0) (nat 1) (word_of_int i)) v0 v1 v2 v3) \<and> globals_frame_intact (setMRs (setMR (setMR s (nat 0) 0) (nat 1) (word_of_int i)) v0 v1 v2 v3) \<and> ipc_buffer_valid (setMRs (setMR (setMR s (nat 0) 0) (nat 1) (word_of_int i)) v0 v1 v2 v3)))) proof (prove)
goal:
No subgoals!