informalsystems / partnership-heliax

1 stars 0 forks source link

PoS updates to ensure non-negative stakes + misc upgrades #50

Closed brentstone closed 1 year ago

brentstone commented 1 year ago

Based on #43.

The changes in this PR were initiated by the need to adjust the pseudocode to reflect changes in the Namada implementation that prevent the validator's deltas from going negative with the existence of more arbitrary slashing conditions.

Some other pseudocode updates that are not directly related to this are included as well.

angbrav commented 1 year ago

I am adding these changes to the Quint spec to see what happens. I'll get then back to you :)

angbrav commented 1 year ago
  • I've reviewed the total_unbonded optimization and looks good to me. It is already in the Quint spec and seems to be working fine. Can we maybe change the variable name set_unbonds to something else (total_unbonded for instance)? it is not a set anymore.
  • Adding cubic_slash_window_width seems fine. I am adding to Quint to see what happens.

Done, looks good :)

  • I have not checked the remaining: (i) preventing stake becoming zero; (ii) slash pool. Although I have left a comment about the latter.

@brentstone what do you think about splitting once more this PR into two: one with the optimization for total_unbonded and cubic_slash_window_width, which I believe would be ready to merge; and a second one with the logic specific for preventing stake becoming zero and the slash pool?

brentstone commented 1 year ago

Closed in favor of splitting out into #54 and #55.