kings-crown/FVELER_Isabelle huggingface dataset:
theory RPCTo

lemma seL4_GetIPCBuffer_wp':
  "\<forall>s'. \<lbrace>\<lambda>s. globals_frame_intact s \<and>
             s = s'\<rbrace>
     seL4_GetIPCBuffer'
   \<lbrace>\<lambda>r s. r = heap_seL4_IPCBuffer__C'ptr s (Ptr (scast seL4_GlobalsFrame)) \<and>
          s = s'\<rbrace>!" apply (rule allI) apply (simp add:seL4_GetIPCBuffer'_def) apply wp apply (clarsimp simp:globals_frame_intact_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s'. \<lbrace>\<lambda>s. globals_frame_intact s \<and> s = s'\<rbrace> seL4_GetIPCBuffer' \<lbrace>\<lambda>r s. r = heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) \<and> s = s'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrace>\<lambda>s. globals_frame_intact s \<and> s = s'\<rbrace> seL4_GetIPCBuffer' \<lbrace>\<lambda>r s. r = heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) \<and> s = s'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrace>\<lambda>s. globals_frame_intact s \<and> s = s'\<rbrace> do y <- guard (\<lambda>s. is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)));
gets (\<lambda>s. heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))
od \<lbrace>\<lambda>r s. r = heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) \<and> s = s'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s' s. globals_frame_intact s \<and> s = s' \<Longrightarrow> (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) = heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) \<and> s = s') \<and> is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) proof (prove)
goal:
No subgoals!
theory RPCTo

lemma seL4_SetMR_wp[wp_unsafe]:
  notes seL4_SetMR_axiom[simp]
  shows
  "\<lbrace>\<lambda>s. globals_frame_intact s \<and>
        ipc_buffer_valid s \<and>
        i \<ge> 0 \<and>
        i < seL4_MsgMaxLength \<and>
        (\<forall>x. P x (setMR s (nat i) v))\<rbrace>
     exec_concrete lift_global_heap (seL4_SetMR' i v)
   \<lbrace>P\<rbrace>!" apply (simp add:seL4_SetMR_lifted'_def) apply (wp seL4_GetIPCBuffer_wp) apply (simp add:setMR_def globals_frame_intact_def ipc_buffer_valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> i \<and> i < 120 \<and> (\<forall>x. P x (setMR s (nat i) v))\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' i v) \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> i \<and> i < 120 \<and> P () (setMR s (nat i) v)\<rbrace> do ret' <- seL4_GetIPCBuffer';
y <- guard (\<lambda>s. i < 120);
y <- guard (\<lambda>s. 0 \<le> i);
modify (\<lambda>s. s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(ret' := msg_C_update (\<lambda>a. Arrays.update a (nat i) v) (heap_seL4_IPCBuffer__C s ret'))\<rparr>)
od \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> i \<and> i < 120 \<and> P () (setMR s (nat i) v) \<Longrightarrow> globals_frame_intact s \<and> (P () (s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a (nat i) v) (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))))\<rparr>) \<and> 0 \<le> i) \<and> i < 120 proof (prove)
goal:
No subgoals!
theory RPCTo

lemma seL4_GetMR_wp[wp_unsafe]:
  "\<lbrace>\<lambda>s. \<forall>x. i \<ge> 0 \<and>
            i < seL4_MsgMaxLength \<and>
            globals_frame_intact s \<and>
            ipc_buffer_valid s \<and>
            P x s\<rbrace>
     seL4_GetMR' i
   \<lbrace>P\<rbrace>!" apply (simp add:seL4_GetMR'_def) apply (wp seL4_GetIPCBuffer_wp) apply (simp add:globals_frame_intact_def ipc_buffer_valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x. 0 \<le> i \<and> i < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> P x s\<rbrace> seL4_GetMR' i \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 \<le> i \<and> i < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x. P x s)\<rbrace> do ret' <- seL4_GetIPCBuffer';
y <- guard (\<lambda>s. i < 120);
y <- guard (\<lambda>s. 0 \<le> i);
y <- guard (\<lambda>s. is_valid_seL4_IPCBuffer__C s ret');
gets (\<lambda>s. msg_C (heap_seL4_IPCBuffer__C s ret').[unat (word_of_int i)])
od \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. 0 \<le> i \<and> i < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x. P x s) \<Longrightarrow> globals_frame_intact s \<and> ((P (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))).[unat (word_of_int i)]) s \<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> 0 \<le> i) \<and> i < 120 proof (prove)
goal:
No subgoals!
theory RPCTo

