Consensus Trace Validation improvements

[achamayou]

Resolved

1. (Document lack of request payload validation in ctv #6187) All client requests are identical at the moment [request -> 42, contentType |-> TypeEntry]. Two ways to go here:

• Fill them with something unique to distinguish them, perhaps a digest of the entry (with real traces in mind). We would need to capture them, and pre-fill the spec to produce ClientRequest from them.
• Accept that the content does not matter to the consensus spec, and remove request altogether. Done.

To be discussed

2. In IsSendAppendEntries, sent_idx does not match nextIndex[i][j]. Investigated, explained, and options proposed. @achamayou prefers options 1 or 2.

Requires Investigation:

4. In IsSendAppendEntries Len(log'[logline.msg.state.node_id]) does not match logline.msg.state.last_idx. Needs investigation.
5. In IsRcvAppendEntriesRequest, leadershipState[logline.msg.state.node_id] does not match ToLeadershipState[logline.msg.state.leadership_state]. Needs investigation.
6. In IsRcvAppendEntriesRequest Len(log'[logline.msg.state.node_id]) does not match logline.msg.state.last_idx. Needs investigation.
7. In IsAddConfiguration, committable indices, commit Index, membershipState and last_idx don't match. I looked at this, and in situations where we receive an AE range that contains a configuration at first followed by committable indices, recv_append_entries will update the committable indices in the spec, but not in the impl state, which then goes on to handle an add_configuration event on which state->committable_indices is empty. Needs investigation.
8. In IsAdvanceCommitIndex, the commit_idx and last_idx don't match in the Follower case. Needs investigation.
9. In IsRcvAppendEntriesResponse, the leadershipState does not match. Needs investigation.
10. In IsRcvRequestVoteRequest, the leadershipState and last_idx do not match. Needs investigation.
11. In IsExecuteAppendEntries, the commit_idx and last_idx do not match. Needs investigation.
12. In IsRcvRequestVoteResponse, the leadershipState does not match. Needs investigation.

[lemmy]

To be discussed:

1. All client requests are identical at the moment [request -> 42, contentType |-> TypeEntry].

Two ways to go here:

• Fill them with something unique to distinguish them, perhaps a digest of the entry (with real traces in mind). We would need to capture them, and pre-fill the spec to produce ClientRequest from them.
• Accept that the content does not matter to the consensus spec, and remove request altogether.

+1 for the second proposal. However, there should be a comment for the benefit of beginners that explains why the actual requests do not matter.

[lemmy]

For the record, I disagree with the removal of the formulas that are commented with TODO that need investigation. These are exactly the formulas that have to be added, thus, more precise than any github issue can be. If there is a clear reason why an assertion does not hold, the formula should be replaced with a proper comment that explain why the assertions do not hold.

[achamayou]

@lemmy the project uses GitHub issues to track, discuss and prioritise work items. Please see the contributing guidelines for code formatting rules. If an issue is important to you, please feel free to open a PR with a corresponding code change.

This issue can be used to claim items and avoid duplicate effort.