fact: Definition log_net_handlers dst src m st : list (disk_op log_files) * list output * log_state * list (name * msg) := let '(out, d, ps) := net_handlers dst src m (log_data st) in log_handler_result (log_num_entries st) (inr (src , m)) out d ps.
imports: Verdi(Verdi) Cheerios(Cheerios)