spec: Collection of open points

[josef-widder]

This is perhaps a bit unstructured. But while reviewing recent changes and PRs things come to my mind.

• spec: clean up #151

• spec: Test and logic for line 32 (two cases (i) invalid (ii) locked round) #155

• spec: Sync between driver/consensus and code #81: Check what precisely is happening. I guess we can capture the logic by using the set value to propose. But it seems that the decision should be on the environment. Start timeoutpropose also for the proposer.

• spec: Align names between the Quint and English specs and implementation #161 E.g., consensus steps (e.g., NewRound) which are not defined in the arXiv paper are not aligned. Discuss alignment between step change in spec and code w.r.t. PrecommitAny check in the beginning in the spec

• Test and logic for line 26

• Update: This is handled by adding the "step change" logic. Handling of proposals for future rounds. Currently, when we receive a proposal for a future round we store it, but we don't call the consensus statemachine and we don't store a pending event. However, if we go to a round where we have already received the proposal, we need to execute line 22. I guess we need to

  • store a pending event (with the future round number).
  • we need to update the pending check in nextAction to look for the current height/round only
  • write a test

• Update: added spec: Validation of specifications #143 for Phase 2* we should write invariants for agreement and validity and see whether quint run and quint verify can find something (also for cases with more than 1/3 faults)

[josef-widder]

• Write a test for the scenario for a proposal for a past round is needed

• One process receives a precommit nil from a faulty validator -> timeoutPrecommit -> go to round 2

• all other processes decide (don't go to round 2)

• The one processes receives all the old messages (proposal and precommits to decide)

Update: cannot be completed at the moment. When trying to address it in #101, we found that there is an issue in the votekeeper. We need to fix the votekeeper first which is tracked in #103.

[josef-widder]

• remove timeouts for round 0 upon going to round 1 ("the started timeouts should be stopped").

Update: is not necessary at the moment as nextAction uses existsTimeout which filters for the current height and round.

[josef-widder]

• add specific tests for step change introduced in spec: adding step change #104

Update: I think the concern is best handled by the local transition invariants in #143

[josef-widder]

• Encode into Quint our tests in Rust: Anca’s tests:
  https://github.com/informalsystems/malachite/pull/106/files#diff-36179399ce40d2e8f24a117611189bbe4256694abc3bc56dad3815d5681d1f82R671
  https://github.com/informalsystems/malachite/pull/106/files#diff-36179399ce40d2e8f24a117611189bbe4256694abc3bc56dad3815d5681d1f82R730
  https://github.com/informalsystems/malachite/pull/106/files#diff-36179399ce40d2e8f24a117611189bbe4256694abc3bc56dad3815d5681d1f82R793

Update: Let's push this for later to see whether it is actually useful.

[josef-widder]

• step action in statemachineAsync to capture deliverSomeProposal and deliverSomeVote (todo)

Update: action deliver already there