Skip to content

Commit

Permalink
Shared state with light store and in memory store implementation.
Browse files Browse the repository at this point in the history
  • Loading branch information
OStevan authored Jul 6, 2020
1 parent 2a1a2f9 commit f2abdcb
Show file tree
Hide file tree
Showing 7 changed files with 171 additions and 39 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VerificationErrors.Ve
import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VerificationOutcomes._
import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VerifierStates._
import ch.epfl.ognjanovic.stevan.tendermint.verified.types.LightBlock
import stainless.lang.StaticChecks.Ensuring
import stainless.lang._
import stainless.lang.StaticChecks.Ensuring

case class MultiStepVerifier(
lightBlockProvider: LightBlockProvider,
Expand All @@ -19,20 +19,25 @@ case class MultiStepVerifier(

def verifyUntrusted(trustedState: TrustedState, untrustedState: UntrustedState): Finished = {
require(
trustedState.currentHeight() < untrustedState.targetLimit &&
trustedState.currentHeight() <= untrustedState.targetLimit &&
untrustedState.bottomHeight().isEmpty &&
untrustedState.targetLimit <= lightBlockProvider.currentHeight)

val nextHeight =
if (trustedState.currentHeight() + 1 == untrustedState.targetLimit)
untrustedState.targetLimit
else
heightCalculator.nextHeight(trustedState.currentHeight(), untrustedState.targetLimit)
if (trustedState.currentHeight() == untrustedState.targetLimit)
Finished(Left(()), trustedState, untrustedState)
else {

assert(untrustedState.bottomHeight().map(nextHeight < _).getOrElse(true))
assert(trustedState.currentHeight() < nextHeight)
assert(nextHeight <= untrustedState.targetLimit)
verify(WaitingForHeader(nextHeight, trustedState, untrustedState))
val nextHeight =
if (trustedState.currentHeight() + 1 == untrustedState.targetLimit)
untrustedState.targetLimit
else
heightCalculator.nextHeight(trustedState.currentHeight(), untrustedState.targetLimit)

assert(untrustedState.bottomHeight().map(nextHeight < _).getOrElse(true))
assert(trustedState.currentHeight() < nextHeight)
assert(nextHeight <= untrustedState.targetLimit)
verify(WaitingForHeader(nextHeight, trustedState, untrustedState))
}
}

@scala.annotation.tailrec
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -8,13 +8,14 @@ object TrustedStates {

abstract class TrustedState {

/**
* The height of the last block that we trust.
*/
@pure
def currentHeight(): Height = {
??? : Height
}.ensuring(res => res == trustedLightBlock.header.height)
def trusted(lightBlock: LightBlock): Boolean = {
require(lightBlock.header.height > currentHeight())
??? : Boolean
}

@pure
def trustedLightBlock: LightBlock

/**
* Tries to "improve" the current trusted state with addition of a new signed header of a greater height.
Expand All @@ -28,23 +29,22 @@ object TrustedStates {
??? : TrustedState
}.ensuring(res => res.currentHeight() > currentHeight() && res.currentHeight() == lightBlock.header.height)

/**
* The height of the last block that we trust.
*/
@pure
def currentHeight(): Height = {
trustedLightBlock.header.height
}.ensuring(res => res == trustedLightBlock.header.height)

@pure
def isAdjacent(lightBlock: LightBlock): Boolean = {
require(currentHeight() < lightBlock.header.height)
??? : Boolean
lightBlock.header.height == trustedLightBlock.header.height + 1
}.ensuring(res =>
(res && currentHeight() + 1 == lightBlock.header.height) ||
(!res && currentHeight() + 1 < lightBlock.header.height))

@pure
def trusted(lightBlock: LightBlock): Boolean = {
require(lightBlock.header.height > currentHeight())
??? : Boolean
}

@pure
def trustedLightBlock: LightBlock

}

case class SimpleTrustedState(trustedLightBlock: LightBlock, trustVerifier: VotingPowerVerifier)
Expand All @@ -59,10 +59,6 @@ object TrustedStates {
SimpleTrustedState(lightBlock, trustVerifier)
}.ensuring(res => res.currentHeight() > currentHeight() && res.currentHeight() == lightBlock.header.height)

@pure
override def isAdjacent(lightBlock: LightBlock): Boolean =
lightBlock.header.height == trustedLightBlock.header.height + 1

@pure
override def trusted(lightBlock: LightBlock): Boolean = {
require(lightBlock.header.height > currentHeight())
Expand All @@ -74,13 +70,13 @@ object TrustedStates {

@pure
private def internalAdjacentHeaderTrust(lightBlock: LightBlock): Boolean = {
require(isAdjacent(lightBlock))
require(currentHeight() < lightBlock.header.height && isAdjacent(lightBlock))
trustedLightBlock.nextValidatorSet.toInfoHashable == lightBlock.validatorSet.toInfoHashable
}

@pure
private def internalNonAdjacentHeaderTrust(lightBlock: LightBlock): Boolean = {
require(lightBlock.header.height > this.trustedLightBlock.header.height && !isAdjacent(lightBlock))
require(currentHeight() < lightBlock.header.height && !isAdjacent(lightBlock))

trustVerifier.trustedCommit(trustedLightBlock.nextValidatorSet, lightBlock.commit)
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,16 +4,18 @@ import java.util.concurrent.Executors

import ch.epfl.ognjanovic.stevan.tendermint.light.ForkDetection.{ForkDetector, Forked}
import ch.epfl.ognjanovic.stevan.tendermint.light.MultiStepVerifierFactories.MultiStepVerifierFactory
import ch.epfl.ognjanovic.stevan.tendermint.light.Supervisor.{ForkDetected, NoPrimary, NoWitnesses}
import ch.epfl.ognjanovic.stevan.tendermint.light.Supervisor.{ForkDetected, NoPrimary, NoTrustedState, NoWitnesses}
import ch.epfl.ognjanovic.stevan.tendermint.light.store.{InMemoryLightStore, LightStore, LightStoreBackedTrustedState}
import ch.epfl.ognjanovic.stevan.tendermint.light.LightBlockStatuses.{Trusted, Verified}
import ch.epfl.ognjanovic.stevan.tendermint.verified.fork.{PeerList GenericPeerList}
import ch.epfl.ognjanovic.stevan.tendermint.verified.light.LightBlockProviders.LightBlockProvider
import ch.epfl.ognjanovic.stevan.tendermint.verified.light.TrustedStates.TrustedState
import ch.epfl.ognjanovic.stevan.tendermint.verified.light.UntrustedStates
import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VotingPowerVerifiers.VotingPowerVerifier
import ch.epfl.ognjanovic.stevan.tendermint.verified.types.{Duration, Height, LightBlock, PeerId}
import stainless.lang

import scala.annotation.tailrec
import scala.collection.mutable
import scala.concurrent.{ExecutionContext, ExecutionContextExecutorService, Future}

object EventLoopClient {
Expand All @@ -26,10 +28,15 @@ object EventLoopClient {
private val votingPowerVerifier: VotingPowerVerifier,
private val verifierBuilder: MultiStepVerifierFactory,
private val trustDuration: Duration,
private var trustedState: TrustedState, // currently var, but should be changed with store and recreate a trusted state for verification
private val lightStore: LightStore,
private val forkDetector: ForkDetector)
extends Supervisor {

implicit private val heightOrdering: Ordering[Height] = (x: Height, y: Height) => {
val diff = x.value - y.value
if (diff < 0) -1 else if (diff == 0) 0 else 1
}

override def verifyToHeight(height: Height): Either[LightBlock, Supervisor.Error] = {
val (newPeerList, result) = verifyToTarget(Some(height), peerList)
peerList = newPeerList
Expand All @@ -53,9 +60,19 @@ object EventLoopClient {
peerList: PeerList): (PeerList, Either[LightBlock, Supervisor.Error]) = {
val primaryVerifier = verifierBuilder.constructVerifier(peerList.primary, votingPowerVerifier, trustDuration)

val trustedLightBlock = lightStore.latest(Trusted)

if (trustedLightBlock.isEmpty)
return (peerList, Right(NoTrustedState))

val inMemoryLightStore: LightStore =
new InMemoryLightStore(mutable.SortedMap.empty[Height, LightBlock], mutable.SortedMap.empty, mutable.Map.empty)

val primaryInMemoryBacked = new LightStoreBackedTrustedState(inMemoryLightStore, votingPowerVerifier)

val primaryResult =
primaryVerifier.verifyUntrusted(
trustedState,
primaryInMemoryBacked,
UntrustedStates.empty(height.getOrElse(peerList.primary.currentHeight)))

primaryResult.outcome match {
Expand All @@ -65,7 +82,7 @@ object EventLoopClient {

val forkDetectionResult = forkDetector.detectForks(
primaryResult.trustedState.trustedLightBlock,
trustedState.trustedLightBlock,
trustedLightBlock.get,
peerList.witnesses.map(verifierBuilder.constructVerifier(_, votingPowerVerifier, trustDuration)).toScala
)

Expand All @@ -79,7 +96,7 @@ object EventLoopClient {
verifyToTarget(height, newPeerList)

case ForkDetection.NoForks
trustedState = primaryResult.trustedState
inMemoryLightStore.all(Verified).foreach(lightStore.update(_, Trusted))
(peerList, Left(primaryResult.trustedState.trustedLightBlock))
}
case lang.Right(_)
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
package ch.epfl.ognjanovic.stevan.tendermint.light

object LightBlockStatuses {
sealed trait LightBlockStatus

object Verified extends LightBlockStatus

object Trusted extends LightBlockStatus
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
package ch.epfl.ognjanovic.stevan.tendermint.light.store

import ch.epfl.ognjanovic.stevan.tendermint.light.LightBlockStatuses.{LightBlockStatus, Trusted, Verified}
import ch.epfl.ognjanovic.stevan.tendermint.verified.types.{Height, LightBlock}

import scala.collection.mutable

sealed class InMemoryLightStore(
private val verified: mutable.SortedMap[Height, LightBlock],
private val trusted: mutable.SortedMap[Height, LightBlock],
private val inverse: mutable.Map[Height, LightBlockStatus]
) extends LightStore {

override def get(height: Height, status: LightBlockStatus): Option[LightBlock] = {
statusNamespace(status).get(height)
}

override def update(lightBlock: LightBlock, status: LightBlockStatus): Unit = {
inverse
.get(lightBlock.header.height)
.foreach(previousStatus statusNamespace(previousStatus).remove(lightBlock.header.height))
statusNamespace(status).put(lightBlock.header.height, lightBlock)
inverse.put(lightBlock.header.height, status)
}

override def remove(height: Height): Unit = {
inverse.get(height).foreach(status statusNamespace(status).remove(height))
}

override def latest(status: LightBlockStatus): Option[LightBlock] = {
val map = statusNamespace(status)
map.get(map.lastKey)
}

override def all(status: LightBlockStatus): Iterable[LightBlock] = statusNamespace(status).values

private def statusNamespace(status: LightBlockStatus): mutable.SortedMap[Height, LightBlock] = {
status match {
case Verified verified
case Trusted trusted
}
}

}
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
package ch.epfl.ognjanovic.stevan.tendermint.light.store

import ch.epfl.ognjanovic.stevan.tendermint.light.LightBlockStatuses.LightBlockStatus
import ch.epfl.ognjanovic.stevan.tendermint.verified.types.{Height, LightBlock}

// ported from tendermint-rs
/**
* Implementations need to be stateful.
*/
trait LightStore {
def get(height: Height, status: LightBlockStatus): Option[LightBlock]

def update(lightBlock: LightBlock, status: LightBlockStatus)

def remove(height: Height)

def latest(status: LightBlockStatus): Option[LightBlock]

def all(status: LightBlockStatus): Iterable[LightBlock]
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
package ch.epfl.ognjanovic.stevan.tendermint.light.store

import ch.epfl.ognjanovic.stevan.tendermint.light.LightBlockStatuses.{Trusted, Verified}
import ch.epfl.ognjanovic.stevan.tendermint.verified.light.TrustedStates.TrustedState
import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VotingPowerVerifiers.VotingPowerVerifier
import ch.epfl.ognjanovic.stevan.tendermint.verified.types.LightBlock

class LightStoreBackedTrustedState(private val lightStore: LightStore, private val trustVerifier: VotingPowerVerifier)
extends TrustedState {

override def trusted(lightBlock: LightBlock): Boolean = {
if (!(lightBlock.header.height > currentHeight()))
throw new IllegalArgumentException(
"It is not possible to call this method with a block lower that the latest verified one")

if (isAdjacent(lightBlock))
trustedLightBlock.header.nextValidators == lightBlock.header.validators
else
trustVerifier.trustedCommit(trustedLightBlock.nextValidatorSet, lightBlock.commit)
}

override def trustedLightBlock: LightBlock = {
val possibleTrusted = lightStore.latest(Trusted)
val possibleVerified = lightStore.latest(Verified)

(possibleTrusted, possibleVerified) match {
case (Some(trusted), Some(verified)) if trusted.header.height < verified.header.height
verified
case (Some(trusted), None) trusted
case _ throw new IllegalStateException("Trusted state should never end up in this situation")
}
}

override def increaseTrust(lightBlock: LightBlock): TrustedState = {
if (!(lightBlock.header.height > currentHeight() && trusted(lightBlock)))
throw new IllegalArgumentException("Illegal light block:" + lightBlock)
lightStore.update(lightBlock, Verified)
new LightStoreBackedTrustedState(lightStore, trustVerifier)
}

}

0 comments on commit f2abdcb

Please sign in to comment.