Fix to issue #27

[angbrav]

This PR proposes a change in how slashable amounts are computed when a user withdraws. This fixes issue #27.

Note that for this to work, we need to iterate over the slashes in slash.epoch order. It would be great to get rid of this requirement (at least for the TLA+ model) but I could not figure out how.

[brentstone]

Was this mistakenly removed? L305 below updates amount_after_slashing, except now this variable isn't declared explicitly anywhere

[angbrav]

My fault, the intention is that line 305 declares it (just missing the var keyword). Fixed. Thanks ;)

[tzemanovic]

I think a naive approach that works for more than 2 slashes (e.g. 3 slashes where no 2 consecutive slashes have unbonding_length epochs between them, but the first and the last slash do) with another loop would be something like:

Suggested change

	var previous_slash_epoch = -1
	forall (slash in slashes[validator_address] in slash.epoch order s.t. start <= slash.epoch && slash.epoch <= end)
	if previous_slash_epoch == -1 || previous_slash_epoch + unbonding_length < slash.epoch do
	updated_amount = amount - slashed_amount
	slashed_amount += updated_amount*slash.rate
	previous_slash_epoch = slash.epoch
	forall (slash in slashes[validator_address] in slash.epoch order s.t. start <= slash.epoch && slash.epoch <= end) do
	//Update amount with slashes that happened more than `unbonding_length` before this slash
	forall (other_slash in slashes[validator_address] s.t. start <= other_slash.epoch && other_slash.epoch + unbonding_length < slash.end) do
	updated_amount = amount - updated_amount*other_slash.rate
	slashed_amount += updated_amount*slash.rate

[angbrav]

I think a naive approach that works for more than 2 slashes (e.g. 3 slashes where no 2 consecutive slashes have unbonding_length epochs between them, but the first and the last slash do) with another loop would be something like:

I think it does not work. I tried to run it with 4 infractions that occurred at epochs e, e+1, e+unbonding_lenght+1, and e+unbonding_lenght+2. Assume that a user has x tokens delegated to the misbehaving validator by e, and unbonds them and attempts to withdraw at an epoch > e+2*unbonding_lenght+2 i.e., all infractions have been processed. Assume the slash rate is 0.2 for all infractions.

• The slashed amount of infraction 1 should be 0.2*x.
• The slashed amount of infraction 2 should be 0.2*x. This is because infraction 1 is not processed at e+1: the epoch of infraction 2.
• The slashed amount of infraction 3 should be 0.2*0.8*x=0.16*x. This is because infraction 1 has been processed at e+unbonding_lenght+1: the epoch of infraction 3; but not infraction 2.
• The slashed amount of infraction 4 should be 0.2*0.6*x=0.12*x. This is because infraction 1 and 2 have been processed at e+unbonding_lenght+2: the epoch of infraction 4; but not infraction 3.

I think running your pseudocode, we get the slashed amount of infraction 4 wrong:
After processing the third slash, updated_amount = x - 0.2*x = 0.8*x. Then, while processing the fourth we take the following steps:

• updated_amount=x - 0.2*0.8*x=0.84*x
• updated_amount=x - 0.2*0.84*x=x-0.168*x=0.832*x
• slashed_amount= 0.2*0.832*x=0.1664*x and it should be 0.12*x

I may have made a mistake in the calculations (or maybe there is a bug in your pseudocode). I am proposing an alternative that I think works (maybe not the most efficient solution):

forall (<start,end,amount> in selfunbonds) do
    
    var computed_amounts = {}
    forall (slash in slashes in slash.epoch order s.t. start <= slash.epoch && slash.epoch <= end) do
      var updated_amount = amount
      //Update amount with slashes that happened more than `unbonding_length` before this slash
      forall (slashed_amount in computed_amounts s.t. slashed_amount.epoch + unbonding_length < slash.epoch) do
        updated_amount -= slashed_amount.amount
      computed_amounts = add(computed_amounts, SlashedAmount{epoch: slash.epoch, amount: updated_amount*slash.rate})

    var amount_after_slashing = amount - sum({computed_amount.amount | computed_amount in computed_amounts})
    balance[delegator_address] += amount_after_slashing
    balance[pos] -= amount_after_slashing

@tzemanovic what do you think?

[angbrav]

A couple of minor changes that improve things a bit:

    var computed_amounts = {}
    var updated_amount = amount
    forall (slash in slashes in slash.epoch order s.t. start <= slash.epoch && slash.epoch <= end) do
      //Update amount with slashes that happened more than `unbonding_length` before this slash
      forall (slashed_amount in computed_amounts s.t. slashed_amount.epoch + unbonding_length < slash.epoch) do
        updated_amount -= slashed_amount.amount
        computed_amounts = computed_amounts \ {slashed_amount}
      computed_amounts = computed_amounts \union {SlashedAmount{epoch: slash.epoch, amount: updated_amount*slash.rate}}

    var amount_after_slashing = updated_amount - sum({computed_amount.amount | computed_amount in computed_amounts})
    balance[delegator_address] += amount_after_slashing
    balance[pos] -= amount_after_slashing

[tzemanovic]

ah I see! I think I was meaning to do updated_amount = updated_amount - updated_amount*other_slash.rate, but even that would have been wrong as that would reapply other_slashes multiple times.

computed_amounts = computed_amounts \ {slashed_amount} removes slashed_amount from the set, right? Your solutions LGTM!

[angbrav]

computed_amounts = computed_amounts \ {slashed_amount} removes slashed_amount from the set, right?

Yes!

our solutions LGTM!

Awesome, I'll work on the TLA+ version :)