Discrepancy between Quint and Namada: stake vs total_deltas

[angbrav]

The stake map in the Quint spec maps epochs to stake while total_deltas in Namada maps epochs to deltas.

[angbrav]

During our last meeting, we discussed whether keeping deltas instead of absolute stake values may simplify the design. Some context:

• In the Quint spec in which we keep absolute values. When a validator is slashed, we need to update the stake map for all epochs >= cur_epoch + PIPELINE_OFFSET. There are a few reasons to do so, the most obvious one being that since we keep absolute values, we need to subtract the slashed amount from all epochs.
• The question by @brentstone: is it enough to update just epoch cur_epoch+1 in the stake map if we maintain deltas?

My answer after some thinking:

• No, it is not enough, even when keeping deltas, we may still need to update epochs >= cur_epoch + PIPELINE_OFFSET to deal with unbonds. A simple example:
  • Assume we slash a validator because it misbehaved at epoch e.
  • Assume that the validator had X tokens at e and that the slash rate is 1 for simplicity.
  • Assume also that the validator does not get any more bonds after e.
  • We have to subtract X tokens at cur_epoch + 1.
  • If the validator unbonded half of the X tokens before the evidence was found, i.e, before the validator was jailed, then we may need to update an epoch >cur_epoch + 1 in the stake's map to compensate, even if the map keeps deltas.
  • Assume that the tokens were unbonded at epoch cur_epoch + 2 - PIPELINE_OFFSET, i.e, the tokens are effectively unbonded at cur_epoch + 2. Then, if we only update epoch cur_epoch + 1 when slashing, the validator will end up with a negative stake at cur_epoch + 2: stake[e]=X + stake[cur_epoch + 1]=-X + stake[cur_epoch + 2]=-0.5*X = -0.5*X

[angbrav]

Agreed to revisit it later

[angbrav]

Not planning to do it.