proposition: Lemma locks_correct_net_handlers : forall p sigma u st' out ms, NetHandler (pDst p) (pSrc p) (pBody p) (sigma (pDst p)) = (u, out, st', ms) -> locks_correct sigma -> locks_correct_unlock sigma p -> locks_correct_locked sigma p -> locks_correct (update name_eq_dec sigma (pDst p) st').
proof: Proof. Proof using. set_up_net_handlers; eauto using locks_correct_update_true, locks_correct_locked_at_head, all_clients_false_locks_correct_server_update, empty_queue_all_clients_false, locks_correct_at_head_preserved, snoc_at_head_of_queue_preserved, all_clients_false_locks_correct_server_update, unlock_in_flight_all_clients_false. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)