spec: Formally define the valid(v) properties

[cason]

          When executed on a correct node `valid(getValue())` should always return true. For some application we discussed to lift this property, by requiring that we don't need this always, but only from some round on. This is related to whether `valid` should be a function or a relation... if it is not a function, at least we need a strong enough link to `getValue` to ensure liveness.

Originally posted by @josef-widder in #389 (comment)

The valid(v) function is supposed to be deterministic. In particular, if v is produced and proposed by a correct proposer, then valid(v) should return true at every correct process.

Definition of done: add details to this section.

[cason]

An important observation regarding value validity is to consider that, typically due to bugs, we might need to fix or update our implementation of valid(v). So, in a more general way, we consider a sequence of valid_i(v) implementations, with increasing indexes i, so that to represent multiple backwards compatible implementations of the validity checks, so that:

valid_i(v) => valid_j(v) for every j > i

The rationale here is the following. If a value was considered valid by an implementation of valid(v), say the ith implementation of it, then every subsequent implementation valid_j with j > i has to return the same output as valid_i. This is covered by above relation since V -> F is the only attribution that makes the implication false.

At the same time, it is possible that valid_i returns false for a value v due to a bug. Then a new implementation valid_i+1 is produced in order to fix the bug. We have then the attribution F -> V which is also in line with the implication. Of course, if valid_i(x) = false, then valid_i+1(x) can be either true or false.

[josef-widder]

An important point to note here is that the implication valid_i(v) -> valid_j(v) is property of the application that is needed for consensus-level protocols (e.g., synchronization protocols, light clients). The application developers need to be aware of this requirement, and they need to make sure that the implication holds for a new version of valid that they introduce.

Do we have a document that that collects such requirements?

[cason]

Do we have a document that that collects such requirements?

We have some TODOs: https://github.com/informalsystems/malachite/blob/main/specs/consensus/overview.md#validation

[matan-starkware]

Does V -> F refer to a valid consensus node becoming a faulty consensus node?

So the claim is that if a node's valid_i(v) returns true, then any subsequent version must also return true? Specifically, if valid_i was faulty and should have returned false, does the fixed version of the node need to return true (satisfying backward compatibility) or false (satisfying the fundamental validity of the proposal)?

• If true to what extent does this hold? Must we return true anytime the node sees this proposal again, only within the same height, only within the same (H, R)?

.

Are you claiming that reversing a faulty invalidation is ok? valid_i(v) -> false to valid_j(v) -> true

• If so why does this not require backwards compatibility? Is it because a NIL vote commits to nothing (e.g. failed validation votes like a timeout)? Is it a result of the locking mechanism specifically? Something else?

[cason]

Does V -> F refer to a valid consensus node becoming a faulty consensus node?

V -> F is the only attribution that is not accepted. This means that if some value was found valid and, for instance, was committed, future version of the valid(v) function must find it valid as well. This is the backwards compatibility part.

We however accept F -> V, meaning that a block that is currently rejected can be accepted by a future (fixed) version of valid(v).

[cason]

Specifically, if valid_i was faulty and should have returned false, does the fixed version of the node need to return true (satisfying backward compatibility) or false (satisfying the fundamental validity of the proposal)?

If valid_i was faulty in enough nodes, the values that is has (wrongly) accepted may be committed now. So the next version of it should accept them as well. This is actually backwards compatibility.

[cason]

Are you claiming that reversing a faulty invalidation is ok? valid_i(v) -> false to valid_j(v) -> true

* If so why does this not require backwards compatibility? Is it because a NIL vote commits to nothing (e.g. failed validation votes like a timeout)? Is it a result of the locking mechanism specifically? Something else?

I am claiming that reversing a faulty invalidation is acceptable. Notice that if valid_i(v) was false in enough nodes, v could never been decided. So we are not changing the history in this case.

