diff --git a/2023/Q2/artifacts/PoS-quint/extraSpells.qnt b/2023/Q2/artifacts/PoS-quint/extraSpells.qnt index da869ed..85ec28b 100644 --- a/2023/Q2/artifacts/PoS-quint/extraSpells.qnt +++ b/2023/Q2/artifacts/PoS-quint/extraSpells.qnt @@ -9,6 +9,10 @@ module extraSpells { import basicSpells.* from "./basicSpells" + pure def printVariable(name: str, variable: a): bool = true + + pure def printMapVariables(__map: a -> b): bool = true + /// Compute the minimum of two integers. /// /// - @param __i first integer @@ -94,7 +98,7 @@ module extraSpells { assert(Map(2 -> 3, 4 -> 5).mapSafeSet(2, 7) == Map(2 -> 7, 4 -> 5)) } - /// Remove a set of map entries. + /// Remove a set of map entries. /// /// - @param __map a map to remove the set of entries from /// - @param __keys the set of keys to remove diff --git a/2023/Q2/artifacts/PoS-quint/helper-functions.qnt b/2023/Q2/artifacts/PoS-quint/helper-functions.qnt new file mode 100644 index 0000000..a1ab55c --- /dev/null +++ b/2023/Q2/artifacts/PoS-quint/helper-functions.qnt @@ -0,0 +1,1024 @@ +// -*- mode: Bluespec; -*- +/** + * + * Manuel Bravo, Informal Systems, 2023 + */ +module helperFunctions { + + import basicSpells.* from "./basicSpells" + import extraSpells.* from "./extraSpells" + import Dec.* from "./dec" + import types.* from "./namada-types" + + pure def slashProcessingDelay = CUBIC_OFFSET + UNBONDING_OFFSET + + pure def inRedelegationSlashingWindow(infractionEpoch: Epoch, redelegationStart: Epoch, redelegationEnd: Epoch): bool = { + redelegationStart - UNBONDING_OFFSET - CUBIC_OFFSET <= infractionEpoch and infractionEpoch < redelegationEnd + } + + pure def endRedelegationFromStart(redelegationStart: Epoch): Epoch = { + redelegationStart + PIPELINE_OFFSET + } + + pure def startRedelegationFromEnd(redelegationEnd: Epoch): Epoch = { + redelegationEnd - PIPELINE_OFFSET + } + + // ************************************************************************** + // Delegate helper functions + // ************************************************************************* + + // The function addBond adds a bond to a map of bonds. If there is an existing bond with the same + // starting epoch, then the function simply adds the amount of tokens to the existing entry. + // - @param bonds a map of bonds. + // - @param start the starting epoch of the bond to add. + // - @param amount the amount of tokens of the bond to add. + // - @returns a map of bonds accounting for the new bond. + pure def addBond(bonds: Epoch -> int, start: Epoch, amount: int): Epoch -> int = { + if (bonds.has(start)) bonds.set(start, bonds.get(start) + amount) + else bonds.mapSafeSet(start, amount) + } + + run addBondTest = all { + val bonds = Map(1 -> 5, 2 -> 3, 6 -> 8) + all { + assert(addBond(bonds, 2, 6) == Map(1 -> 5, 2 -> 9, 6 -> 8)), + assert(addBond(bonds, 3, 6) == Map(1 -> 5, 2 -> 3, 3 -> 6, 6 -> 8)), + } + } + + // ************************************************************************** + // Unbond helper functions + // ************************************************************************* + + // The function unbonds a bond record contraint to a maximum amount (acc.remainder). + // - @param acc a record with three fields: + // - remainder: the maximum amount of tokens to be unbonded. + // - toRemove: a set of bond records which includes the set of bond records that have been unbonded so far. + // - new: a bond record with start epoch equal to -1. + // - @param bond the bond record to be unbonded by the function. + // - @returns an update acc record: subtracts the minimum between bond.amount and acc.remainder from acc.remainder; adds the bond to acc.toRemove; + // and if bond.amount if gretaer than acc.remainder (meaning that the bond is only partially unbonded), creates a new bond record in acc.new + // of bond.amount - acc.remainder tokens. + pure def unbondBond(acc: {remainder: int, toRemove: Set[Epoch], new: {start: int, amount: int}}, bond: {start: int, amount: int}): {remainder: int, toRemove: Set[Epoch], new: {start: int, amount: int}} = { + val amountUnbonded = min(bond.amount, acc.remainder) + {remainder: acc.remainder - amountUnbonded, + toRemove: if (bond.amount <= acc.remainder) acc.toRemove.setAdd(bond.start) else acc.toRemove, + new: if (bond.amount > acc.remainder) {start: bond.start, amount: bond.amount - acc.remainder} else acc.new} + } + + run unbondBondTest = all { + assert(unbondBond({remainder: 10, toRemove: Set(9, 8), new: {start: -1, amount: 0}}, {start: 6, amount: 5}) == + {remainder: 5, toRemove: Set(9, 8, 6), new: {start: -1, amount: 0}}), + assert(unbondBond({remainder: 10, toRemove: Set(9, 8), new: {start: -1, amount: 0}}, {start: 6, amount: 11}) == + {remainder: 0, toRemove: Set(9, 8), new: {start: 6, amount: 1}}) + } + + // The function `iterateBondsUpToAmount` computes the set of bonds that have to be unbonded in order to unbond a given amount. To do so, it iterates + // over a map of bonds in decreasing starting epoch order until the amount is reached. For each iterated bond, the function calls unbondBond while + // there are still tokens to be unbonded. + // - @param bonds a map of bonds that can be unbonded. + // - @param amount the amount of tokens that have to be unbonded. + // - @returns a record with two fields: toRemove the set of bonds starting epochs that have been unbonded and a new bond + // that contains a bond record (starting epoch and amount) if a bond has to be partially unbonded or a bond record with start epoch equal to -1 + // otherwise, indicating that no bond has to be partially unbonded. + pure def iterateBondsUpToAmount(bonds: Epoch -> int, amount: int): {toRemove: Set[Epoch], new: {start: int, amount: int}} = { + val setEpochs = sortSetDecreasing(bonds.keys()) + val result = setEpochs.foldl({remainder: amount, toRemove: Set(), new: {start: -1, amount: 0}}, + (acc, e) => if (acc.remainder == 0) acc else unbondBond(acc, {start: e, amount: bonds.get(e)})) + {toRemove: result.toRemove, new: result.new} + } + + run iterateBondsUpToAmountTest = { + val bonds = Map(1 -> 5, 2 -> 3, 6 -> 8) + all { + assert(iterateBondsUpToAmount(bonds, 8) == {toRemove: Set(6), new: {start: -1, amount: 0}}), + assert(iterateBondsUpToAmount(bonds, 10) == {toRemove: Set(6), new: {start: 2, amount: 1}}), + assert(iterateBondsUpToAmount(bonds, 11) == {toRemove: Set(6, 2), new: {start: -1, amount: 0}}), + assert(iterateBondsUpToAmount(bonds, 12) == {toRemove: Set(6, 2), new: {start: 1, amount: 4}}) + } + } + + // ************************************************************************** + // Redelegation helper functions + // ************************************************************************* + + // It partially unbonds a redelegated bonds map. + // - @param redelegatedBonds a map of redelegated bonds from source validator to bond starting epoch at the source validator to amount. + // - @param epoch the epoch at which the redelegated bonds being modified were bonded to the validator + // - @param amount the amount of tokens that have to be unbonded. + // - @returns a ModifiedRedelegation record with all information related to the partially unbonded redelegated tokens. The iteration over source validators is non-deterministic at the moment + // (this should be made deterministic). Within a source validator, the iteration over bond starting epochs is done deterministically in the epoch order + // picked by the iterateBondsUpToAmount function. At the moment, the iterateBondsUpToAmount function iterates over these epochs in decreasing order. + // Note that valsToRemove includes valToModify if different to "" and epochsToRemove includes epochToModify if different to -1. + pure def computeModifiedRedelegation(redelegatedBonds: RedelegatedBondsMap, epoch: Epoch, amount: int): ModifiedRedelegation = { + val totalRedelegated = redelegatedBonds.keys().fold(0, (sum, src) => redelegatedBonds.get(src).keys().fold(sum, (acc, e) => acc + redelegatedBonds.get(src).get(e))) + // If the total amount of redelegated bonds is less than the target amount, then all redelegated bonds must be unbonded. + if (totalRedelegated <= amount) {epoch: -1, valsToRemove: Set(), valToModify: "", epochsToRemove: Set(), epochToModify: -1, newAmount: -1} + // If the total amount of redelegated bonds is greater than the target amount, then we need to iterate over the redelegated bonds + // until the target amount is unbonded. The iteration works as follows (comments interleaved with the folds): + // 1. It first iterates over source validators. We should iterate in a deterministic order over validators here. Do not know how to do it in Quint at the moment. + else redelegatedBonds.keys().fold({remainder: amount, modified: {epoch: epoch, valsToRemove: Set(), valToModify: "", epochsToRemove: Set(), epochToModify: -1, newAmount: -1}}, + (acc, src) => if (acc.remainder == 0) acc + else { + val totalSrcValidator = redelegatedBonds.get(src).keys().fold(0, (sum, e) => sum + redelegatedBonds.get(src).get(e)) + // 2. For a given validator, if the remaining is greater or equal to the total amount of redelegated tokens of that source validator, the + // function removes the source validator: all its redelegated tokens will be effectively unbonded. + if (totalRedelegated <= acc.remainder) {remainder: acc.remainder - totalSrcValidator, + modified: acc.modified.with("valsToRemove", acc.modified.valsToRemove.setAdd(src))} + else { + // 3. If the remaining is less than the total amount of redelegated tokens of that source validator, the function iterates over all the bonds + // of that validator in epoch decreasing order until the remaining is unbonded. + val resultIteration = iterateBondsUpToAmount(redelegatedBonds.get(src), acc.remainder) + {remainder: 0, + modified: if (resultIteration.new.start == -1) acc.modified.with("valsToRemove", acc.modified.valsToRemove.setAdd(src)) + .with("valToModify", src) + .with("epochsToRemove", resultIteration.toRemove) + else acc.modified.with("valsToRemove", acc.modified.valsToRemove.setAdd(src)) + .with("valToModify", src) + .with("epochsToRemove", resultIteration.toRemove.setAdd(resultIteration.new.start)) + .with("epochToModify", resultIteration.new.start) + .with("newAmount", resultIteration.new.amount)} + } + }).modified + } + + // TODO: more tests here when we can iterate over srouce validators deterministically + run computeModifiedRedelegationTest = { + val redelegatedBonds = Map("alice" -> Map(2 -> 6, 4 -> 7), "bob" -> Map(1 -> 5, 4 -> 7)) + all { + assert(computeModifiedRedelegation(redelegatedBonds, 5, 25) == {epoch: -1, + valsToRemove: Set(), + valToModify: "", + epochsToRemove: Set(), + epochToModify: -1, + newAmount: -1}), + assert(computeModifiedRedelegation(redelegatedBonds, 5, 30) == {epoch: -1, + valsToRemove: Set(), + valToModify: "", + epochsToRemove: Set(), + epochToModify: -1, + newAmount: -1}) + } + } + + // The function computeNewRedelegatedUnbonds computes a set of redelegated unbonds from a set of redelegated bonds. + // - @param redelegatedBonds a map of redelegated bonds from epoch to RedelegatedBondsMap. + // - @param unbondedEpochs a set of epochs that indicate the set of epochs unbonded. + // - @param modified a ModifiedRedelegation record that represents a redelegated bond that it is only partially unbonded. + // - @returns a map with the redelegated unbonds. + // The function assumes that + // - modified.epoch is not in the unbondedEpochs set. + // - modified.valToModify is in modified.valsToRemove. + // - modified.epochToModify is in in modified.epochsToRemove. + pure def computeNewRedelegatedUnbonds(redelegatedBonds: Epoch -> RedelegatedBondsMap, unbondedEpochs: Set[Epoch], modified: ModifiedRedelegation): Epoch -> RedelegatedBondsMap = { + // Add the modified epoch if there exists and filter out those epochs that do not include redelegations + val updatedUnbondedEpochs = if (modified.epoch == -1) unbondedEpochs.filter(e => redelegatedBonds.has(e)) else unbondedEpochs.setAdd(modified.epoch).filter(e => redelegatedBonds.has(e)) + updatedUnbondedEpochs.mapBy(start => if (start != modified.epoch) redelegatedBonds.get(start) + else modified.valsToRemove.mapBy(src => if (src != modified.valToModify) redelegatedBonds.get(start).get(src) + else modified.epochsToRemove.mapBy(bondStart => if (bondStart != modified.epochToModify) redelegatedBonds.get(start).get(src).get(bondStart) + else redelegatedBonds.get(start).get(src).get(bondStart) - modified.newAmount))) + } + + run computeNewRedelegatedUnbondsTest = { + val redelegatedBonds = Map(5 -> Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 2)), + 7 -> Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 2))) + val emptyModified = {epoch: -1, valsToRemove: Set(), valToModify: "", epochsToRemove: Set(), epochToModify: -1, newAmount: -1} + val modifiedAll = {epoch: 7, valsToRemove: Set("alice", "bob"), valToModify: "", epochsToRemove: Set(), epochToModify: -1, newAmount: -1} + val modifiedValidator = {epoch: 7, valsToRemove: Set("alice"), valToModify: "", epochsToRemove: Set(), epochToModify: -1, newAmount: -1} + val modifiedValidatorPartial = {epoch: 7, valsToRemove: Set("alice", "bob"), valToModify: "bob", epochsToRemove: Set(1), epochToModify: -1, newAmount: -1} + val modifiedEpochPartial = {epoch: 7, valsToRemove: Set("alice", "bob"), valToModify: "bob", epochsToRemove: Set(1, 4), epochToModify: 4, newAmount: 1} + all { + assert(computeNewRedelegatedUnbonds(redelegatedBonds, Set(), emptyModified) == Map()), + assert(computeNewRedelegatedUnbonds(redelegatedBonds, Set(5), emptyModified) == Map(5 -> Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 2)))), + assert(computeNewRedelegatedUnbonds(redelegatedBonds, Set(5, 6), emptyModified) == Map(5 -> Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 2)))), + assert(computeNewRedelegatedUnbonds(redelegatedBonds, Set(5, 6), emptyModified) == Map(5 -> Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 2)))), + assert(computeNewRedelegatedUnbonds(redelegatedBonds, Set(5, 6), modifiedAll) == Map(5 -> Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 2)), + 7 -> Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 2)))), + assert(computeNewRedelegatedUnbonds(redelegatedBonds, Set(5, 6), modifiedValidator) == Map(5 -> Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 2)), + 7 -> Map("alice" -> Map(2 -> 1, 4 -> 1)))), + assert(computeNewRedelegatedUnbonds(redelegatedBonds, Set(5, 6), modifiedValidatorPartial) == Map(5 -> Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 2)), + 7 -> Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1)))), + assert(computeNewRedelegatedUnbonds(redelegatedBonds, Set(5, 6), modifiedEpochPartial) == Map(5 -> Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 2)), + 7 -> Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 1)))), + } + } + + // The function mergeBondsMap merges two maps of bonds from epoch to bond amount. + // - @param map1 a map from epoch to int. + // - @param map2 a map from epoch to int. + // - @returns a map resulting from merging map1 and map2. If both maps have the same entry, the + // resulting entry would be the sum of both. + pure def mergeBondsMap(map1: Epoch -> int, map2: Epoch -> int): Epoch -> int = { + map1.keys().union(map2.keys()).mapBy(e => if (map1.has(e) and map2.has(e)) map1.get(e) + map2.get(e) + else if (map1.has(e)) map1.get(e) else map2.get(e)) + + } + + run mergeBondsMapTest() = all { + assert(mergeBondsMap(Map(), Map()) == Map()), + assert(mergeBondsMap(Map(1 -> 2, 2 -> 3), Map()) == Map(1 -> 2, 2 -> 3)), + assert(mergeBondsMap(Map(), Map(1 -> 2, 2 -> 3)) == Map(1 -> 2, 2 -> 3)), + assert(mergeBondsMap(Map(1 -> 2, 2 -> 3), Map(3 -> 4, 4 -> 5)) == Map(1 -> 2, 2 -> 3, 3 -> 4, 4 -> 5)), + assert(mergeBondsMap(Map(1 -> 2, 2 -> 3), Map(2 -> 4, 4 -> 5)) == Map(1 -> 2, 2 -> 7, 4 -> 5)), + } + + // The function mergeRedelegatedBondsMap merges two RedelegatedBondsMap. + // - @param map1 a RedelegatedBondsMap. + // - @param map2 a RedelegatedBondsMap. + // - @returns a RedelegatedBondsMap resulting from merging map1 and map2. If a given entry is in both maps, the + // resulting map merges boths leveraging mergeBondsMap + pure def mergeRedelegatedBondsMap(map1: RedelegatedBondsMap, map2: RedelegatedBondsMap): RedelegatedBondsMap = { + map1.keys().union(map2.keys()).mapBy(src => if (map1.has(src) and map2.has(src)) mergeBondsMap( map1.get(src), map2.get(src)) + else if (map1.has(src)) map1.get(src) else map2.get(src)) + + } + + run mergeRedelegatedBondsMapTest = all { + assert(mergeRedelegatedBondsMap(Map(), Map()) == Map()), + assert(mergeRedelegatedBondsMap(Map("alice" -> Map(1 -> 2, 2 -> 3), "bob" -> Map(1 -> 2, 2 -> 3)), Map()) == Map("alice" -> Map(1 -> 2, 2 -> 3), "bob" -> Map(1 -> 2, 2 -> 3))), + assert(mergeRedelegatedBondsMap(Map(), Map("alice" -> Map(1 -> 2, 2 -> 3), "bob" -> Map(1 -> 2, 2 -> 3))) == Map("alice" -> Map(1 -> 2, 2 -> 3), "bob" -> Map(1 -> 2, 2 -> 3))), + assert(mergeRedelegatedBondsMap(Map("bob" -> Map(1 -> 2, 2 -> 3)), Map("alice" -> Map(1 -> 2, 2 -> 3))) == Map("alice" -> Map(1 -> 2, 2 -> 3), "bob" -> Map(1 -> 2, 2 -> 3))), + assert(mergeRedelegatedBondsMap(Map("bob" -> Map(1 -> 2, 2 -> 3), "tom" -> Map(4 -> 3, 5 -> 6)), Map("tom" -> Map(4 -> 3, 7 -> 6), "alice" -> Map(1 -> 2, 2 -> 3))) == + Map("alice" -> Map(1 -> 2, 2 -> 3), "bob" -> Map(1 -> 2, 2 -> 3), "tom" -> Map(4 -> 6, 5 -> 6, 7 -> 6))), + } + + // The function updateRedelegatedBonded updates a map of redelegated bonds according to a modified bond record. + // - @param redelegatedBonds a map of redelegated bonds. + // - @param modified a ModifiedRedelegation record. + // - @returns an updated map. + pure def updateRedelegatedBondsMap(redelegatedBonds: RedelegatedBondsMap, modified: ModifiedRedelegation): RedelegatedBondsMap = { + if (modified.valToModify == "") redelegatedBonds.mapRemoveSet(modified.valsToRemove) + else { + val updatedValsToRemoved = modified.valsToRemove.setRemove(modified.valToModify) + if (modified.epochToModify == -1) redelegatedBonds.mapRemoveSet(updatedValsToRemoved).set(modified.valToModify, redelegatedBonds.get(modified.valToModify).mapRemoveSet(modified.epochsToRemove)) + else { + val updatedEpochsToRemove = modified.epochsToRemove.setRemove(modified.epochToModify) + val updatedValBonds = redelegatedBonds.get(modified.valToModify).mapRemoveSet(updatedEpochsToRemove).set(modified.epochToModify, modified.newAmount) + redelegatedBonds.mapRemoveSet(updatedValsToRemoved).set(modified.valToModify, updatedValBonds) + } + } + } + + run updateRedelegatedBondsMapTest = { + val redelegatedBonds = Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 2)) + val emptyModified = {epoch: -1, valsToRemove: Set(), valToModify: "", epochsToRemove: Set(), epochToModify: -1, newAmount: -1} + val modifiedAll = {epoch: 7, valsToRemove: Set("alice", "bob"), valToModify: "", epochsToRemove: Set(), epochToModify: -1, newAmount: -1} + val modifiedValidator = {epoch: 7, valsToRemove: Set("alice"), valToModify: "", epochsToRemove: Set(), epochToModify: -1, newAmount: -1} + val modifiedValidatorPartial = {epoch: 7, valsToRemove: Set("alice", "bob"), valToModify: "bob", epochsToRemove: Set(1), epochToModify: -1, newAmount: -1} + val modifiedEpochPartial = {epoch: 7, valsToRemove: Set("alice", "bob"), valToModify: "bob", epochsToRemove: Set(1, 4), epochToModify: 4, newAmount: 1} + all { + assert(updateRedelegatedBondsMap(redelegatedBonds, emptyModified) == redelegatedBonds), + assert(updateRedelegatedBondsMap(redelegatedBonds, modifiedAll) == Map()), + assert(updateRedelegatedBondsMap(redelegatedBonds, modifiedValidator) == Map("bob" -> Map(1 -> 1, 4 -> 2))), + assert(updateRedelegatedBondsMap(redelegatedBonds, modifiedValidatorPartial) == Map("bob" -> Map(4 -> 2))), + assert(updateRedelegatedBondsMap(redelegatedBonds, modifiedEpochPartial) == Map("bob" -> Map(4 -> 1))), + } + } + + // The function updateRedelegatedUnbonded updates an entry of a delegator's redelegated unbonded map. + // - @param existing a map of redelegated unbonds from starting bonded epoch and ending bonded epoch to RedelegatedBondsMap. + // - @param redelegatedUnbonds a map from bond starting epoch to RedelegatedBondsMap. + // - @param end the epoch at which the redelegated bonds being added are withdrawable. + // - @returns an updated map that includes redelegatedUnbonds. + pure def updateRedelegatedUnbonded(existing: (Epoch, Epoch) -> RedelegatedBondsMap, redelegatedUnbonds: Epoch -> RedelegatedBondsMap, end: Epoch): (Epoch, Epoch) -> RedelegatedBondsMap = { + val newTuples = tuples(redelegatedUnbonds.keys(), Set(end)) + val existingTuples = existing.keys() + existingTuples.union(newTuples).mapBy(pair => val start = pair._1 + if (pair.in(existingTuples) and pair.in(newTuples)) mergeRedelegatedBondsMap(existing.get(pair), redelegatedUnbonds.get(start)) + else if (pair.in(existingTuples)) existing.get(pair) else redelegatedUnbonds.get(start)) + } + + run updateRedelegatedUnbondedTest = { + val existing = Map((2, 6) -> Map("alice" -> Map(1 -> 2, 3 -> 4), "bob" -> Map(1 -> 2, 3 -> 4)), + (2, 5) -> Map("alice" -> Map(1 -> 2, 3 -> 4)), + (3, 6) -> Map("bob" -> Map(1 -> 2, 3 -> 4))) + all { + assert(updateRedelegatedUnbonded(Map(),Map(), 6) == Map()), + assert(updateRedelegatedUnbonded(existing, Map(), 6) == existing ), + assert(updateRedelegatedUnbonded(Map(), Map(2 -> Map("alice" -> Map(1 -> 2, 3 -> 4), "bob" -> Map(1 -> 2, 3 -> 4))), 6) == + Map((2, 6) -> Map("alice" -> Map(1 -> 2, 3 -> 4), "bob" -> Map(1 -> 2, 3 -> 4)))), + assert(updateRedelegatedUnbonded(existing, Map(2 -> Map("alice" -> Map(1 -> 2, 3 -> 4), "bob" -> Map(1 -> 2, 3 -> 4))), 6) == + Map((2, 6) -> Map("alice" -> Map(1 -> 4, 3 -> 8), "bob" -> Map(1 -> 4, 3 -> 8)), + (2, 5) -> Map("alice" -> Map(1 -> 2, 3 -> 4)), + (3, 6) -> Map("bob" -> Map(1 -> 2, 3 -> 4)))), + } + } + + // The function updateTotalRedelegatedUnbonded updates an entry of a delegator's total redelegated unbonded map. + // - @param existing a map of total redelegated unbonds from starting bonded epoch and source validator to a map of bonds. + // - @param redelegatedUnbonds a set of redelegated unbonds. + // - @returns an updated map that includes redelegatedUnbonds. + pure def updateTotalRedelegatedUnbonded(existing: Epoch -> RedelegatedBondsMap, new: Epoch -> RedelegatedBondsMap): Epoch -> RedelegatedBondsMap = { + existing.keys().union(new.keys()).mapBy(e => if (existing.has(e) and new.has(e)) mergeRedelegatedBondsMap(existing.get(e), new.get(e)) + else if (existing.has(e)) existing.get(e) else new.get(e)) + } + + run updateTotalRedelegatedUnbondedTest = { + val existing = Map(2 -> Map("alice" -> Map(1 -> 2, 3 -> 4), "bob" -> Map(1 -> 2, 3 -> 4)), + 3 -> Map("alice" -> Map(1 -> 2, 3 -> 4))) + all { + assert(updateTotalRedelegatedUnbonded(Map(), Map()) == Map()), + assert(updateTotalRedelegatedUnbonded(existing, Map()) == existing), + assert(updateTotalRedelegatedUnbonded(Map(), Map(2 -> Map("alice" -> Map(1 -> 2, 3 -> 4), "bob" -> Map(1 -> 2, 3 -> 4)))) == + Map(2 -> Map("alice" -> Map(1 -> 2, 3 -> 4), "bob" -> Map(1 -> 2, 3 -> 4)))), + assert(updateTotalRedelegatedUnbonded(existing, Map(2 -> Map("alice" -> Map(1 -> 2, 3 -> 4), "bob" -> Map(1 -> 2, 3 -> 4)))) == + Map(2 -> Map("alice" -> Map(1 -> 4, 3 -> 8), "bob" -> Map(1 -> 4, 3 -> 8)), + 3 -> Map("alice" -> Map(1 -> 2, 3 -> 4)))) + } + } + + // The function mergeOutgoingRedelegations updates a validators's outgoing redelegations variable. + // - @param existing a map of outgoing redelegations. + // - @param new a new outgoing redelegation. + // - @param curEpoch the current epoch + // - @returns an updated map that includes new. + pure def mergeOutgoingRedelegations(existing: (Epoch, Epoch) -> int, new: Epoch -> int, curEpoch: Epoch): (Epoch, Epoch) -> int = { + val newTuples = tuples(new.keys(), Set(curEpoch)) + existing.keys().union(newTuples).mapBy(pair => val start = pair._1 + if (existing.has(pair) and pair.in(newTuples)) existing.get(pair) + new.get(start) + else if (existing.has(pair)) existing.get(pair) + else new.get(start)) + } + + run mergeOutgoingRedelegationsTest = { + val existing = Map((2, 6) -> 4, + (2, 5) -> 6, + (3, 6) -> 3) + all { + assert(mergeOutgoingRedelegations(Map(),Map(), 6) == Map()), + assert(mergeOutgoingRedelegations(existing, Map(), 6) == existing ), + assert(mergeOutgoingRedelegations(Map(), Map(2 -> 5), 6) == Map((2, 6) -> 5)), + assert(mergeOutgoingRedelegations(existing, Map(2 -> 5), 6) == Map((2, 6) -> 9, (2, 5) -> 6, (3, 6) -> 3)) + } + } + + // ************************************************************************** + // Slashing helper functions + // ************************************************************************* + + // The function computeSlashableAmount computes how much is left from a bond or unbond after applying a slash given that a set of slashes may have been + // previously applied. + // - @param slash the slash record to be applied. + // - @param initAmount the tokens to be slashed. + // - @param computeSlashes a map from misbehaving epoch to already computed slashable amount. + // - @returns an integer with the amount that remains after applying slash constraint to computeSlashes. + pure def computeSlashableAmount(slash: Slash, initAmount: int, computedSlashes: Epoch -> int): int = { + val updatedAmount = computedSlashes.keys().filter(x => x + slashProcessingDelay < slash.epoch) + .fold(initAmount, (acc, e) => max(0, acc - computedSlashes.get(e))) + updatedAmount*slash.rate + } + + run computeSlashableAmountTest = { + val initEpoch = 2 + all { + assert(computeSlashableAmount({epoch: initEpoch + UNBONDING_OFFSET + CUBIC_OFFSET, rate: 1}, 100, Map()) == 100), + assert(computeSlashableAmount({epoch: initEpoch + UNBONDING_OFFSET + CUBIC_OFFSET + 1, rate: 1}, 100, Map(initEpoch -> 50)) == 50), + assert(computeSlashableAmount({epoch: initEpoch + UNBONDING_OFFSET + CUBIC_OFFSET, rate: 1}, 100, Map(initEpoch -> 50)) == 100) + } + } + + // The function applyListSlashes computes how much remains from an amount of tokens after applying a list of slashes. + // - @param listSlashes a list of slashes ordered by misbehaving epoch. + // - @param amount the amount of slashable tokens. + // - @returns an integer with the amount that remains after applying the list of slashes. + pure def applyListSlashes(listSlashes: List[Slash], amount: int): int = { + listSlashes.foldl({finalAmount: amount, computedSlashes: Map()}, (acc, slash) => val slashAmount = computeSlashableAmount(slash, amount, acc.computedSlashes) + {finalAmount: max(0, acc.finalAmount - slashAmount), + computedSlashes: acc.computedSlashes.mapSafeSet(slash.epoch, slashAmount)}).finalAmount + } + + run applyListSlashesTest = { + val initEpoch = 2 + val list1 = [{epoch: initEpoch, rate: 1}] + val list2 = [{epoch: initEpoch, rate: 1}, {epoch: initEpoch+UNBONDING_OFFSET+CUBIC_OFFSET+1, rate: 1} ] + val list3 = [{epoch: initEpoch, rate: 1}, + {epoch: initEpoch, rate: 1}] + val list4 = [{epoch: initEpoch, rate: 1}, + {epoch: initEpoch, rate: 1}, + {epoch: initEpoch+UNBONDING_OFFSET+CUBIC_OFFSET+1, rate: 1} ] + all { + assert(applyListSlashes([], 100) == 100), + assert(applyListSlashes(list1, 100) == 0), + assert(applyListSlashes(list2, 100) == 0), + assert(applyListSlashes(list3, 100) == 0), + assert(applyListSlashes(list4, 100) == 0) + } + } + + // The function nextSlash compares the slash at the head of two lists and returns the one with smaller + // misbheaving epoch. It assumes that at least one list has an element. + // - @param list1 a list of slashes ordered by misbehaving epoch. + // - @param list2 a second list of slashes ordered by misbehaving epoch. + // - @returns the slash at the head of any of the lists with smaller misbheaving epoch. + + pure def nextSlash(list1: List[Slash], list2: List[Slash]): (Slash, List[Slash], List[Slash]) = { + if (list1 == List()) (head(list2), list1, tail(list2)) + else if (list2 == List()) (head(list1), tail(list1), list2) + else if (head(list1).epoch <= head(list2).epoch) (head(list1), tail(list1), list2) + else (head(list2), list1, tail(list2)) + } + + run nextSlashTest = { + val slash = {epoch: 0, rate: 1} + val list1 = [slash.with("epoch", 1), + slash.with("epoch", 6), + slash.with("epoch", 9)] + val list2 = [slash.with("epoch", 2), + slash.with("epoch", 6), + slash.with("epoch", 8)] + all { + assert(nextSlash(List(), List(slash.with("epoch", 1))) == (slash.with("epoch", 1), List(), List())), + assert(nextSlash(List(slash.with("epoch", 1)), List()) == (slash.with("epoch", 1), List(), List())) + } + } + + // The function mergeListSlashes merges two lists of slashes ordered by misbehaving epoch. + // - @param list1 a list of slashes ordered by misbehaving epoch. + // - @param list2 a second list of slashes ordered by misbehaving epoch. + // - @returns a third list of slashes including all elements in both imput lists ordered by misbehaving epoch. + pure def mergeListSlashes(list1: List[Slash], list2: List[Slash]): List[Slash] = { + val sumLength = length(list1) + length(list2) + if (sumLength == 0) List() + else 1.to(sumLength).fold(([], list1, list2), (acc, _) => val result = nextSlash(acc._2, acc._3) + (acc._1.append(result._1), result._2, result._3))._1 + } + + run mergeListSlashesTest = all { + val slash = {epoch: 0, rate: 1} + val list1 = [slash.with("epoch", 1), + slash.with("epoch", 6), + slash.with("epoch", 9)] + val list2 = [slash.with("epoch", 2), + slash.with("epoch", 6), + slash.with("epoch", 8)] + val resultMerge = [slash.with("epoch", 1), + slash.with("epoch", 2), + slash.with("epoch", 6), + slash.with("epoch", 6), + slash.with("epoch", 8), + slash.with("epoch", 9)] + all { + assert(mergeListSlashes(list1, list2) == resultMerge), + assert(mergeListSlashes(list2, list1) == resultMerge), + assert(mergeListSlashes(List(), List()) == List()), + assert(mergeListSlashes(list1, List()) == list1), + assert(mergeListSlashes(List(), list2) == list2) + } + } + + // The function foldAndSlashRedelegatedBondsMap iterates over a RedelegatedBondsMap and computes the both the sum of all rdelegated tokens and + // how much is left after applying all relevant slashes. + // - @param bonds a RedelegatedBondsMap. + // - @param start the epoch at which the redelegated bonds were effectively bonded. + // - @param listSlashes a list of slashes to be applied to the redelegated bonds. + // - @param slashes a map from validator address to list of slashes. + // - @returns the total amount of redelegated tokens and the total amount after slashing. + pure def foldAndSlashRedelegatedBondsMap(bonds: RedelegatedBondsMap, start: Epoch, listSlashes: List[Slash], slashes: Address -> List[Slash]): {totalRedelegated: int, totalAfterSlashing: int} = { + bonds.keys().fold({totalRedelegated: 0, totalAfterSlashing: 0}, + (accSrc, src) => bonds.get(src).keys().fold(accSrc, + (accEpoch, redBondStart) => val selectList = slashes.get(src).select(slash => inRedelegationSlashingWindow(slash.epoch, startRedelegationFromEnd(start), start) and + redBondStart <= slash.epoch) + val mergedList = mergeListSlashes(listSlashes, selectList) + {totalRedelegated: accEpoch.totalRedelegated + bonds.get(src).get(redBondStart), + totalAfterSlashing: accEpoch.totalAfterSlashing + applyListSlashes(mergedList, bonds.get(src).get(redBondStart))})) + } + + run foldAndSlashRedelegatedBondsMapTest = { + val allValidators = Set("alice", "bob") + val start = 7 + val redelegatedBonds = Map("alice" -> Map(2 -> 1, 4 -> 1), "bob" -> Map(1 -> 1, 4 -> 2)) + all { + assert(foldAndSlashRedelegatedBondsMap(redelegatedBonds, start, List(), allValidators.mapBy(x => List())) == {totalRedelegated: 5, totalAfterSlashing: 5}), + assert(foldAndSlashRedelegatedBondsMap(redelegatedBonds, start, List({epoch: 0, rate: 1}), allValidators.mapBy(x => List())) == {totalRedelegated: 5, totalAfterSlashing: 0}), + assert(foldAndSlashRedelegatedBondsMap(redelegatedBonds, start, List(), allValidators.mapBy(x => if (x=="alice") List({epoch: 6, rate: 1}) else List())) == {totalRedelegated: 5, totalAfterSlashing: 3}), + } + } + + // The function computeAmountAfterSlashingUnbond computes from a set of unbonds (both redelegated and not) how much is left after applying all relevant + // slashes. + // - @param unbonds a set of unbonds: a map from bond starting epoch and unbond ending epoch to amount of tokens. + // - @param redelegatedUnbonds a set of redelegated unbonds: a map from bonds tarting epoch to RedelegatedBondsMap. + // - @param validator the address of the validator from which the the bonds have been unbonded. + // - @param slashes a map from validator address to list of slashes. + // - @returns the total amount after slashing and a map from bond starting epoch to amount after slashing. + pure def computeAmountAfterSlashingUnbond(unbonds: (Epoch, Epoch) -> int, redelegatedUnbonds: Epoch -> RedelegatedBondsMap, validator: Address, slashes: Address -> List[Slash]): {sum: int, epochMap: Epoch -> int} = { + val initMap = unbonds.keys().map(pair => pair._1).mapBy(e => 0) + unbonds.keys().fold({sum: 0, epochMap: initMap}, (acc, unbondKey) => val start = unbondKey._1 + val listSlashes = slashes.get(validator).select(slash => start <= slash.epoch) + val resultFold = if (redelegatedUnbonds.has(start)) foldAndSlashRedelegatedBondsMap(redelegatedUnbonds.get(start), start, listSlashes, slashes) + else {totalRedelegated: 0, totalAfterSlashing: 0} + val totalNoRedelegated = unbonds.get(unbondKey) - resultFold.totalRedelegated + val afterNoRedelegated = applyListSlashes(listSlashes, totalNoRedelegated) + val amountAfterSlashing = afterNoRedelegated + resultFold.totalAfterSlashing + {sum: acc.sum + amountAfterSlashing, + epochMap: acc.epochMap.set(start, amountAfterSlashing)}) + } + + run computeAmountAfterSlashingUnbondTest = { + val allValidators = Set("alice", "bob") + val unbonds = Map((2, 6) -> 5, (4, 6) -> 6) + val redelegatedBonds = Map(2 -> Map("alice" -> Map(1 -> 1))) + all { + assert(computeAmountAfterSlashingUnbond(unbonds, redelegatedBonds, "bob", allValidators.mapBy(x => List())) == {sum: 11, epochMap: Map(2 -> 5, 4 -> 6)}), + assert(computeAmountAfterSlashingUnbond(unbonds, redelegatedBonds, "bob", allValidators.mapBy(x => if (x=="bob") List({epoch: 5, rate: 1}) else List())) == {sum: 0, epochMap: Map(2 -> 0, 4 -> 0)}), + assert(computeAmountAfterSlashingUnbond(unbonds, redelegatedBonds, "bob", allValidators.mapBy(x => if (x=="alice") List({epoch: 0, rate: 1}) else List())) == {sum: 11, epochMap: Map(2 -> 5, 4 -> 6)}), + assert(computeAmountAfterSlashingUnbond(unbonds, redelegatedBonds, "bob", allValidators.mapBy(x => if (x=="alice") List({epoch: 1, rate: 1}) else List())) == {sum: 10, epochMap: Map(2 -> 4, 4 -> 6)}) + } + } + + // The function computeAmountAfterSlashingWithdraw computes from a set of unbonds (both redelegated and not) how much is left after applying all relevant + // slashes. + // - @param unbonds a set of unbonds: a map from bond starting epoch and unbond ending epoch to amount of tokens. + // - @param redelegatedUnbonds a set of redelegated unbonds: a map from bonds tarting epoch to RedelegatedBondsMap. + // - @param validator the address of the validator from which the the bonds have been unbonded. + // - @param slashes a map from validator address to list of slashes. + // - @returns the total amount after slashing and a map from bond starting epoch to amount after slashing. + pure def computeAmountAfterSlashingWithdraw(unbonds: (Epoch, Epoch) -> int, redelegatedUnbonds: (Epoch, Epoch) -> RedelegatedBondsMap, validator: Address, slashes: Address -> List[Slash]): {sum: int, epochMap: Epoch -> int} = { + val initMap = unbonds.keys().map(pair => pair._1).mapBy(e => 0) + unbonds.keys().fold({sum: 0, epochMap: initMap}, (acc, unbondKey) => val start = unbondKey._1 + val end = unbondKey._2 + val listSlashes = slashes.get(validator).select(slash => start <= slash.epoch and + end - UNBONDING_OFFSET - CUBIC_OFFSET > slash.epoch) + val resultFold = if (redelegatedUnbonds.has(unbondKey)) foldAndSlashRedelegatedBondsMap(redelegatedUnbonds.get(unbondKey), start, listSlashes, slashes) + else {totalRedelegated: 0, totalAfterSlashing: 0} + val totalNoRedelegated = unbonds.get(unbondKey) - resultFold.totalRedelegated + val afterNoRedelegated = applyListSlashes(listSlashes, totalNoRedelegated) + val amountAfterSlashing = afterNoRedelegated + resultFold.totalAfterSlashing + {sum: acc.sum + amountAfterSlashing, + epochMap: acc.epochMap.set(start, amountAfterSlashing)}) + } + + run computeAmountAfterSlashingWithdrawTest = { + val allValidators = Set("alice", "bob") + val unbonds = Map((2, 20) -> 5, (4, 20) -> 6) + val redelegatedBonds = Map((2, 20) -> Map("alice" -> Map(1 -> 1))) + all { + assert(computeAmountAfterSlashingWithdraw(unbonds, redelegatedBonds, "bob", allValidators.mapBy(x => List())) == {sum: 11, epochMap: Map(2 -> 5, 4 -> 6)}), + assert(computeAmountAfterSlashingWithdraw(unbonds, redelegatedBonds, "bob", allValidators.mapBy(x => if (x=="bob") List({epoch: 5, rate: 1}) else List())) == {sum: 0, epochMap: Map(2 -> 0, 4 -> 0)}), + assert(computeAmountAfterSlashingWithdraw(unbonds, redelegatedBonds, "bob", allValidators.mapBy(x => if (x=="alice") List({epoch: 0, rate: 1}) else List())) == {sum: 11, epochMap: Map(2 -> 5, 4 -> 6)}), + assert(computeAmountAfterSlashingWithdraw(unbonds, redelegatedBonds, "bob", allValidators.mapBy(x => if (x=="alice") List({epoch: 1, rate: 1}) else List())) == {sum: 10, epochMap: Map(2 -> 4, 4 -> 6)}) + } + } + + // The function computeTotalUnbonded computes the total amount of tokens unbonded from a validator that were contributing to the validator's stake when this misbehaved at + // a previous epoch, after applying a set of relevant slashes. + // - @param validator the misbehaving validator's address. + // - @param infractionEpoch the epoch at which the validator misbehaved. + // - @param slashes a map from validator address to a list of already processed slashes. + // - @param totalUnbonded a map of bonds from epoch to amount of tokens from which the final amount is computed. + // - @param totalRedelegatedUnbonded a map of redelegated bonds from epoch to RedelegatedBondsMap. + // - @returns an integer with the amount of tokens that were contributing to the validator at the misbehaving epoch that have been unbonded. + pure def computeTotalUnbonded(validator: Address, infractionEpoch: Epoch, slashes: Address -> List[Slash], totalUnbonded: Epoch -> int, totalRedelegatedUnbonded: Epoch -> RedelegatedBondsMap): int = { + val epochs = totalUnbonded.keys().filter(e => e <= infractionEpoch and totalUnbonded.get(e) > 0) + epochs.fold(0, (sum, e) => val listSlashes = slashes.get(validator).select(s => e <= s.epoch and s.epoch + slashProcessingDelay < infractionEpoch) + val filteredSlashMap = slashes.keys().mapBy(v => slashes.get(v).select(s => s.epoch + slashProcessingDelay < infractionEpoch)) + val resultFold = if (totalRedelegatedUnbonded.has(e)) foldAndSlashRedelegatedBondsMap(totalRedelegatedUnbonded.get(e), e, listSlashes, filteredSlashMap) + else {totalRedelegated: 0, totalAfterSlashing: 0} + val totalNoRedelegated = totalUnbonded.get(e) - resultFold.totalRedelegated + val afterNoRedelegated = applyListSlashes(listSlashes, totalNoRedelegated) + val amountAfterSlashing = afterNoRedelegated + resultFold.totalAfterSlashing + sum + amountAfterSlashing) + } + + run computeTotalUnbondedTest = { + val allValidators = Set("alice", "bob") + val totalUnbonded = Map(2 -> 5, 8 -> 20) + val totalRedelegateUnbonded = Map(8 -> Map("bob" -> Map(4 -> 10))) + all { + assert(computeTotalUnbonded("alice", 10, allValidators.mapBy(v => List()), totalUnbonded, totalRedelegateUnbonded) == 25), + assert(computeTotalUnbonded("alice", 7, allValidators.mapBy(v => List()), totalUnbonded, totalRedelegateUnbonded) == 5), + assert(computeTotalUnbonded("alice", 10, allValidators.mapBy(v => if (v == "alice") List({epoch: 2, rate: 1}) else List()), totalUnbonded, totalRedelegateUnbonded) == 20), + assert(computeTotalUnbonded("alice", 10, allValidators.mapBy(v => if (v == "alice") List({epoch: 2, rate: 1}) else List({epoch: 4, rate: 1})), totalUnbonded, totalRedelegateUnbonded) == 10), + } + } + // The function foldBondsMap computes the total amount of tokens in a map of bonds. + // - @param bonds a map of bonds from epoch to amount of tokens. + // - @returns the sum of all bonds. + pure def foldBondsMap(bonds: Epoch -> int): int = { + bonds.keys().fold(0, (sum, e) => sum + bonds.get(e)) + } + + run foldBondsMapTest = all { + assert(foldBondsMap(Map()) == 0), + assert(foldBondsMap(Map(5 -> 6)) == 6), + assert(foldBondsMap(Map(5 -> 6, 7 -> 8)) == 14), + } + + // The function foldRedelegatedBondsMap computes the total amount of redelegated tokens in a RedelegatedBondsMap. + // - @param redelegatedBonds a RedelegatedBondsMap map. + // - @returns the sum of all redelegated tokens. + pure def foldRedelegatedBondsMap(redelegatedBonds: RedelegatedBondsMap): int = { + redelegatedBonds.keys().fold(0, (sum, src) => sum + redelegatedBonds.get(src).foldBondsMap()) + } + + run foldRedelegatedBondsMapTest = all { + assert(foldRedelegatedBondsMap(Map()) == 0), + assert(foldRedelegatedBondsMap(Map("alice" -> Map(5 -> 6))) == 6), + assert(foldRedelegatedBondsMap(Map("alice" -> Map(5 -> 6, 6 -> 8))) == 14), + assert(foldRedelegatedBondsMap(Map("alice" -> Map(5 -> 6, 6 -> 8), "bob" -> Map(3 -> 7))) == 21), + } + + // The function computeRecentTotalUnbonded the total amount of non-redelegated tokens unbonded by a validator that were bonded after this misbehaved at a given epoch. + // - @param infractionEpoch the misbehaving epoch. + // - @param totalUnbonded the set of unbonded tokens in a map from bond starting epoch to amount of tokens. + // - @param totalRedelegatedUnbonded a map from epoch to RedelegatedBondsMap. + // - @returns an integer with the amount of tokens unbonded. + pure def computeRecentTotalUnbonded(infractionEpoch: Epoch, totalUnbonded: Epoch -> int, totalRedelegatedUnbonded: Epoch -> RedelegatedBondsMap): int = { + val epochs = totalUnbonded.keys().filter(e => e > infractionEpoch and totalUnbonded.get(e) > 0) + epochs.fold(0, (sum, e) => val nonRedelegatedAmount = if (totalRedelegatedUnbonded.has(e)) totalUnbonded.get(e) - totalRedelegatedUnbonded.get(e).foldRedelegatedBondsMap() + else totalUnbonded.get(e) + sum + nonRedelegatedAmount) + } + + run computeRecentTotalUnbondedTest = all { + assert(computeRecentTotalUnbonded(5, Map(), Map()) == 0), + assert(computeRecentTotalUnbonded(5, Map(6 -> 10, 7 -> 20), Map()) == 30), + assert(computeRecentTotalUnbonded(5, Map(4 -> 10, 7 -> 20), Map()) == 20), + assert(computeRecentTotalUnbonded(8, Map(4 -> 10, 7 -> 20), Map()) == 0), + assert(computeRecentTotalUnbonded(5, Map(6 -> 10, 7 -> 20), Map(6 -> Map("alice" -> Map(5 -> 6, 6 -> 4)))) == 20), + } + + // The function minSlashRate returns a slash rate depending on the type of infraction. + // - @param infraction a string identifying the type of infraction. + // - @returns a Dec representing the slash rate + pure def minSlashRate(infraction: str): Dec = { + if (infraction == "duplicate_vote") DUPLICATE_RATE else LIGHT_RATE + } + + // The function computeFinalRate computes a slash rate based on a set of slashes + // - @param setSlashes a set of slashes + // - @returns an integer representing the slash rate + pure def computeFinalRate(setInfractions: Set[Infraction]): int = { + 1 + } + + // The function hasRedelegation checks whether a map of redelegations contains a given redelegation. + // - @param mapRedelegations a map of redelegations from epoch to RedelegatedBondsMap. + // - @param redBondStart the epoch at which the redelegated bonds started contributing the destination validator. We also say the end of the redelegation. + // - @param validator the address of the source validator. + // - @param bondStart the epoch at which the tokens started contributing at the source validator. + // - @returns true if the mapRedelegations contains the redelegation defined by redBondStart, validator and bondStart; it returns false otherwise. + pure def hasRedelegation(mapRedelegations: Epoch -> RedelegatedBondsMap, redBondStart: Epoch, validator: Address, bondStart: Epoch): bool = { + if (mapRedelegations.has(redBondStart)) + if (mapRedelegations.get(redBondStart).has(validator)) + if (mapRedelegations.get(redBondStart).get(validator).has(bondStart)) true + else false + else false + else false + } + + + run hasRedelegationTest = { + val mapRedelegations = Map(4 -> Map("alice" -> Map(2 -> 6, 3 -> 7)), 6 -> Map("bob" -> Map(1 -> 8))) + all { + assert(hasRedelegation(Map(), 4, "alice", 3) == false), + assert(hasRedelegation(mapRedelegations, 4, "alice", 3) == true), + assert(hasRedelegation(mapRedelegations, 4, "alice", 4) == false), + assert(hasRedelegation(mapRedelegations, 4, "bob", 3) == false), + assert(hasRedelegation(mapRedelegations, 6, "alice", 3) == false), + } + } + + // The function computeRemainderRedelegation takes a redelegation record and computes how many tokens are left from the redelegation at the destination validator considering + // that the source validator may have misbehaved while the redelegated tokens were contributing to its stake and that some may have unbonded from the destination + // validator. The function computes the how muchis left at the destination validator at epochs from curEpoch + 1 to curEpoch + PIPELINE_LENGTH. + // - @param redelegation a Redelegation record. + // - @param curEpoch the the current epoch. + // - @param slashes a list of slashes of the source validator. + // - @param totalRedelegatedUnbonded a map from epoch to unbonded redelegated tokens. + // - @param balanceMap a map from epoch to stake. It accumulates how much stake is left at a given epoch from all already processed redelegation records. + // - @returns an updated balanceMap resulting from processing redelegation. + pure def computeRemainderRedelegation(redelegation: Redelegation, + curEpoch: Epoch, + slashes: List[Slash], + totalRedelegatedUnbonded: Epoch -> Epoch -> RedelegatedBondsMap, + balanceMap: Epoch -> int): Epoch -> int = { + // We should iterate in epoch increasing order. TODO: transform this into a list and use foldl. + (redelegation.redBondStart).to(curEpoch+PIPELINE_OFFSET).fold((0, balanceMap), (acc, e) => val updatedTotalUnbonded = if (not(totalRedelegatedUnbonded.get(e).hasRedelegation(redelegation.redBondStart, redelegation.srcValidator, redelegation.bondStart))) acc._1 + else acc._1 + totalRedelegatedUnbonded.get(e).get(redelegation.redBondStart).get(redelegation.srcValidator).get(redelegation.bondStart) + if (e <= curEpoch) (updatedTotalUnbonded, acc._2) + else { + val stakeLeft = val listSlashes = slashes.select(s => inRedelegationSlashingWindow(s.epoch, startRedelegationFromEnd(redelegation.redBondStart), redelegation.redBondStart) and + redelegation.bondStart <= s.epoch) + applyListSlashes(listSlashes, redelegation.amount - updatedTotalUnbonded) + (updatedTotalUnbonded, acc._2.set(e, acc._2.get(e) + stakeLeft))})._2 + } + + run computeRemainderRedelegationTest = { + val emptyRedelegatedTotalUnbonded = Map(5 -> Map(), 6 -> Map(), 7 -> Map(), 8 -> Map(), 9 -> Map(), 10 -> Map()) + val redelegation = {redBondStart: 8, srcValidator: "alice", bondStart: 5, amount: 10} + all { + assert(computeRemainderRedelegation(redelegation, 8, [], emptyRedelegatedTotalUnbonded, Map(9 -> 0, 10 -> 0)) == Map(9 -> 10, 10 -> 10)), + assert(computeRemainderRedelegation(redelegation, 8, [{epoch: 4, rate: 1}], emptyRedelegatedTotalUnbonded, Map(9 -> 0, 10 -> 0)) == Map(9 -> 10, 10 -> 10)), + assert(computeRemainderRedelegation(redelegation, 8, [{epoch: 4, rate: 1}], emptyRedelegatedTotalUnbonded, Map(9 -> 5, 10 -> 4)) == Map(9 -> 15, 10 -> 14)), + assert(computeRemainderRedelegation(redelegation, 8, [{epoch: 5, rate: 1}], emptyRedelegatedTotalUnbonded, Map(9 -> 0, 10 -> 0)) == Map(9 -> 0, 10 -> 0)), + assert(computeRemainderRedelegation(redelegation, 8, [{epoch: 5, rate: 1}, {epoch: 6, rate: 1}], emptyRedelegatedTotalUnbonded, Map(9 -> 0, 10 -> 0)) == Map(9 -> 0, 10 -> 0)), + assert(computeRemainderRedelegation(redelegation, 8, [], emptyRedelegatedTotalUnbonded.set(8, Map(8 -> Map("bob" -> Map(5 -> 8)))), Map(9 -> 0, 10 -> 0)) == Map(9 -> 10, 10 -> 10)), + assert(computeRemainderRedelegation(redelegation, 8, [], emptyRedelegatedTotalUnbonded.set(8, Map(8 -> Map("alice" -> Map(5 -> 8)))), Map(9 -> 0, 10 -> 0)) == Map(9 -> 2, 10 -> 2)), + assert(computeRemainderRedelegation(redelegation, 8, [], emptyRedelegatedTotalUnbonded.set(10, Map(8 -> Map("alice" -> Map(5 -> 8)))), Map(9 -> 0, 10 -> 0)) == Map(9 -> 10, 10 -> 2)), + } + } + + // The function computeBalanceRedelegatedBonds takes a set of redelegations in a RedelegatedBondsMap and computes how many tokens are left at the destination validator considering + // that source validators may have misbehaved while redelegated tokens were contributing to its stake and that some may have unbonded from the destination + // validator. The function computes how much is left at the destination validator at epochs from curEpoch + 1 to curEpoch + PIPELINE_LENGTH. + // - @param totalRedelegatedBonded a RedelegatedBondsMap map. + // - @param redBondStart the epoch at which the redelegations in totalRedelegatedBonded started contributing to the destination validator's stake. + // - @param curEpoch the the current epoch. + // - @param slashes a map from validator address to list of slashes. + // - @param totalRedelegatedUnbonded a map from epoch to unbonded redelegated tokens. + // - @param balanceMap a map from epoch to stake. It accumulates how much stake is left at a given epoch from all already processed redelegation records. + // - @returns an updated balanceMap resulting from processing totalRedelegatedBonded. + pure def computeBalanceRedelegatedBonds(totalRedelegatedBonded: RedelegatedBondsMap, + redBondStart: Epoch, + curEpoch: Epoch, + slashes: Address -> List[Slash], + totalRedelegatedUnbonded: Epoch -> Epoch -> RedelegatedBondsMap, + balanceMap: Epoch -> int): Epoch -> int = { + totalRedelegatedBonded.keys().fold(balanceMap, (accSrcMap, src) => totalRedelegatedBonded.get(src).keys().fold(accSrcMap, (accEpochMap, e) => val redelegation = {redBondStart: redBondStart, srcValidator: src, bondStart: e, amount: totalRedelegatedBonded.get(src).get(e)} + computeRemainderRedelegation(redelegation, curEpoch, slashes.get(src), totalRedelegatedUnbonded, accEpochMap))) + } + + run computeBalanceRedelegatedBondsTest = { + val redelegations = Map("alice" -> Map(5 -> 10, 6 -> 5), "bob" -> Map(5 -> 9, 6 -> 5)) + val emptyTotalRedelegatedUnbonded = Map(5 -> Map(), 6 -> Map(), 7 -> Map(), 8 -> Map(), 9 -> Map(), 10 -> Map()) + all { + assert(computeBalanceRedelegatedBonds(redelegations, 7, 8, Map("alice" -> [], "bob" -> []), emptyTotalRedelegatedUnbonded, Map(9 -> 0, 10 -> 0)) == Map(9 -> 29, 10 -> 29)), + assert(computeBalanceRedelegatedBonds(redelegations, 7, 8, Map("alice" -> [], "bob" -> []), emptyTotalRedelegatedUnbonded, Map(9 -> 2, 10 -> 1)) == Map(9 -> 31, 10 -> 30)), + assert(computeBalanceRedelegatedBonds(redelegations, 7, 8, Map("alice" -> [{epoch: 4, rate: 1}], "bob" -> []), emptyTotalRedelegatedUnbonded, Map(9 -> 0, 10 -> 0)) == Map(9 -> 29, 10 -> 29)), + assert(computeBalanceRedelegatedBonds(redelegations, 7, 8, Map("alice" -> [{epoch: 5, rate: 1}], "bob" -> []), emptyTotalRedelegatedUnbonded, Map(9 -> 0, 10 -> 0)) == Map(9 -> 19, 10 -> 19)), + assert(computeBalanceRedelegatedBonds(redelegations, 7, 8, Map("alice" -> [{epoch: 5, rate: 1}], "bob" -> []), emptyTotalRedelegatedUnbonded.set(10, Map(7 -> Map("bob" -> Map(5 -> 9, 6 -> 3)))), Map(9 -> 0, 10 -> 0)) == Map(9 -> 19, 10 -> 7)), + } + } + + // The slashValidator function computes for a given validator and a slash how much should be slashed at all epochs between the currentå + // epoch (curEpoch) + 1 and the current epoch + 1 + PIPELINE_OFFSET, accounting for any tokens already unbonded. + // - @param validator the misbehaving validator. + // - @param stakes a map from epoch to validator stake. This is used to compute slashableStake. + // - @param curEpoch the current epoch. + // - @param infractionStake the validator's stake at the misbehaving epoch. + // - @param slashes list of slashes already processed slashes of the misbehaving validator. + // - @param totalUnbonded a map from epoch to unbonded tokens. + // - @param totalRedelegatedUnbonded a map from epoch to unbonded redelegated tokens. + // - @param totalBonded a map from epoch to amount of bonded tokens. + // - @param finalRate the rate of the slash being processed. + // - @param slashedAmountsMap a map from epoch to already processed slash amounts. + // - @returns a map that adds any newly processed slash amount to slashedAmountsMap. + pure def slashValidator(validator: Address, + stakes: Epoch -> int, + curEpoch: Epoch, + infractionStake: int, + slashes: Address -> List[Slash], + totalUnbonded: Epoch -> Epoch -> int, + totalRedelegatedUnbonded: Epoch -> Epoch -> RedelegatedBondsMap, + totalBonded: Epoch -> int, + totalRedelegatedBonded: Epoch -> RedelegatedBondsMap, + finalRate: int, + slashedAmountsMap: Epoch -> int): Epoch -> int = { + val infractionEpoch = curEpoch - slashProcessingDelay + val initTotalUnbonded = (infractionEpoch+1).to(curEpoch).fold(0, (sum, e) => sum + computeTotalUnbonded(validator, infractionEpoch, slashes, totalUnbonded.get(e), totalRedelegatedUnbonded.get(e))) + val initBalanceBonds = (infractionEpoch+1).to(curEpoch).fold(0, (sum, e) => sum + (totalBonded.get(e) - computeRecentTotalUnbonded(infractionEpoch, totalUnbonded.get(e), totalRedelegatedUnbonded.get(e)))) + val zeroedBalanceRedelegatedBonds = (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).mapBy(e => 0) + val initBalanceRedelegatedBonds = (infractionEpoch+1).to(curEpoch).fold(zeroedBalanceRedelegatedBonds, (acc, e) => computeBalanceRedelegatedBonds(totalRedelegatedBonded.get(e), e, curEpoch, slashes, totalRedelegatedUnbonded, acc)) + // We should iterate in epoch increasing order. TODO: transform this into a list and use foldl. + val result = (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).fold((initTotalUnbonded, + initBalanceBonds, + initBalanceRedelegatedBonds, + slashedAmountsMap), (acc, e) => val updatedTotalUnbonded = acc._1 + computeTotalUnbonded(validator, infractionEpoch, slashes, totalUnbonded.get(e), totalRedelegatedUnbonded.get(e)) + val updatedBalanceBonds = acc._2 + (totalBonded.get(e) - computeRecentTotalUnbonded(infractionEpoch, totalUnbonded.get(e), totalRedelegatedUnbonded.get(e))) + val updatedBalanceRedelegatedBonds = computeBalanceRedelegatedBonds(totalRedelegatedBonded.get(e), e, curEpoch, slashes, totalRedelegatedUnbonded, acc._3) + val slashedAmount = (infractionStake - updatedTotalUnbonded) * finalRate + val currentStake = stakes.get(e) - acc._4.get(e) + val slashableStake = (currentStake - updatedBalanceBonds - updatedBalanceRedelegatedBonds.get(e)) + (updatedTotalUnbonded, updatedBalanceBonds, updatedBalanceRedelegatedBonds, acc._4.set(e, acc._4.get(e) + min(slashedAmount, slashableStake)))) + result._4 + } + + run slashValidatorTest = { + val infractionStake = 23 + val curEpoch = 10 + val rate = 1 + val emptyTotalUnbonded = (curEpoch-CUBIC_OFFSET-UNBONDING_OFFSET).to(curEpoch+PIPELINE_OFFSET).mapBy(e => Map()) + val emptyTotalRedelegatedUnbonded = emptyTotalUnbonded + val emptytotalRedelegatedBonded = emptyTotalUnbonded + val emptyTotalBonded = (curEpoch-CUBIC_OFFSET-UNBONDING_OFFSET).to(curEpoch+PIPELINE_OFFSET).mapBy(e => 0) + val initStakesMap = (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).mapBy(e => infractionStake) + val emptySlashAmountsMap = (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).mapBy(e => 0) + val emptySlashes = Map("alice" -> [], "bob" -> []) + all { + // clean slashing: no new bonds or slashes + assert(slashValidator("bob", + initStakesMap, + curEpoch, + infractionStake, + emptySlashes, + emptyTotalUnbonded, + emptyTotalRedelegatedUnbonded, + emptyTotalBonded, + emptytotalRedelegatedBonded, + rate, + emptySlashAmountsMap) == initStakesMap), + // there is a bond happening at curEpoch + assert(slashValidator("bob", + (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).mapBy(e => infractionStake + 6), + curEpoch, + infractionStake, + emptySlashes, + emptyTotalUnbonded, + emptyTotalRedelegatedUnbonded, + emptyTotalBonded.set(curEpoch, 6), + emptytotalRedelegatedBonded, + rate, + emptySlashAmountsMap) == initStakesMap), + // there is a bond happening at curEpoch which is unbonded at curEpoch + 1 + assert(slashValidator("bob", + initStakesMap, + curEpoch, + infractionStake, + emptySlashes, + emptyTotalUnbonded.set(curEpoch+1, Map(curEpoch -> 6)), + emptyTotalRedelegatedUnbonded, + emptyTotalBonded.set(curEpoch, 6), + emptytotalRedelegatedBonded, + rate, + emptySlashAmountsMap) == initStakesMap), + // there is a bond happening at curEpoch which is partially unbonded at curEpoch + 1 + assert(slashValidator("bob", + (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).mapBy(e => infractionStake + 3), + curEpoch, + infractionStake, + emptySlashes, + emptyTotalUnbonded.set(curEpoch+1, Map(curEpoch -> 3)), + emptyTotalRedelegatedUnbonded, + emptyTotalBonded.set(curEpoch, 6), + emptytotalRedelegatedBonded, + rate, + emptySlashAmountsMap) == initStakesMap), + // there is a redelegation happening at curEpoch + assert(slashValidator("bob", + (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).mapBy(e => infractionStake + 6), + curEpoch, + infractionStake, + emptySlashes, + emptyTotalUnbonded, + emptyTotalRedelegatedUnbonded, + emptyTotalBonded, + emptytotalRedelegatedBonded.set(curEpoch, Map("alice" -> Map(2 -> 5, 3 -> 1))), + rate, + emptySlashAmountsMap) == initStakesMap), + // there is a redelegation happening at curEpoch that is unbonded at curEpoch + 1 + assert(slashValidator("bob", + initStakesMap, + curEpoch, + infractionStake, + emptySlashes, + emptyTotalUnbonded, + emptyTotalRedelegatedUnbonded.set(curEpoch+1, Map(curEpoch -> Map("alice" -> Map(2 -> 5, 3 -> 1)))), + emptyTotalBonded, + emptytotalRedelegatedBonded.set(curEpoch, Map("alice" -> Map(2 -> 5, 3 -> 1))), + rate, + emptySlashAmountsMap) == initStakesMap), + // there is a redelegation at curEpoch that is partially unbonded at curEpoch + 1 + assert(slashValidator("bob", + (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).mapBy(e => infractionStake + 2), + curEpoch, + infractionStake, + emptySlashes, + emptyTotalUnbonded, + emptyTotalRedelegatedUnbonded.set(curEpoch+1, Map(curEpoch -> Map("alice" -> Map(2 -> 4)))), + emptyTotalBonded, + emptytotalRedelegatedBonded.set(curEpoch, Map("alice" -> Map(2 -> 5, 3 -> 1))), + rate, + emptySlashAmountsMap) == initStakesMap), + // there is a bond at curEpoch, redelegation at curEpoch+1 that is partially unbonded at curEpoch+1 + assert(slashValidator("bob", + (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).mapBy(e => infractionStake + 8), + curEpoch, + infractionStake, + emptySlashes, + emptyTotalUnbonded, + emptyTotalRedelegatedUnbonded.set(curEpoch+1, Map(curEpoch+1 -> Map("alice" -> Map(2 -> 4)))), + emptyTotalBonded.set(curEpoch, 6), + emptytotalRedelegatedBonded.set(curEpoch+1, Map("alice" -> Map(2 -> 5, 3 -> 1))), + rate, + emptySlashAmountsMap) == initStakesMap), + // there is a bond at curEpoch and there exists a slash for "alice" + assert(slashValidator("bob", + (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).mapBy(e => 6), + curEpoch, + infractionStake, + emptySlashes.set("alice", [{epoch: curEpoch-slashProcessingDelay-1, rate: 1}]), + emptyTotalUnbonded, + emptyTotalRedelegatedUnbonded, + emptyTotalBonded.set(curEpoch, 6), + emptytotalRedelegatedBonded, + rate, + emptySlashAmountsMap) == (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).mapBy(e => 0)), + } + } + + // The function slashRedelegation computes how much can be slashed from a redelegated bond considering that the bond may have been completely or partially + // unbonded and that the source validator may have misbehaved already within the redelegation slashing window. + // - @param amount the amount of tokens of the redelegated bond. + // - @param bondStart the epoch at which the redelegated tokens started contributing to the source validator's stake. + // - @param redBondStart the epoch at which the redelegated tokens started contributing to the destination validator's stake. + // - @param srcValidator the source validator. + // - @param curEpoch the current epoch. + // - @param slashes a list of slashes of the source validator. + // - @param totalRedelegatedUnbonded a map of unbonded redelegated tokens at the destination validator. + // - @param finalRate the rate of the slash being processed. + // - @param slashedAmountsMap a map from epoch to already processed slash amounts. + // - @returns a map that adds any newly processed slash amount to slashedAmountsMap. + pure def slashRedelegation(amount: int, + bondStart: Epoch, + redBondStart: Epoch, + srcValidator: Address, + curEpoch: Epoch, + slashes: List[Slash], + totalRedelegatedUnbonded: Epoch -> Epoch -> RedelegatedBondsMap, + finalRate: int, + slashedAmountsMap: Epoch -> int): Epoch -> int = { + val infractionEpoch = curEpoch - slashProcessingDelay + val initTotalUnbonded = (infractionEpoch+1).to(curEpoch).fold(0, (sum, e) => if (not(totalRedelegatedUnbonded.get(e).hasRedelegation(redBondStart, srcValidator, bondStart))) sum + else sum + totalRedelegatedUnbonded.get(e).get(redBondStart).get(srcValidator).get(bondStart)) + // We should iterate in epoch increasing order. TODO: transform this into a list and use foldl. + val result = (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).fold((initTotalUnbonded, slashedAmountsMap), (acc, e) => val updatedTotalUnbonded = if (not(totalRedelegatedUnbonded.get(e).hasRedelegation(redBondStart, srcValidator, bondStart))) acc._1 + else acc._1 + totalRedelegatedUnbonded.get(e).get(redBondStart).get(srcValidator).get(bondStart) + val slashAmount = val listSlashes = slashes.select(s => inRedelegationSlashingWindow(s.epoch, startRedelegationFromEnd(redBondStart), redBondStart) and + s.epoch + slashProcessingDelay < infractionEpoch and + bondStart <= s.epoch) + applyListSlashes(listSlashes, amount - updatedTotalUnbonded) * finalRate + val slashableStake = val listSlashes = slashes.select(s => inRedelegationSlashingWindow(s.epoch, startRedelegationFromEnd(redBondStart), redBondStart) and + bondStart <= s.epoch) + applyListSlashes(listSlashes, amount - updatedTotalUnbonded) + (updatedTotalUnbonded, acc._2.set(e, acc._2.get(e) + min(slashAmount, slashableStake)))) + result._2 + } + + run slashRedelegationTest = { + val totalRedelegatedUnbonded = Map(10 -> Map(), 11 -> Map(), 12 -> Map(), 13 -> Map(10 -> Map("alice" -> Map(7 -> 2))), 14 -> Map(), 15 -> Map(), 16 -> Map(), 9 -> Map()) + val slashedAmountsMap = Map(15 -> 0, 16 -> 0) + all { + assert(slashRedelegation(7, 7, 10, "alice", 14, [], totalRedelegatedUnbonded, 1, slashedAmountsMap) == Map(15 -> 5, 16 -> 5)), + assert(slashRedelegation(7, 7, 11, "alice", 14, [], totalRedelegatedUnbonded, 1, slashedAmountsMap) == Map(15 -> 7, 16 -> 7)), + assert(slashRedelegation(7, 7, 10, "alice", 14, [], totalRedelegatedUnbonded, 1, Map(15 -> 2, 16 -> 3)) == Map(15 -> 7, 16 -> 8)), + // existing slash processed before the one being computed + assert(slashRedelegation(7, 7, 10, "alice", 14, [{epoch: 8, rate: 1}], totalRedelegatedUnbonded, 1, slashedAmountsMap) == Map(15 -> 0, 16 -> 0)), + // existing slash not processed before the one being computed + assert(slashRedelegation(7, 7, 10, "alice", 14, [{epoch: 9, rate: 1}], totalRedelegatedUnbonded, 1, slashedAmountsMap) == Map(15 -> 0, 16 -> 0)), + // existing slashes one processed before the one being computed and one not + assert(slashRedelegation(7, 7, 10, "alice", 14, [{epoch: 8, rate: 1}, {epoch: 9, rate: 1}], totalRedelegatedUnbonded, 1, slashedAmountsMap) == Map(15 -> 0, 16 -> 0)), + } + } + + // In the context of a redelegation, the slashValidatorRedelegation function computes how much a validator (the destination validator of the redelegation) should be slashed + // due to the misbehaving of a second validator (the source validator of the redelegation). The function computes how much the validator whould be slashed at all epochs + // between the current epoch (curEpoch) + 1 and the current epoch + 1 + PIPELINE_OFFSET, accounting for any tokens of the redelegation already unbonded. + // - @param srcValidator the source validator + // - @param curEpoch the current epoch + // - @param redelegations a map from pair of epochs to int that includes all the redelegations from the source validator to the destination validator. + // - The first epoch in the pair is the epoch at which the bond started at the source validator. + // - The second epoch in the pair is the epoch at which the redelegation started (the epoch at which was issued). + // - @param slashes a list of slashes of the source validator. + // - @param totalRedelegatedUnbonded a map of unbonded redelegated tokens at the destination validator. + // - @param finalRate the rate of the slash being processed. + // - @param slashedAmountsMap a map from epoch to already processed slash amounts. + // - @returns a map that adds any newly processed slash amount to slashedAmountsMap. + pure def slashValidatorRedelegation(srcValidator: Address, + curEpoch: Epoch, + redelegations: (Epoch, Epoch) -> int, + slashes: List[Slash], + totalRedelegatedUnbonded: Epoch -> Epoch -> RedelegatedBondsMap, + finalRate: int, + slashedAmountsMap: Epoch -> int): Epoch -> int = { + val infractionEpoch = curEpoch - slashProcessingDelay + redelegations.keys().fold(slashedAmountsMap, (acc, pairEpochs) => val bondStart = pairEpochs._1 + val redelegationStart = pairEpochs._2 + if (inRedelegationSlashingWindow(infractionEpoch, redelegationStart, endRedelegationFromStart(redelegationStart)) and + bondStart <= infractionEpoch) slashRedelegation(redelegations.get(pairEpochs), + bondStart, + endRedelegationFromStart(redelegationStart), + srcValidator, + curEpoch, + slashes, + totalRedelegatedUnbonded, + finalRate, + acc) + else acc) + } + + run slashValidatorRedelegationTest = { + val redelegations = Map((7, 8) -> 7) + val totalRedelegatedUnbonded = Map(10 -> Map(), 11 -> Map(), 12 -> Map(), 13 -> Map(10 -> Map("alice" -> Map(7 -> 2))), 14 -> Map(), 15 -> Map(), 16 -> Map(), 9 -> Map()) + val slashedAmountsMap = Map(15 -> 0, 16 -> 0) + all { + assert(slashValidatorRedelegation("alice", 14, Map(), [], totalRedelegatedUnbonded, 1, slashedAmountsMap) == Map(15 -> 0, 16 -> 0)), + assert(slashValidatorRedelegation("alice", 14, Map(), [], Map(), 1, slashedAmountsMap) == Map(15 -> 0, 16 -> 0)), + assert(slashValidatorRedelegation("alice", 14, Map((6, 8) -> 7), [], totalRedelegatedUnbonded, 1, slashedAmountsMap) == Map(15 -> 7, 16 -> 7)), + assert(slashValidatorRedelegation("alice", 14, redelegations, [], totalRedelegatedUnbonded, 1, slashedAmountsMap) == Map(15 -> 5, 16 -> 5)), + assert(slashValidatorRedelegation("alice", 14, redelegations, [], totalRedelegatedUnbonded, 1, Map(15 -> 2, 16 -> 3)) == Map(15 -> 7, 16 -> 8)), + assert(slashValidatorRedelegation("alice", 14, redelegations, [{epoch: 8, rate: 1}], totalRedelegatedUnbonded, 1, slashedAmountsMap) == Map(15 -> 0, 16 -> 0)) + } + } +} \ No newline at end of file diff --git a/2023/Q2/artifacts/PoS-quint/namada-redelegation.qnt b/2023/Q2/artifacts/PoS-quint/namada-redelegation.qnt new file mode 100644 index 0000000..81b585f --- /dev/null +++ b/2023/Q2/artifacts/PoS-quint/namada-redelegation.qnt @@ -0,0 +1,791 @@ +// -*- mode: Bluespec; -*- +// **************************************************************************** +// This encodes the proof-of-stake system of Namada. +// +// Manuel Bravo, Informal Systems, 2023 +// **************************************************************************** + +module namada { + + import helperFunctions.* from "./helper-functions" + import basicSpells.* from "./basicSpells" + import extraSpells.* from "./extraSpells" + import Dec.* from "./dec" + import types.* from "./namada-types" + + // **************************************************************************** + // State machine state + // ************************************************************************* + + // Delegator state + var delegators: Address -> DelegatorState + // Validator state + var validators: Address -> ValidatorState + // Proof-of-stake state + var pos: PosState + + // **************************************************************************** + // Execution state + // ************************************************************************* + + + // Used to limit the misbehaving of a validator: + // 0: no limit + // 1: limited but it allows multiple infractions with the same stake + // 2: disallow multiple infractions with the same stake + pure val limitEvidence = 0 + + // Used to guarantee every step produces a state transition + // IMPORTANT: Set to false for tests + pure val enforceStateTransition = false + + // Last transaction executed by step. + // Amount is over used by the actions: + // It respresents the amount delegated or unbonded for delegate and unbond respectively; + // It is always 0 for withdraw and actionFauxTransaction; + // It is the misbehaving epoch in Processevidence; + var lastTx: {tag: str, result: bool, user: Address, validator: Address, amount: int} + + // Keeps tracks of when a validator may misbehave again in the case when limitEvidence == 1 + var nextInfractionEpoch: Address -> int + + // ************************************************************************** + // Main functions + // ************************************************************************* + + // The function delegate is called when a user wants to delegate tokens to a validator. + // 1. It first checks that the user has enough tokens in its account. + // 2. Then it locks those tokens by transferring them from the user's account to the PoS special account. + // 3. It records that the user has delegated amount tokens to the validator. + // 4. It increases the validator's stake at the PIPELINE_OFFSET and updates the totalBonded variable. + pure def delegate(delegator: DelegatorState, validator: ValidatorState, posState: PosState, amount: int): ResultTx = { + if (amount <= delegator.balance and amount > 0) { + val updatedDelegator = delegator.with("balance", delegator.balance - amount) + .with("bonded", delegator.bonded.set(validator.address, + delegator.bonded.get(validator.address).addBond(posState.epoch + PIPELINE_OFFSET, amount))) + val updatedValidator = validator.with("stake", validator.stake.set(posState.epoch + PIPELINE_OFFSET, + validator.stake.get(posState.epoch + PIPELINE_OFFSET) + amount)) + .with("totalBonded", validator.totalBonded.set(posState.epoch + PIPELINE_OFFSET, + validator.totalBonded.get(posState.epoch + PIPELINE_OFFSET) + amount)) + val updatedPos = posState.with("posAccount", posState.posAccount + amount) + {success: true, delegator: updatedDelegator, validator: updatedValidator, posState: updatedPos} + } else { + {success: false, delegator: delegator, validator: validator, posState: posState} + } + } + + // The function unbond is called when a user wants to unbond tokens from a validator. + // 1. It first checks that the user has enough tokens bonded to the validator and that the validator is not frozen. + // 2. Then it uses iterateBondsUpToAmount to compute the set of bonds that must be unbonded. + // 3. It computes the set of unbond records to be added to the delegators unbonded variable. + // 4. It updates the delegator state by removing the unbonded bonds and adding the newly computed unbonds. + // 5. It applies any slashes to the unbonded bonds and stroes it in amountAfterSlashing. + // 6. It updates the validator's totalUnbonded. + // 7. It finally updates the validator's stale at the PIPELINE_OFFSET by subtracting amountAfterSlashing. + + pure def unbond(delegator: DelegatorState, validatorAddress: Address, allValidators: Address -> ValidatorState, posState: PosState, amount: int, isRedelegation: bool): ResultUnbondTx = { + val validator = allValidators.get(validatorAddress) + val bonds = delegator.bonded.get(validator.address) + val redelegatedBonds = delegator.redelegatedBonded.get(validator.address) + val totalBonded = bonds.keys().fold(0, (sum, e) => sum + bonds.get(e)) + if (amount > 0 and amount <= totalBonded and validator.frozen < posState.epoch) { + // Compute the epoch at which the unbonded bonds will be withdrawable + val endEpoch = posState.epoch + PIPELINE_OFFSET + CUBIC_OFFSET + UNBONDING_OFFSET + // Compute the set of bonds to be unbonded + val resultUnbonding = iterateBondsUpToAmount(bonds, amount) + // Compute the updated delegators bonded variable by removing the unbonded bonds and adding a new bond in case one was partially unbonded + val updatedBonded = if (resultUnbonding.new.start == -1) bonds.mapRemoveSet(resultUnbonding.toRemove) + else bonds.mapRemoveSet(resultUnbonding.toRemove).set(resultUnbonding.new.start, resultUnbonding.new.amount) + // Compute a modified redelegation bond in case one was partially unbonded + val modifiedRedelegation = if (not(redelegatedBonds.has(resultUnbonding.new.start))) {epoch: -1, valsToRemove: Set(), valToModify: "", epochsToRemove: Set(), epochToModify: -1, newAmount: -1} + else computeModifiedRedelegation(redelegatedBonds.get(resultUnbonding.new.start), resultUnbonding.new.start, bonds.get(resultUnbonding.new.start) - resultUnbonding.new.amount) + // Compute the updated delegator's redelegated bonded by removing the unbonded bonds and updating the partially unbonded one computed in the previous step + val updatedRedelegatedBonded = if (modifiedRedelegation.epoch == -1) redelegatedBonds.mapRemoveSet(resultUnbonding.toRemove) + else redelegatedBonds.mapRemoveSet(resultUnbonding.toRemove).set(modifiedRedelegation.epoch, updateRedelegatedBondsMap(redelegatedBonds.get(modifiedRedelegation.epoch), modifiedRedelegation)) + // Compute the set of unbond records that have to be recorded out of the set of unbonded bonds computed at the previous step + val keysUnbonds = if (resultUnbonding.new.start == -1) resultUnbonding.toRemove else resultUnbonding.toRemove.setAdd(resultUnbonding.new.start) + val newUnbonds = tuples(keysUnbonds, Set(endEpoch)).mapBy(unbondKey => val start = unbondKey._1 + if (start == resultUnbonding.new.start) bonds.get(start) - resultUnbonding.new.amount + else bonds.get(start)) + // Compute the updated delegators unbonded variable by adding the new unbonds if the unbonding is not happenging due to a redelegation + val updatedUnbonded = if (isRedelegation) delegator.unbonded.get(validator.address) else delegator.unbonded.get(validator.address).mapAddSet(newUnbonds) + // Compute the new redelegated unbonds + val newRedelegatedUnbonds = computeNewRedelegatedUnbonds(redelegatedBonds, resultUnbonding.toRemove, modifiedRedelegation) + val updatedRedelegatedUnbonded = if (isRedelegation) delegator.redelegatedUnbonded.get(validator.address) + else updateRedelegatedUnbonded(delegator.redelegatedUnbonded.get(validator.address), newRedelegatedUnbonds, endEpoch) + // Compute the updated delegator's state + val updatedDelegator = delegator.with("bonded", delegator.bonded.set(validator.address, updatedBonded)) + .with("redelegatedBonded", delegator.redelegatedBonded.set(validator.address, updatedRedelegatedBonded)) + .with("unbonded", delegator.unbonded.set(validator.address, updatedUnbonded)) + .with("redelegatedUnbonded", delegator.redelegatedUnbonded.set(validator.address, updatedRedelegatedUnbonded)) + // Compute the updated validator's totalUnbonded variable + val updatedTotalUnbonded = newUnbonds.keys().fold(validator.totalUnbonded.get(posState.epoch + PIPELINE_OFFSET), + (acc, unbondKey) => val start = unbondKey._1 + acc.mapSafeSet(start, acc.getOrElse(start, 0) + newUnbonds.get(unbondKey))) + // Compute the updated validator's total redelegated unbonded + val updatedTotalRedelegatedUnbonded = updateTotalRedelegatedUnbonded(validator.totalRedelegatedUnbonded.get(posState.epoch + PIPELINE_OFFSET), newRedelegatedUnbonds) + // Compute how much out of amount has not been already removed from the validator's stake when slashing validators + // at the end of previous epochs + val resultSlashing = computeAmountAfterSlashingUnbond(newUnbonds, newRedelegatedUnbonds, validatorAddress, allValidators.keys().mapBy(v => allValidators.get(v).slashes)) + val amountAfterSlashing = resultSlashing.sum + val mapEpochAmountAfterSlashing = resultSlashing.epochMap.keys().filter(e => resultSlashing.epochMap.get(e) > 0).mapBy(e => resultSlashing.epochMap.get(e)) + // Compute the updated validator's state by updating its state and totalUnbonded. + val updatedValidator = validator.with("stake", validator.stake.set(posState.epoch + PIPELINE_OFFSET, + validator.stake.get(posState.epoch + PIPELINE_OFFSET) - amountAfterSlashing)) + .with("totalUnbonded", validator.totalUnbonded.set(posState.epoch + PIPELINE_OFFSET, updatedTotalUnbonded)) + .with("totalRedelegatedUnbonded", validator.totalRedelegatedUnbonded.set(posState.epoch + PIPELINE_OFFSET, updatedTotalRedelegatedUnbonded)) + {result: {success: true, delegator: updatedDelegator, validator: updatedValidator, posState: posState}, resultSlashing: {sum: amountAfterSlashing, epochMap: mapEpochAmountAfterSlashing}} + } else { + {result: {success: false, delegator: delegator, validator: validator, posState: posState}, resultSlashing: {sum: -1, epochMap: Map()}} + } + } + + // The function withdraw is called when a user wants to withdraw tokens from a validator. + // 1. First it computes whether there are tokens ready to be withdrawn and returns an error in case there are none. + // 2. Then records that those tokens are withdrawn by removing the withdrawable unbond records from unbonded. + // 3. Finally, it unlocks the tokens by transferring them from the PoS special account to the user's account, after slashing them. + pure def withdraw(delegator: DelegatorState, validatorAddress: Address, allValidators: Address -> ValidatorState, posState: PosState): ResultTx = { + val validator = allValidators.get(validatorAddress) + val unbonds = delegator.unbonded.get(validator.address) + val redelegatedUnbonds = delegator.redelegatedUnbonded.get(validator.address) + // Select the set of unbonds that can be withdrawn + val setWithdrawn = unbonds.keys().filter(unbondKey => unbondKey._2 <= posState.epoch).mapBy(unbondKey => unbonds.get(unbondKey)) + if (size(setWithdrawn.keys()) > 0) { + // Compute how much out of amount is withdrawn after slashing by leveraging applyListSlashes + val amountAfterSlashing = computeAmountAfterSlashingWithdraw(setWithdrawn, redelegatedUnbonds, validatorAddress, allValidators.keys().mapBy(v => allValidators.get(v).slashes)).sum + // Remove the sent of withdrawn unbonds from the set of unbonds + // Transfer withdrawn tokens from the PoS account to the user's account + val updatedDelegator = delegator.with("unbonded", delegator.unbonded.set(validator.address, unbonds.mapRemoveSet(setWithdrawn.keys()))) + .with("redelegatedUnbonded", delegator.redelegatedUnbonded.set(validator.address, redelegatedUnbonds.mapRemoveSet(setWithdrawn.keys()))) + .with("balance", delegator.balance + amountAfterSlashing) + val updatedPos = posState.with("posAccount", posState.posAccount - amountAfterSlashing) + {success: true, delegator: updatedDelegator, validator: validator, posState: updatedPos} + } else { + {success: false, delegator: delegator, validator: validator, posState: posState} + } + } + + // The function redelegate is called when a user wants to redelegate tokens from a source validator to a destination validator. + // 1. The function first attempts to unbond the desired amount from the source validator. + // 2. It only proceeds if the redelegation is not a chain redelegation and the unbonding succeeded. + // 3. It updates the delegator's variables bonded and redelegatedBonded to register that the target amount of tokens are now + // bonded to the destination validator. + // 4. It registers the redelegation in the source validator's outgoingRedelegations variable. + // 5. It updates the destinations validator stake, registers the redelegation in its incomingRedelegations and updates its totalBonded variable. + pure def redelegate(delegator: DelegatorState, allValidators: Address -> ValidatorState, srcAddress: Address, destAddress: Address, posState: PosState, amount: int): ResultRedelegationTx = { + val srcValidator = allValidators.get(srcAddress) + val destValidator = allValidators.get(destAddress) + val endEpochRedelegation = srcValidator.incomingRedelegations.get(delegator.address) + val isNotChained = endEpochRedelegation >=0 implies posState.epoch >= endEpochRedelegation + slashProcessingDelay + val resultUnbond = unbond(delegator, srcAddress, allValidators, posState, amount, true) + if (isNotChained and resultUnbond.result.success == true) { + val newDelegatorState = resultUnbond.result.delegator + val newSrcValidatorState = resultUnbond.result.validator + val amountAfterSlashing = resultUnbond.resultSlashing.sum + val updatedRedelegatedBonds = val existing = newDelegatorState.redelegatedBonded.get(destAddress).getOrElse(posState.epoch + PIPELINE_OFFSET, Map()).getOrElse(srcAddress, Map()) + val updatedMap = mergeBondsMap(existing, resultUnbond.resultSlashing.epochMap) + newDelegatorState.redelegatedBonded.get(destAddress).mapSafeSet(posState.epoch + PIPELINE_OFFSET, + newDelegatorState.redelegatedBonded.get(destAddress).getOrElse(posState.epoch + PIPELINE_OFFSET, Map()).mapSafeSet(srcAddress, updatedMap)) + val updatedDelegator = resultUnbond.result.delegator.with("bonded", newDelegatorState.bonded.set(destValidator.address, + newDelegatorState.bonded.get(destValidator.address).addBond(posState.epoch + PIPELINE_OFFSET, amountAfterSlashing))) + .with("redelegatedBonded", newDelegatorState.redelegatedBonded.set(destValidator.address, updatedRedelegatedBonds)) + val updatedOutgoingRedelegations = mergeOutgoingRedelegations(newSrcValidatorState.outgoingRedelegations.get(destAddress), resultUnbond.resultSlashing.epochMap, posState.epoch) + val updatedSrcValidator = newSrcValidatorState.with("outgoingRedelegations", newSrcValidatorState.outgoingRedelegations.set(destAddress, updatedOutgoingRedelegations)) + val updatedDestValidator = destValidator.with("stake", destValidator.stake.set(posState.epoch + PIPELINE_OFFSET, + destValidator.stake.get(posState.epoch + PIPELINE_OFFSET) + amountAfterSlashing)) + .with("totalRedelegatedBonded", destValidator.totalRedelegatedBonded.set(posState.epoch + PIPELINE_OFFSET, mergeRedelegatedBondsMap(destValidator.totalRedelegatedBonded.get(posState.epoch + PIPELINE_OFFSET), + Map(srcAddress -> resultUnbond.resultSlashing.epochMap)))) + .with("incomingRedelegations", destValidator.incomingRedelegations.set(delegator.address, posState.epoch + PIPELINE_OFFSET)) + {success: true, delegator: updatedDelegator, srcValidator: updatedSrcValidator, destValidator: updatedDestValidator, posState: posState} + } else { + {success: false, delegator: delegator, srcValidator: srcValidator, destValidator: destValidator, posState: posState} + } + } + + // The function processSlash processes a slash by (i) slashing the misbehaving validator; and (ii) any validator to which it has redelegated some tokens and the slash misbehaving epoch + // is wihtin the redelegation slashing window. + // - @param misbehavingValidator the misbehaving validator. + // - @param slashRate the slash rate. + // - @param curEpoch the current epoch. + // - @param slashedAmountsMap a map from validator address to a map from epoch to already processed slash amounts. + // - @param validatorsState a map from validatro address to validator's state. + // - @returns a map that adds any newly processed slash amount of any involved validator to slashedAmountsMap. + pure def processSlash(misbehavingValidator: Address, + slashRate: int, + curEpoch: Epoch, + slashedAmountMap: Address -> Epoch -> int, + validatorsState: Address -> ValidatorState, + slashes: Address -> List[Slash]): Address -> Epoch -> int = { + val infractionEpoch = curEpoch - slashProcessingDelay + val resultSlashValidator = slashValidator(misbehavingValidator, + (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).mapBy(e => validatorsState.get(misbehavingValidator).stake.get(e)), + curEpoch, + validatorsState.get(misbehavingValidator).stake.get(infractionEpoch), + slashes, + //validatorsState.keys().mapBy(v => validatorsState.get(v).slashes), + validatorsState.get(misbehavingValidator).totalUnbonded, + validatorsState.get(misbehavingValidator).totalRedelegatedUnbonded, + validatorsState.get(misbehavingValidator).totalBonded, + validatorsState.get(misbehavingValidator).totalRedelegatedBonded, + slashRate, + slashedAmountMap.get(misbehavingValidator)) + val updatedSlashedAmountMap = slashedAmountMap.set(misbehavingValidator, resultSlashValidator) + val outgoingRedelegations = validatorsState.get(misbehavingValidator).outgoingRedelegations + outgoingRedelegations.keys().fold(updatedSlashedAmountMap, (acc, destValidator) => acc.set(destValidator, slashValidatorRedelegation(misbehavingValidator, + curEpoch, + outgoingRedelegations.get(destValidator), + validatorsState.get(misbehavingValidator).slashes, + validatorsState.get(destValidator).totalRedelegatedUnbonded, + slashRate, + acc.get(destValidator)))) + } + + // This function is executed at the end of an epoch. + // 1. It first computes the final rate for all slashes scheduled to be processed at the end of the current epoch. + // 2. It computes for each validator how much it should be slashed based of the slashes scheduled to be processed. It already computes + // how much should be substracted from each validator's stake variable at every epoch between the current epoch and the current epoch + PIPELINE_OFFSET. + // 3. It updates the validators' state by (i) shifting the epoched stake variable and applying any precomputed slash; (ii) shifting totalUnbonded, totalRedelegatedUnbonded and totalBonded; + // and (iii) appending newly created slash records. + // 4. It update PoS state by increasing the epoch, setting counterTxs to zero, transferring totalAmountSlashed from the PoS accoun tot the slash pool + // and shifting equeued slashes. + pure def endOfEpoch(validatorsState: Address -> ValidatorState, posState: PosState, curEpoch: Epoch): {validatorsState: Address -> ValidatorState, posState: PosState} = { + val finalRate = computeFinalRate((curEpoch-CUBIC_OFFSET).to(curEpoch+CUBIC_OFFSET).fold(Set(), (acc, e) => acc.union(posState.enqueuedSlashes.get(e)))) + val initMap = VALIDATORS.mapBy(v => (curEpoch+1).to(curEpoch+PIPELINE_OFFSET).mapBy(e => 0)) + val infractionEpoch = posState.epoch - CUBIC_OFFSET - UNBONDING_OFFSET + val slashPerValidator = posState.enqueuedSlashes.get(curEpoch).fold(Map(), (acc, slash) => acc.mapSafeSet(slash.validator, min(1, acc.getOrElse(slash.validator, 0) + finalRate))) + val slashesMap = VALIDATORS.mapBy(v => validatorsState.get(v).slashes) + val resultSlashing = slashPerValidator.keys().fold((initMap, slashesMap), (acc, validator) => (processSlash(validator, slashPerValidator.get(validator), curEpoch, acc._1, validatorsState, acc._2), + acc._2.set(validator, acc._2.get(validator).append({epoch: infractionEpoch, rate: slashPerValidator.get(validator)})))) + val mapValidatorSlash = resultSlashing._1 + val updatedValidators = VALIDATORS.mapBy(v => validatorsState.get(v).with("stake",(curEpoch-UNBONDING_OFFSET-CUBIC_OFFSET+1).to(curEpoch+1+PIPELINE_OFFSET).mapBy(e => if (e < curEpoch+1+PIPELINE_OFFSET) validatorsState.get(v).stake.get(e) - + if (e >= curEpoch+1) mapValidatorSlash.get(v).get(e) else 0 + else validatorsState.get(v).stake.get(e-1) - mapValidatorSlash.get(v).get(e-1))) + .with("totalUnbonded", (curEpoch-CUBIC_OFFSET-UNBONDING_OFFSET+1).to(curEpoch+1+PIPELINE_OFFSET).mapBy(e => if (e < curEpoch+1+PIPELINE_OFFSET) validatorsState.get(v).totalUnbonded.get(e) + else Map())) + .with("totalRedelegatedUnbonded", (curEpoch-CUBIC_OFFSET-UNBONDING_OFFSET+1).to(curEpoch+1+PIPELINE_OFFSET).mapBy(e => if (e < curEpoch+1+PIPELINE_OFFSET) validatorsState.get(v).totalRedelegatedUnbonded.get(e) + else Map())) + .with("totalBonded", (curEpoch-CUBIC_OFFSET-UNBONDING_OFFSET+1).to(curEpoch+1+PIPELINE_OFFSET).mapBy(e => if (e < curEpoch+1+PIPELINE_OFFSET) validatorsState.get(v).totalBonded.get(e) + else 0)) + .with("totalRedelegatedBonded", (curEpoch-CUBIC_OFFSET-UNBONDING_OFFSET+1).to(curEpoch+1+PIPELINE_OFFSET).mapBy(e => if (e < curEpoch+1+PIPELINE_OFFSET) validatorsState.get(v).totalRedelegatedBonded.get(e) + else Map())) + .with("slashes", if (slashPerValidator.has(v)) validatorsState.get(v).slashes.append({epoch: infractionEpoch, rate: slashPerValidator.get(v)}) + else validatorsState.get(v).slashes)) + //val totalAmountSlashed = slashPerValidator.keys().fold(0, (sum, validator) => sum + validatorsState.get(validator).stake.get(infractionEpoch)*slashPerValidator.get(validator)) + val updatedPos = posState.with("epoch", curEpoch + 1) + .with("counterTxs", 0) + .with("counterInfractions", 0) + //.with("posAccount", posState.posAccount - totalAmountSlashed) + //.with("slashPool", posState.slashPool + totalAmountSlashed) + .with("enqueuedSlashes", (curEpoch-CUBIC_OFFSET+1).to(curEpoch+1+CUBIC_OFFSET+UNBONDING_OFFSET).mapBy(e => if (e < curEpoch+1+CUBIC_OFFSET+UNBONDING_OFFSET) posState.enqueuedSlashes.get(e) + else Set())) + {validatorsState: updatedValidators, posState: updatedPos} + } + + // The function proccessEvidence is called when a validator misbehaves. + // 1. It first creates a slash record. + // 2. Then it updates the validator's state by freezing the validator. + // 3. It finally enqueues the slash and schedules it to be proccessed at the end of the epoch resulting from adding UNBONDING_OFFSET + // to the misbehaving epoch. + pure def proccessEvidence(e: Epoch, validator: ValidatorState, posState: PosState): {validator: ValidatorState, posState: PosState} = { + val id = posState.counterInfractions + 1 + val infraction = {id: id, epoch: e, validator: validator.address} + {validator: validator.with("frozen", max(validator.frozen, e + CUBIC_OFFSET + UNBONDING_OFFSET)), + posState: posState.with("enqueuedSlashes", posState.enqueuedSlashes.set(e + CUBIC_OFFSET + UNBONDING_OFFSET, posState.enqueuedSlashes.get(e + CUBIC_OFFSET + UNBONDING_OFFSET).union(Set(infraction)))) + .with("counterInfractions", id)} + } + + + // **************************************************************************** + // Actions + // ************************************************************************* + + // The action commonTxAfter is called after a transaction is executed. + // 1. It first checks if it is the last transaction of the current epoch. + // 2. If it is the last transaction of the epoch, it calls the endOfEpoch function. + // 3. Otherwise, it updates the variables using the result of the transaciton and increases counterTxs. + action commonTxAfter(updateDelegators: Address -> DelegatorState, updatedValidators: Address -> ValidatorState, updatedPos: PosState): bool = all { + delegators' = updateDelegators, + nextInfractionEpoch' = nextInfractionEpoch, + if (pos.counterTxs + 1 == TXS_EPOCH) { + val resultEndOfEpoch = endOfEpoch(updatedValidators, updatedPos, pos.epoch) + all { + validators' = resultEndOfEpoch.validatorsState, + pos' = resultEndOfEpoch.posState, + } + } else { + all { + validators' = updatedValidators, + pos' = updatedPos.with("counterTxs", updatedPos.counterTxs + 1), + } + } + } + + action actionDelegate(user: Address, validator: Address, amount: int): bool = all { + val result = delegate(delegators.get(user), validators.get(validator), pos, amount) + all { + require(enforceStateTransition implies result.success), + commonTxAfter(delegators.set(user, result.delegator), + validators.set(validator, result.validator), + result.posState), + lastTx' = {tag: "Delegate", result: result.success, user: user, validator: validator, amount: amount} + } + } + + action actionUnbond(user: Address, validator: Address, amount: int): bool = all { + val result = unbond(delegators.get(user), validator, validators, pos, amount, false).result + all { + require(enforceStateTransition implies result.success), + commonTxAfter(delegators.set(user, result.delegator), + validators.set(validator, result.validator), + result.posState), + lastTx' = {tag: "Unbond", result: result.success, user: user, validator: validator, amount: amount} + } + } + + action actionWithdraw(user: Address, validator: Address): bool = all { + val result = withdraw(delegators.get(user), validator, validators, pos) + all { + require(enforceStateTransition implies result.success), + commonTxAfter(delegators.set(user, result.delegator), + validators.set(validator, result.validator), + result.posState), + lastTx' = {tag: "Withdraw", result: result.success, user: user, validator: validator, amount: 0} + } + } + + action actionRedelegate(user: Address, srcValidator: Address, destValidator: Address, amount: int): bool = all { + val result = redelegate(delegators.get(user), validators, srcValidator, destValidator, pos, amount) + all { + require(enforceStateTransition implies result.success), + commonTxAfter(delegators.set(user, result.delegator), + validators.set(srcValidator, result.srcValidator).set(destValidator, result.destValidator), + result.posState), + lastTx' = {tag: "Redelegate", result: result.success, user: user, validator: srcValidator, amount: amount} + } + } + + action actionEvidence(e: Epoch, validator: Address): bool = all { + require(limitEvidence == 1 implies nextInfractionEpoch.get(validator) < e), + require(limitEvidence == 2 implies validators.get(validator).frozen < e), + val result = proccessEvidence(e, validators.get(validator), pos) + all { + validators' = validators.set(validator, result.validator), + pos' = result.posState, + delegators' = delegators, + lastTx' = {tag: "Evidence", result: true, user: "", validator: validator, amount: e}, + nextInfractionEpoch' = nextInfractionEpoch.set(validator, e + UNBONDING_OFFSET) + } + } + + action actionFauxTransaction(user: Address, validator: Address, amountDelegate: int, amountUnbond: int, e: Epoch): bool = all { + require(limitEvidence == 1 implies nextInfractionEpoch.get(validator) >= e), + require(limitEvidence == 2 implies validators.get(validator).frozen >= e), + require(amountUnbond == 0 or validators.get(validator).frozen >= pos.epoch), + require(amountDelegate == 0), + commonTxAfter(delegators, validators, pos), + lastTx' = {tag: "Advance", result: true, user: user, validator: validator, amount: 0} + } + + // **************************************************************************** + // Invariants + // ************************************************************************* + + // Invariant 1: A delegator's balance cannot become negative. + val balanceGreaterZero = USERS.forall(user => delegators.get(user).balance >= 0) + + // Invariant 2: The PoS account cannot become negative. + val posAccountGreaterZero = pos.posAccount >= 0 + + // Invariant 3: If there are no bonds and all unbonds have been withdrawn, the PoS balance must be equal to zero. + val posAccountZero = USERS.forall(user => VALIDATORS.forall(validator => delegators.get(user).bonded.get(validator) == Map() and + delegators.get(user).unbonded.get(validator) == Map())) implies pos.posAccount == 0 + + // Invariant 4: The validator's voting power at a given epoch is less or equal to the total amount of tokens delegated to that validator. + // This is not an equality due to slashing. Next invariant checks the equality restricted to no slashing. + val stakeEqualOrLessSumBonds = VALIDATORS.forall(validator => USERS.fold(0, (sum, user) => val bonds = delegators.get(user).bonded.get(validator) + sum + bonds.keys().fold(0, (total, start) => total + bonds.get(start))) >= validators.get(validator).stake.get(pos.epoch + PIPELINE_OFFSET)) + + // Invariant 5: If no slashing occurs, the validator's voting power at a given epoch is equal to the total amount of tokens delegated to that validator. + val noSlashingStakeEqualSumBonds = pos.slashPool == 0 implies VALIDATORS.forall(validator => USERS.fold(0, (sum, user) => val bonds = delegators.get(user).bonded.get(validator) + sum + bonds.keys().fold(0, (total, start) => total + bonds.get(start))) == validators.get(validator).stake.get(pos.epoch + PIPELINE_OFFSET)) + + // Invariant 6: The total amount of tokens is constant. + val totalAmountTokensConstant = USERS.fold(0, (sum, user) => sum + delegators.get(user).balance) + pos.posAccount + pos.slashPool == size(USERS)*INIT_BALANCE + + // Invariant 7: A validator's stake cannot become negative. + val stakeGreaterZero = VALIDATORS.forall(validator => + pos.epoch.to(pos.epoch + PIPELINE_OFFSET).forall(e => validators.get(validator).stake.get(e) >= 0)) + + //Invariant 8: The user's balance cannot become greater than the initial balance + val boundedBalance = USERS.forall(user => delegators.get(user).balance <= INIT_BALANCE) + + // All invariants + val allInvariants = balanceGreaterZero and + posAccountGreaterZero and + posAccountZero and + stakeEqualOrLessSumBonds and + noSlashingStakeEqualSumBonds and + totalAmountTokensConstant and + stakeGreaterZero and + boundedBalance + + // All invariants without slash pool + // Due to the lack of slashing pool posAccountZero and noSlashingStakeEqualSumBonds do not hold + val allInvariantsWithNoSlashPool = balanceGreaterZero and + posAccountGreaterZero and + stakeEqualOrLessSumBonds and + totalAmountTokensConstant and + stakeGreaterZero and + boundedBalance + + // **************************************************************************** + // Execution + // ************************************************************************* + + action allUnchanged: bool = all { + delegators' = delegators, + validators' = validators, + pos' = pos, + lastTx' = lastTx, + nextInfractionEpoch' = nextInfractionEpoch + } + + // State initialization: assumes that users start with some initial balance. + action init: bool = all { + val initEpoch = UNBONDING_OFFSET + CUBIC_OFFSET + all { + delegators' = USERS.mapBy(user => {address: user, + balance: INIT_BALANCE, + bonded: VALIDATORS.mapBy(x => Map()), + redelegatedBonded: VALIDATORS.mapBy(x => Map()), + redelegatedUnbonded: VALIDATORS.mapBy(x => Map()), + unbonded: VALIDATORS.mapBy(x => Map())}), + validators' = VALIDATORS.mapBy(validator => {address: validator, + stake: 0.to(initEpoch+PIPELINE_OFFSET).mapBy(e => 0), + totalUnbonded: 0.to(initEpoch+PIPELINE_OFFSET).mapBy(e => Map()), + totalRedelegatedUnbonded: 0.to(initEpoch+PIPELINE_OFFSET).mapBy(e => Map()), + totalRedelegatedBonded: 0.to(initEpoch+PIPELINE_OFFSET).mapBy(e => Map()), + totalBonded: 0.to(initEpoch+PIPELINE_OFFSET).mapBy(e => 0), + incomingRedelegations: USERS.mapBy(user => -1), + outgoingRedelegations: VALIDATORS.setRemove(validator).mapBy(x => Map()), + slashes: List(), + frozen: 0}), + pos' = {posAccount: 0, + slashPool: 0, + epoch: initEpoch, + counterTxs: 0, + counterInfractions: 0, + enqueuedSlashes: (initEpoch-CUBIC_OFFSET).to(initEpoch+CUBIC_OFFSET+UNBONDING_OFFSET).mapBy(e => Set())}, + lastTx' = { tag: "Init", result: true, user: "", validator: "", amount: 0}, + nextInfractionEpoch' = VALIDATORS.mapBy(validator => 0) + } + } + + // Execution of the state machine. + // 1. Pick a random amount from 0 to MAX_UINT, a user, a validator, and an epoch between + // the current epoch and the current epoch - UNBONDING_OFFSET + // 2. Execute one of the actions: delegate, unbond, withdraw or evidence. + // 3. In case none of the above actions are executable, it executes the actionFauxTransaction action. + // 4. The above logic is implemented by the precondition in actionFauxTransaction. + action step: bool = { + nondet user = USERS.oneOf() + nondet validator = VALIDATORS.oneOf() + nondet destValidator = VALIDATORS.setRemove(validator).oneOf() + //nondet amount = 0.to(MAX_UINT).oneOf() + nondet amountDelegate = 0.to(delegators.get(user).balance).oneOf() + nondet amountUnbond = 0.to(delegators.get(user).bonded.get(validator).keys().fold(0, (sum, e) => sum + delegators.get(user).bonded.get(validator).get(e))).oneOf() + nondet e = (pos.epoch - UNBONDING_OFFSET).to(pos.epoch).oneOf() + // Execute one of the available actions/methods + any { + actionDelegate(user, validator, amountDelegate), + actionUnbond(user, validator, amountUnbond), + actionWithdraw(user, validator), + actionEvidence(e, validator), + actionRedelegate(user, validator, destValidator, amountUnbond), + //allUnchanged + actionFauxTransaction(user, validator, amountDelegate, amountUnbond, e) + } + } + + // **************************************************************************** + // Tests + // ************************************************************************* + + //The test testDelegate is a unitest-like test for the delegate function. + //TODO: refactor, epoch ranges are off. + run delegateTest = { + val delegatorState = {address: "bob", + balance: INIT_BALANCE, + bonded: USERS.mapBy(x => Map()), + redelegatedBonded: VALIDATORS.mapBy(x => Map()), + redelegatedUnbonded: VALIDATORS.mapBy(x => Map()), + unbonded: USERS.mapBy(x => Map())} + val validatorState = {address: "alice", + stake: 0.to(UNBONDING_OFFSET).mapBy(e => 0), + totalUnbonded: 1.to(1+PIPELINE_OFFSET).mapBy(e => Map()), + totalRedelegatedUnbonded: 1.to(1+PIPELINE_OFFSET).mapBy(e => Map()), + totalRedelegatedBonded: 1.to(1+PIPELINE_OFFSET).mapBy(e => Map()), + totalBonded: 1.to(1+PIPELINE_OFFSET).mapBy(e => 0), + incomingRedelegations: USERS.mapBy(user => -1), + outgoingRedelegations: VALIDATORS.mapBy(x => Map()), + slashes: List(), + frozen: 0} + val posState = {posAccount: 0, + slashPool: 0, + epoch: 1, + counterTxs: 0, + counterInfractions: 0, + enqueuedSlashes: 0.to(UNBONDING_OFFSET).mapBy(e => Set())} + nondet amount = 0.to(MAX_UINT).oneOf() + val result = delegate(delegatorState, validatorState, posState, amount) + if (result.success) { + all { + assert(result.delegator.balance == INIT_BALANCE - amount), + assert(result.delegator.bonded.get(validatorState.address).get(1 + PIPELINE_OFFSET) == amount), + assert(result.delegator.unbonded.get(validatorState.address) == Map()), + assert(result.validator.stake.get(1 + PIPELINE_OFFSET) == amount), + assert(result.posState.posAccount == amount) + } + } else { + all { + assert(amount > INIT_BALANCE or amount == 0), + assert(result.delegator == delegatorState), + assert(result.validator == validatorState), + assert(result.posState == posState) + } + } + } + + // The test successfulWithdrawTest checks that the withdraw works. + run successfulWithdrawTest = { + nondet user = USERS.oneOf() + nondet validator = VALIDATORS.oneOf() + all { + init + .then(actionDelegate(user, validator, 10)) + .then(actionUnbond(user, validator, 5)) + .then(actionFauxTransaction(user, validator, 0, 0, -1).repeated(UNBONDING_OFFSET+PIPELINE_OFFSET+CUBIC_OFFSET)) + .then(actionWithdraw(user, validator)) + .then(all{ assert(delegators.get(user).balance == 15), allUnchanged}) + + } + } + + // The test testUnbondingPeriod checks that the unbonding period is enforced. + run unbondingPeriodTest = { + nondet user = USERS.oneOf() + nondet validator = VALIDATORS.oneOf() + all { + init + .then(actionDelegate(user, validator, 8)) + .then(actionUnbond(user, validator, 5)) + .then(actionWithdraw(user, validator)) + .then(all{ assert(delegators.get(user).balance == 12), allUnchanged}) + } + } + + // The test fullExecutionTest describes an execution that involves all actions. + run fullExecutionTest = { + nondet user = USERS.oneOf() + nondet validator = VALIDATORS.oneOf() + nondet amount = 1.to(INIT_BALANCE).oneOf() + nondet amountUnbonded = 1.to(amount).oneOf() + val initEpoch = UNBONDING_OFFSET + CUBIC_OFFSET + all { + init + .then(actionDelegate(user, validator, amount)) + .then(actionUnbond(user, validator, amountUnbonded))//epoch=UNBONDING_OFFSET+1 + .then(actionEvidence(initEpoch + 1, validator))//to be processed at the end of 2*UNBONDING_OFFSET+2*CUBIC_OFFSET+1 + .then(actionFauxTransaction(user, validator, 0, 0, -1).repeated(UNBONDING_OFFSET+CUBIC_OFFSET)) + //slash already processed + .then(actionWithdraw(user, validator)) + // the 5 tokens unbonded shoul be slashed + .then(all{ assert(delegators.get(user).balance == INIT_BALANCE - amount), + //assert(pos.slashPool == amount), + allUnchanged }) + + } + } + + // The test earlyUnbondingTest is the most complete test involving all actions. + run earlyUnbondingTest = { + nondet user = USERS.oneOf() + nondet validator = VALIDATORS.oneOf() + nondet amount = 1.to(INIT_BALANCE).oneOf() + nondet amountUnbonded = 1.to(amount).oneOf() + //when the evidence will be processed + val initEpoch = UNBONDING_OFFSET+CUBIC_OFFSET + val slashingOffset = UNBONDING_OFFSET+CUBIC_OFFSET + all { + init + .then(actionDelegate(user, validator, amount)) //epoch=UNBONDING_OFFSET assuming init epoch=UNBONDING_OFFSET + .then(actionUnbond(user, validator, amountUnbonded))//epoch=UNBONDING_OFFSET+CUBIC_OFFSET+1 + .then(actionEvidence(initEpoch + 1, validator)) //to be processed at the end of 2*UNBONDING_OFFSET+2*CUBIC_OFFSET+1 + .then(actionFauxTransaction(user, validator, 0, 0, -1).repeated(slashingOffset - 1))//epoch=2*UNBONDING_OFFSET+2*CUBIC_OFFSET + //check that slash has not been processed yet + .then(all{ assert(validators.get(validator).slashes == List()), + allUnchanged }) + .then(actionWithdraw(user, validator))//epoch=2*UNBONDING_OFFSET+2*CUBIC_OFFSET+1 + //no withdrawing should be allowed yet + .then(all{ assert(delegators.get(user).balance == INIT_BALANCE - amount), + assert(pos.epoch == 2*UNBONDING_OFFSET+2*CUBIC_OFFSET+2), + allUnchanged }) + //check that slash has been processed + .then(actionWithdraw(user, validator))//epoch=2*UNBONDING_OFFSET+2+PIPELINE_OFFSET+CUBIC_OFFSET + //all tokens are slashed + .then(all{ assert(delegators.get(user).balance == INIT_BALANCE - amount), + //assert(pos.slashPool == amount), + allUnchanged }) + } + } + + //namadaScenarioTest tests a specific scenario that the Namada team use to test their implementation + //It requires a different intialization of state variables whihc is done in initNamadaTest + action initNamadaScenario: bool = all { + val initEpoch = UNBONDING_OFFSET + CUBIC_OFFSET + all { + delegators' = USERS.mapBy(user => {address: user, + balance: 1000000, + bonded: VALIDATORS.mapBy(x => if (x == "alice" and user == "alice") Map(UNBONDING_OFFSET + CUBIC_OFFSET - 1 -> 200000) else Map()), + redelegatedBonded: VALIDATORS.mapBy(x => Map()), + redelegatedUnbonded: VALIDATORS.mapBy(x => Map()), + unbonded: VALIDATORS.mapBy(x => Map())}), + validators' = VALIDATORS.mapBy(validator => {address: validator, + stake: 0.to(initEpoch+PIPELINE_OFFSET).mapBy(e => if (validator=="alice" and e >= UNBONDING_OFFSET + CUBIC_OFFSET - 1) 200000 else 0), + totalUnbonded: 0.to(initEpoch+PIPELINE_OFFSET).mapBy(e => Map()), + totalRedelegatedUnbonded: 0.to(initEpoch+PIPELINE_OFFSET).mapBy(e => Map()), + totalRedelegatedBonded: 0.to(initEpoch+PIPELINE_OFFSET).mapBy(e => Map()), + totalBonded: 0.to(initEpoch+PIPELINE_OFFSET).mapBy(e => if (validator=="alice" and e==UNBONDING_OFFSET + CUBIC_OFFSET - 1) 200000 else 0), + incomingRedelegations: USERS.mapBy(user => -1), + outgoingRedelegations: VALIDATORS.mapBy(x => Map()), + slashes: List(), + frozen: 0}), + pos' = {posAccount: 200000, + slashPool: 0, + epoch: initEpoch, + counterTxs: 0, + counterInfractions: 0, + enqueuedSlashes: (initEpoch-CUBIC_OFFSET).to(initEpoch+CUBIC_OFFSET+UNBONDING_OFFSET).mapBy(e => Set())}, + lastTx' = { tag: "Init", result: true, user: "", validator: "", amount: 0}, + nextInfractionEpoch' = VALIDATORS.mapBy(validator => 0) + } + } + + run namadaScenarioTest = { + val validator = "alice" + nondet user = USERS.exclude(Set(validator)).oneOf() + val initEpoch = UNBONDING_OFFSET + CUBIC_OFFSET // = 5 + val cubicSlashingRate = 1 + val initialStake = 200000 + val del1Amount = 67231 + val selfUnbond1Amount = 154654 + val delUnbond1Amount = 18000 + val selfBond1Amount = 9123 + val selfUnbond2Amount = 15000 + val del2Amount = 8144 + val stakeAfterProcessing = (1 - min(1, 2*cubicSlashingRate))*(initialStake + del1Amount - selfUnbond1Amount - delUnbond1Amount - selfUnbond2Amount + selfBond1Amount) + del2Amount + all{ + //making preconditions explicit to ease debugging + require(UNBONDING_OFFSET == 4), + require(PIPELINE_OFFSET == 2), + require(CUBIC_OFFSET == 1), + require(VALIDATORS.exists(v => v == "alice")), + require(size(USERS.exclude(Set(validator))) > 0), + initNamadaScenario + //bonded at initEpoch + PIPELINE_OFFSET = initEpoch + 2 + .then(actionDelegate(user, validator, 67231)) // epoch = initEpoch + //unbonded at initEpoch + 1 + PIPELINE_OFFSET = initEpoch + 3 + .then(actionUnbond(validator, validator, 154654)) // epoch = initEpoch + 1 + //unbonded at initEpoch + 2 + PIPELINE_OFFSET = initEpoch + 4 + .then(actionUnbond(user, validator, 18000)) // epoch = initEpoch + 2 + //bonded at initEpoch + 3 + PIPELINE_OFFSET = initEpoch + 5 + .then(actionDelegate(validator, validator, 9123)) // epoch = initEpoch + 3 + //unbonded at initEpoch + 4 + PIPELINE_OFFSET = initEpoch + 6 + .then(actionUnbond(validator, validator, 15000)) // epoch = initEpoch + 4 + //bonded at initEpoch + 5 + PIPELINE_OFFSET = initEpoch + 7 + .then(actionDelegate(user, validator, 8144)) // epoch = initEpoch + 5 + //slash processed at initEpoch + PIPELINE_OFFSET + 1 + CUBIC_OFFSET + UNBONDING_OFFSET = (initEpoch + 3) + 5 = initEpoch + 8 + .then(actionEvidence(initEpoch + PIPELINE_OFFSET + 1, validator)) // epoch = initEpoch + 6 + //slash processed at initEpoch + PIPELINE_OFFSET + 1 + CUBIC_OFFSET + UNBONDING_OFFSET = (initEpoch + 3) + 5 = initEpoch + 8 + .then(actionEvidence(initEpoch + PIPELINE_OFFSET + 1, validator)) // epoch = initEpoch + 6 + //slash processed at initEpoch + PIPELINE_OFFSET + 2 + CUBIC_OFFSET + UNBONDING_OFFSET = (initEpoch + 4) + 5 = initEpoch + 9 + .then(actionEvidence(initEpoch + PIPELINE_OFFSET + 2, validator)) // epoch = initEpoch + 6 + .then(actionFauxTransaction(user, validator, 0, 0, -1).repeated(3)) // epoch = initEpoch + 6..initEpoch + 8 + .then(all{assert(validators.get(validator).stake.get(initEpoch + 9) == stakeAfterProcessing), + allUnchanged }) + } + } + + run redelegateTest = { + nondet user = USERS.oneOf() + nondet srcValidator = VALIDATORS.oneOf() + nondet destValidator = VALIDATORS.setRemove(srcValidator).oneOf() + nondet amountDelegate = 2.to(INIT_BALANCE).oneOf() + nondet amountRedelegate = 2.to(amountDelegate).oneOf() + nondet amountUnbond = 1.to(amountRedelegate-1).oneOf() + val initEpoch = UNBONDING_OFFSET + CUBIC_OFFSET + all { + require(size(VALIDATORS) >= 2), + init + .then(actionDelegate(user, srcValidator, amountDelegate)) + .then(actionFauxTransaction(user, srcValidator, 0, 0, -1).repeated(PIPELINE_OFFSET)) + .then(actionRedelegate(user, srcValidator, destValidator, amountRedelegate)) + .then(all {assert(delegators.get(user).redelegatedBonded.get(destValidator).get(initEpoch+2*PIPELINE_OFFSET+1).get(srcValidator).get(initEpoch+PIPELINE_OFFSET) == amountRedelegate), + assert(validators.get(destValidator).incomingRedelegations.get(user) == initEpoch+2*PIPELINE_OFFSET+1), + assert(validators.get(srcValidator).outgoingRedelegations.get(destValidator).get((initEpoch+PIPELINE_OFFSET, initEpoch+PIPELINE_OFFSET+1)) == amountRedelegate), + allUnchanged}) + .then(actionFauxTransaction(user, srcValidator, 0, 0, -1).repeated(PIPELINE_OFFSET)) + .then(actionUnbond(user, destValidator, amountUnbond)) + .then(val bondStart = initEpoch+PIPELINE_OFFSET + val redelegationEnd = bondStart+PIPELINE_OFFSET+1 + val unbondEnd = redelegationEnd+PIPELINE_OFFSET+CUBIC_OFFSET+UNBONDING_OFFSET+1 + val unbondMaterialized = redelegationEnd+PIPELINE_OFFSET+1 + all {assert(delegators.get(user).redelegatedBonded.get(destValidator).get(redelegationEnd).get(srcValidator).get(bondStart) == amountRedelegate - amountUnbond), + assert(delegators.get(user).redelegatedUnbonded.get(destValidator).get((redelegationEnd, unbondEnd)).get(srcValidator).get(bondStart) == amountUnbond), + assert(validators.get(destValidator).totalRedelegatedUnbonded.get(unbondMaterialized).get(redelegationEnd).get(srcValidator).get(bondStart) == amountUnbond), + allUnchanged}) + .then(actionFauxTransaction(user, srcValidator, 0, 0, -1).repeated(CUBIC_OFFSET+UNBONDING_OFFSET+1)) + .then(actionWithdraw(user, destValidator)) + .then(all {assert(delegators.get(user).redelegatedUnbonded.get(destValidator) == Map()), + assert(delegators.get(user).balance == INIT_BALANCE - amountDelegate + amountUnbond), + allUnchanged}) + } + } + run redelegateWithSlashingTest = { + nondet user = USERS.oneOf() + nondet srcValidator = VALIDATORS.oneOf() + nondet destValidator = VALIDATORS.setRemove(srcValidator).oneOf() + nondet amountDelegate = 2.to(INIT_BALANCE).oneOf() + nondet amountRedelegate = 2.to(amountDelegate).oneOf() + nondet amountUnbond = 1.to(amountRedelegate-1).oneOf() + val initEpoch = UNBONDING_OFFSET + CUBIC_OFFSET + all { + require(size(VALIDATORS) >= 2), + init + .then(actionDelegate(user, srcValidator, amountDelegate)) + .then(actionFauxTransaction(user, srcValidator, 0, 0, -1).repeated(PIPELINE_OFFSET)) + .then(actionRedelegate(user, srcValidator, destValidator, amountRedelegate)) + .then(all {assert(delegators.get(user).redelegatedBonded.get(destValidator).get(initEpoch+2*PIPELINE_OFFSET+1).get(srcValidator).get(initEpoch+PIPELINE_OFFSET) == amountRedelegate), + assert(validators.get(destValidator).incomingRedelegations.get(user) == initEpoch+2*PIPELINE_OFFSET+1), + assert(validators.get(srcValidator).outgoingRedelegations.get(destValidator).get((initEpoch+PIPELINE_OFFSET, initEpoch+PIPELINE_OFFSET+1)) == amountRedelegate), + allUnchanged}) + .then(actionFauxTransaction(user, srcValidator, 0, 0, -1).repeated(PIPELINE_OFFSET)) + .then(actionUnbond(user, destValidator, amountUnbond)) + //an epoch before the end of the redelegation, i.e., within the redelegation slashing window + .then(actionEvidence(initEpoch+2*PIPELINE_OFFSET, srcValidator)) + .then(val bondStart = initEpoch+PIPELINE_OFFSET + val redelegationEnd = bondStart+PIPELINE_OFFSET+1 + val unbondEnd = redelegationEnd+PIPELINE_OFFSET+CUBIC_OFFSET+UNBONDING_OFFSET+1 + val unbondMaterialized = redelegationEnd+PIPELINE_OFFSET+1 + all {assert(delegators.get(user).redelegatedBonded.get(destValidator).get(redelegationEnd).get(srcValidator).get(bondStart) == amountRedelegate - amountUnbond), + assert(delegators.get(user).redelegatedUnbonded.get(destValidator).get((redelegationEnd, unbondEnd)).get(srcValidator).get(bondStart) == amountUnbond), + assert(validators.get(destValidator).totalRedelegatedUnbonded.get(unbondMaterialized).get(redelegationEnd).get(srcValidator).get(bondStart) == amountUnbond), + allUnchanged}) + .then(actionFauxTransaction(user, srcValidator, 0, 0, -1).repeated(CUBIC_OFFSET+UNBONDING_OFFSET+1)) + .then(actionWithdraw(user, destValidator)) + .then(all {assert(delegators.get(user).redelegatedUnbonded.get(destValidator) == Map()), + assert(delegators.get(user).balance == INIT_BALANCE - amountDelegate), + allUnchanged}) + } + } +} \ No newline at end of file diff --git a/2023/Q2/artifacts/PoS-quint/namada-types.qnt b/2023/Q2/artifacts/PoS-quint/namada-types.qnt new file mode 100644 index 0000000..f8b986d --- /dev/null +++ b/2023/Q2/artifacts/PoS-quint/namada-types.qnt @@ -0,0 +1,194 @@ +// -*- mode: Bluespec; -*- +/** + * + * Manuel Bravo, Informal Systems, 2023 + */ + +module types { + + import Dec.* from "./dec" + + // **************************************************************************** + // Data Types + // ************************************************************************* + // Represent addresses as strings + type Address = str + + // Represent epochs as integers + type Epoch = int + + // A map from source validator to a map of bonds: from bond starting epoch at the source validator to amount of tokens + type RedelegatedBondsMap = Address -> Epoch -> int + + type Redelegation = { + redBondStart: Epoch, + srcValidator: Address, + bondStart: Epoch, + amount: int + } + + type ModifiedRedelegation = { + epoch: Epoch, + valsToRemove: Set[Address], + valToModify: Address, + epochsToRemove: Set[Epoch], + epochToModify: Epoch, + newAmount: int + } + + // Slash record + type Slash = { + // Misbehaving epoch + epoch: Epoch, + // slash rate + rate: int + } + + // Enqueued infraction record + type Infraction = { + // Unique identifier + id: int, + // Misbehaving epoch + epoch: Epoch, + // Misbehaving validator + validator: Address, + } + + // Delegator state + type DelegatorState = { + // Delegator's address + address: Address, + // User's current balance + balance: int, + // User's bonds: a map from validator to a map storing the tokens that the user has currently delegated to the validator + // The latter maps bond starting epoch to amount of tokens + bonded: Address -> Epoch -> int, + // User's bonds that come from redelegations: a map from validator to a map storing the redelegated tokens that the user has currently + //delegated to the validator. The latter maps bond starting epoch to a RedelegatedBondsMap (from source validator to a map of bonds from bond starting epoch at the source validator to amount of tokens) + redelegatedBonded: Address -> Epoch -> RedelegatedBondsMap, + // User's unbonds: a map from validator to a map storing the tokens that the user has unbonded (not yet withdrawn) from the validator + // The latter maps the pair bond starting epoch and unbond ending epoch to amount of tokens + unbonded: Address -> (Epoch, Epoch) -> int, + // User's unbonds that come from redelegations: a map from validator to a map storing the redelegtated tokens that the user has unbonded (not yet withdrawn)/ + // The latter maps the pair bond starting epoch and unbond ending epoch to a RedelegatedBondsMap (from source validator to a map of bonds from bond starting epoch at the source validator to amount of tokens) + redelegatedUnbonded: Address -> (Epoch, Epoch) -> RedelegatedBondsMap + } + + // Validator state + type ValidatorState = { + // Validator's address + address: Address, + // Epoched stake: a map from epoch to stake + stake: Epoch -> int, + // Ordered by epoch list of already processed slashes + slashes: List[Slash], + // Keeps tracks of the epoch until which a validator is frozen + frozen: Epoch, + // Each validator keeps track of the amount of tokens that have been unbonded at a given epoch. + // totalUnbonded is a map from unbonding epoch to unbonded bonds + // The unbonded bonds are tracked in a map from bond starting epoch to amount of tokens + totalUnbonded: Epoch -> Epoch -> int, + // Each validator keeps track of the amount of redelegated tokens that have been unbonded at a given epoch. + // totalRedelegatedUnbonded is a map from unbonding epoch to unbonded redelegated bonds + // The unbonded redelegated bonds are tracked in a map from bond starting epoch at the validator to RedelegatedBondsMap. + // (from source validator to a map of bonds from bond starting epoch at the source validator to amount of tokens) + totalRedelegatedUnbonded: Epoch -> Epoch -> RedelegatedBondsMap, + // Each validator keeps track of the amount of tokens bonded at a given epoch + // totalBonded is a map from bond starting epoch to amount of bonded tokens + // It is used an the end of an epoch to compute how many tokens have been delegated + // to a validator after a given infraction epoch. + totalBonded: Epoch -> int, + // Each validator keeps track of the amount of redelegated tokens bonded at a given epoch. + // totalBonded is a map from bond starting epoch to RedelegatedBondsMap. + // (from source validator to a map of bonds from bond starting epoch at the source validator to amount of tokens) + // It is used an the end of an epoch to compute how many redelegated tokens have been delegated + // to a validator after a given infraction epoch. + totalRedelegatedBonded: Epoch -> RedelegatedBondsMap, + // Each validator keeps track of incoming redelegations. + // For each source validator, the validator keeps track the epoch at which the latest + // redelegation ends: when the redelegated tokens start contributing to the validator. + // This is used to prevent chain redelegations. + incomingRedelegations: Address -> Epoch, + // Each validator keeps track of outgoing redelegations. + // For each destination validator, the validator keeps a map of redelegated tokens. + // The map uses a pair of epochs as key: bond starting epoch at the validator, redelegation starting epoch (when the redelagation was issued). + // This is used to slash destination validator when a slash for the validator is processed at the end of an epoch. + outgoingRedelegations: Address -> (Epoch, Epoch) -> int + } + + // Proof-of-stake system state + type PosState = { + // A special PoS account that receives staked tokens + posAccount: int, + // The slash pool receives slashed tokens + slashPool: int, + // Current epoch + epoch: Epoch, + // Number of transactions executed in the current epoch + counterTxs: int, + // Number of infractions submitted at the current epoch + counterInfractions: int, + // A map from epoch to the set of slashes scheduled to be processed + enqueuedSlashes: Epoch -> Set[Infraction], + } + + // Result record returned by any of the three PoS functions: delegate, unbond and withdraw + type ResultTx = { + success: bool, + delegator: DelegatorState, + validator: ValidatorState, + posState: PosState + } + + // Result record returned by any of the unbond function + type ResultUnbondTx = { + result: ResultTx, + resultSlashing: {sum: int, epochMap: Epoch -> int} + } + + // Result record returned by the redelegation PoS function + type ResultRedelegationTx = { + success: bool, + delegator: DelegatorState, + srcValidator: ValidatorState, + destValidator: ValidatorState, + posState: PosState + } + + // **************************************************************************** + // Specification Parameters + // ************************************************************************* + + // Max uint + pure val MAX_UINT: int = 10 + + // Users initial balances + pure val INIT_BALANCE: int = 20 + + // Set of all user addresses + pure val USERS: Set[str] = Set("alice", "bob") + + // Set of all validator addresses + pure val VALIDATORS: Set[str] = Set("alice", "bob") + + // Transactions per epoch + // the spec is not fully ready to handle multiple txs per epoch + // we would need to handle duplicate bonds and unbonds + pure val TXS_EPOCH: int = 1 + + // Unbonding offset + pure val UNBONDING_OFFSET: int = 4 + + // Pipeline offset + pure val PIPELINE_OFFSET: int = 2 + + // Cubic offset + pure val CUBIC_OFFSET: int = 1 + + // Slash rate duplicate vote + pure val DUPLICATE_RATE: Dec = (1, 5) + + // Slash rate light client attack + pure val LIGHT_RATE: Dec = (1, 5) + +} \ No newline at end of file