README.md

Approach to property based testing

We generate traces of update events. These traces are analyzed per-update proposal. Given a trace and an update proposal, we divide the trace in fragments, where in each fragment the state of a proposal (as reported by the update system) remains unchanged. The states a proposal can be in are enumerated below:

• unknown: the SIP for the update proposal is not know to the update system.

The division of the trace in fragments depend on the update system giving the right information. For instance, it should report the earliest state when an SIP was submitted. We have tests in place to make sure the update system reports the correct state. These are described in the next section.

State query tests

State of an SIP is correctly reported

• It the update system reports that an SIP submission is unknown in the system, then only implementation submissions corresponding to that SIP are allowed.
• If the system transitions from unknown to SIP submitted for a given SIP, then the action that led to the new state must be the submission of said SIP.
• If an SIP is in a submitted state, then only implementation submissions are allowed.
• If an SIP transitions from submitted to stably submitted, then the difference between the first slot in which the SIP was reported as submitted and the first slot in which it was reported as stably submitted is equal to the slot length stability window.
• The length in slots of a submitted fragment cannot exceed the slot length of the stability window.

Update system requirements

Open participation

No valid update payload is rejected

As long as an update payload is valid, and pays the required fees the system should not reject it.

This property is validated through several properties.

if a SIP submission is rejected, it is because either the signature is invalid, or it was submitted before. The reciprocal of this property implies that a valid submission should be accepted.

In the code we check that for all SIP's, and fragments where the SIP is in an unknown state, if a submission of a SIP was rejected in that fragment, then it is because the signature was invalid.

This ensures that an SIP can always be submitted if it was not submitted before. If it was submitted before then the system will not report it as unknown (this is checked in a different property-test) so this case is not interested for this property.

if a SIP revelation is rejected, it is because either:

• the revelation was submitted before
• there is no corresponding stable SIP

In the code we check that when an SIP is in the stably submitted state, then the revelation of this SIP cannot be rejected.

TODO we can make an analogous consideration for votes.

Decentralized decision making

A SIP voted by enough participants can move to the next phase

In the code we check that for any SIP, in the fragment when the SIP is stably revealed (which means that its voting period is open), then:

• No verdict can be reached earlier than the last voting period.
• In the last voting period, the reached verdict coincides with the outcome we expect (from counting the votes in that period).

This means that if an SIP should be approved according to the votes we see in any of its voting periods, then the system should report it as approved.

We also check that once an SIP is approved and its implementation submitted, it can go into the implementation submitted state (and from there proceed with the approval phase).

A SIP not voted by enough participants cannot move to the next phase

It the code we check that for any SIP, in the fragment when the SIP is stably revealed (which means that its voting period is open), then:

• No verdict can be reached earlier than the last voting period.
• In the last voting period, the reached verdict coincides with the outcome we expect (from counting the votes in that period).

The checks above ensure that if an SIP should be not be approved according to the votes we see in any of its voting periods, then the system should report it as not-approved. Conversely, they also ensure the proposals with enough votes are reported as approved by the system.

We check as well that implementation submissions are always

accepted (one per proposal), and once an implementation is stably submitted, the corresponding revelation is not rejected.

We also check that the system can only enter in the implementation submitted state if the SIP is approved. This ensures that a software update that hasn't been approved will not be allowed to pass to the next phase.

TODO: similar considerations for implementation votes and endorsements

On-chain and protocol-driven

Uniqueness of proposals

For every update proposal there is an unique author that submitted it to the chain.

We ensure this by enforcing a commit-reveal scheme.

In the code we check that SIP's and implementations can only be revealed when their submissions are stable.

Transparent and auditable

Securely activated

The endorsement threshold at the end of the safety lag is 51%

At the end of the safety lag the activation of a proposal requires 51% of stake endorsed.

In the tests we make sure that the threshold we consider at the last endorsement interval is 51%.

Low impact on blockchain performance

Scalable

Metadata-driven

Priorities are honored

Updates with higher priority are activated before the ones with lower priorities (priorities are specified in the proposal's metadata)

In the tests we check that when a proposal starts an endorsement period, then all the other candidate proposals have lower priority. On the other hand, we check that when a proposal is put in the endorsements queue, then any proposal being endorsed must have a higher priority. Furthermore, we ensure that only scheduled proposals can be activated, and the activated state can only be reached from the being endorsed state. This guarantees that when a proposal is activated, the there is no other proposal with higher priority that could have been endorsed.

Voting period duration is honored

The voting period duration of a proposal coincides with the one specified in its metadata.

In the tests we divide the fragment in which a proposal is in the stably revealed state (i.e. its voting interval) in voting periods according to the proposal's metadata. The we tally the votes in those periods and make sure no valid votes are rejected in any of those period. Thus if the system would have a different voting period duration a property based tests with good coverage should detect a case in which either a valid vote was rejected, or we arrive at a different tally result (either because the interval that the system under test considers will be shorter or longer, and contain a different number of votes).

Dependency and conflict resolving

Alternative way to test requirements

For each proposal p:

• while p is in the unknown state:
  • the system should not reject a valid SIP submission for p, this is, a submission with a valid signature. This is a necessary condition for open participation.
• when p transitions from unknown to SIP submitted:
  • the action that led to the SIP submitted state must be the SIP submission of p.
  • the length of the trace fragment in which the system is in the SIP submitted state must be less than the length of the stability window. Otherwise the system would be reporting the state of the SIP incorrectly.
• when p transitions from SIP submitted to SIP stably submitted:
  • the difference between the first slot in which p was in the SIP submitted state, and the first slot in which p was in the SIP stably submitted state must be exactly the length of the stability window.
  • there should be no rejections of valid SIP revelations for the commit of p. This is a necessary condition for open participation.

The third option

How and why do we test with traces.

How and why we divide a trace into events, per update proposal.

How do we define the validation criteria

Per each requirement:

• Enumerate the state changes that are relevant to it. This means stating which changes are allowed, and which changes aren't.
• Enumerate the conditions (relative to the requirement) that the transition has to satisfy.

TODO: the fact that no unexpected payload is allowed might have to do with the no negative impact on performance: allowing votes outside the voting period will increase the blockchain size.