theory RPCFrom

lemma RPCFrom_increment_char_nf:
  notes seL4_SetMR_wp[wp] seL4_GetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s3'. globals_frame_intact s3' \<and>
          is_valid_w8 s3' (ptr_coerce x) \<and>
          ipc_buffer_valid s3'\<rbrace>
   RPCFrom_increment_char' x
  \<lbrace>\<lambda>_ s3'. globals_frame_intact s3' \<and>
           is_valid_w8 s3' (ptr_coerce x) \<and>
           ipc_buffer_valid s3'\<rbrace>!" apply (simp add:RPCFrom_increment_char'_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>s3'. globals_frame_intact s3' \<and> is_valid_w8 s3' (PTR_COERCE(8 word \<rightarrow> 8 word) x) \<and> ipc_buffer_valid s3'\<rbrace> RPCFrom_increment_char' x \<lbrace>\<lambda>_ s3'. globals_frame_intact s3' \<and> is_valid_w8 s3' (PTR_COERCE(8 word \<rightarrow> 8 word) x) \<and> ipc_buffer_valid s3'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s3'. globals_frame_intact s3' \<and> is_valid_w8 s3' x \<and> ipc_buffer_valid s3'\<rbrace> do y <- exec_concrete lift_global_heap (seL4_SetMR' 0 3);
y <- guard (\<lambda>s. is_valid_w8 s x);
mr___unsigned'param <- gets (\<lambda>s. UCAST(8 \<rightarrow> 32) (heap_w8 s x));
y <- exec_concrete lift_global_heap (seL4_SetMR' 1 mr___unsigned'param);
ret' <- seL4_MessageInfo_new' 0 0 0 2;
ret' <- seL4_Call' 6 ret';
ret' <- seL4_GetMR' 0;
y <- guard (\<lambda>s. is_valid_w8 s x);
modify (heap_w8_update (\<lambda>a. a(x := UCAST(32 \<rightarrow> 8) ret')))
od \<lbrace>\<lambda>_ s3'. globals_frame_intact s3' \<and> is_valid_w8 s3' x \<and> ipc_buffer_valid s3'\<rbrace>! proof (prove)
goal (6 subgoals):
 1. \<And>xa y mr___unsigned'param ya. \<lbrace>?B7 xa y mr___unsigned'param ya\<rbrace> seL4_MessageInfo_new' 0 0 0 2 \<lbrace>\<lambda>ret' s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>xa v0 v1 v2 v3 xb. 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 (heap_w8_update (\<lambda>a. a(x := UCAST(32 \<rightarrow> 8) xb)) (setMRs s v0 v1 v2 v3)) \<and> is_valid_w8 (heap_w8_update (\<lambda>a. a(x := UCAST(32 \<rightarrow> 8) xb)) (setMRs s v0 v1 v2 v3)) x \<and> ipc_buffer_valid (heap_w8_update (\<lambda>a. a(x := UCAST(32 \<rightarrow> 8) xb)) (setMRs s v0 v1 v2 v3))) \<and> is_valid_w8 (setMRs s v0 v1 v2 v3) x)\<rbrace>!
 2. \<And>x y mr___unsigned'param. \<lbrace>?B6 x y mr___unsigned'param\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 1 mr___unsigned'param) \<lbrace>?B7 x y mr___unsigned'param\<rbrace>!
 3. \<And>xa y. \<lbrace>?B5 xa y\<rbrace> gets (\<lambda>s. UCAST(8 \<rightarrow> 32) (heap_w8 s x)) \<lbrace>?B6 xa y\<rbrace>!
 4. \<And>xa. \<lbrace>?B4 xa\<rbrace> guard (\<lambda>s. is_valid_w8 s x) \<lbrace>?B5 xa\<rbrace>!
 5. \<lbrace>?Q3\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 0 3) \<lbrace>?B4\<rbrace>!
 6. \<And>s. globals_frame_intact s \<and> is_valid_w8 s x \<and> ipc_buffer_valid s \<Longrightarrow> ?Q3 s proof (prove)
