Fix issue 34

[angbrav]

This PR fixes issue #34 in the pseudocode model.

The current model disregards a corner case that should be taken care of in the implementation:

• Assume a user delegates 10 tokens to a validator at epoch e1
• Assume the user unbonds twice 5 tokens from the same validator in the same epoch in two different transactions e2
• When executing the first undelegate tx, the model creates the record UnbondRecord{amount: 5, start: e1 } and updates the bond to 5 tokens
• When executing the second undelegate tx, the model creates the same record UnbondRecord{amount: 5, start: e1 } and removes the bond.
• The problem is that we keep unbond records in a set and when we try to add the second record, since it is a duplicate, it will be discarded.

It is an easy fix I'd say: use a bag instead of a set to allow duplicates, or check if the set includes the record and act upon (remove it, create a new one with double the amount, and add it). For now, I've left a comment on the model; I didn't want to "pollute" it. If we decide not to deal with it in the mode, I'll open an issue and refer to it in the model.

[brentstone]

Should remain = 0 come after the loop over the slashes and validators[validator_address].total_unbonds[cur_epoch+pipeline_length] = {UnbondRecord{amount: remain, start: start}}?

[angbrav]

Thanks @brentstone! You are completely right. Fixed.

[brentstone]

total_unbonds should really be total_unbonded, correct?

[angbrav]

Do you mean the field in the Validator's struct? If I am not wrong, we use total_unbonds throughout the spec and total_unbonded at the end-of-epoch function when folding total_unbonds. I agree we could find better names. Was that your concern, or I misunderstood it?

[brentstone]

Ok thanks for clarifying that these are intended to be different.

I'll elaborate a bit. First, yes, the field total_unbonds inside the Validator struct should be a map<Epoch, UnbondRecord> judging by the unbond code. It also seems that the Validator struct should explicitly have a total_unbonded field that is a map<Epoch, uint>, right? I think I was confused by the lack of a declaration of total_unbonded anywhere outside the end_of_epoch() code.

I'm still somewhat confused by what the purpose of Validator::total_unbonds is. From the pseudocode, it seems only to be used in func unbond, where we set values inside of it, but I don't see any other place where its data is read and then used for something. It is not in end_of_epoch, but perhaps there is another bug. From the following code from end_of_epoch:

      var total_unbonded = 0
      //find the total unbonded from the slash epoch up to the current epoch first
      //a..b notation determines an integer range: all integers between a and b inclusive
      forall (epoch in slash.epoch+1..cur_epoch) do
        forall (unbond in validators[validator_address].total_unbonded[epoch] s.t. unbond.start <= slash.epoch)
          total_unbonded += unbond.amount

it looks like perhaps forall (unbond in validators[validator_address].total_unbonded[epoch] should be forall (unbond in validators[validator_address].total_unbonds[epoch]. Does this seem to be the intention?

[brentstone]

actually I think I'm realizing that total_unbonds should be a map<Epoch, Set<UnbondRecord>>, where Set<UnbondRecord> could also be a Vec or similar

[angbrav]

Yes, the code in end_of_epoch has a typo and validator's total_unbonds should be map<Epoch, Set<UnbondRecord>>. Both are now fixed, thanks for spotting them! It is difficult to produce typo-free pseudocode for non-executable specs...

[brentstone]

Going through the pseudocode again as I work on anoma/namada#892, apologies if some of my questions are technically out of scope for this PR but I figure here is a good place to put them anyway...

Looks like in withdrawing we are using a struct that looks like

type SlashedAmount struct {
  epoch Epoch
  amount uint
}

If I understand this correctly, we should add it to the other type declarations at the top of PoS-model.md

[brentstone]

What is the meaning of computed_amounts = computed_amounts \ {slashed_amount} in func withdraw?

[angbrav]

Going through the pseudocode again as I work on anoma/namada#892, apologies if some of my questions are technically out of scope for this PR but I figure here is a good place to put them anyway...

Sure, no problem.

Looks like in withdrawing we are using a struct that looks like

type SlashedAmount struct {
  epoch Epoch
  amount uint
}

If I understand this correctly, we should add it to the other type declarations at the top of PoS-model.md

Yes, done.

What is the meaning of computed_amounts = computed_amounts \ {slashed_amount} in func withdraw?

Set difference: X\Y is the set of elements that belong to X but not to Y. In this case it removes slashed_amount from the set computed_amounts.

[brentstone]

I think that we should be tracking something like total_slashed_amount rather than amount_after_slashing. Looks like we want to supply update_total_deltas with the deltas change, rather than the new value post-slashing.

So instead of amount_after_slashing -= amount*slash.rate, want total_slashed_amount += amount*slash.rate.

[brentstone]

Sorry, realized I am wrong in the above comment.