proposition: Lemma locks_correct_locked_net_handlers_old : forall p sigma u st' out ms q, NetHandler (pDst p) (pSrc p) (pBody p) (sigma (pDst p)) = (u, out, st', ms) -> locks_correct sigma -> locks_correct_locked sigma q -> LockServ_network_network_invariant p q -> locks_correct_locked (update name_eq_dec sigma (pDst p) st') q.
proof: Proof. Proof using. set_up_net_handlers; eauto using locks_correct_locked_sent_lock, nwnw_locked_lock, locks_correct_locked_at_head_preserved, snoc_at_head_of_queue_preserved, nwnw_unlock_lock, nil_at_head_of_queue_preserved. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)