Revert.

OStevan · Aug 12, 2020 · 27c913f · 27c913f
1 parent 1747736
commit 27c913f
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 10 deletions.
diff --git a/...ain/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/blockchain/BlockchainStates.scala b/...ain/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/blockchain/BlockchainStates.scala
@@ -5,6 +5,7 @@ import ch.epfl.ognjanovic.stevan.tendermint.verified.light.VotingPowerVerifiers
 import ch.epfl.ognjanovic.stevan.tendermint.verified.types._
 import stainless.annotation._
 import stainless.lang._
+import stainless.lang.StaticChecks.assert
 import utils.ListSet
 
 object BlockchainStates {
@@ -131,8 +132,8 @@ object BlockchainStates {
             blockchain.faultChecker.isCorrect(nextValidatorSet, faulty)
           ) {
             val newBlockchain = blockchain.appendBlock(lastCommit, nextValidatorSet)
-//            assert(newBlockchain.chain.head.validatorSet.keys.subsetOf(allNodes))
-//            assert(globalStateInvariant(allNodes, faulty, newBlockchain))
+            assert(newBlockchain.chain.head.validatorSet.keys.subsetOf(allNodes))
+            assert(globalStateInvariant(allNodes, faulty, newBlockchain))
 
             if (newBlockchain.finished)
               Finished(allNodes, faulty, newBlockchain)

diff --git a/...in/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/integration/ModelIntegration.scala b/...in/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/integration/ModelIntegration.scala
@@ -33,9 +33,9 @@ object ModelIntegration {
     val verifiedState: VerifiedState =
       SimpleVerifiedState(trustedSignedHeader, VotingPowerVerifiers.defaultVotingPowerVerifier)
     val untrustedTrace = InMemoryUntrustedTrace(heightToVerify, List.empty)
-//    assert(untrustedTrace.bottomHeight().forall(heightToVerify < _))
-//    assert(verifiedState.currentHeight() < heightToVerify)
-//    assert(heightToVerify <= untrustedTrace.targetLimit)
+    assert(untrustedTrace.bottomHeight().forall(heightToVerify < _))
+    assert(verifiedState.currentHeight() < heightToVerify)
+    assert(heightToVerify <= untrustedTrace.targetLimit)
 
     val lightBlockVerifier = DefaultTrustVerifier()
 

diff --git a/.../main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/light/LightBlockProviders.scala b/.../main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/light/LightBlockProviders.scala
@@ -1,12 +1,13 @@
 package ch.epfl.ognjanovic.stevan.tendermint.verified.light
 
 import ch.epfl.ognjanovic.stevan.tendermint.verified.types.{Height, LightBlock, PeerId}
-import stainless.lang.StaticChecks._
+import stainless.annotation._
 
 object LightBlockProviders {
 
   abstract class LightBlockProvider {
 
+    @pure
     def lightBlock(height: Height): LightBlock = {
       require(height <= currentHeight)
       ??? : LightBlock
@@ -16,6 +17,7 @@ object LightBlockProviders {
 
     def currentHeight: Height
 
+    @pure
     def chainId: String
 
     def peerId: PeerId

diff --git a/...rc/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/light/MultiStepVerifier.scala b/...rc/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/light/MultiStepVerifier.scala
@@ -29,9 +29,9 @@ case class MultiStepVerifier(
 
       val nextHeight = untrustedTrace.targetLimit
 
-//      assert(untrustedTrace.bottomHeight().map(nextHeight < _).getOrElse(true))
-//      assert(verifiedState.currentHeight() < nextHeight)
-//      assert(nextHeight <= untrustedTrace.targetLimit)
+      assert(untrustedTrace.bottomHeight().map(nextHeight < _).getOrElse(true))
+      assert(verifiedState.currentHeight() < nextHeight)
+      assert(nextHeight <= untrustedTrace.targetLimit)
       verify(WaitingForHeader(nextHeight, verifiedState, untrustedTrace))
     }
   }
@@ -82,7 +82,7 @@ case class MultiStepVerifier(
     decreases(untrustedTrace.targetLimit.value - verifiedState.currentHeight().value)
 
     val lightBlock = lightBlockProvider.lightBlock(next)
-//    assert(lightBlock.header.height == next)
+    assert(lightBlock.header.height == next)
 
     // without a caching light block provider this is extremely wasteful but the algorithm is simpler.
     verifier.verify(verifiedState, lightBlock) match {