theory RPCTo

lemma seL4_ReplyWait_wp[wp_unsafe]:
  "\<lbrace>\<lambda>s. globals_frame_intact s \<and>
        ipc_buffer_valid s \<and>
        (\<forall>x v0 v1 v2 v3. P x (setMRs s v0 v1 v2 v3))\<rbrace>
     seL4_ReplyWait' cap info NULL
   \<lbrace>P\<rbrace>!" apply (simp add:seL4_ReplyWait'_def seL4_GetMR'_def) apply (wp seL4_SetMR_wp seL4_GetIPCBuffer_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>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x v0 v1 v2 v3. P x (setMRs s v0 v1 v2 v3))\<rbrace> seL4_ReplyWait' cap info NULL \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x v0 v1 v2 v3. P x (setMRs s v0 v1 v2 v3))\<rbrace> do ret' <- do ret' <- seL4_GetIPCBuffer';
y <- guard (\<lambda>s. is_valid_seL4_IPCBuffer__C s ret');
gets (\<lambda>s. msg_C (heap_seL4_IPCBuffer__C s ret').[0])
od;
ret'a <- do ret' <- seL4_GetIPCBuffer';
y <- guard (\<lambda>s. is_valid_seL4_IPCBuffer__C s ret');
gets (\<lambda>s. msg_C (heap_seL4_IPCBuffer__C s ret').[Suc 0])
od;
ret'b <- do ret' <- seL4_GetIPCBuffer';
y <- guard (\<lambda>s. is_valid_seL4_IPCBuffer__C s ret');
gets (\<lambda>s. msg_C (heap_seL4_IPCBuffer__C s ret').[2])
od;
ret'c <- do ret' <- seL4_GetIPCBuffer';
y <- guard (\<lambda>s. is_valid_seL4_IPCBuffer__C s ret');
gets (\<lambda>s. msg_C (heap_seL4_IPCBuffer__C s ret').[3])
od;
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 ret');
y <- exec_concrete lift_global_heap (seL4_SetMR' 1 ret'a);
y <- exec_concrete lift_global_heap (seL4_SetMR' 2 ret'b);
y <- exec_concrete lift_global_heap (seL4_SetMR' 3 ret'c);
return info
od \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x v0 v1 v2 v3. P x (setMRs s v0 v1 v2 v3)) \<Longrightarrow> globals_frame_intact s \<and> (globals_frame_intact s \<and> (globals_frame_intact s \<and> (globals_frame_intact s \<and> (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) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[0])) \<and> ipc_buffer_valid (setMR s (nat 0) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[0])) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>x. globals_frame_intact (setMR (setMR s (nat 0) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[0])) (nat 1) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[Suc 0])) \<and> ipc_buffer_valid (setMR (setMR s (nat 0) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[0])) (nat 1) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[Suc 0])) \<and> 0 \<le> 2 \<and> 2 < 120 \<and> (\<forall>x. globals_frame_intact (setMR (setMR (setMR s (nat 0) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[0])) (nat 1) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[Suc 0])) (nat 2) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[2])) \<and> ipc_buffer_valid (setMR (setMR (setMR s (nat 0) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[0])) (nat 1) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[Suc 0])) (nat 2) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[2])) \<and> 0 \<le> 3 \<and> 3 < 120 \<and> (\<forall>x. P info (setMR (setMR (setMR (setMR s (nat 0) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[0])) (nat 1) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[Suc 0])) (nat 2) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[2])) (nat 3) (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[3]))))))) \<and> is_valid_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))) \<and> is_valid_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))) \<and> is_valid_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))) \<and> is_valid_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame))) proof (prove)
goal:
No subgoals!