lemma seL4_Wait_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_Wait' cap NULL
   \<lbrace>P\<rbrace>!" apply (simp add:seL4_Wait'_def) apply (wp seL4_SetMR_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_Wait' cap 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 info___struct_seL4_MessageInfo_C <- unknown;
msg0___unsigned <- unknown;
msg1___unsigned <- unknown;
msg2___unsigned <- unknown;
msg3___unsigned <- unknown;
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 msg0___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 1 msg1___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 2 msg2___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 3 msg3___unsigned);
return info___struct_seL4_MessageInfo_C
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> \<forall>x xa xb xc xd. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR s (nat 0) xa) \<and> ipc_buffer_valid (setMR s (nat 0) xa) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR (setMR s (nat 0) xa) (nat 1) xb) \<and> ipc_buffer_valid (setMR (setMR s (nat 0) xa) (nat 1) xb) \<and> 0 \<le> 2 \<and> 2 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) \<and> ipc_buffer_valid (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) \<and> 0 \<le> 3 \<and> 3 < 120 \<and> (\<forall>xe. P x (setMR (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) (nat 3) xd))))) proof (prove)
goal:
No subgoals!
theory RPCTo

lemma camkes_get_tls_wp':
  "\<forall>s'. \<lbrace>\<lambda>s. tls_valid s \<and> globals_frame_intact s \<and> s = s'\<rbrace>
     camkes_get_tls'
   \<lbrace>\<lambda>r s. s = s' \<and> r = tls_ptr s\<rbrace>!" apply (rule allI) apply (simp add:camkes_get_tls'_def seL4_GetIPCBuffer'_def tls_valid_def) apply wp apply (clarsimp simp:globals_frame_intact_def tls_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s'. \<lbrace>\<lambda>s. tls_valid s \<and> globals_frame_intact s \<and> s = s'\<rbrace> camkes_get_tls' \<lbrace>\<lambda>r s. s = s' \<and> r = tls_ptr s\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrace>\<lambda>s. tls_valid s \<and> globals_frame_intact s \<and> s = s'\<rbrace> camkes_get_tls' \<lbrace>\<lambda>r s. s = s' \<and> r = tls_ptr s\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrace>\<lambda>s. is_valid_camkes_tls_t_C s (tls_ptr s) \<and> globals_frame_intact s \<and> s = s'\<rbrace> do ret' <- do y <- guard (\<lambda>s. is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)));
gets (\<lambda>s. heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)))
od;
return (PTR(camkes_tls_t_C) (ptr_val ret' && 0xFFFFF000))
od \<lbrace>\<lambda>r s. s = s' \<and> r = tls_ptr s\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s' s. is_valid_camkes_tls_t_C s (tls_ptr s) \<and> globals_frame_intact s \<and> s = s' \<Longrightarrow> (s = s' \<and> PTR(camkes_tls_t_C) (ptr_val (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame))) && 0xFFFFF000) = tls_ptr s) \<and> is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (scast_s32_to_32 seL4_GlobalsFrame)) proof (prove)
goal:
No subgoals!
theory EventFrom

lemma EventFrom__run_nf: "\<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> EventFrom__run' \<lbrace>P\<rbrace>!" apply (unfold EventFrom__run'_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> EventFrom__run' \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> return 0 \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>r. P r s \<Longrightarrow> P 0 s proof (prove)
goal:
No subgoals!
theory EventFrom

lemma EventFrom_emit_nf: "\<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> EventFrom_emit_underlying' \<lbrace>P\<rbrace>!" apply (simp add:EventFrom_emit_underlying'_def) apply (wp seL4_Notify_wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> EventFrom_emit_underlying' \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>P ()\<rbrace> seL4_Notify' 6 0 \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. P () s \<Longrightarrow> \<forall>x. P x s proof (prove)
goal:
No subgoals!
theory EventTo

lemma seL4_SetMR_wp[wp_unsafe]:
  notes seL4_SetMR_axiom[simp]
  shows
  "\<lbrace>\<lambda>s. globals_frame_intact s \<and>
        ipc_buffer_valid s \<and>
        i \<ge> 0 \<and>
        i < seL4_MsgMaxLength \<and>
        (\<forall>x. P x (setMR s (nat i) v))\<rbrace>
     exec_concrete lift_global_heap (seL4_SetMR' i v)
   \<lbrace>P\<rbrace>!" apply (simp add:seL4_SetMR_lifted'_def seL4_GetIPCBuffer'_def) apply wp apply (simp add:setMR_def globals_frame_intact_def ipc_buffer_valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> i \<and> i < 120 \<and> (\<forall>x. P x (setMR s (nat i) v))\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' i v) \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> i \<and> i < 120 \<and> P () (setMR s (nat i) v)\<rbrace> do ret' <- do y <- guard (\<lambda>s. is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)));
gets (\<lambda>s. heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)))
od;
y <- guard (\<lambda>s. i < 120);
y <- guard (\<lambda>s. 0 \<le> i);
modify (\<lambda>s. s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(ret' := msg_C_update (\<lambda>a. Arrays.update a (nat i) v) (heap_seL4_IPCBuffer__C s ret'))\<rparr>)
od \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> i \<and> i < 120 \<and> P () (setMR s (nat i) v) \<Longrightarrow> ((P () (s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a (nat i) v) (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)))))\<rparr>) \<and> 0 \<le> i) \<and> i < 120) \<and> is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)) proof (prove)
goal:
No subgoals!
theory EventTo

