feat(spec): Requirements on valid(v) #748
Conversation
There was a problem hiding this comment.
Great work.
Most of the suggestions I made were to align the content of this section with the "format" used in the remainder of this document.
Regarding the last sub(*)section, from line 540, I think it should not be part of this document. The same for the linked commend in issue 510.
They end up being too much specific for the level of detail that is considered in this document.
| The external function `valid` is used to guard any value-specific action in | ||
| the algorithm. The purpose is to restrict the domain of values that consensus | ||
| may decide. There is the assumption that if `v` is a value returned | ||
| by the `getValue()` function of a correct process in the current height, then |
There was a problem hiding this comment.
| by the `getValue()` function of a correct process in the current height, then | |
| by the [`getValue()` function](#proposal-value) of a correct process in the current height, then |
There was a problem hiding this comment.
There is a section on getValue().
| is correct, `valid(v)` does not serve any purpose. It only becomes relevant if | ||
| there is a faulty proposer; it limits "how bad" proposed values can be. | ||
|
|
||
| In the arXiv paper, the pseudo code uses `valid(v)`, that is, a function that |
There was a problem hiding this comment.
| In the arXiv paper, the pseudo code uses `valid(v)`, that is, a function that | |
| The [pseudo-code][pseudo-code] uses `valid(v)`, that is, a function that |
| of a mathematical (pure) function: | ||
| 1. the function must only depend on `v` but not on other data | ||
| (e.g., an application state at a given point in time, the current local time | ||
| or temperature). |
|
|
||
| The correctness of the consensus algorithm depends heavily on these points. | ||
| Most obviously for termination, we require that all correct processes find | ||
| the value by a correct proposer valid under all circumstances, because we |
There was a problem hiding this comment.
| the value by a correct proposer valid under all circumstances, because we | |
| the value proposed by a correct process valid under all circumstances, because we |
| The correctness of the consensus algorithm depends heavily on these points. | ||
| Most obviously for termination, we require that all correct processes find | ||
| the value by a correct proposer valid under all circumstances, because we | ||
| need them to all prevote for the value. A deviation in `valid` would |
There was a problem hiding this comment.
| need them to all prevote for the value. A deviation in `valid` would | |
| need them to accept the value. A deviation in `valid` would |
|
|
||
| `valid_i(v) == true` implies `valid_j(v) == true `, for `j > i` and every value `v` | ||
|
|
||
| The logical implications allows to be more permissive in later versions (as required to |
There was a problem hiding this comment.
| The logical implications allows to be more permissive in later versions (as required to | |
| The logical implication allows newer versions of `valid(v)` to be more permissive (as required to |
| `valid_i(v) == true` implies `valid_j(v) == true `, for `j > i` and every value `v` | ||
|
|
||
| The logical implications allows to be more permissive in later versions (as required to | ||
| fix the bug), while maintaining the need that newer versions allow to check validity |
There was a problem hiding this comment.
| fix the bug), while maintaining the need that newer versions allow to check validity | |
| fix bugs), while ensuring that newer versions allow to check validity |
| `valid`) should be deemed valid with the current version of the function. | ||
|
|
||
| These two requirements lead us to the following requirement on the implementations: | ||
| we consider a sequence of `valid_i(v)` implementations, with increasing indexes `i`, |
There was a problem hiding this comment.
| we consider a sequence of `valid_i(v)` implementations, with increasing indexes `i`, | |
| we consider a sequence of `valid_i(v)` implementations, with increasing versions `i`, |
| fix the bug), while maintaining the need that newer versions allow to check validity | ||
| of previously decided values. | ||
|
|
||
| #### Backward compatibility of `valid(v, chain, height)` |
There was a problem hiding this comment.
I see this section as an example of the requirement of the previous section.
Although I agree that it is only a legit example if v somehow included a height or h_p is also known by the valid(v) implementation. Not sure if we need this. Maybe a pointer to issue 510 is enough here.
| the logic that was in place for that height is used by using the proper "if" branch. | ||
| This addresses Requirement 1 and 2 from above. | ||
|
|
||
| TODO: I think in this [remark](https://github.com/informalsystems/malachite/issues/510#issuecomment-2505632410), different use cases (soft upgrades) are mixed. |
There was a problem hiding this comment.
Indeed, the example in the code above is almost the definition of software upgrades.
There was a problem hiding this comment.
The linked comment is a short-back of the code snippet and the software upgrades approach. This is the case where a bug identified during a given height forces us to the most general approach described in the "Backwards Compatibility" section.
Closes: #510
PR author checklist
For all contributors
For external contributors