Rename TrustedState to VerifiedState. (#78)

* Update top level name.

* Renamed TrustedState to VerifiedState with all occurrences.

light-client-core/src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/integration/ModelIntegration.scala

@@ -6,7 +6,7 @@ import ch.epfl.ognjanovic.stevan.tendermint.verified.light.CommitValidators.Defa
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.LightBlockProviders.LightBlockProvider
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.LightBlockValidators.DummyLightBlockValidator
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.NextHeightCalculators.NextHeightCalculator
-import ch.epfl.ognjanovic.stevan.tendermint.verified.light.TrustedStates.{SimpleTrustedState, TrustedState}
+import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VerifiedStates.{SimpleVerifiedState, VerifiedState}
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.TrustVerifiers.DefaultTrustVerifier
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.UntrustedStates.InMemoryUntrustedState
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VerificationErrors.VerificationError
@@ -30,11 +30,11 @@ object ModelIntegration {
     val soundSignedHeaderProvider = BlockchainLightBlockProviders(blockchainState)
     val trustedSignedHeader = soundSignedHeaderProvider.lightBlock(trustedHeight)
 
-    val trustedState: TrustedState =
-      SimpleTrustedState(trustedSignedHeader, VotingPowerVerifiers.defaultVotingPowerVerifier)
+    val verifiedState: VerifiedState =
+      SimpleVerifiedState(trustedSignedHeader, VotingPowerVerifiers.defaultVotingPowerVerifier)
     val untrustedState = InMemoryUntrustedState(heightToVerify, List.empty)
     assert(untrustedState.bottomHeight().forall(heightToVerify < _))
-    assert(trustedState.currentHeight() < heightToVerify)
+    assert(verifiedState.currentHeight() < heightToVerify)
     assert(heightToVerify <= untrustedState.targetLimit)
 
     val lightBlockVerifier = DefaultTrustVerifier()
@@ -47,7 +47,7 @@ object ModelIntegration {
         DefaultCommitValidator(VotingPowerVerifiers.defaultVotingPowerVerifier, DummyCommitSignatureVerifier())),
       nextHeightCalculator
     )
-      .verifyUntrusted(trustedState, untrustedState)
+      .verifyUntrusted(verifiedState, untrustedState)
       .outcome
   }
 

light-client-core/src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/light/LightClientLemmas.scala

