Add redelegation to the pseudocode model

[angbrav]

This PR adds redelegation to the pseudocode model and English text to describe the main logic and some definitions.

Note that the text below may be a bit outdatet.

Definitions

• We use source and destination validators to refer to the validator from which the tokens are redelegation and the validator to which the tokens are redelegated respectively.
• We say that a redelegation starts the epoch at which the tx_redelegate tx is issued and ends when the redelegated tokens stop contributing to the source validator and start contributing to the destination validator.
• Chain redelegations occur when some redelegated tokens are redelegated within less than unbonding_length epochs.

Desired Properties

The solution aim to guarantee the following desired properties:

• Fast redelegation: Redelegated tokens start contributing to the destination validator stake after pipeline_length epochs. This means that if a delegator redelegates X tokens at epoch e, then these tokens stop contributing to the source validator stake and start contributing to the destination validator stake at e+pipeline_length.
• Minimize changes: Adding redelegation should not require a major redesign of the existing protocol.

Data Structures

The solution introduces the following data structures to track redelegations:

• Redelegation is a record with two fields: the source validator and the amount of tokens redelegated.
• redelegated_bonds in (Addr X Addr X Epoch) → Redelegation: A map from delegator to a map from redelegation's destination validator to a map from the epoch at which the redelegation ends to a Redelegation record. This sounds more complex than it is. This is accessed by simply redelegated_bonds[delegator][dest_validator][epoch]. It is the counterparty of the bonds data structure.
• redelegated_unbonds[][][] in (Addr X Addr X (Epoch, Epoch)) → Redelegation: Similar to redelegated_bonds but the key of the last map is a tuple to track not only the end of the redelegation but also the when the tokens are unbonded at the destination validator. It is the counterparty of the unbonds data structure.
• Each validator now keeps track of incoming validators in a map: redelegations map<Addr, map<Addr, IncomingRedelegation>>. This is useful to prevent redelegations. IncomingRedelegation is a record that stores the amount redelegated and the epoch at which the redelegation started.

How it roughly works

