Add cubic slashing to pseudocode model #16

angbrav · 2022-07-04T13:53:48Z

This PR integrates cubic slashing to the pseudocode model.

I have created a new file because this PR does not add a new feature but changes the slashing mechanism. This makes it more challenging to review, as the whole file is marked a new by GitHub. Things to review:

func new_evidence
func end_of_epoch

Open issues:

Some epoched variables get updated at different offsets: validator.state and validator_sets

tzemanovic · 2022-07-04T16:49:21Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+balances[] in Addr → int //map from address to integer
+bonds[][] in (Addr X Addr) → Bond //map from address to map from address to bond
+unbonds[][] in (Addr X Addr) → Unbond  //map from (address, address) to unbond
+slashes[] in Epoch → 2^Slash //map from address to list of slashes


Suggested change

slashes[] in Epoch → 2^Slash //map from address to list of slashes

slashes[] in Epoch → 2^Slash //map from epoch to list of slashes

Thanks, fixed.

tzemanovic · 2022-07-04T17:11:15Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+
+type Validator struct {
+  consensus_key map<Epoch, Key>
+  state map<Epoch, {inactive, candidate, frozen, jailed}>


I think the frozen state may need to be a separate field as it needs to be set as soon as evidence is found

That's the behavior now: the validator's state is set to frozen as soon as evidence is found. But I agree this needs more analysis as it may interfere with other behaviors.

sergio-mena · 2022-07-05T08:29:27Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+  epoch Epoch
+  validator Addr
+  voting_power VotingPower //new in cubic slashing
+  slash_type {duplicate_vote, ligth_client_attack} //not used in cubic slashing


I might have misunderstood, but I think we still have different types of misbehavior

This is something I want to clarify. In the spec, the infraction type is never used explicitely.

sergio-mena · 2022-07-05T08:35:01Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+}
+
+type Slash struct {
+  epoch Epoch


Do we need this? (it is now the key of the map containing this structure)

Actually, there are some inconsistencies. Withdrawing is till using the slashes variables indexed by validators. I'll fix this and remove the epoch field if it is not needed. Thanks for pointing it out!

I think I fixed it.

sergio-mena · 2022-07-05T08:38:20Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+{
+  //disallow unbonding if the validator is frozen
+  var state = read_epoched_field(validators[validator_address].state, cur_epoch, ⊥)
+  if (state != frozen) then


how about jailed?

I think this is intended, one should allow delegators to unbond their tokens if the validator gets jalied.

sergio-mena · 2022-07-05T08:44:22Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+  var vpower = read_epoched_field(validators[evidence.validator].total_deltas, evidence.epoch, 0)
+  var slash = Slash{epoch: evidence.epoch, rate: 0, voting_power: vpower}
+  //enqueue slash (Step 1.1 of cubic slashing)
+  append(enqueued_slashes[evidence.epoch + unbonding_epoch], slash)


I can't find the definition of enqueued_slashes

Also, what would happen if evidence.epoch is too far in the past? (is it possible?)

jmalicevic · 2022-07-05T08:45:14Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+    validators[validator_address].state[cur_epoch+1] = jailed
+    remove_from_validator_sets(validator_address, cur_epoch+1)
+    //iterate over all slashes for infractions within (-1,+1) epochs range (Step 2.1 of cubic slashing)
+    var set_slashes = {s | s in enqueued_slashes[epoch] && cur_epoch-1 <= epoch <= cur_epoch+1 && s.validator == validator_address}


As we are iterating over the previous and next epochs, and we will repeat this step for cur_epoch + 1, are we not punishing the validator multiple times for the same evidence. So for evidence from cur_epoch, the validator is punished in epochs cur_epoch -1, cur_epoch and cur_epoch + 1.

Related to this, at the end of curr_epoch, we decrease the voting power (and the total voting power). But then at the end ofcurr_epoch + 1we will do the same thing taking into account an at that point invalid voting power and decreasing it again.

As we are iterating over the previous and next epochs, and we will repeat this step for cur_epoch + 1, are we not punishing the validator multiple times for the same evidence. So for evidence from cur_epoch, the validator is punished in epochs cur_epoch -1, cur_epoch and cur_epoch + 1.

I think I made the same comment during one meeting. This is intended though. The way I currently interpret this is that any evidence may contribute to multiple slashes, instead of thinking a validator may be punished twice for the same evidence. So for instance, if there is evidence for a validator at epochs cur_epoch and cur_epoch + 1, the evidence at cur_epoch contributes to the slash rate of the slash computed at cur_epoch + 1 and vice-versa. Once of the goals of the slashing mechanism is to severe punishing to validators that misbehave in consecutive epochs.

Related to this, at the end of curr_epoch, we decrease the voting power (and the total voting power). But then at the end ofcurr_epoch + 1we will do the same thing taking into account an at that point invalid voting power and decreasing it again.

I think my previous answer may clarify this. Let me know if it does not.

Yes, my understanding of what Heliax want (we discussed it in one of the last meetings) matches Manu's. I believe they are aware of the implications that @jmalicevic points out in her comment above

sergio-mena · 2022-07-05T08:48:28Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+      //set the slash on the now "finalised" slash in storage (Step 2.3 of cubic slashing)
+      slash.rate = rate
+      append(slashes[cur_epoch], slash)
+      slashed_amount = slash.voting_power * slash.rate


So all misbehavior types have the same severity?

Unclear from the spec. Need clarification

sergio-mena · 2022-07-05T08:53:02Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+//This function is called by transactions tx_self_bond, tx_delegate and tx_redelegate
+//the only possible values for offset_length are pipeline_length and unbonding_length
+func bond(validator_address, delegator_address, amount, offset_length)
+{


Do we need to block this as well for frozen validators?

sergio-mena · 2022-07-05T08:56:51Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+      //set the slash on the now "finalised" slash in storage (Step 2.3 of cubic slashing)
+      slash.rate = rate
+      append(slashes[cur_epoch], slash)
+      slashed_amount = slash.voting_power * slash.rate


Should we unfreeze validators here?
Otherwise, how does a frozen validator leave that state?

Oh, I see they get jailed. Please ignore my comment

jmalicevic · 2022-07-05T09:17:59Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+  forall (validator_address in set_validators) do
+    //jail validator (Step 1.2 of cubic slashing). This also unfreeze the validator (Step 2.5 of cubic slashing)
+    validators[validator_address].state[cur_epoch+1] = jailed
+    remove_from_validator_sets(validator_address, cur_epoch+1)


In bond(), we allow delegators to bond assets to any validator that is a validator for a current epoch. As the epochs we bond to can be in the future compared to when the validator is jailed, technically, we allow bonding assets to a validator that is currently jailed. Should we have a condition for bonding to a validator only if this validotor.state != jailed in any of the epochs before bonding_epoch ?

This is a possibility. I lean towards making delegators responsible for tracking validators though. I agree that some support from the PoS module will help delegators to avoid delegating to non-active or jailed validators, but it complicates the model. I think it is more interesting to simplify this type of logic as much as possible and focus on the most fundamental aspects of the PoS model, e.g., make sure that if a validator misbehaves and this is detected on time, we are able to slash.

sergio-mena · 2022-07-19T08:13:02Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+type Slash struct {
+  epoch Epoch
+  rate float
+  vpower_fraction VotinPower //new in cubic slashing


Suggested change

vpower_fraction VotinPower //new in cubic slashing

vpower_fraction VotingPower //new in cubic slashing

sergio-mena · 2022-07-19T08:17:10Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+  append(enqueued_slashes[evidence.epoch + unbonding_length], slash)
+  //jail validator (Step 1.2 of cubic slashing)
+  validators[validator_address].state[cur_epoch + 1] = jailed
+  remove_from_validator_sets(validator_address, cur_epoch + 1)
  //freeze validator to prevent delegrators from altering their delegations (Step 1.3 of cubic slashing)


Suggested change

//freeze validator to prevent delegrators from altering their delegations (Step 1.3 of cubic slashing)

//freeze validator to prevent delegators from altering their delegations (Step 1.3 of cubic slashing)

sergio-mena · 2022-07-19T08:43:47Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+  //enqueue slash (Step 1.1 of cubic slashing)
+  append(enqueued_slashes[evidence.epoch + unbonding_length], slash)
+  //jail validator (Step 1.2 of cubic slashing)
+  validators[validator_address].state[cur_epoch + 1] = jailed


Isn't jailed a different state now? (non-epoched)

sergio-mena · 2022-07-19T08:45:08Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+  //enqueue slash (Step 1.1 of cubic slashing)
+  append(enqueued_slashes[evidence.epoch + unbonding_length], slash)
+  //jail validator (Step 1.2 of cubic slashing)
+  validators[validator_address].state[cur_epoch + 1] = jailed


Suggested change

validators[validator_address].state[cur_epoch + 1] = jailed

validators[validator_address].jailed = true

sergio-mena · 2022-07-19T08:50:04Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+    var set_slashes = {s | s in enqueued_slashes[epoch] && cur_epoch-1 <= epoch <= cur_epoch+1 && s.validator == validator_address}
+    //calculate the slash rate (Step 2.2 of cubic slashing)
+    var rate = compute_final_rate(set_slashes)
+    forall (slash in {s | s in enqueued_slashes[cur_epoch] && slash.validator == validator_address}) do


The nested "forall" delimited by indentation (à la python) is a bit confusing. Would it be possible to extract the logic of the inner "forall" into its own function? (or something similar)

By slash.validator, did you mean s.validator ?

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

sergio-mena · 2022-07-19T09:03:01Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+```
+
+```go
+func remove_from_validator_sets(validator_address)


Two comments (related to each other):

Isn't this the job of update_validator_sets?

As we are not marking the removed validator, won't the next execution of update_validator_sets override the result of this function?

N.B.: It is not totally true that we are not marking the removed validator, because the caller of this function is jailing it, but update_validator_sets doesn't take it into account.

So, IMO, we should remove remove_from_validator_sets, and modify update_validator_sets to remove any jailed validator from the active set.

Follow up...
I see you remove the validator from both sets, so I realize update_validator_sets won't really override the effects of this.
However, how (and when) will we reintroduce that validator back into one of the two sets?

However, how (and when) will we reintroduce that validator back into one of the two sets?

There is no way to unjail validators at the moment, it is unspecified in Heliax's specification.

So, IMO, we should remove remove_from_validator_sets, and modify update_validator_sets to remove any jailed validator from the active set.

It is cosmetics. Let's first make sure it behaves as expected. We can later merge both functions if we think it is useful.

OK, please add a TODO in the model so we don't forget to specify unjailing (after discussing with Heliax, and understanding how they want to model unjailing)

sergio-mena · 2022-07-19T09:18:19Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+    //unfrozen the validator (Step 2.5 of cubic slashing)
+    frozen[validator_address] = false


Suggested change

//unfrozen the validator (Step 2.5 of cubic slashing)

frozen[validator_address] = false

//unfreeze the validator (Step 2.5 of cubic slashing)

validators[validator_address].frozen = false

sergio-mena · 2022-07-19T09:49:10Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+  jailed bool
+  frozen bool


From what was discussed in the last meeting with Heliax folks, I understand why frozen is not epoched.
However, I don't think I understand why jailed is not epoched. Probably has to do with the fact that we don't have the "unjailing" mechanism in the model yet

No particular reason, trying to stick to the specification: in my understanding, jailed is not epoched. We have to figure out a way to deal with epoched variables that can be updated at different offsets. Once we resolve that, we could think of merging jailed (or frozen) into the variable state.

I agree that dealing with epoched variables that can be updated at different offsets is the biggest and most urgent of our concerns, given the ramifications it has (this is an example).

sergio-mena · 2022-07-19T09:56:14Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+```go
+end_of_epoch()
+{
+  set_validators = {val | val = slash.validator && slash in enqueued_slashes[cur_epoch]}


Suggested change

set_validators = {val | val = slash.validator && slash in enqueued_slashes[cur_epoch]}

var set_validators = {val | val = slash.validator && slash in enqueued_slashes[cur_epoch]}

Not sure about this

sergio-mena · 2022-07-19T10:15:14Z

2022/Q2/artifacts/pos-model/PoS-model-cubic.md

+  //substract any pending slash before withdrawing
+  forall (<start,end,amount> in selfunbonds) do
+    var amount_after_slashing = amount
+    forall (slash in slashes[validator_address] s.t. start <= slash.epoch && slash.epoch <= end)


So, what would happen if validator validator_address:

doesn't have slashes (meaning, no punishment against it was processed -- yet -- as part of end_of_epoch)

there are items in enqueued_slashes (for an epoch e > cur_epoch) that refer to validator_address

How is this case handled?

These are the type of things we want to check with the TLA+ model. I believe this is related to issue #7, for which there is no solution currently.

I see. If there is no TODO in the model's text, please add one, as this has to be dealt with to have a correct model

I have copied the link to this comment above the withdraw function

angbrav · 2022-07-29T17:03:20Z

I think everything is addressed and discussed. I am merging this and working on how to deal with epoched variables that are updated at different offsets in a different PR.

firs version cubic slashing pseudocode

bda2d39

tzemanovic reviewed Jul 4, 2022

View reviewed changes

sergio-mena reviewed Jul 5, 2022

View reviewed changes

jmalicevic reviewed Jul 5, 2022

View reviewed changes

sergio-mena reviewed Jul 5, 2022

View reviewed changes

some fixes

0e74dbd

jmalicevic reviewed Jul 5, 2022

View reviewed changes

changes after meeting

036f810

sergio-mena reviewed Jul 19, 2022

View reviewed changes

2022/Q2/artifacts/pos-model/PoS-model-cubic.md Show resolved Hide resolved

sergio-mena reviewed Jul 19, 2022

View reviewed changes

angbrav added 2 commits July 26, 2022 16:09

address more comments

9b5d585

add a couple of TODOs

9612ba7

angbrav merged commit 46a6006 into trunk Jul 29, 2022

angbrav mentioned this pull request Aug 18, 2022

Move Q3 pseudocode model to the Q3 folder #20

Merged

angbrav deleted the manuel/cubic-slashing-psuedo branch February 17, 2023 15:35

	slashes[] in Epoch → 2^Slash //map from address to list of slashes
	slashes[] in Epoch → 2^Slash //map from epoch to list of slashes

	vpower_fraction VotinPower //new in cubic slashing
	vpower_fraction VotingPower //new in cubic slashing

	//freeze validator to prevent delegrators from altering their delegations (Step 1.3 of cubic slashing)
	//freeze validator to prevent delegators from altering their delegations (Step 1.3 of cubic slashing)

	validators[validator_address].state[cur_epoch + 1] = jailed
	validators[validator_address].jailed = true

		//unfrozen the validator (Step 2.5 of cubic slashing)
		frozen[validator_address] = false

	set_validators = {val \| val = slash.validator && slash in enqueued_slashes[cur_epoch]}
	var set_validators = {val \| val = slash.validator && slash in enqueued_slashes[cur_epoch]}

Add cubic slashing to pseudocode model #16

Add cubic slashing to pseudocode model #16

Conversation

angbrav commented Jul 4, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

angbrav Jul 5, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

angbrav Jul 26, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sergio-mena Jul 5, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

angbrav Jul 26, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sergio-mena Jul 19, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sergio-mena Jul 19, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sergio-mena Jul 19, 2022 • edited Loading

Choose a reason for hiding this comment

sergio-mena Jul 19, 2022 • edited Loading

Choose a reason for hiding this comment

angbrav Jul 26, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

angbrav Jul 29, 2022 • edited Loading

Choose a reason for hiding this comment

angbrav commented Jul 29, 2022

angbrav commented Jul 4, 2022 •

edited

Loading

angbrav Jul 5, 2022 •

edited

Loading

angbrav Jul 26, 2022 •

edited

Loading

sergio-mena Jul 5, 2022 •

edited

Loading

angbrav Jul 26, 2022 •

edited

Loading

sergio-mena Jul 19, 2022 •

edited

Loading

sergio-mena Jul 19, 2022 •

edited

Loading

sergio-mena Jul 19, 2022 •

edited

Loading

sergio-mena Jul 19, 2022 •

edited

Loading

angbrav Jul 26, 2022 •

edited

Loading

angbrav Jul 29, 2022 •

edited

Loading