goal (6 subgoals):
 1. \<And>mr___unsigned'param. \<lbrace>?B7 () () mr___unsigned'param ()\<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> (\<forall>xa. globals_frame_intact (heap_w8_update (\<lambda>a. a(x := UCAST(32 \<rightarrow> 8) xa)) (setMRs s v0 v1 v2 v3)) \<and> is_valid_w8 (setMRs s v0 v1 v2 v3) x \<and> ipc_buffer_valid (heap_w8_update (\<lambda>a. a(x := UCAST(32 \<rightarrow> 8) xa)) (setMRs s v0 v1 v2 v3)) \<and> is_valid_w8 (setMRs s v0 v1 v2 v3) x))\<rbrace>!
 2. \<And>x y mr___unsigned'param. \<lbrace>?B6 x y mr___unsigned'param\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 1 mr___unsigned'param) \<lbrace>?B7 x y mr___unsigned'param\<rbrace>!
 3. \<And>xa y. \<lbrace>?B5 xa y\<rbrace> gets (\<lambda>s. UCAST(8 \<rightarrow> 32) (heap_w8 s x)) \<lbrace>?B6 xa y\<rbrace>!
 4. \<And>xa. \<lbrace>?B4 xa\<rbrace> guard (\<lambda>s. is_valid_w8 s x) \<lbrace>?B5 xa\<rbrace>!
 5. \<lbrace>?Q3\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 0 3) \<lbrace>?B4\<rbrace>!
 6. \<And>s. globals_frame_intact s \<and> is_valid_w8 s x \<and> ipc_buffer_valid s \<Longrightarrow> ?Q3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_frame_intact s \<and> is_valid_w8 s x \<and> ipc_buffer_valid s \<Longrightarrow> globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xa. (globals_frame_intact (setMR s (nat 0) 3) \<and> ipc_buffer_valid (setMR s (nat 0) 3) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xa xb. globals_frame_intact (setMR (setMR s (nat 0) 3) (nat 1) (UCAST(8 \<rightarrow> 32) (heap_w8 (setMR s (nat 0) 3) x))) \<and> ipc_buffer_valid (setMR (setMR s (nat 0) 3) (nat 1) (UCAST(8 \<rightarrow> 32) (heap_w8 (setMR s (nat 0) 3) x))) \<and> (\<forall>v0 v1 v2 v3. globals_frame_intact (setMRs (setMR (setMR s (nat 0) 3) (nat 1) (UCAST(8 \<rightarrow> 32) (heap_w8 (setMR s (nat 0) 3) x))) v0 v1 v2 v3) \<and> ipc_buffer_valid (setMRs (setMR (setMR s (nat 0) 3) (nat 1) (UCAST(8 \<rightarrow> 32) (heap_w8 (setMR s (nat 0) 3) x))) v0 v1 v2 v3) \<and> (\<forall>xa. globals_frame_intact (heap_w8_update (\<lambda>a. a(x := UCAST(32 \<rightarrow> 8) xa)) (setMRs (setMR (setMR s (nat 0) 3) (nat 1) (UCAST(8 \<rightarrow> 32) (heap_w8 (setMR s (nat 0) 3) x))) v0 v1 v2 v3)) \<and> is_valid_w8 (setMRs (setMR (setMR s (nat 0) 3) (nat 1) (UCAST(8 \<rightarrow> 32) (heap_w8 (setMR s (nat 0) 3) x))) v0 v1 v2 v3) x \<and> ipc_buffer_valid (heap_w8_update (\<lambda>a. a(x := UCAST(32 \<rightarrow> 8) xa)) (setMRs (setMR (setMR s (nat 0) 3) (nat 1) (UCAST(8 \<rightarrow> 32) (heap_w8 (setMR s (nat 0) 3) x))) v0 v1 v2 v3)) \<and> is_valid_w8 (setMRs (setMR (setMR s (nat 0) 3) (nat 1) (UCAST(8 \<rightarrow> 32) (heap_w8 (setMR s (nat 0) 3) x))) v0 v1 v2 v3) x)))) \<and> is_valid_w8 (setMR s (nat 0) 3) x) proof (prove)
goal:
No subgoals!