Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix issue 34 #37

Merged
merged 9 commits into from
Feb 15, 2023
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 27 additions & 6 deletions 2022/Q4/artifacts/PoS-pseudocode/PoS-model.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,11 +17,21 @@ type JailRecord struct {
epoch Epoch
}

type UnbondRecord struct {
amount uint
start Epoch
}

type SlashedAmount struct {
epoch Epoch
amount uint
}

type Validator struct {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

total_unbonds should really be total_unbonded, correct?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

@angbrav angbrav Feb 15, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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...

consensus_key map<Epoch, Key>
state map<Epoch, {inactive, candidate}>
total_deltas map<Epoch, amount:int>
total_unbonds map<Epoch, amount:int>
total_unbonds map<Epoch, Set<UnbondRecord>>
voting_power map<Epoch, VotingPower>
reward_address Addr
jail_record JailRecord
Expand Down Expand Up @@ -269,17 +279,26 @@ func unbond(validator_address, delegator_address, unbond_amount)
if amount > remain && remain > 0 do
bonds[delegator_address][validator_address].deltas[start] = amount - remain
unbonds[delegator_address][validator_address].deltas[start, cur_epoch+pipeline_length+unbonding_length] = remain
remain = 0
forall (slash in slashes[validator_address] s.t. start <= slash.epoch)
amount_after_slashing -= remain*slash.rate
//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).
//Same below
validators[validator_address].total_unbonds[cur_epoch+pipeline_length] = {UnbondRecord{amount: remain, start: start}} \union validators[validator_address].total_unbonds[cur_epoch+pipeline_length]
remain = 0
//If the remaining is greater or equal than the next bond amount
else if amount <= remain && remain > 0 do
bonds[delegator_address][validator_address].deltas[start] = 0
unbonds[delegator_address][validator_address].deltas[start, cur_epoch+pipeline_length+unbonding_length] = amount
remain -= amount
validators[validator_address].total_unbonds[cur_epoch+pipeline_length] = {UnbondRecord{amount: amount, start: start}} \union validators[validator_address].total_unbonds[cur_epoch+pipeline_length]
forall (slash in slashes[validator_address] s.t. start <= slash.epoch)
amount_after_slashing -= amount*slash.rate
validators[validator_address].total_unbonds[cur_epoch+pipeline_length] += unbond_amount
remain -= amount
update_total_deltas(validator_address, pipeline_length, -1*amount_after_slashing)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, realized I am wrong in the above comment.

update_voting_power(validator_address, pipeline_length)
update_total_voting_power(pipeline_length)
Expand Down Expand Up @@ -500,11 +519,13 @@ end_of_epoch()
//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
total_unbonded += validators[validator_address].total_unbonded[epoch]
forall (unbond in validators[validator_address].total_unbonds[epoch] s.t. unbond.start <= slash.epoch)
total_unbonded += unbond.amount

var last_slash = 0
forall (offset in 1..unbonding_length) do
total_unbonded += validators[validator_address].total_unbonded[cur_epoch + offset]
forall (unbond in validators[validator_address].total_unbonds[epoch] s.t. unbond.start <= slash.epoch)
total_unbonded += unbond.amount
var this_slash = (total_staked - total_unbonded) * slash.rate
var diff_slashed_amount = last_slash - this_slash
last_slash = this_slash
Expand Down