• The main complexity comes from the fact that we do not keep a separate record for each bond/unbond but we accumulate them per epoch (epochs for unbonds) in a delta data structure. This makes things complicated because when slashing we need to know the precise amount of tokens that come from a redelegation to be able to apply slashes of the source validator if required. redelegated_bonds and redelegated_unbonds aim at solving this issue. Let's take the following example:
  • Assume a delegator del and two validators val1 and val2.
  • del redelegates X tokens from val1 to val2 in epoch e. Then the redelegation ends at e + pipeline_length. Then bonds[del][val2].deltas[e+pipeline_length]=X, assuming that there were no bonds before.
  • del delegates Y tokens to val2 in epoch e as well. Then bonds[del][val2].deltas[e+pipeline_length]=X+Y.
  • Assume now that del want to unbond at an epoch e' >= e+pipeline_length and the bonds in bonds[del][val2].deltas[e+pipeline_length] are going to be unbonded. We need to do two things:
  • Apply all slashes processed by e' that val2 committed in any epoch >= e+ pipeline_length to the whole amount (X+Y).
  • Also, we need to apply any slashes that the source validator committed while the Y tokens were being redelegated (any slash not processed before the redelegation started and committed before the redelegation ends.
  • To compute X and Y precisely, the solution relies on redelegated_bonds. Thus:
  • bonds[del][val2].deltas[e+pipeline_length]=X+Y
  • redelegated_bonds[del][val2][e+pipeline_length]=Y
  • X can be computed from the above.
• The above logic has to be applied not only on unbonding, but also when withdrawing and at the end of an epoch when a validator is slashed.
• Other details:
  • When we redelegate tokens, we do not just simply move the bond amounts to the destination validator, but we slash first. Thus, the bonded amount at the destination validator already accounts for all the slashes committed by the source validator processed before the redelegation starts. This means that we only need to care about slashes of the source validator that were processed after the redelegation started and before it ended (at that point, the tokens do not contribute to the source validator stake).
  • Another tricky part is what happens at the end of an epoch. We first need to slash the misbehaving validator. Then we have to slash any validator for which the misbehaving validator redelegated tokens to. Slashes are always filtered based on when the infraction was committed and when the redelegation started/ended.

[cwgoes]

(ref some discussions in https://github.com/anoma/namada/issues/34)

We need to make sure not to iterate over delegations or redelegations (DoS vector). In this case I think we can treat all redelegations from X to Y in epoch e the same (so e.g. when slashing we can just store the total amount from X to Y in e and slash based on this, we don't have to iterate over the redelegations).

[tzemanovic]

(ref some discussions in anoma/namada#34)

We need to make sure not to iterate over delegations or redelegations (DoS vector). In this case I think we can treat all redelegations from X to Y in epoch e the same (so e.g. when slashing we can just store the total amount from X to Y in e and slash based on this, we don't have to iterate over the redelegations).

Thanks, that's a very important point! I think we unwittingly introduced iteration in https://github.com/informalsystems/partnership-heliax/pull/38 that's being carried over to here too, where in end_of_epoch we started iterating over validator.set_unbonds.

For the redelegations themselves, we suggested grouping these by a triple of src validator, dest validator and redelegation epoch, and then iteration over the groups is acceptable.

I think we could solve the iteration over the set_unbonds the same way - i.e. group unbonds by a pair of bond start epoch and unbond epoch.

[tzemanovic]

I tried to check for these properties:

1. bonding, unbonding, withdrawal and slashing from a validator that has no outgoing or incoming re-delegations is unaffected by the changes
2. when a re-delegation src validator is slashed before re-delegation epoch + pipeline and the src bond was in slashable epoch range, the slash for the re-delegated amount is subtracted for the slash applied on the src validator and applied on the dest validator instead
3. when a re-delegation src validator is slashed at or after re-delegation epoch + pipeline, the dest validator is unaffected
4. when a re-delegation dest validator is slashed before re-delegation epoch + pipeline, the re-delegated amount is unaffected
5. when a re-delegation dest validator is slashed at or after re-delegation epoch + pipeline, the re-delegated amount is slashed
6. when a re-delegation is unbonded after a slash on the src validator that's applicable to the re-delegation is discovered, the unbond gets slashed and the final amount that can be withdrawn is not slashed again
7. when a re-delegation is unbonded before a slash on the src validator that's applicable to the re-delegation is discovered, the unbond isn't slashed and the final amount that can be withdrawn gets slashed
8. when a re-delegation is unbonded and a slash on the dest validator that's applicable to the re-delegation is discovered, the unbond isn't slashed and the final amount that can be withdrawn gets slashed (like a regular bond unbond)

I haven't found any issues with the logic besides the comments, most of which are minor.

As per https://github.com/informalsystems/partnership-heliax/pull/45#discussion_r1174870619 I think for 2., 6. and 7. we're ignoring the start epochs of the src bond deltas, which I think is ok as we never skip a slash on something that should be slashed, only potentially slashing a re-delegation that might not need to be slashed if we were to track the start epochs of re-delegations in detail from the source deltas. I think this is applied consistently across the different paths (unbond/withdraw/end of epoch).

[angbrav]

I tried to check for these properties:

1. bonding, unbonding, withdrawal and slashing from a validator that has no outgoing or incoming re-delegations is unaffected by the changes
2. when a re-delegation src validator is slashed before re-delegation epoch + pipeline and the src bond was in slashable epoch range, the slash for the re-delegated amount is subtracted for the slash applied on the src validator and applied on the dest validator instead
3. when a re-delegation src validator is slashed at or after re-delegation epoch + pipeline, the dest validator is unaffected
4. when a re-delegation dest validator is slashed before re-delegation epoch + pipeline, the re-delegated amount is unaffected
5. when a re-delegation dest validator is slashed at or after re-delegation epoch + pipeline, the re-delegated amount is slashed
6. when a re-delegation is unbonded after a slash on the src validator that's applicable to the re-delegation is discovered, the unbond gets slashed and the final amount that can be withdrawn is not slashed again
7. when a re-delegation is unbonded before a slash on the src validator that's applicable to the re-delegation is discovered, the unbond isn't slashed and the final amount that can be withdrawn gets slashed
8. when a re-delegation is unbonded and a slash on the dest validator that's applicable to the re-delegation is discovered, the unbond isn't slashed and the final amount that can be withdrawn gets slashed (like a regular bond unbond)

I haven't found any issues with the logic besides the comments, most of which are minor.

As per #45 (comment) I think for 2., 6. and 7. we're ignoring the start epochs of the src bond deltas, which I think is ok as we never skip a slash on something that should be slashed, only potentially slashing a re-delegation that might not need to be slashed if we were to track the start epochs of re-delegations in detail from the source deltas. I think this is applied consistently across the different paths (unbond/withdraw/end of epoch).

Thanks for the detailed analysis @tzemanovic . I am transforming the spec into a Quint executable spec, so we will be able to test those scenarios much more easily. Regarding your last comment, see my response.

[angbrav]

@tzemanovic @cwgoes I've gotten rid of the expensive iterations, in case you want to take a look!

[cwgoes]

@angbrav should we merge this?

[angbrav]

We could, but it is not in sync with the Quint spec. Do we want to spend some time correcting it?

[angbrav]

Closed as agreed to stop maintaining pseudocode specs in favor of Quint specs.