proposition: Lemma LockServ_nwnw_input_handlers_old_new : forall h i sigma u st' out ms p p', InputHandler h i (sigma h) = (u, out, st', ms) -> locks_correct sigma -> LockServ_network_invariant sigma p -> In (pDst p', pBody p') ms -> pSrc p' = h -> LockServ_network_network_invariant p p'.
proof: Proof. Proof using. unfold LockServ_network_invariant. set_up_input_handlers. - auto using nwnw_sym, nwnw_lock. - destruct (pBody p) eqn:?. + auto using nwnw_lock. + now erewrite unlock_in_flight_all_clients_false in * by eauto. + now erewrite locked_in_flight_all_clients_false in * by eauto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)