proposition: Lemma LockServ_nwnw_net_handlers_old_new : forall p sigma u st' out ms q p', NetHandler (pDst p) (pSrc p) (pBody p) (sigma (pDst p)) = (u, out, st', ms) -> locks_correct sigma -> LockServ_network_invariant sigma p -> LockServ_network_invariant sigma q -> LockServ_network_network_invariant p q -> In (pDst p', pBody p') ms -> LockServ_network_network_invariant p' q.
proof: Proof. Proof using. set_up_net_handlers; eauto using nwnw_sym, nwnw_lock, nw_empty_queue_lock, nwnw_unlock_lock. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)