lemma seL4_GetIPCBuffer_wp[wp_unsafe]: "\<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> seL4_GetIPCBuffer' \<lbrace>P\<rbrace>" apply (unfold seL4_GetIPCBuffer'_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> seL4_GetIPCBuffer' \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> do guard (\<lambda>s. is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)));
gets (\<lambda>s. heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)))
od \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>x. P x s \<Longrightarrow> is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)) \<longrightarrow> P (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame))) s proof (prove)
goal:
No subgoals!
theory EventTo

lemma camkes_get_tls_wp':
  "\<forall>s'. \<lbrace>\<lambda>s. tls_valid s \<and> globals_frame_intact s \<and> s = s'\<rbrace>
     camkes_get_tls'
   \<lbrace>\<lambda>r s. s = s' \<and> r = tls_ptr s\<rbrace>!" apply (rule allI) apply (simp add:camkes_get_tls'_def seL4_GetIPCBuffer'_def tls_valid_def) apply wp apply (clarsimp simp:globals_frame_intact_def tls_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s'. \<lbrace>\<lambda>s. tls_valid s \<and> globals_frame_intact s \<and> s = s'\<rbrace> camkes_get_tls' \<lbrace>\<lambda>r s. s = s' \<and> r = tls_ptr s\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrace>\<lambda>s. tls_valid s \<and> globals_frame_intact s \<and> s = s'\<rbrace> camkes_get_tls' \<lbrace>\<lambda>r s. s = s' \<and> r = tls_ptr s\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrace>\<lambda>s. is_valid_camkes_tls_t_C s (tls_ptr s) \<and> globals_frame_intact s \<and> s = s'\<rbrace> do ret' <- do y <- guard (\<lambda>s. is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)));
gets (\<lambda>s. heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)))
od;
return (PTR(camkes_tls_t_C) (ptr_val ret' && 0xFFFFF000))
od \<lbrace>\<lambda>r s. s = s' \<and> r = tls_ptr s\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s' s. is_valid_camkes_tls_t_C s (tls_ptr s) \<and> globals_frame_intact s \<and> s = s' \<Longrightarrow> (s = s' \<and> PTR(camkes_tls_t_C) (ptr_val (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame))) && 0xFFFFF000) = tls_ptr s) \<and> is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)) proof (prove)
goal:
No subgoals!
theory EventTo

lemma abort_wp[wp]:
  "\<lbrace>\<lambda>_. False\<rbrace> abort' \<lbrace>P\<rbrace>!" apply (rule validNF_false_pre) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. False\<rbrace> abort' \<lbrace>P\<rbrace>! proof (prove)
goal:
No subgoals!
theory EventTo

lemma seL4_Poll_wp[wp_unsafe]:
  "\<lbrace>\<lambda>s. globals_frame_intact s \<and>
        ipc_buffer_valid s \<and>
        (\<forall>x b v0 v1 v2 v3. P x (heap_w32_update (\<lambda>a. a(badge := b)) (setMRs s v0 v1 v2 v3))) \<and>
        badge \<noteq> NULL \<and>
        is_valid_w32 s badge \<rbrace>
     seL4_Poll' cap badge
   \<lbrace>P\<rbrace>!" apply (simp add:seL4_Poll'_def seL4_GetIPCBuffer'_def) apply (wp seL4_SetMR_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 b v0 v1 v2 v3. P x (heap_w32_update (\<lambda>a. a(badge := b)) (setMRs s v0 v1 v2 v3))) \<and> badge \<noteq> NULL \<and> is_valid_w32 s badge\<rbrace> seL4_Poll' cap badge \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x b v0 v1 v2 v3. P x (heap_w32_update (\<lambda>a. a(badge := b)) (setMRs s v0 v1 v2 v3))) \<and> badge \<noteq> NULL \<and> is_valid_w32 s badge\<rbrace> do info___struct_seL4_MessageInfo_C <- unknown;