@@ -10,17 +10,17 @@ object LightClientLemmas {
   @pure
   def terminationMeasure(waitingForHeader: WaitingForHeader): (BigInt, BigInt) = {
     val res: (BigInt, BigInt) = (
-      waitingForHeader.untrustedState.targetLimit.value - waitingForHeader.trustedState.currentHeight().value,
-      waitingForHeader.requestHeight.value - waitingForHeader.trustedState.currentHeight().value
+      waitingForHeader.untrustedState.targetLimit.value - waitingForHeader.verifiedState.currentHeight().value,
+      waitingForHeader.requestHeight.value - waitingForHeader.verifiedState.currentHeight().value
     )
     res
   }.ensuring(res => res._1 >= BigInt(0) && res._2 >= BigInt(0))
 
   @opaque
-  def sameTrustedStateTerminationMeasure(previous: WaitingForHeader, current: WaitingForHeader): Unit = {
+  def sameVerifiedStateTerminationMeasure(previous: WaitingForHeader, current: WaitingForHeader): Unit = {
     require(
       previous.untrustedState.targetLimit == current.untrustedState.targetLimit &&
-        previous.trustedState.currentHeight() == current.trustedState.currentHeight() &&
+        previous.verifiedState.currentHeight() == current.verifiedState.currentHeight() &&
         previous.requestHeight > current.requestHeight)
   }.ensuring { _ =>
     val previousTerminationMeasure = terminationMeasure(previous)
@@ -31,10 +31,10 @@ object LightClientLemmas {
   }
 
   @opaque
-  def improvedTrustedStateLemma(previous: WaitingForHeader, current: WaitingForHeader): Unit = {
+  def improvedVerifiedStateLemma(previous: WaitingForHeader, current: WaitingForHeader): Unit = {
     require(
       previous.untrustedState.targetLimit == current.untrustedState.targetLimit &&
-        previous.trustedState.currentHeight() < current.trustedState.currentHeight())
+        previous.verifiedState.currentHeight() < current.verifiedState.currentHeight())
   }.ensuring { _ =>
     val previousTerminationMeasure = terminationMeasure(previous)
     val currentTerminationMeasure = terminationMeasure(current)

light-client-core/src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/light/MultiStepVerifier.scala

@@ -3,7 +3,7 @@ package ch.epfl.ognjanovic.stevan.tendermint.verified.light
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.LightBlockProviders.LightBlockProvider
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.LightClientLemmas._
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.NextHeightCalculators.NextHeightCalculator
-import ch.epfl.ognjanovic.stevan.tendermint.verified.light.TrustedStates.TrustedState
+import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VerifiedStates.VerifiedState
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.UntrustedStates.UntrustedState
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VerificationErrors.VerificationError
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VerificationOutcomes._
@@ -17,22 +17,22 @@ case class MultiStepVerifier(
   verifier: Verifier,
   heightCalculator: NextHeightCalculator) {
 
-  def verifyUntrusted(trustedState: TrustedState, untrustedState: UntrustedState): Finished = {
+  def verifyUntrusted(verifiedState: VerifiedState, untrustedState: UntrustedState): Finished = {
     require(
-      trustedState.currentHeight() <= untrustedState.targetLimit &&
+      verifiedState.currentHeight() <= untrustedState.targetLimit &&
         untrustedState.bottomHeight().isEmpty &&
         untrustedState.targetLimit <= lightBlockProvider.currentHeight)
 
-    if (trustedState.currentHeight() == untrustedState.targetLimit)
-      Finished(Left(()), trustedState, untrustedState)
+    if (verifiedState.currentHeight() == untrustedState.targetLimit)
+      Finished(Left(()), verifiedState, untrustedState)
     else {
 
       val nextHeight = untrustedState.targetLimit
 
       assert(untrustedState.bottomHeight().map(nextHeight < _).getOrElse(true))
-      assert(trustedState.currentHeight() < nextHeight)
+      assert(verifiedState.currentHeight() < nextHeight)
       assert(nextHeight <= untrustedState.targetLimit)
-      verify(WaitingForHeader(nextHeight, trustedState, untrustedState))
+      verify(WaitingForHeader(nextHeight, verifiedState, untrustedState))
     }
   }
 
@@ -50,13 +50,13 @@ case class MultiStepVerifier(
   private def processHeader(waitingForHeader: WaitingForHeader, lightBlock: LightBlock): VerifierState = {
     require(lightBlock.header.height == waitingForHeader.requestHeight)
 
-    stepByStepVerification(lightBlock, waitingForHeader.trustedState, waitingForHeader.untrustedState)
+    stepByStepVerification(lightBlock, waitingForHeader.verifiedState, waitingForHeader.untrustedState)
   }.ensuring {
     case state: WaitingForHeader =>
-      if (waitingForHeader.trustedState.currentHeight() == state.trustedState.currentHeight())
-        sameTrustedStateTerminationMeasure(waitingForHeader, state)
+      if (waitingForHeader.verifiedState.currentHeight() == state.verifiedState.currentHeight())
+        sameVerifiedStateTerminationMeasure(waitingForHeader, state)
       else
-        improvedTrustedStateLemma(waitingForHeader, state)
+        improvedVerifiedStateLemma(waitingForHeader, state)
 
       val previousTerminationMeasure = terminationMeasure(waitingForHeader)
       val currentTerminationMeasure = terminationMeasure(state)
@@ -70,48 +70,48 @@ case class MultiStepVerifier(
 
   private def stepByStepVerification(
     lightBlock: LightBlock,
-    trustedState: TrustedState,
+    verifiedState: VerifiedState,
     untrustedState: UntrustedState): VerifierState = {
     require(
       lightBlock.header.height <= untrustedState.targetLimit &&
-        trustedState.currentHeight() < lightBlock.header.height &&
+        verifiedState.currentHeight() < lightBlock.header.height &&
         untrustedState.bottomHeight().map(lightBlock.header.height < _).getOrElse(true))
-    decreases(untrustedState.targetLimit.value - trustedState.currentHeight().value)
+    decreases(untrustedState.targetLimit.value - verifiedState.currentHeight().value)
 
-    verifier.verify(trustedState, lightBlock) match {
+    verifier.verify(verifiedState, lightBlock) match {
       case VerificationOutcomes.Success =>
-        val newTrustedState = trustedState.increaseTrust(lightBlock)
-        if (newTrustedState.currentHeight() == untrustedState.targetLimit) {
+        val newVerifiedState = verifiedState.increaseTrust(lightBlock)
+        if (newVerifiedState.currentHeight() == untrustedState.targetLimit) {
           val result = Left[Unit, VerificationError](())
-          Finished(result, newTrustedState, untrustedState)
-        } else if (untrustedState.hasNextHeader(newTrustedState.currentHeight(), untrustedState.targetLimit)) {
+          Finished(result, newVerifiedState, untrustedState)
+        } else if (untrustedState.hasNextHeader(newVerifiedState.currentHeight(), untrustedState.targetLimit)) {
           val (nextLightBlock, nextUntrustedState) = untrustedState.removeBottom()
-          stepByStepVerification(nextLightBlock, newTrustedState, nextUntrustedState)
-        } else if (newTrustedState.currentHeight() + 1 == untrustedState.targetLimit)
-          WaitingForHeader(untrustedState.targetLimit, newTrustedState, untrustedState)
+          stepByStepVerification(nextLightBlock, newVerifiedState, nextUntrustedState)
+        } else if (newVerifiedState.currentHeight() + 1 == untrustedState.targetLimit)
+          WaitingForHeader(untrustedState.targetLimit, newVerifiedState, untrustedState)
         else {
           val newTargetHeight = heightCalculator.nextHeight(
-            newTrustedState.currentHeight(),
+            newVerifiedState.currentHeight(),
             untrustedState.bottomHeight().getOrElse(untrustedState.targetLimit))
-          WaitingForHeader(newTargetHeight, newTrustedState, untrustedState)
+          WaitingForHeader(newTargetHeight, newVerifiedState, untrustedState)
         }
 
       case VerificationOutcomes.InsufficientTrust =>
-        val nextHeight = heightCalculator.nextHeight(trustedState.currentHeight(), lightBlock.header.height)
+        val nextHeight = heightCalculator.nextHeight(verifiedState.currentHeight(), lightBlock.header.height)
         val nextUntrustedState = untrustedState.insertLightBlock(lightBlock)
-        WaitingForHeader(nextHeight, trustedState, nextUntrustedState)
+        WaitingForHeader(nextHeight, verifiedState, nextUntrustedState)
 
       case Failure(reason) =>
         val error = Right[Unit, VerificationError](reason)
         val newUntrustedState = untrustedState.insertLightBlock(lightBlock)
 
-        Finished(error, trustedState, newUntrustedState)
+        Finished(error, verifiedState, newUntrustedState)
     }
   }.ensuring {
     case waitingForHeader: WaitingForHeader =>
       waitingForHeader.untrustedState.targetLimit == untrustedState.targetLimit &&
-        waitingForHeader.trustedState.currentHeight() >= trustedState.currentHeight() &&
-        (waitingForHeader.trustedState.currentHeight() > trustedState.currentHeight() ||
+        waitingForHeader.verifiedState.currentHeight() >= verifiedState.currentHeight() &&
+        (waitingForHeader.verifiedState.currentHeight() > verifiedState.currentHeight() ||
           waitingForHeader.requestHeight < lightBlock.header.height)
     case _ => true
   }

light-client-core/src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/light/TrustVerifiers.scala

@@ -1,6 +1,6 @@
 package ch.epfl.ognjanovic.stevan.tendermint.verified.light
 
-import ch.epfl.ognjanovic.stevan.tendermint.verified.light.TrustedStates.TrustedState
+import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VerifiedStates.VerifiedState
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VerificationErrors.InvalidNextValidatorSet
 import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VerificationOutcomes._
 import ch.epfl.ognjanovic.stevan.tendermint.verified.types.LightBlock
@@ -12,29 +12,29 @@ object TrustVerifiers {
   abstract class TrustVerifier {
 
     @pure
-    def verify(trustedState: TrustedState, untrustedLightBlock: LightBlock): VerificationOutcome = {
-      require(trustedState.currentHeight() < untrustedLightBlock.header.height)
+    def verify(verifiedState: VerifiedState, untrustedLightBlock: LightBlock): VerificationOutcome = {
+      require(verifiedState.currentHeight() < untrustedLightBlock.header.height)
       ??? : VerificationOutcome
     }.ensuring(res =>
-      ((res == Success) ==> trustedState.trusted(untrustedLightBlock)) &&
-        ((res == InsufficientTrust) ==> (trustedState.currentHeight() + 1 < untrustedLightBlock.header.height)))
+      ((res == Success) ==> verifiedState.isTrusted(untrustedLightBlock)) &&
+        ((res == InsufficientTrust) ==> (verifiedState.currentHeight() + 1 < untrustedLightBlock.header.height)))
 
   }
 
   case class DefaultTrustVerifier() extends TrustVerifier {
 
     @pure @opaque
-    override def verify(trustedState: TrustedState, untrustedLightBlock: LightBlock): VerificationOutcome = {
-      require(trustedState.currentHeight() < untrustedLightBlock.header.height)
-      if (trustedState.trusted(untrustedLightBlock))
+    override def verify(verifiedState: VerifiedState, untrustedLightBlock: LightBlock): VerificationOutcome = {
+      require(verifiedState.currentHeight() < untrustedLightBlock.header.height)
+      if (verifiedState.isTrusted(untrustedLightBlock))
         Success
-      else if (trustedState.isAdjacent(untrustedLightBlock))
+      else if (verifiedState.isAdjacent(untrustedLightBlock))
         Failure(InvalidNextValidatorSet)
       else
         InsufficientTrust
     }.ensuring(res =>
-      ((res == Success) ==> trustedState.trusted(untrustedLightBlock)) &&
-        ((res == InsufficientTrust) ==> (trustedState.currentHeight() + 1 < untrustedLightBlock.header.height)))
+      ((res == Success) ==> verifiedState.isTrusted(untrustedLightBlock)) &&
+        ((res == InsufficientTrust) ==> (verifiedState.currentHeight() + 1 < untrustedLightBlock.header.height)))
 
   }
 

light-client-core/src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/light/VerificationErrors.scala

@@ -22,6 +22,6 @@ object VerificationErrors {
 
   case object InvalidCommitVoteSignature extends VerificationError
 
-  case object ExpiredTrustedState extends VerificationError
+  case object ExpiredVerifiedState extends VerificationError
 
 }

light-client-core/src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/light/TrustedStates.scala → light-client-core/src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/light/VerifiedStates.scala

@@ -4,63 +4,62 @@ import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VotingPowerVerifiers.
 import ch.epfl.ognjanovic.stevan.tendermint.verified.types.{Height, LightBlock}
 import stainless.annotation.pure
 
-object TrustedStates {
+object VerifiedStates {
 
-  abstract class TrustedState {
+  abstract class VerifiedState {
 
     @pure
-    def trusted(lightBlock: LightBlock): Boolean = {
+    def isTrusted(lightBlock: LightBlock): Boolean = {
       require(lightBlock.header.height > currentHeight())
       ??? : Boolean
     }
 
     @pure
-    def trustedLightBlock: LightBlock
+    def verified: LightBlock
 
     /**
-     * Tries to "improve" the current trusted state with addition of a new signed header of a greater height.
+     * Tries to "improve" the current verified state with addition of a new signed header of a greater height.
      *
-     * @param lightBlock which will be the new trusted header if it can be trusted
-     * @return new trusted state or the old one if the trust is not reachable
+     * @param lightBlock which will be the new verified header if it can be trusted
+     * @return new verified state
      */
     @pure
-    def increaseTrust(lightBlock: LightBlock): TrustedState = {
-      require(lightBlock.header.height > currentHeight() && trusted(lightBlock))
-      ??? : TrustedState
+    def increaseTrust(lightBlock: LightBlock): VerifiedState = {
+      require(lightBlock.header.height > currentHeight() && isTrusted(lightBlock))
+      ??? : VerifiedState
     }.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)
+      verified.header.height
+    }.ensuring(res => res == verified.header.height)
 
     @pure
     def isAdjacent(lightBlock: LightBlock): Boolean = {
       require(currentHeight() < lightBlock.header.height)
-      lightBlock.header.height == trustedLightBlock.header.height + 1
+      lightBlock.header.height == verified.header.height + 1
     }.ensuring(res =>
       (res && currentHeight() + 1 == lightBlock.header.height) ||
         (!res && currentHeight() + 1 < lightBlock.header.height))
 
   }
 
-  case class SimpleTrustedState(trustedLightBlock: LightBlock, trustVerifier: VotingPowerVerifier)
-      extends TrustedState {
+  case class SimpleVerifiedState(verified: LightBlock, trustVerifier: VotingPowerVerifier) extends VerifiedState {
 
     @pure
-    override def currentHeight(): Height = trustedLightBlock.header.height
+    override def currentHeight(): Height = verified.header.height
 
     @pure
-    override def increaseTrust(lightBlock: LightBlock): TrustedState = {
-      require(lightBlock.header.height > this.trustedLightBlock.header.height && trusted(lightBlock))
-      SimpleTrustedState(lightBlock, trustVerifier)
+    override def increaseTrust(lightBlock: LightBlock): VerifiedState = {
+      require(lightBlock.header.height > this.verified.header.height && isTrusted(lightBlock))
+      SimpleVerifiedState(lightBlock, trustVerifier)
     }.ensuring(res => res.currentHeight() > currentHeight() && res.currentHeight() == lightBlock.header.height)
 
     @pure
-    override def trusted(lightBlock: LightBlock): Boolean = {
+    override def isTrusted(lightBlock: LightBlock): Boolean = {
       require(lightBlock.header.height > currentHeight())
       if (isAdjacent(lightBlock))
         internalAdjacentHeaderTrust(lightBlock)
@@ -71,14 +70,14 @@ object TrustedStates {
     @pure
     private def internalAdjacentHeaderTrust(lightBlock: LightBlock): Boolean = {
       require(currentHeight() < lightBlock.header.height && isAdjacent(lightBlock))
-      trustedLightBlock.nextValidatorSet.toInfoHashable == lightBlock.validatorSet.toInfoHashable
+      verified.nextValidatorSet.toInfoHashable == lightBlock.validatorSet.toInfoHashable
     }
 
     @pure
     private def internalNonAdjacentHeaderTrust(lightBlock: LightBlock): Boolean = {
       require(currentHeight() < lightBlock.header.height && !isAdjacent(lightBlock))
 
-      trustVerifier.trustedCommit(trustedLightBlock.nextValidatorSet, lightBlock.commit)
+      trustVerifier.trustedCommit(verified.nextValidatorSet, lightBlock.commit)
     }
 
   }