spec: Introduce a ValidValue(v, r) event

[cason]

When a value v is received and 2/3+ Prevotes for id(v) are received during a round, v becomes a valid value at that round. If a value becomes valid while the node hasn't yet issued a Precommit for that round, the valid value also becomes the locked value.

When a value becomes valid for a node it is liked to be precommitted and locked by other nodes, which renders this event particular relevant for liveness. Moreover, due to equivocation (#309), it is possible that a node learns that a value is valid while other node, but considering a different vote from equivocating senders, does not. This, again, can harm liveness.

As a result, nodes that observe that a value have became valid in a round should be able to forward this information to other nodes, with a distinct view of the system state. This is one element to be considered for the sake of node synchronization (#260).

At the moment, however, updating the valid_value and valid_round fields is an internal transition in the consensus state-machine. I argue here that this event should be exported by it so that synchronization protocols can be aware of this scenario and provide the associated prevotes, from the 2/3+ certificate, to peers.

[cason]

A relevant question on this regard is whether we need to know the full value v in order to emit the ValidValue(v,r) event.

We possibly can update it to be ValidValue(id(v), r) and produce it even though we have not received the full value v. In fact, emitting this event can be a trigger for the synchronization protocol to retrieve the full value v, as the validator has learned that it is a valid value, therefore a value that is very likely to eventually be decided.

Notice that the distinction of v and id(v) is still not really clear, see #365.

Notice also that the consensus state machine cannot update validValue_p and validRound_p if the full value v was not received.

This proposal also means that the driver can produce the ValidValue events, i.e., that we don't need consensus to produce it.

[cason]

Partially covered in Quint by #364.