msg0___unsigned <- unknown;
msg1___unsigned <- unknown;
msg2___unsigned <- unknown;
msg3___unsigned <- unknown;
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 msg0___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 1 msg1___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 2 msg2___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 3 msg3___unsigned);
y <- when (badge \<noteq> NULL) (do y <- guard (\<lambda>s. is_valid_w32 s badge);
modify (heap_w32_update (\<lambda>a. a(badge := cap)))
od);
return info___struct_seL4_MessageInfo_C
od \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x b v0 v1 v2 v3. P x (heap_w32_update (\<lambda>a. a(badge := b)) (setMRs s v0 v1 v2 v3))) \<and> badge \<noteq> NULL \<and> is_valid_w32 s badge \<Longrightarrow> \<forall>x xa xb xc xd. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR s (nat 0) xa) \<and> ipc_buffer_valid (setMR s (nat 0) xa) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR (setMR s (nat 0) xa) (nat 1) xb) \<and> ipc_buffer_valid (setMR (setMR s (nat 0) xa) (nat 1) xb) \<and> 0 \<le> 2 \<and> 2 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) \<and> ipc_buffer_valid (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) \<and> 0 \<le> 3 \<and> 3 < 120 \<and> (\<forall>xe. if badge \<noteq> NULL then P x (heap_w32_update (\<lambda>a. a(badge := cap)) (setMR (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) (nat 3) xd)) \<and> is_valid_w32 (setMR (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) (nat 3) xd) badge else P x (setMR (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) (nat 3) xd))))) proof (prove)
goal:
No subgoals!
theory EventTo

lemma seL4_Wait_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_Wait' cap NULL
   \<lbrace>P\<rbrace>!" apply (simp add:seL4_Wait'_def seL4_GetIPCBuffer'_def) apply (wp seL4_SetMR_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_Wait' cap 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 info___struct_seL4_MessageInfo_C <- unknown;
msg0___unsigned <- unknown;
msg1___unsigned <- unknown;
msg2___unsigned <- unknown;
msg3___unsigned <- unknown;
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 msg0___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 1 msg1___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 2 msg2___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 3 msg3___unsigned);
return info___struct_seL4_MessageInfo_C
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> \<forall>x xa xb xc xd. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR s (nat 0) xa) \<and> ipc_buffer_valid (setMR s (nat 0) xa) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR (setMR s (nat 0) xa) (nat 1) xb) \<and> ipc_buffer_valid (setMR (setMR s (nat 0) xa) (nat 1) xb) \<and> 0 \<le> 2 \<and> 2 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) \<and> ipc_buffer_valid (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) \<and> 0 \<le> 3 \<and> 3 < 120 \<and> (\<forall>xe. P x (setMR (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) (nat 3) xd))))) proof (prove)
goal:
No subgoals!
theory EventTo

lemma EventTo_run_nf: "\<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> EventTo__run' \<lbrace>P\<rbrace>!" apply (unfold EventTo__run'_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> EventTo__run' \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> return 0 \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>r. P r s \<Longrightarrow> P 0 s proof (prove)
goal:
No subgoals!
theory EventTo

lemma EventTo_wait_nf:
  notes seL4_SetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s\<rbrace>
    EventTo_wait'
   \<lbrace>\<lambda>_ s. globals_frame_intact s \<and> ipc_buffer_valid s\<rbrace>!" apply (simp add:EventTo_wait'_def) apply (wp seL4_Wait_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\<rbrace> EventTo_wait' \<lbrace>\<lambda>_ s. globals_frame_intact s \<and> ipc_buffer_valid s\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s\<rbrace> do ret' <- seL4_Wait' 6 NULL;
skip
od \<lbrace>\<lambda>_ s. globals_frame_intact s \<and> ipc_buffer_valid s\<rbrace>! 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> (\<forall>x v0 v1 v2 v3. globals_frame_intact (setMRs s v0 v1 v2 v3) \<and> ipc_buffer_valid (setMRs s v0 v1 v2 v3)) proof (prove)
goal:
No subgoals!
theory DataIn

lemma DataIn__run_nf: "\<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> DataIn__run' \<lbrace>P\<rbrace>!" apply (simp add:DataIn__run'_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> DataIn__run' \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> return 0 \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>r. P r s \<Longrightarrow> P 0 s proof (prove)
goal:
No subgoals!