theory RPCFrom

lemma RPCFrom_increment_parameter_nf:
  notes seL4_SetMR_wp[wp] seL4_GetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s4'. globals_frame_intact s4' \<and>
          is_valid_w32 s4' (ptr_coerce x) \<and>
          ipc_buffer_valid s4'\<rbrace>
   RPCFrom_increment_parameter' x
  \<lbrace>\<lambda>_ s4'. globals_frame_intact s4' \<and>
           is_valid_w32 s4' (ptr_coerce x) \<and>
           ipc_buffer_valid s4'\<rbrace>!" apply (simp add:RPCFrom_increment_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>s4'. globals_frame_intact s4' \<and> is_valid_w32 s4' (PTR_COERCE(32 signed word \<rightarrow> 32 word) x) \<and> ipc_buffer_valid s4'\<rbrace> RPCFrom_increment_parameter' x \<lbrace>\<lambda>_ s4'. globals_frame_intact s4' \<and> is_valid_w32 s4' (PTR_COERCE(32 signed word \<rightarrow> 32 word) x) \<and> ipc_buffer_valid s4'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s4'. globals_frame_intact s4' \<and> is_valid_w32 s4' (PTR_COERCE(32 signed word \<rightarrow> 32 word) x) \<and> ipc_buffer_valid s4'\<rbrace> do y <- exec_concrete lift_global_heap (seL4_SetMR' 0 4);
y <- guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) x));
mr___unsigned'param <- gets (\<lambda>s. heap_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) 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_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) x));
modify (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) x := ret')))
od \<lbrace>\<lambda>_ s4'. globals_frame_intact s4' \<and> is_valid_w32 s4' (PTR_COERCE(32 signed word \<rightarrow> 32 word) x) \<and> ipc_buffer_valid s4'\<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_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) x := xb)) (setMRs s v0 v1 v2 v3)) \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) x := xb)) (setMRs s v0 v1 v2 v3)) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) x := xb)) (setMRs s v0 v1 v2 v3))) \<and> is_valid_w32 (setMRs s v0 v1 v2 v3) (PTR_COERCE(32 signed word \<rightarrow> 32 word) 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. heap_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) x)) \<lbrace>?B6 xa y\<rbrace>!
 4. \<And>xa. \<lbrace>?B4 xa\<rbrace> guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) x)) \<lbrace>?B5 xa\<rbrace>!
 5. \<lbrace>?Q3\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 0 4) \<lbrace>?B4\<rbrace>!
 6. \<And>s. globals_frame_intact s \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) 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_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) x := xa)) (setMRs s v0 v1 v2 v3)) \<and> is_valid_w32 (setMRs s v0 v1 v2 v3) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) x := xa)) (setMRs s v0 v1 v2 v3)) \<and> is_valid_w32 (setMRs s v0 v1 v2 v3) (PTR_COERCE(32 signed word \<rightarrow> 32 word) 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. heap_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) x)) \<lbrace>?B6 xa y\<rbrace>!
 4. \<And>xa. \<lbrace>?B4 xa\<rbrace> guard (\<lambda>s. is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) x)) \<lbrace>?B5 xa\<rbrace>!
 5. \<lbrace>?Q3\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' 0 4) \<lbrace>?B4\<rbrace>!
 6. \<And>s. globals_frame_intact s \<and> is_valid_w32 s (PTR_COERCE(32 signed word \<rightarrow> 32 word) x) \<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) 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) 4) \<and> ipc_buffer_valid (setMR s (nat 0) 4) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xa xb. globals_frame_intact (setMR (setMR s (nat 0) 4) (nat 1) (heap_w32 (setMR s (nat 0) 4) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x))) \<and> ipc_buffer_valid (setMR (setMR s (nat 0) 4) (nat 1) (heap_w32 (setMR s (nat 0) 4) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x))) \<and> (\<forall>v0 v1 v2 v3. globals_frame_intact (setMRs (setMR (setMR s (nat 0) 4) (nat 1) (heap_w32 (setMR s (nat 0) 4) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x))) v0 v1 v2 v3) \<and> ipc_buffer_valid (setMRs (setMR (setMR s (nat 0) 4) (nat 1) (heap_w32 (setMR s (nat 0) 4) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x))) v0 v1 v2 v3) \<and> (\<forall>xa. globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) x := xa)) (setMRs (setMR (setMR s (nat 0) 4) (nat 1) (heap_w32 (setMR s (nat 0) 4) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x))) v0 v1 v2 v3)) \<and> is_valid_w32 (setMRs (setMR (setMR s (nat 0) 4) (nat 1) (heap_w32 (setMR s (nat 0) 4) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x))) v0 v1 v2 v3) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR_COERCE(32 signed word \<rightarrow> 32 word) x := xa)) (setMRs (setMR (setMR s (nat 0) 4) (nat 1) (heap_w32 (setMR s (nat 0) 4) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x))) v0 v1 v2 v3)) \<and> is_valid_w32 (setMRs (setMR (setMR s (nat 0) 4) (nat 1) (heap_w32 (setMR s (nat 0) 4) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x))) v0 v1 v2 v3) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x))))) \<and> is_valid_w32 (setMR s (nat 0) 4) (PTR_COERCE(32 signed word \<rightarrow> 32 word) x)) proof (prove)
goal:
No subgoals!