theory EventTo

lemma EventTo_poll_nf:
  notes seL4_SetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s. is_valid_w32 s (Ptr (symbol_table ''badge_1'')) \<and>
        Ptr (symbol_table ''badge_1'') \<noteq> NULL \<and>
        is_valid_w32 s (Ptr (symbol_table ''badge_2'')) \<and>
        Ptr (symbol_table ''badge_2'') \<noteq> NULL \<and>
        globals_frame_intact s \<and>
        ipc_buffer_valid s \<and>
        tls_valid s \<and>
        thread_index_C (tls s) \<in> {1..thread_count}\<rbrace>
   EventTo_poll'
  \<lbrace>\<lambda>r s. is_valid_w32 s (Ptr (symbol_table ''badge_1'')) \<and>
         Ptr (symbol_table ''badge_1'') \<noteq> NULL \<and>
         is_valid_w32 s (Ptr (symbol_table ''badge_2'')) \<and>
         Ptr (symbol_table ''badge_2'') \<noteq> NULL \<and>
         globals_frame_intact s \<and>
         ipc_buffer_valid s \<and>
         tls_valid s \<and>
         thread_index_C (tls s) \<in> {1..thread_count} \<and>
         (r = 0 \<or> r = 1)\<rbrace>!" apply (simp add:EventTo_poll'_def get_badge'_def) apply (wp seL4_Poll_wp) apply (clarsimp simp:globals_frame_intact_def seL4_GetIPCBuffer'_def
                       thread_count_def setMRs_def setMR_def
                       ipc_buffer_valid_def tls_valid_def tls_ptr_def
                       tls_def) apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_valid_w32 s (PTR(32 word) (symbol_table ''badge_1'')) \<and> PTR('a) (symbol_table ''badge_1'') \<noteq> NULL \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''badge_2'')) \<and> PTR('b) (symbol_table ''badge_2'') \<noteq> NULL \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> tls_valid s \<and> thread_index_C (tls s) \<in> {1..thread_count}\<rbrace> EventTo_poll' \<lbrace>\<lambda>r s. is_valid_w32 s (PTR(32 word) (symbol_table ''badge_1'')) \<and> PTR('c) (symbol_table ''badge_1'') \<noteq> NULL \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''badge_2'')) \<and> PTR('d) (symbol_table ''badge_2'') \<noteq> NULL \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> tls_valid s \<and> thread_index_C (tls s) \<in> {1..thread_count} \<and> (r = 0 \<or> r = 1)\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_valid_w32 s (PTR(32 word) (symbol_table ''badge_1'')) \<and> symbol_table ''badge_1'' \<noteq> 0 \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''badge_2'')) \<and> symbol_table ''badge_2'' \<noteq> 0 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> tls_valid s \<and> 1 \<le> thread_index_C (tls s) \<and> thread_index_C (tls s) \<le> thread_count\<rbrace> do ret' <- do ret' <- camkes_get_tls';
y <- guard (\<lambda>s. is_valid_camkes_tls_t_C s ret');
condition (\<lambda>s. thread_index_C (heap_camkes_tls_t_C s ret') = 1)
  (do y <- guard (\<lambda>s. is_valid_w32 s (PTR(32 word) (symbol_table ''badge_1'')));
return (PTR(32 word) (symbol_table ''badge_1''))
od)
  condition (\<lambda>s. thread_index_C (heap_camkes_tls_t_C s ret') = 2)
  (do y <- guard (\<lambda>s. is_valid_w32 s (PTR(32 word) (symbol_table ''badge_2'')));
return (PTR(32 word) (symbol_table ''badge_2''))
od)
  (do y <- abort';
fail
od)
od;
ret'a <- seL4_Poll' 6 ret';
y <- guard (\<lambda>s. is_valid_w32 s ret');
gets (\<lambda>s. if heap_w32 s ret' = 0xBAD1DEA then 1 else 0)
od \<lbrace>\<lambda>r s. is_valid_w32 s (PTR(32 word) (symbol_table ''badge_1'')) \<and> symbol_table ''badge_1'' \<noteq> 0 \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''badge_2'')) \<and> symbol_table ''badge_2'' \<noteq> 0 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> tls_valid s \<and> 1 \<le> thread_index_C (tls s) \<and> thread_index_C (tls s) \<le> thread_count \<and> (r = 0 \<or> r = 1)\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. is_valid_w32 s (PTR(32 word) (symbol_table ''badge_1'')) \<and> symbol_table ''badge_1'' \<noteq> 0 \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''badge_2'')) \<and> symbol_table ''badge_2'' \<noteq> 0 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> tls_valid s \<and> 1 \<le> thread_index_C (tls s) \<and> thread_index_C (tls s) \<le> thread_count \<Longrightarrow> tls_valid s \<and> globals_frame_intact s \<and> (if thread_index_C (heap_camkes_tls_t_C s (tls_ptr s)) = 1 then (globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x b v0 v1 v2 v3. (is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_1'') := b)) (setMRs s v0 v1 v2 v3)) (PTR(32 word) (symbol_table ''badge_1'')) \<and> symbol_table ''badge_1'' \<noteq> 0 \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_1'') := b)) (setMRs s v0 v1 v2 v3)) (PTR(32 word) (symbol_table ''badge_2'')) \<and> symbol_table ''badge_2'' \<noteq> 0 \<and> globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_1'') := b)) (setMRs s v0 v1 v2 v3)) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_1'') := b)) (setMRs s v0 v1 v2 v3)) \<and> tls_valid (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_1'') := b)) (setMRs s v0 v1 v2 v3)) \<and> 1 \<le> thread_index_C (tls (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_1'') := b)) (setMRs s v0 v1 v2 v3))) \<and> thread_index_C (tls (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_1'') := b)) (setMRs s v0 v1 v2 v3))) \<le> thread_count \<and> ((if heap_w32 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_1'') := b)) (setMRs s v0 v1 v2 v3)) (PTR(32 word) (symbol_table ''badge_1'')) = 0xBAD1DEA then 1 else 0) = 0 \<or> (if heap_w32 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_1'') := b)) (setMRs s v0 v1 v2 v3)) (PTR(32 word) (symbol_table ''badge_1'')) = 0xBAD1DEA then 1 else 0) = 1)) \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_1'') := b)) (setMRs s v0 v1 v2 v3)) (PTR(32 word) (symbol_table ''badge_1''))) \<and> PTR(32 word) (symbol_table ''badge_1'') \<noteq> NULL \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''badge_1''))) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''badge_1'')) else if thread_index_C (heap_camkes_tls_t_C s (tls_ptr s)) = 2 then (globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x b v0 v1 v2 v3. (is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_2'') := b)) (setMRs s v0 v1 v2 v3)) (PTR(32 word) (symbol_table ''badge_1'')) \<and> symbol_table ''badge_1'' \<noteq> 0 \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_2'') := b)) (setMRs s v0 v1 v2 v3)) (PTR(32 word) (symbol_table ''badge_2'')) \<and> symbol_table ''badge_2'' \<noteq> 0 \<and> globals_frame_intact (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_2'') := b)) (setMRs s v0 v1 v2 v3)) \<and> ipc_buffer_valid (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_2'') := b)) (setMRs s v0 v1 v2 v3)) \<and> tls_valid (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_2'') := b)) (setMRs s v0 v1 v2 v3)) \<and> 1 \<le> thread_index_C (tls (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_2'') := b)) (setMRs s v0 v1 v2 v3))) \<and> thread_index_C (tls (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_2'') := b)) (setMRs s v0 v1 v2 v3))) \<le> thread_count \<and> ((if heap_w32 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_2'') := b)) (setMRs s v0 v1 v2 v3)) (PTR(32 word) (symbol_table ''badge_2'')) = 0xBAD1DEA then 1 else 0) = 0 \<or> (if heap_w32 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_2'') := b)) (setMRs s v0 v1 v2 v3)) (PTR(32 word) (symbol_table ''badge_2'')) = 0xBAD1DEA then 1 else 0) = 1)) \<and> is_valid_w32 (heap_w32_update (\<lambda>a. a(PTR(32 word) (symbol_table ''badge_2'') := b)) (setMRs s v0 v1 v2 v3)) (PTR(32 word) (symbol_table ''badge_2''))) \<and> PTR(32 word) (symbol_table ''badge_2'') \<noteq> NULL \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''badge_2''))) \<and> is_valid_w32 s (PTR(32 word) (symbol_table ''badge_2'')) else False) \<and> is_valid_camkes_tls_t_C s (tls_ptr s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_valid_w32 s (PTR(32 word) (symbol_table ''badge_1'')); symbol_table ''badge_1'' \<noteq> 0; is_valid_w32 s (PTR(32 word) (symbol_table ''badge_2'')); symbol_table ''badge_2'' \<noteq> 0; is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)); is_valid_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame))); is_valid_camkes_tls_t_C s (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)); 1 \<le> thread_index_C (heap_camkes_tls_t_C s (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))); thread_index_C (heap_camkes_tls_t_C s (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))) \<le> 2; thread_index_C (heap_camkes_tls_t_C s (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))) \<noteq> 2\<rbrakk> \<Longrightarrow> thread_index_C (heap_camkes_tls_t_C s (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))) = 1 proof (prove)
goal:
No subgoals!