From 36867d51312c92eed9e5b8868aab2c9e306116c9 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Fri, 26 Jan 2024 14:28:31 +0100 Subject: [PATCH] Refactor utility functions to type module --- tests/mbt/model/ccv.qnt | 1386 ++++++++++++++++++++------------------- 1 file changed, 699 insertions(+), 687 deletions(-) diff --git a/tests/mbt/model/ccv.qnt b/tests/mbt/model/ccv.qnt index cbd664b326..efe865ee4e 100644 --- a/tests/mbt/model/ccv.qnt +++ b/tests/mbt/model/ccv.qnt @@ -287,543 +287,118 @@ module ccv_types { ) } - -} - -module ccv { - // Implements the core logic of the cross-chain validation protocol. - - // Things that are not modelled: - // * Reward distribution - // * Slashes - - // Things that explicitly are modelled: - // * Validator set changes are propagated from provider to consumers - // * Vsc packets mature - - // We assume that packet receive + ack happen synchronously, - // i.e. when the packet is delivered, the ack is delivered right afterwards. - // This is because it is nontrivial in practice to get a relayer to relay a packet, but not its ack. - - import Time.* from "./libraries/Time" - import extraSpells.* from "./libraries/extraSpells" - import ccv_types.* - - // =================== - // PROTOCOL PARAMETERS + // UTILITY FUNCTIONS + // which do not hold the core logic of the protocol, but are still part of it // =================== - // the set of all possible consumer chains. - const ConsumerChains: Set[Chain] - - // For each chain, this defines the time between the initiation of an unbonding and its maturation. - const UnbondingPeriodPerChain: Chain -> int - - // The maximum time duration between sending any VscPacket to any consumer chain and receiving the - // corresponding VscMaturedPacket, without timing out the consumer chain and consequently removing it. - const VscTimeout: int - - // The timeoutTimestamp for sent packets. Can differ by chain. - const CcvTimeout: Chain -> int + // Appends the key assignment for the given oldConsAddr on the consumer by a validator + // to be pruned when a VscMaturedPacket for the current runningVscId is received from the consumer. + pure def AppendConsumerAddrToPrune(currentState: ProtocolState, oldConsAddr: ConsumerAddr, consumer: Chain): ProtocolState = { + pure val vscId = currentState.providerState.runningVscId + pure val consumerAddrsToPrune = currentState.providerState.consumerAddrsToPrune.getOrElse(consumer, Map()) + pure val prevConsAddrs = consumerAddrsToPrune.getOrElse(oldConsAddr, Map()).getOrElse(vscId, []) - // The trusting period on each chain. - // If headers on a channel between two chains are not updated within this period, - // they expire and the channel will be closed. - const TrustingPeriodPerChain: Chain -> int + pure val newConsAddrsToPrune = consumerAddrsToPrune.put(vscId, prevConsAddrs.append(oldConsAddr)) - // =================== - // PROTOCOL LOGIC contains the meat of the protocol - // functions here roughly correspond to API calls that can be triggered from external sources - // =================== - - // the power of a validator on the provider chain is changed by the given amount. We do not care how this happens, - // e.g. via undelegations, or delegations, ... - pure def votingPowerChange(currentState: ProtocolState, validator: Node, amount: int): Result = { - pure val currentValidatorSet = currentState.providerState.chainState.currentValidatorSet - pure val oldVotingPower = if (currentValidatorSet.keys().contains(validator)) currentValidatorSet.get(validator) else 0 - if (amount == 0) { - Err("Voting power cannot change by zero!") - } else if (oldVotingPower == 0) { - Err("Voting power cannot be changed for a validator that is not in the current validator set!") - } else { - pure val newVotingPower = oldVotingPower + amount - pure val newValidatorSet = currentValidatorSet.put(validator, if(newVotingPower >= 0) newVotingPower else 0) - // if the new validator set contains no validators with positive voting power, the validator set is invalid - if (newValidatorSet.values().filter(votingPower => votingPower > 0).size() == 0) { - Err("Voting power change resulted in empty validator set!") - } else { - // set the validator set changed flag - val newProviderState = currentState.providerState.with( - "providerValidatorSetChangedInThisBlock", true - ) - pure val tmpState = currentState.with( - "providerState", newProviderState - ) - pure val newState = setProviderValidatorSet(tmpState, newValidatorSet) - Ok(newState) - } - } + currentState.with( + "providerState", + currentState.providerState.with( + "consumerAddrsToPrune", + currentState.providerState.consumerAddrsToPrune.put(consumer, newConsAddrsToPrune) + ) + ) } - // Delivers the next queued VscMaturedPacket from a consumer chain to the provider chain. - // Arguments are the currentState and the the consumer chain, from which the packet will be delivered. - // If this packet will time out on the provider on delivery, - // the consumer will be dropped. - // The first return is the result of the operation, the second result is a boolean - // that indicates whether the consumer timed out or not. - // If the result has an error, the second return should be ignored. - pure def deliverPacketToProvider(currentState: ProtocolState, sender: Chain): (Result, bool) = { - if (not(isRunningConsumer(sender, currentState.providerState))) { - (Err("Sender is not currently a consumer - must have 'running' status!"), false) - } else if (length(currentState.consumerStates.get(sender).outstandingPacketsToProvider) == 0) { - (Err("No outstanding packets to deliver"), false) - } else { - val packet = currentState.consumerStates.get(sender).outstandingPacketsToProvider.head() - if(packet.timeoutTime <= currentState.providerState.chainState.runningTimestamp) { - // drop consumer - val result = stopConsumers( - currentState.providerState.consumerStatus, - Set(), - Set(sender) + // Returns the new ConsumerStatusMap according to the consumers to stop + // and the consumers to time out. + // If a consumer is both stopped and timed out, it will be timed out. + // The second return is an error string: If it is not equal to "", + // it contains an error message, and the first return should be ignored. + pure def stopConsumers( + currentConsumerStatusMap: Chain -> str, + consumersToStop: Set[Chain], + consumersToTimeout: Set[Chain]): (Chain -> str, str) = { + val runningConsumers = currentConsumerStatusMap.keys().filter( + chain => currentConsumerStatusMap.get(chain) == RUNNING + ) + // all consumers to stop must be running right now, else we have an error + if (consumersToStop.exclude(runningConsumers).size() > 0) { + (currentConsumerStatusMap, "Cannot stop a consumer that is not running") + } else { + val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( + (chain) => + if (consumersToTimeout.contains(chain)) { + TIMEDOUT + } else if (consumersToStop.contains(chain)) { + STOPPED + } else { + currentConsumerStatusMap.get(chain) + } ) - - val newConsumerStatus = result._1 - val err = result._2 - if (err != "") { - (Err(err), false) - } else { - val newProviderState = currentState.providerState.with( - "consumerStatus", newConsumerStatus - ) - val newState: ProtocolState = currentState.with( - "providerState", newProviderState - ) - (Ok(newState), true) // true because the packet timed out - } + (newConsumerStatusMap, "") + } + } + + // Returns the new ConsumerStatusMap according to the consumers to start. + // The second return is an error string: If it is not equal to "", + // it contains an error message, and the first return should be ignored. + pure def startConsumers( + currentConsumerStatusMap: Chain -> str, + consumersToStart: Set[Chain]): (Chain -> str, str) = { + val nonConsumers = currentConsumerStatusMap.keys().filter( + chain => currentConsumerStatusMap.get(chain) == NOT_CONSUMER + ) + // all consumers to start must be nonConsumers right now, otherwise we have an error + if (consumersToStart.exclude(nonConsumers).size() > 0) { + (currentConsumerStatusMap, "cannot start a consumer that is stopped or already a consumer") } else { - // the packet has not timed out, so receive it on the provider - val result = recvPacketOnProvider(currentState, sender, packet) - val tmpState = result.newState - if (result.hasError()) { - (result, false) - } else { - (Ok(removeOutstandingPacketFromConsumer(tmpState, sender)), false) // false because the packet did not time out - } + val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( + (chain) => + if (consumersToStart.contains(chain)) { + RUNNING + } else { + currentConsumerStatusMap.get(chain) + } + ) + (newConsumerStatusMap, "") } } - } - // Delivers the next queued VscPacket from the provider chain to a consumer chain. - // Arguments are the current state and the consumer chain, to which the packet will be delivered. - // If this packet will time out on the consumer on delivery, - // the consumer will be dropped. - // The first return is the result of the operation, the second result is a boolean - // that indicates whether the consumer timed out or not. - // If the result has an error, the second return should be ignored. - pure def deliverPacketToConsumer(currentState: ProtocolState, receiver: Chain): (Result, bool) = { - if (not(isRunningConsumer(receiver, currentState.providerState))) { - (Err("Receiver is not currently a consumer - must have 'running' status!"), false) - } else if (length(currentState.providerState.outstandingPacketsToConsumer.get(receiver)) == 0) { - (Err("No outstanding packets to deliver"), false) + pure def StartStopConsumers( + currentConsumerStatusMap: Chain -> str, + consumersToStart: Set[Chain], + consumersToStop: Set[Chain], + consumersToTimeout: Set[Chain] + ): (Chain -> str, str) = { + // check if any consumer is both started and stopped + if (consumersToStart.intersect(consumersToStop).size() > 0) { + (currentConsumerStatusMap, "Cannot start and stop a consumer at the same time") } else { - val packet = currentState.providerState.outstandingPacketsToConsumer.get(receiver).head() - // check if the consumer timed out - if (packet.timeoutTime <= currentState.consumerStates.get(receiver).chainState.runningTimestamp) { - // drop consumer - val result = stopConsumers( - currentState.providerState.consumerStatus, - Set(), - Set(receiver) - ) - - val newConsumerStatus = result._1 - val err = result._2 - if (err != "") { - (Err(err), false) - } else { - val newProviderState = currentState.providerState.with( - "consumerStatus", newConsumerStatus - ) - val newState: ProtocolState = currentState.with( - "providerState", newProviderState - ) - (Ok(newState), true) // true because the packet timed out - } + val res1 = currentConsumerStatusMap.startConsumers(consumersToStart) + val newConsumerStatus = res1._1 + val err1 = res1._2 + val res2 = newConsumerStatus.stopConsumers(consumersToStop, consumersToTimeout) + val err2 = res2._2 + if (err1 != "") { + (currentConsumerStatusMap, err1) + } else if (err2 != "") { + (currentConsumerStatusMap, err2) } else { - // the packet has not timed out, so receive it on the consumer - val result = recvPacketOnConsumer(currentState, receiver, packet) - val tmpState = result.newState - if (result.hasError()) { - (result, false) - } else { - (Ok(removeOutstandingPacketFromProvider(tmpState, receiver)), false) // false because the packet did not time out - } + (res2._1, "") } } } - - /// Ends a block on the provider. This means that the current validator set is committed on chain, - /// packets are queued, and the next block is started. Also, consumers that have passed - /// the VscTimeout without responding to a pending vscpacket are dropped. - pure def endAndBeginBlockForProvider( - currentState: ProtocolState, - // by how much the timestamp should be advanced, - // i.e. the timestamp for the next block is oldTimestamp + timeAdvancement - timeAdvancement: Time, - // a set of consumers that were not consumers before, but should be set to running now. - consumersToStart: Set[Chain], - // a set of consumers that were running before, but should be set to stopped now. - // This argument only needs to contain "voluntary" stops - - // forced stops, e.g. because a consumer timed out, - // will be added automatically. - consumersToStop: Set[Chain]): Result = { - val currentProviderState = currentState.providerState - - // check for vsc timeouts - val timedOutConsumers = getRunningConsumers(currentProviderState).filter( - consumer => - val res = TimeoutDueToVscTimeout(currentState, consumer) - res._1 - ) - - // for each consumer chain, apply the key assignment to the current validator set - val currentValSets = ConsumerChains.mapBy( - (consumer) => - currentProviderState.applyKeyAssignmentToValSet( - consumer, - currentProviderState.chainState.currentValidatorSet - ) - ) - // store the current validator set with the key assignments applied in the history - val newKeyAssignedValSetHistory = currentValSets.keys().mapBy( - (consumer) => - currentProviderState.keyAssignedValSetHistory - .getOrElse(consumer, List()) // get the existing history (empty list if no history yet) - .prepend(currentValSets.get(consumer)) // prepend the current validator set with key assignments applied - ) - - // run the shared core chainState logic - val newChainState = currentProviderState.chainState.endAndBeginBlockShared(timeAdvancement) - val providerStateAfterTimeAdvancement = - {...currentProviderState, chainState: newChainState, keyAssignedValSetHistory: newKeyAssignedValSetHistory} - val tmpState = currentState.with( - "providerState", providerStateAfterTimeAdvancement - ) - - - // send vsc packets (will be a noop if no sends are necessary) - val providerStateAfterSending = - providerStateAfterTimeAdvancement.sendVscPackets(currentProviderState.chainState.runningTimestamp) - - - // start/stop chains - val res = providerStateAfterSending.consumerStatus.StartStopConsumers( - consumersToStart, - consumersToStop, - timedOutConsumers - ) - val newConsumerStatus = res._1 - val err = res._2 - val providerStateAfterConsumerAdvancement = providerStateAfterSending.with( - "consumerStatus", newConsumerStatus - ).with( - "providerValidatorSetChangedInThisBlock", false - ) - - if (err != "") { - Err(err) - } else { - // for each consumer we just set to running, set its initial validator set to be the current one on the provider... - val valSet = providerStateAfterConsumerAdvancement.chainState.currentValidatorSet - val newConsumerStateMap = - tmpState.consumerStates.keys().mapBy( - (consumer) => - if (consumersToStart.contains(consumer)) { - // ...modified by the key assignments for the consumer - val consValSet = applyKeyAssignmentToValSet(providerStateAfterConsumerAdvancement, consumer, valSet) - val currentConsumerState: ConsumerState = tmpState.consumerStates.get(consumer) - val newConsumerState: ConsumerState = currentConsumerState.with( - "chainState", currentConsumerState.chainState.with( - "currentValidatorSet", consValSet - ).with( - "votingPowerHistory", - List(consValSet) - ).with( - "lastTimestamp", - providerStateAfterConsumerAdvancement.chainState.lastTimestamp - ).with( - "runningTimestamp", - providerStateAfterConsumerAdvancement.chainState.runningTimestamp - ) - ) - newConsumerState - } else { - currentState.consumerStates.get(consumer) - } - ) - val newState = tmpState.with( - "providerState", providerStateAfterConsumerAdvancement - ).with( - "consumerStates", newConsumerStateMap - ) - - Ok(newState) - } - } - - pure def endAndBeginBlockForConsumer( - currentState: ProtocolState, - chain: Chain, - // by how much the timestamp of the chain should be advanced for the next block - timeAdvancement: Time): Result = { - if (not(currentState.consumerStates.keys().contains(chain))) { - // if the chain is not a consumer, return an error - Err("chain is not a consumer") - } else { - val currentConsumerState: ConsumerState = currentState.consumerStates.get(chain) - val oldChainState: ChainState = currentConsumerState.chainState - val newChainState: ChainState = currentConsumerState.chainState.endAndBeginBlockShared(timeAdvancement) - val newConsumerState: ConsumerState = currentConsumerState.with( - "chainState", newChainState - ) - val maturedPackets = newConsumerState.maturationTimes.select( - pair => - val packet = pair._1 - val maturationTime: Time = pair._2 - // important: this uses the last committed timestamp, not the running timestamp! - maturationTime <= newChainState.lastTimestamp - ).transform(pair => pair._1) - val newMaturationTimes = newConsumerState.maturationTimes.select( - pair => - val packet = pair._1 - val maturationTime: Time = pair._2 - // important: this uses the last committed timestamp, not the running timestamp! - - maturationTime > newChainState.lastTimestamp - ) - val newOutstandingPackets = newConsumerState.outstandingPacketsToProvider.concat( - maturedPackets.transform( - packet => { - id: packet.id, - // it is important to use the oldChainState here, since this happens during EndBlock - sendingTime: oldChainState.runningTimestamp, - timeoutTime: oldChainState.runningTimestamp + CcvTimeout.get(chain) - } - ) - ) - val newConsumerState2: ConsumerState = newConsumerState.with( - "maturationTimes", newMaturationTimes - ).with( - "outstandingPacketsToProvider", newOutstandingPackets - ) - val newConsumerStates = currentState.consumerStates.set(chain, newConsumerState2) - val newState: ProtocolState = currentState.with( - "consumerStates", newConsumerStates - ) - Ok(newState) - } - } - - // Validator providerNode assigns their address for the consumer to be the consumerAddress. - pure def assignConsumerKey(currentState: ProtocolState, consumer: Chain, providerNode: Node, consumerAddr: ConsumerAddr): Result = { - // rule 1: validator A cannot assign consumer key K to consumer chain X - // if there is already a validator B (B!=A) using K on the provider - pure val provCurValSet = currentState.providerState.chainState.currentValidatorSet - if (provCurValSet.keys().exists(node => node != providerNode and node == consumerAddr)) { - Err("validator A cannot assign consumer key K to consumer chain X - if there is already a validator B (B!=A) using K on the provider") - } else { - // rule 2: validator A cannot assign consumer key K to consumer chain X if - // there is already a validator B using K on X - pure val valByConsAddr = currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()) - if (valByConsAddr.keys().contains(consumerAddr)) { - Err("consumer key is already in use on the consumer chain") - } else { - // this key can be assigned - - // get the old assigned key - pure val consKeyByVal = currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()) - pure val p = if (consKeyByVal.keys().contains(providerNode)) { - // providerNode had previously assigned a consumer key - (consKeyByVal.get(providerNode), true) - } else { - (providerNode, false) - } - // the consumer address that was previously associated with the node - pure val oldConsAddr = p._1 - // whether the old address was explicitly assigned, or the default key - pure val prevAssigned = p._2 - - // set the old address for pruning, if it was assigned - pure val tmpState = if (prevAssigned) { - AppendConsumerAddrToPrune(currentState, oldConsAddr, consumer) - } else { - currentState - } - - // check whether the validator has positive power - pure val provValSet = currentState.providerState.chainState.currentValidatorSet - pure val provValPower = if (provValSet.keys().contains(providerNode)) provValSet.get(providerNode) else 0 - pure val consumersWithAddrAssignmentChangesInThisBlock = - if (provValPower > 0) { - // if the consumer has positive power, the relevant key assignment for the consumer changed - currentState.providerState.consumersWithAddrAssignmentChangesInThisBlock.union(Set(consumer)) - } else { - // otherwise, the consumer doesn't need to know about the change, so no change - currentState.providerState.consumersWithAddrAssignmentChangesInThisBlock - } - pure val tmpStateAfterKeyAssignmentReplacement = tmpState.with( - "providerState", tmpState.providerState.with( - "consumersWithAddrAssignmentChangesInThisBlock", consumersWithAddrAssignmentChangesInThisBlock - ) - ) - - pure val newvalidatorToConsumerAddr = currentState.providerState.validatorToConsumerAddr.put( - consumer, - currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()).put( - providerNode, - consumerAddr - ) - ) - - pure val newconsumerAddrToValidator = currentState.providerState.consumerAddrToValidator.put( - consumer, - currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()).put( - consumerAddr, - providerNode - ) - ) - - pure val newProviderState = tmpStateAfterKeyAssignmentReplacement.providerState.with( - "validatorToConsumerAddr", newvalidatorToConsumerAddr - ).with( - "consumerAddrToValidator", newconsumerAddrToValidator - ) - - Ok( - tmpStateAfterKeyAssignmentReplacement.with( - "providerState", newProviderState - ) - ) - } - } - } - - // =================== - // UTILITY FUNCTIONS - // which do not hold the core logic of the protocol, but are still part of it - // =================== - - // Appends the key assignment for the given oldConsAddr on the consumer by a validator - // to be pruned when a VscMaturedPacket for the current runningVscId is received from the consumer. - pure def AppendConsumerAddrToPrune(currentState: ProtocolState, oldConsAddr: ConsumerAddr, consumer: Chain): ProtocolState = { - pure val vscId = currentState.providerState.runningVscId - pure val consumerAddrsToPrune = currentState.providerState.consumerAddrsToPrune.getOrElse(consumer, Map()) - pure val prevConsAddrs = consumerAddrsToPrune.getOrElse(oldConsAddr, Map()).getOrElse(vscId, []) - - pure val newConsAddrsToPrune = consumerAddrsToPrune.put(vscId, prevConsAddrs.append(oldConsAddr)) - - currentState.with( - "providerState", - currentState.providerState.with( - "consumerAddrsToPrune", - currentState.providerState.consumerAddrsToPrune.put(consumer, newConsAddrsToPrune) - ) - ) - } - - // Returns the new ConsumerStatusMap according to the consumers to stop - // and the consumers to time out. - // If a consumer is both stopped and timed out, it will be timed out. - // The second return is an error string: If it is not equal to "", - // it contains an error message, and the first return should be ignored. - pure def stopConsumers( - currentConsumerStatusMap: Chain -> str, - consumersToStop: Set[Chain], - consumersToTimeout: Set[Chain]): (Chain -> str, str) = { - val runningConsumers = currentConsumerStatusMap.keys().filter( - chain => currentConsumerStatusMap.get(chain) == RUNNING - ) - // all consumers to stop must be running right now, else we have an error - if (consumersToStop.exclude(runningConsumers).size() > 0) { - (currentConsumerStatusMap, "Cannot stop a consumer that is not running") - } else { - val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( - (chain) => - if (consumersToTimeout.contains(chain)) { - TIMEDOUT - } else if (consumersToStop.contains(chain)) { - STOPPED - } else { - currentConsumerStatusMap.get(chain) - } - ) - (newConsumerStatusMap, "") - } - } - - // Returns the new ConsumerStatusMap according to the consumers to start. - // The second return is an error string: If it is not equal to "", - // it contains an error message, and the first return should be ignored. - pure def startConsumers( - currentConsumerStatusMap: Chain -> str, - consumersToStart: Set[Chain]): (Chain -> str, str) = { - val nonConsumers = currentConsumerStatusMap.keys().filter( - chain => currentConsumerStatusMap.get(chain) == NOT_CONSUMER - ) - // all consumers to start must be nonConsumers right now, otherwise we have an error - if (consumersToStart.exclude(nonConsumers).size() > 0) { - (currentConsumerStatusMap, "cannot start a consumer that is stopped or already a consumer") - } else { - val newConsumerStatusMap = currentConsumerStatusMap.keys().mapBy( - (chain) => - if (consumersToStart.contains(chain)) { - RUNNING - } else { - currentConsumerStatusMap.get(chain) - } - ) - (newConsumerStatusMap, "") - } - } - - pure def StartStopConsumers( - currentConsumerStatusMap: Chain -> str, - consumersToStart: Set[Chain], - consumersToStop: Set[Chain], - consumersToTimeout: Set[Chain] - ): (Chain -> str, str) = { - // check if any consumer is both started and stopped - if (consumersToStart.intersect(consumersToStop).size() > 0) { - (currentConsumerStatusMap, "Cannot start and stop a consumer at the same time") - } else { - val res1 = currentConsumerStatusMap.startConsumers(consumersToStart) - val newConsumerStatus = res1._1 - val err1 = res1._2 - val res2 = newConsumerStatus.stopConsumers(consumersToStop, consumersToTimeout) - val err2 = res2._2 - if (err1 != "") { - (currentConsumerStatusMap, err1) - } else if (err2 != "") { - (currentConsumerStatusMap, err2) - } else { - (res2._1, "") - } - } - } - - - // Takes the currentValidatorSet and puts it as the newest set of the voting history - pure def enterCurValSetIntoBlock(chainState: ChainState): ChainState = { - chainState.with( - "votingPowerHistory", chainState.votingPowerHistory.prepend( - chainState.currentValidatorSet - ) - ) - } + // Takes the currentValidatorSet and puts it as the newest set of the voting history + pure def enterCurValSetIntoBlock(chainState: ChainState): ChainState = { + chainState.with( + "votingPowerHistory", chainState.votingPowerHistory.prepend( + chainState.currentValidatorSet + ) + ) + } // Advances the timestamp in the chainState by timeAdvancement pure def advanceTime(chainState: ChainState, timeAdvancement: Time): ChainState = @@ -843,8 +418,12 @@ module ccv { // * increments the runningVscId // This should only be called when the provider chain is ending a block. // If no vsc packets need to be sent, this will be a noop. - pure def sendVscPackets(providerState: ProviderState, sendingTimestamp: Time): ProviderState = { - val newSentPacketsPerConsumer = ConsumerChains.mapBy( // compute, for each consumer, a list of new packets to be sent + // the ccv timeout should be the ccv timeout for the provider chain. + pure def sendVscPackets( + providerState: ProviderState, + sendingTimestamp: Time, + ccvTimeout: Time): ProviderState = { + val newSentPacketsPerConsumer = providerState.getRunningConsumers().mapBy( // compute, for each consumer, a list of new packets to be sent (consumer) => // if validator set changed or the key assignments for this chain changed, and the consumer is running, send a packet if ((providerState.providerValidatorSetChangedInThisBlock or @@ -860,20 +439,20 @@ module ccv { providerState.chainState.currentValidatorSet ), sendingTime: sendingTimestamp, - timeoutTime: sendingTimestamp + CcvTimeout.get(PROVIDER_CHAIN) + timeoutTime: sendingTimestamp + ccvTimeout }) } else { // no packet to be sent, so empty list List() } ) - val newOutstandingPacketsToConsumer = ConsumerChains.mapBy( + val newOutstandingPacketsToConsumer = providerState.getRunningConsumers().mapBy( (consumer) => providerState.outstandingPacketsToConsumer.getOrElse(consumer, List()).concat( newSentPacketsPerConsumer.get(consumer) ) ) - val newSentVscPackets = ConsumerChains.mapBy( + val newSentVscPackets = providerState.getRunningConsumers().mapBy( (consumer) => providerState.sentVscPacketsToConsumer.getOrElse(consumer, List()).concat( newSentPacketsPerConsumer.get(consumer) @@ -896,201 +475,634 @@ module ccv { } } - // receives a given packet (sent by the provider) on the consumer. The arguments are the consumer chain that is receiving the packet, and the packet itself. - // To receive a packet, modify the running validator set (not the one entered into the block yet, - // but the candidate that would be put into the block if it ended now) - // and store the maturation time for the packet. - pure def recvPacketOnConsumer(currentState: ProtocolState, receiver: Chain, packet: VscPacket): Result = { - if(not(isRunningConsumer(receiver, currentState.providerState))) { - Err("Receiver is not currently a consumer - must have 'running' status!") - } else { - // update the running validator set, but not the history yet, - // as that only happens when the next block is started - val currentConsumerState: ConsumerState = currentState.consumerStates.get(receiver) - val newConsumerState: ConsumerState = - { - ...currentConsumerState, - chainState: currentConsumerState.chainState.with( - "currentValidatorSet", packet.validatorSet - ), - maturationTimes: currentConsumerState.maturationTimes.append( - ( - packet, - currentConsumerState.chainState.runningTimestamp + UnbondingPeriodPerChain.get(receiver) - ) - ), - receivedVscPackets: currentConsumerState.receivedVscPackets.prepend(packet) + // receives a given packet (sent by the provider) on the consumer. The arguments are the consumer chain that is receiving the packet, and the packet itself, + // as well as the unbonding period for the consumer chain. + // To receive a packet, modify the running validator set (not the one entered into the block yet, + // but the candidate that would be put into the block if it ended now) + // and store the maturation time for the packet. + pure def recvPacketOnConsumer( + currentState: ProtocolState, + receiver: Chain, + packet: VscPacket, + receiverUnbondingPeriod: Time): Result = { + if(not(isRunningConsumer(receiver, currentState.providerState))) { + Err("Receiver is not currently a consumer - must have 'running' status!") + } else { + // update the running validator set, but not the history yet, + // as that only happens when the next block is started + val currentConsumerState: ConsumerState = currentState.consumerStates.get(receiver) + val newConsumerState: ConsumerState = + { + ...currentConsumerState, + chainState: currentConsumerState.chainState.with( + "currentValidatorSet", packet.validatorSet + ), + maturationTimes: currentConsumerState.maturationTimes.append( + ( + packet, + currentConsumerState.chainState.runningTimestamp + receiverUnbondingPeriod + ) + ), + receivedVscPackets: currentConsumerState.receivedVscPackets.prepend(packet) + } + val newConsumerStates = currentState.consumerStates.set(receiver, newConsumerState) + val newState = currentState.with( + "consumerStates", newConsumerStates + ) + Ok(newState) + } + } + + // receives a given packet on the provider. The arguments are the consumer chain that sent the packet, and the packet itself. + // To receive a packet, add it to the list of received maturations. + pure def recvPacketOnProvider(currentState: ProtocolState, sender: Chain, packet: VscMaturedPacket): Result = { + if (not(isRunningConsumer(sender, currentState.providerState))) { + Err("Sender is not currently a consumer - must have 'running' status!") + } else if (currentState.providerState.sentVscPacketsToConsumer.get(sender).head().id != packet.id) { + // the packet is not the oldest sentVscPacket, something went wrong + Err("Received maturation is not for the oldest sentVscPacket") + } else { + val currentReceivedMaturations = currentState.providerState.receivedMaturations + val newReceivedMaturations = currentReceivedMaturations.union(Set(packet)) + val newProviderState = currentState.providerState.with( + "receivedMaturations", newReceivedMaturations + ) + // prune the sentVscPacket + val newSentVscPacket = currentState.providerState.sentVscPacketsToConsumer.get(sender).tail() + val newState = currentState.with( + "providerState", + {...newProviderState, + sentVscPacketsToConsumer: currentState.providerState.sentVscPacketsToConsumer.set(sender, newSentVscPacket) + } + ) + + // prune assigned keys that are no longer needed + + // get the keys that should be pruned + pure val consumerAddrsToPrune = + currentState.providerState.consumerAddrsToPrune + .getOrElse(sender, Map()) + .getOrElse(packet.id, List()).toSet() + + // actually do the pruning + pure val senderValByConsAddr = + // for the sender chain, get the consAddrToValidator mapping + newState.providerState.consumerAddrToValidator.getOrElse(sender, Map()) + pure val newSenderValByConsAddr = + senderValByConsAddr.keys().filter( + // filter out the assigned keys that should be pruned + consAddr => not(consumerAddrsToPrune.contains(consAddr)) + ).mapBy( + // rebuild the map with the pruned keys removed + consAddr => senderValByConsAddr.get(consAddr) + ) + + // update the provider state + pure val newProviderState2 = newState.providerState.with( + // update the consumerAddrToValidator map to remove the pruned keys + "consumerAddrToValidator", + newState.providerState.consumerAddrToValidator.put(sender, newSenderValByConsAddr) + ).with( + // delete the consumer addresses to prune, since they are pruned now + "consumerAddrsToPrune", + newState.providerState.consumerAddrsToPrune.put( + sender, + newState.providerState.consumerAddrsToPrune.getOrElse(sender, Map()).put( + packet.id, + List() + ) + ) + ) + + // update the state + pure val newState2 = newState.with( + "providerState", newProviderState2 + ) + + Ok(newState2) + } + } + + // removes the oldest outstanding packet from the consumer. on-chain, this would happen when the packet is acknowledged. + // only the oldest packet can be removed, since we model ordered channels. + pure def removeOutstandingPacketFromConsumer(currentState: ProtocolState, sender: Chain): ProtocolState = { + val currentOutstandingPackets = currentState.consumerStates.get(sender).outstandingPacketsToProvider + val newOutstandingPackets = currentOutstandingPackets.tail() + val newConsumerState = currentState.consumerStates.get(sender).with( + "outstandingPacketsToProvider", newOutstandingPackets + ) + val newConsumerStates = currentState.consumerStates.set(sender, newConsumerState) + val newState = currentState.with( + "consumerStates", newConsumerStates + ) + newState + } + + // removes the oldest outstanding packet (to the given consumer) from the provider. + // on-chain, this would happen when the packet is acknowledged. + // only the oldest packet can be removed, since we model ordered channels. + pure def removeOutstandingPacketFromProvider(currentState: ProtocolState, receiver: Chain): ProtocolState = { + val currentOutstandingPackets = currentState.providerState.outstandingPacketsToConsumer.get(receiver) + val newOutstandingPackets = currentOutstandingPackets.tail() + val newProviderState = currentState.providerState.with( + "outstandingPacketsToConsumer", + currentState.providerState.outstandingPacketsToConsumer.set(receiver, newOutstandingPackets) + ) + val newState = currentState.with( + "providerState", newProviderState + ) + newState + } + + // Returns a ProtocolState where the current validator set on the provider is set to + // newValidatorSet. + pure def setProviderValidatorSet(currentState: ProtocolState, newValidatorSet: ValidatorSet): ProtocolState = { + pure val newChainState = currentState.providerState.chainState.with( + "currentValidatorSet", newValidatorSet + ) + currentState.with( + "providerState", + currentState.providerState.with( + "chainState", newChainState + ) + ) + } + + // Returns true if the given chain is currently a running consumer, false otherwise. + pure def isRunningConsumer(chain: Chain, providerState: ProviderState): bool = { + val status = providerState.consumerStatus.get(chain) + status == RUNNING + } + + // Returns the set of all consumer chains that currently have the status RUNNING. + pure def getRunningConsumers(providerState: ProviderState): Set[Chain] = { + providerState.consumerStatus.keys().filter( + chain => providerState.consumerStatus.get(chain) == RUNNING + ) + } + + // Returns the set of all consumer chains that currently have the status NOT_CONSUMER. + pure def getNonConsumers(providerState: ProviderState): Set[Chain] = { + providerState.consumerStatus.keys().filter( + chain => providerState.consumerStatus.get(chain) == NOT_CONSUMER + ) + } + + // Returns whether the consumer has timed out due to the vscTimeout, and an error message. + // If the second return is not equal to "", the first return should be ignored. + // If it is equal to "", the first return will be true if the consumer has timed out and should be dropped, + // or false otherwise. + pure def TimeoutDueToVscTimeout(currentState: ProtocolState, consumer: Chain, vscTimeout: Time): (bool, str) = + // check for errors: the consumer is not running + if (not(isRunningConsumer(consumer, currentState.providerState))) { + (false, "Consumer is not currently a consumer - must have 'running' status!") + } else { + val providerState = currentState.providerState + val consumerState: ConsumerState = currentState.consumerStates.get(consumer) + + // has a packet been sent on the provider more than vscTimeout ago, but we have not received an answer since then? + val sentVscPacketsToConsumer = providerState.sentVscPacketsToConsumer.get(consumer) + if(sentVscPacketsToConsumer.length() > 0) { + val oldestSentVscPacket = sentVscPacketsToConsumer.head() // if length is 0, this is undefined, but we check for this before we use it + if(oldestSentVscPacket.sendingTime + vscTimeout < providerState.chainState.runningTimestamp) { + (true, "") + } else { + // no timeout yet, it has not been vscTimeout since that packet was sent + (false, "") + } + } else { + // no packet has been sent yet, so no timeout + (false, "") + } + } + + +} + +module ccv { + // Implements the core logic of the cross-chain validation protocol. + + // Things that are not modelled: + // * Reward distribution + // * Slashes + + // Things that explicitly are modelled: + // * Validator set changes are propagated from provider to consumers + // * Vsc packets mature + + // We assume that packet receive + ack happen synchronously, + // i.e. when the packet is delivered, the ack is delivered right afterwards. + // This is because it is nontrivial in practice to get a relayer to relay a packet, but not its ack. + + import Time.* from "./libraries/Time" + import extraSpells.* from "./libraries/extraSpells" + import ccv_types.* + + + // =================== + // PROTOCOL PARAMETERS + // =================== + + // the set of all possible consumer chains. + const ConsumerChains: Set[Chain] + + // For each chain, this defines the time between the initiation of an unbonding and its maturation. + const UnbondingPeriodPerChain: Chain -> int + + // The maximum time duration between sending any VscPacket to any consumer chain and receiving the + // corresponding VscMaturedPacket, without timing out the consumer chain and consequently removing it. + const VscTimeout: int + + // The timeoutTimestamp for sent packets. Can differ by chain. + const CcvTimeout: Chain -> int + + // The trusting period on each chain. + // If headers on a channel between two chains are not updated within this period, + // they expire and the channel will be closed. + const TrustingPeriodPerChain: Chain -> int + + // =================== + // PROTOCOL LOGIC contains the meat of the protocol + // functions here roughly correspond to API calls that can be triggered from external sources + // =================== + + // the power of a validator on the provider chain is changed by the given amount. We do not care how this happens, + // e.g. via undelegations, or delegations, ... + pure def votingPowerChange(currentState: ProtocolState, validator: Node, amount: int): Result = { + pure val currentValidatorSet = currentState.providerState.chainState.currentValidatorSet + pure val oldVotingPower = if (currentValidatorSet.keys().contains(validator)) currentValidatorSet.get(validator) else 0 + if (amount == 0) { + Err("Voting power cannot change by zero!") + } else if (oldVotingPower == 0) { + Err("Voting power cannot be changed for a validator that is not in the current validator set!") + } else { + pure val newVotingPower = oldVotingPower + amount + pure val newValidatorSet = currentValidatorSet.put(validator, if(newVotingPower >= 0) newVotingPower else 0) + // if the new validator set contains no validators with positive voting power, the validator set is invalid + if (newValidatorSet.values().filter(votingPower => votingPower > 0).size() == 0) { + Err("Voting power change resulted in empty validator set!") + } else { + // set the validator set changed flag + val newProviderState = currentState.providerState.with( + "providerValidatorSetChangedInThisBlock", true + ) + pure val tmpState = currentState.with( + "providerState", newProviderState + ) + pure val newState = setProviderValidatorSet(tmpState, newValidatorSet) + Ok(newState) } - val newConsumerStates = currentState.consumerStates.set(receiver, newConsumerState) - val newState = currentState.with( - "consumerStates", newConsumerStates - ) - Ok(newState) - } + } } - // receives a given packet on the provider. The arguments are the consumer chain that sent the packet, and the packet itself. - // To receive a packet, add it to the list of received maturations. - pure def recvPacketOnProvider(currentState: ProtocolState, sender: Chain, packet: VscMaturedPacket): Result = { + // Delivers the next queued VscMaturedPacket from a consumer chain to the provider chain. + // Arguments are the currentState and the the consumer chain, from which the packet will be delivered. + // If this packet will time out on the provider on delivery, + // the consumer will be dropped. + // The first return is the result of the operation, the second result is a boolean + // that indicates whether the consumer timed out or not. + // If the result has an error, the second return should be ignored. + pure def deliverPacketToProvider(currentState: ProtocolState, sender: Chain): (Result, bool) = { if (not(isRunningConsumer(sender, currentState.providerState))) { - Err("Sender is not currently a consumer - must have 'running' status!") - } else if (currentState.providerState.sentVscPacketsToConsumer.get(sender).head().id != packet.id) { - // the packet is not the oldest sentVscPacket, something went wrong - Err("Received maturation is not for the oldest sentVscPacket") + (Err("Sender is not currently a consumer - must have 'running' status!"), false) + } else if (length(currentState.consumerStates.get(sender).outstandingPacketsToProvider) == 0) { + (Err("No outstanding packets to deliver"), false) } else { - val currentReceivedMaturations = currentState.providerState.receivedMaturations - val newReceivedMaturations = currentReceivedMaturations.union(Set(packet)) - val newProviderState = currentState.providerState.with( - "receivedMaturations", newReceivedMaturations - ) - // prune the sentVscPacket - val newSentVscPacket = currentState.providerState.sentVscPacketsToConsumer.get(sender).tail() - val newState = currentState.with( - "providerState", - {...newProviderState, - sentVscPacketsToConsumer: currentState.providerState.sentVscPacketsToConsumer.set(sender, newSentVscPacket) - } - ) - - // prune assigned keys that are no longer needed - - // get the keys that should be pruned - pure val consumerAddrsToPrune = - currentState.providerState.consumerAddrsToPrune - .getOrElse(sender, Map()) - .getOrElse(packet.id, List()).toSet() - - // actually do the pruning - pure val senderValByConsAddr = - // for the sender chain, get the consAddrToValidator mapping - newState.providerState.consumerAddrToValidator.getOrElse(sender, Map()) - pure val newSenderValByConsAddr = - senderValByConsAddr.keys().filter( - // filter out the assigned keys that should be pruned - consAddr => not(consumerAddrsToPrune.contains(consAddr)) - ).mapBy( - // rebuild the map with the pruned keys removed - consAddr => senderValByConsAddr.get(consAddr) + val packet = currentState.consumerStates.get(sender).outstandingPacketsToProvider.head() + if(packet.timeoutTime <= currentState.providerState.chainState.runningTimestamp) { + // drop consumer + val result = stopConsumers( + currentState.providerState.consumerStatus, + Set(), + Set(sender) ) - // update the provider state - pure val newProviderState2 = newState.providerState.with( - // update the consumerAddrToValidator map to remove the pruned keys - "consumerAddrToValidator", - newState.providerState.consumerAddrToValidator.put(sender, newSenderValByConsAddr) - ).with( - // delete the consumer addresses to prune, since they are pruned now - "consumerAddrsToPrune", - newState.providerState.consumerAddrsToPrune.put( - sender, - newState.providerState.consumerAddrsToPrune.getOrElse(sender, Map()).put( - packet.id, - List() + val newConsumerStatus = result._1 + val err = result._2 + if (err != "") { + (Err(err), false) + } else { + val newProviderState = currentState.providerState.with( + "consumerStatus", newConsumerStatus ) - ) - ) + val newState: ProtocolState = currentState.with( + "providerState", newProviderState + ) + (Ok(newState), true) // true because the packet timed out + } + } else { + // the packet has not timed out, so receive it on the provider + val result = recvPacketOnProvider(currentState, sender, packet) + val tmpState = result.newState + if (result.hasError()) { + (result, false) + } else { + (Ok(removeOutstandingPacketFromConsumer(tmpState, sender)), false) // false because the packet did not time out + } + } + } + } - // update the state - pure val newState2 = newState.with( - "providerState", newProviderState2 - ) + // Delivers the next queued VscPacket from the provider chain to a consumer chain. + // Arguments are the current state and the consumer chain, to which the packet will be delivered. + // If this packet will time out on the consumer on delivery, + // the consumer will be dropped. + // The first return is the result of the operation, the second result is a boolean + // that indicates whether the consumer timed out or not. + // If the result has an error, the second return should be ignored. + pure def deliverPacketToConsumer(currentState: ProtocolState, receiver: Chain): (Result, bool) = { + if (not(isRunningConsumer(receiver, currentState.providerState))) { + (Err("Receiver is not currently a consumer - must have 'running' status!"), false) + } else if (length(currentState.providerState.outstandingPacketsToConsumer.get(receiver)) == 0) { + (Err("No outstanding packets to deliver"), false) + } else { + val packet = currentState.providerState.outstandingPacketsToConsumer.get(receiver).head() + // check if the consumer timed out + if (packet.timeoutTime <= currentState.consumerStates.get(receiver).chainState.runningTimestamp) { + // drop consumer + val result = stopConsumers( + currentState.providerState.consumerStatus, + Set(), + Set(receiver) + ) - Ok(newState2) + val newConsumerStatus = result._1 + val err = result._2 + if (err != "") { + (Err(err), false) + } else { + val newProviderState = currentState.providerState.with( + "consumerStatus", newConsumerStatus + ) + val newState: ProtocolState = currentState.with( + "providerState", newProviderState + ) + (Ok(newState), true) // true because the packet timed out + } + } else { + // the packet has not timed out, so receive it on the consumer + val result = recvPacketOnConsumer(currentState, receiver, packet, UnbondingPeriodPerChain.get(receiver)) + val tmpState = result.newState + if (result.hasError()) { + (result, false) + } else { + (Ok(removeOutstandingPacketFromProvider(tmpState, receiver)), false) // false because the packet did not time out + } + } } } - // removes the oldest outstanding packet from the consumer. on-chain, this would happen when the packet is acknowledged. - // only the oldest packet can be removed, since we model ordered channels. - pure def removeOutstandingPacketFromConsumer(currentState: ProtocolState, sender: Chain): ProtocolState = { - val currentOutstandingPackets = currentState.consumerStates.get(sender).outstandingPacketsToProvider - val newOutstandingPackets = currentOutstandingPackets.tail() - val newConsumerState = currentState.consumerStates.get(sender).with( - "outstandingPacketsToProvider", newOutstandingPackets + + + /// Ends a block on the provider. This means that the current validator set is committed on chain, + /// packets are queued, and the next block is started. Also, consumers that have passed + /// the VscTimeout without responding to a pending vscpacket are dropped. + pure def endAndBeginBlockForProvider( + currentState: ProtocolState, + // by how much the timestamp should be advanced, + // i.e. the timestamp for the next block is oldTimestamp + timeAdvancement + timeAdvancement: Time, + // a set of consumers that were not consumers before, but should be set to running now. + consumersToStart: Set[Chain], + // a set of consumers that were running before, but should be set to stopped now. + // This argument only needs to contain "voluntary" stops - + // forced stops, e.g. because a consumer timed out, + // will be added automatically. + consumersToStop: Set[Chain]): Result = { + val currentProviderState = currentState.providerState + + // check for vsc timeouts + val timedOutConsumers = getRunningConsumers(currentProviderState).filter( + consumer => + val res = TimeoutDueToVscTimeout(currentState, consumer, VscTimeout) + res._1 + ) + + // for each consumer chain, apply the key assignment to the current validator set + val currentValSets = ConsumerChains.mapBy( + (consumer) => + currentProviderState.applyKeyAssignmentToValSet( + consumer, + currentProviderState.chainState.currentValidatorSet + ) + ) + // store the current validator set with the key assignments applied in the history + val newKeyAssignedValSetHistory = currentValSets.keys().mapBy( + (consumer) => + currentProviderState.keyAssignedValSetHistory + .getOrElse(consumer, List()) // get the existing history (empty list if no history yet) + .prepend(currentValSets.get(consumer)) // prepend the current validator set with key assignments applied ) - val newConsumerStates = currentState.consumerStates.set(sender, newConsumerState) - val newState = currentState.with( - "consumerStates", newConsumerStates + + // run the shared core chainState logic + val newChainState = currentProviderState.chainState.endAndBeginBlockShared(timeAdvancement) + val providerStateAfterTimeAdvancement = + {...currentProviderState, chainState: newChainState, keyAssignedValSetHistory: newKeyAssignedValSetHistory} + val tmpState = currentState.with( + "providerState", providerStateAfterTimeAdvancement ) - newState - } + - // removes the oldest outstanding packet (to the given consumer) from the provider. - // on-chain, this would happen when the packet is acknowledged. - // only the oldest packet can be removed, since we model ordered channels. - pure def removeOutstandingPacketFromProvider(currentState: ProtocolState, receiver: Chain): ProtocolState = { - val currentOutstandingPackets = currentState.providerState.outstandingPacketsToConsumer.get(receiver) - val newOutstandingPackets = currentOutstandingPackets.tail() - val newProviderState = currentState.providerState.with( - "outstandingPacketsToConsumer", - currentState.providerState.outstandingPacketsToConsumer.set(receiver, newOutstandingPackets) + // send vsc packets (will be a noop if no sends are necessary) + val providerStateAfterSending = + providerStateAfterTimeAdvancement.sendVscPackets( + currentProviderState.chainState.runningTimestamp, + CcvTimeout.get(PROVIDER_CHAIN) + ) + + + // start/stop chains + val res = providerStateAfterSending.consumerStatus.StartStopConsumers( + consumersToStart, + consumersToStop, + timedOutConsumers ) - val newState = currentState.with( - "providerState", newProviderState + val newConsumerStatus = res._1 + val err = res._2 + val providerStateAfterConsumerAdvancement = providerStateAfterSending.with( + "consumerStatus", newConsumerStatus + ).with( + "providerValidatorSetChangedInThisBlock", false ) - newState - } - // Returns a ProtocolState where the current validator set on the provider is set to - // newValidatorSet. - pure def setProviderValidatorSet(currentState: ProtocolState, newValidatorSet: ValidatorSet): ProtocolState = { - pure val newChainState = currentState.providerState.chainState.with( - "currentValidatorSet", newValidatorSet - ) - currentState.with( - "providerState", - currentState.providerState.with( - "chainState", newChainState + if (err != "") { + Err(err) + } else { + // for each consumer we just set to running, set its initial validator set to be the current one on the provider... + val valSet = providerStateAfterConsumerAdvancement.chainState.currentValidatorSet + val newConsumerStateMap = + tmpState.consumerStates.keys().mapBy( + (consumer) => + if (consumersToStart.contains(consumer)) { + // ...modified by the key assignments for the consumer + val consValSet = applyKeyAssignmentToValSet(providerStateAfterConsumerAdvancement, consumer, valSet) + val currentConsumerState: ConsumerState = tmpState.consumerStates.get(consumer) + val newConsumerState: ConsumerState = currentConsumerState.with( + "chainState", currentConsumerState.chainState.with( + "currentValidatorSet", consValSet + ).with( + "votingPowerHistory", + List(consValSet) + ).with( + "lastTimestamp", + providerStateAfterConsumerAdvancement.chainState.lastTimestamp + ).with( + "runningTimestamp", + providerStateAfterConsumerAdvancement.chainState.runningTimestamp + ) + ) + newConsumerState + } else { + currentState.consumerStates.get(consumer) + } + ) + val newState = tmpState.with( + "providerState", providerStateAfterConsumerAdvancement + ).with( + "consumerStates", newConsumerStateMap ) - ) - } - // Returns true if the given chain is currently a running consumer, false otherwise. - pure def isRunningConsumer(chain: Chain, providerState: ProviderState): bool = { - val status = providerState.consumerStatus.get(chain) - status == RUNNING + Ok(newState) + } } - // Returns the set of all consumer chains that currently have the status RUNNING. - pure def getRunningConsumers(providerState: ProviderState): Set[Chain] = { - providerState.consumerStatus.keys().filter( - chain => providerState.consumerStatus.get(chain) == RUNNING - ) - } + pure def endAndBeginBlockForConsumer( + currentState: ProtocolState, + chain: Chain, + // by how much the timestamp of the chain should be advanced for the next block + timeAdvancement: Time): Result = { + if (not(currentState.consumerStates.keys().contains(chain))) { + // if the chain is not a consumer, return an error + Err("chain is not a consumer") + } else { + val currentConsumerState: ConsumerState = currentState.consumerStates.get(chain) + val oldChainState: ChainState = currentConsumerState.chainState + val newChainState: ChainState = currentConsumerState.chainState.endAndBeginBlockShared(timeAdvancement) + val newConsumerState: ConsumerState = currentConsumerState.with( + "chainState", newChainState + ) + val maturedPackets = newConsumerState.maturationTimes.select( + pair => + val packet = pair._1 + val maturationTime: Time = pair._2 + // important: this uses the last committed timestamp, not the running timestamp! + maturationTime <= newChainState.lastTimestamp + ).transform(pair => pair._1) + val newMaturationTimes = newConsumerState.maturationTimes.select( + pair => + val packet = pair._1 + val maturationTime: Time = pair._2 + // important: this uses the last committed timestamp, not the running timestamp! - // Returns the set of all consumer chains that currently have the status NOT_CONSUMER. - pure def getNonConsumers(providerState: ProviderState): Set[Chain] = { - providerState.consumerStatus.keys().filter( - chain => providerState.consumerStatus.get(chain) == NOT_CONSUMER - ) + maturationTime > newChainState.lastTimestamp + ) + val newOutstandingPackets = newConsumerState.outstandingPacketsToProvider.concat( + maturedPackets.transform( + packet => { + id: packet.id, + // it is important to use the oldChainState here, since this happens during EndBlock + sendingTime: oldChainState.runningTimestamp, + timeoutTime: oldChainState.runningTimestamp + CcvTimeout.get(chain) + } + ) + ) + val newConsumerState2: ConsumerState = newConsumerState.with( + "maturationTimes", newMaturationTimes + ).with( + "outstandingPacketsToProvider", newOutstandingPackets + ) + val newConsumerStates = currentState.consumerStates.set(chain, newConsumerState2) + val newState: ProtocolState = currentState.with( + "consumerStates", newConsumerStates + ) + Ok(newState) + } } - // Returns whether the consumer has timed out due to the VscTimeout, and an error message. - // If the second return is not equal to "", the first return should be ignored. - // If it is equal to "", the first return will be true if the consumer has timed out and should be dropped, - // or false otherwise. - pure def TimeoutDueToVscTimeout(currentState: ProtocolState, consumer: Chain): (bool, str) = - // check for errors: the consumer is not running - if (not(isRunningConsumer(consumer, currentState.providerState))) { - (false, "Consumer is not currently a consumer - must have 'running' status!") + // Validator providerNode assigns their address for the consumer to be the consumerAddress. + pure def assignConsumerKey(currentState: ProtocolState, consumer: Chain, providerNode: Node, consumerAddr: ConsumerAddr): Result = { + // rule 1: validator A cannot assign consumer key K to consumer chain X + // if there is already a validator B (B!=A) using K on the provider + pure val provCurValSet = currentState.providerState.chainState.currentValidatorSet + if (provCurValSet.keys().exists(node => node != providerNode and node == consumerAddr)) { + Err("validator A cannot assign consumer key K to consumer chain X + if there is already a validator B (B!=A) using K on the provider") } else { - val providerState = currentState.providerState - val consumerState: ConsumerState = currentState.consumerStates.get(consumer) - - // has a packet been sent on the provider more than VscTimeout ago, but we have not received an answer since then? - val sentVscPacketsToConsumer = providerState.sentVscPacketsToConsumer.get(consumer) - if(sentVscPacketsToConsumer.length() > 0) { - val oldestSentVscPacket = sentVscPacketsToConsumer.head() // if length is 0, this is undefined, but we check for this before we use it - if(oldestSentVscPacket.sendingTime + VscTimeout < providerState.chainState.runningTimestamp) { - (true, "") + // rule 2: validator A cannot assign consumer key K to consumer chain X if + // there is already a validator B using K on X + pure val valByConsAddr = currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()) + if (valByConsAddr.keys().contains(consumerAddr)) { + Err("consumer key is already in use on the consumer chain") + } else { + // this key can be assigned + + // get the old assigned key + pure val consKeyByVal = currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()) + pure val p = if (consKeyByVal.keys().contains(providerNode)) { + // providerNode had previously assigned a consumer key + (consKeyByVal.get(providerNode), true) } else { - // no timeout yet, it has not been VscTimeout since that packet was sent - (false, "") + (providerNode, false) } - } else { - // no packet has been sent yet, so no timeout - (false, "") + // the consumer address that was previously associated with the node + pure val oldConsAddr = p._1 + // whether the old address was explicitly assigned, or the default key + pure val prevAssigned = p._2 + + // set the old address for pruning, if it was assigned + pure val tmpState = if (prevAssigned) { + AppendConsumerAddrToPrune(currentState, oldConsAddr, consumer) + } else { + currentState + } + + // check whether the validator has positive power + pure val provValSet = currentState.providerState.chainState.currentValidatorSet + pure val provValPower = if (provValSet.keys().contains(providerNode)) provValSet.get(providerNode) else 0 + pure val consumersWithAddrAssignmentChangesInThisBlock = + if (provValPower > 0) { + // if the consumer has positive power, the relevant key assignment for the consumer changed + currentState.providerState.consumersWithAddrAssignmentChangesInThisBlock.union(Set(consumer)) + } else { + // otherwise, the consumer doesn't need to know about the change, so no change + currentState.providerState.consumersWithAddrAssignmentChangesInThisBlock + } + pure val tmpStateAfterKeyAssignmentReplacement = tmpState.with( + "providerState", tmpState.providerState.with( + "consumersWithAddrAssignmentChangesInThisBlock", consumersWithAddrAssignmentChangesInThisBlock + ) + ) + + pure val newvalidatorToConsumerAddr = currentState.providerState.validatorToConsumerAddr.put( + consumer, + currentState.providerState.validatorToConsumerAddr.getOrElse(consumer, Map()).put( + providerNode, + consumerAddr + ) + ) + + pure val newconsumerAddrToValidator = currentState.providerState.consumerAddrToValidator.put( + consumer, + currentState.providerState.consumerAddrToValidator.getOrElse(consumer, Map()).put( + consumerAddr, + providerNode + ) + ) + + pure val newProviderState = tmpStateAfterKeyAssignmentReplacement.providerState.with( + "validatorToConsumerAddr", newvalidatorToConsumerAddr + ).with( + "consumerAddrToValidator", newconsumerAddrToValidator + ) + + Ok( + tmpStateAfterKeyAssignmentReplacement.with( + "providerState", newProviderState + ) + ) } } + } // =================== // ASSUMPTIONS ON MODEL PARAMETERS