proposition: Lemma locks_correct_locked_net_handlers_new : 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_unlock sigma p -> In (pDst q, pBody q) ms -> 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_intro, empty_queue_all_clients_false, unlock_in_flight_all_clients_false. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)