Refactor the Quint specification after #144

[konnov]

What ❔

Following the pseudo-code updates in #144, this PR introduces updates in the Quint specification, namely, moving CommitQC into TimeoutQC and storing only high_commit_qc_view in TimeoutVote instead of storing high_commit_qc.

Why ❔

This update speeds-up model checking times dramatically, as CommitQC fields in TimeoutVote were a major bottleneck.

This change has broken multiple invariants. Hence, we have to further fix the specification and the invariants before merging.

Preliminary experiments show that the model checking times have improved dramatically. For instance, we were able to find the expected violation of agreement for N=6, F=1, and B=2.

[konnov]

I have fixed committed_blocks_have_justification_inv today and the model checker has not found counterexamples today. So I will re-run the experiments to see whether all the invariants pass.