The opposite, however, is not true. If valid_i(v) was true in enough nodes, v could have been decided. If we start rejecting values like v in a new version valid_j, then we are potentially rejecting committed values.

Regarding the second part, notice that a node must remember the votes it has previously issued. So if it has rejected v at round (H, R) because valid_i(v) was false, it must recall that output (see #469 (comment)) so that in case of a restart, it will act accordingly and reject v again.

But if H is still undecided, valid_i was replaced by valid_j, and we see v proposed again in a round (H, R') with R' > R we may accept v in round R' since valid_j(v) will in this case return true. There is no actual inconsistency in this behavior. Notice that a super-majority should find v valid in round R' in order to decide it. Which means that a super majority is using the updated valid_j when running round R'.

I understand this logical implication is confusing, it took a while to me to phrase it properly.

[cason]

I think it is worth to define a way to implement the above mentioned property using what we call soft-upgrades:

valid_i(v) => valid_j(v) for every j > i

For this we need to define a set of heights associated to each implementation of valid(v). Namely, valid_i starts being adopted from height H_i. From this we can define the valid(v) method as follows:

• if v is a value for height H, find the maximum H_i so that H >= H_i
• then use valid_i(v) to implement valid(v) in height H

In this way, we split the execution into multiple height intervals [H_{i}, H_{i+1}) and for each of such interval starting from H_i we use valid_i function to evaluate value validity. From H_{i+1}, if any exist, we start using valid_{i+1} for heights H >= H_{i+1} but we still use valid_i for heights H < H_{i+1}. As a result, if valid_i(v) is true then valid valid_{i+1} for the same value v, that must be validated previously to height H_{i+1} by definition, is also true because we are resorting to the previous version valid_i of the method.

[cason]

From the above definition, namely, from the adoption of soft upgrades, it remains to discuss what happens in the transition heights H_j when we start using a new validation method valid_j.

Without lack of generality, I assume that when starting H_j we are still using valid_i, with i < j, because it was not scheduled a change of the validation method using soft upgrades.

We have then two possibilities to consider.

A. valid_i is accepting values v that should not be accepted

In this case, we are likely committing a value v that should not be committed. This value, however, won't be proved or its proof will not be accepted by L1. Therefore, H_j is from a dead branch that will discarded, as a fork will happen at a height H < H_j. Fixing valid_i in order to produce a valid_j, with j > i, that rejects v will potentially halt the chain. But the chain, or at least its suffix, is already doomed because we accepted values that are not acceptable.

B. valid_i is rejecting values v that should be accepted

In this case, we are probably stuck in height H_j, since we assume that correct processes are adopting valid_i. In order to get out from this stall, we have two possibilities:

1. A proposer of a round R > 0 proposes a different value x != v that is accepted (valid_i(x) == true)
2. After multiple failed rounds, since all proposed values are rejected, we introduce a fixed version valid_j to replace valid_i. We have then a situation where different nodes use different versions of valid(v).

Notice that case 1. must be covered by case 2. Namely, if valid_i(x) = true then we must have valid_j(x) = true.

But if we keep proposing values that, like v, have valid_i(v) = false, we only achieve progress when a super majority of processes adopt valid_j that was fixed so that valid_j(v) = true for values proposed in future rounds.

So, for ensuring that nodes do not crash in case 1., we need V -> V for values like x. While for ensuring progress in case 2. we need F -> V for values like v. What we cannot have is a solution of the V -> F style.

[josef-widder]

A different way to look at soft-upgrades is as follows:
The idea is that if valid should be changed in that from height hon, a function new_valid should be used to check validity, while up to height h-1 the function old_valid has been used, then we can get something along these lines:

valid(v, chain, height) = 
  if (height >= h)
    new_valid(v, chain, height)
  else
    old_valid(v, chain, height)

In this way, we effectively split evaluation of valid into different height
intervals. Whenever a new version is needed, and new interval is added on top. Moreover
if in the future validity of a value is checked with a new version of valid, effectively
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.