Add scalafmt configuration.

OStevan · Jun 26, 2020 · d800529 · d800529
1 parent df15489
commit d800529
Show file tree

Hide file tree

Showing 48 changed files with 477 additions and 402 deletions.
diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml
@@ -7,6 +7,19 @@ on:
     branches: [ master ]
 
 jobs:
+  style-check:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+      - name: Set up JDK 1.8
+        uses: actions/setup-java@v1
+        with:
+          java-version: 1.8
+      - name: Style check
+        run: |
+          sbt update
+          sbt scalafmtCheck
+
   test:
     runs-on: ubuntu-latest
     steps:

diff --git a/.scalafmt.conf b/.scalafmt.conf
@@ -0,0 +1,16 @@
+version = 2.6.1
+
+maxColumn = 120
+continuationIndent.defnSite = 2
+align.preset = none
+danglingParentheses.callSite = false
+danglingParentheses.defnSite = false
+assumeStandardLibraryStripMargin = true
+newlines.topLevelStatements = [before,after]
+newlines.alwaysBeforeMultilineDef = false
+newlines.implicitParamListModifierPrefer = before
+newlines.avoidForSimpleOverflow = [tooLong, punct]
+rewrite.rules = [AvoidInfix, SortImports, RedundantParens, SortModifiers]
+docstrings = JavaDoc
+docstrings.style = Asterisk
+docstrings.oneline = unfold
diff --git a/.../src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/blockchain/Blockchain.scala b/.../src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/blockchain/Blockchain.scala
@@ -17,13 +17,7 @@ case class Blockchain(
   @pure
   def increaseTime(timeDelta: Duration): Blockchain = {
     val newNow = now.addTime(timeDelta)
-    Blockchain.timeProgressDoesNotDeteriorateTheState(
-      faultChecker,
-      newNow,
-      now,
-      trustingPeriod,
-      chain,
-      faulty)
+    Blockchain.timeProgressDoesNotDeteriorateTheState(faultChecker, newNow, now, trustingPeriod, chain, faulty)
     Blockchain(maxHeight, now, trustingPeriod, chain, faulty, faultChecker)
   }.ensuring(res => faultAssumption() ==> res.faultAssumption())
 
@@ -36,13 +30,14 @@ case class Blockchain(
   @pure
   def appendBlock(lastCommit: Commit, nextVS: ValidatorSet): Blockchain = {
     require(
-        !finished &&
+      !finished &&
         faultChecker.isCorrect(nextVS, faulty) &&
         faultAssumption())
     val header = BlockHeader(
       Blockchain.constructHeader(chain.height + 1, chain.head.header.time),
       lastCommit,
-      chain.head.nextValidatorSet, nextVS)
+      chain.head.nextValidatorSet,
+      nextVS)
     val newChain = chain.appendBlock(header)
     Blockchain(maxHeight, now, trustingPeriod, newChain, faulty, faultChecker)
   }.ensuring(res =>
@@ -64,7 +59,7 @@ case class Blockchain(
 
   @inline
   def setFaulty(newFaulty: Set[Address]): Blockchain = {
-    require(faulty subsetOf newFaulty)
+    require(faulty.subsetOf(newFaulty))
     Blockchain.faultyChainDoesNotRecoverWithNewFault(faultChecker, now, trustingPeriod, chain, faulty, newFaulty)
     Blockchain(maxHeight, now, trustingPeriod, chain, newFaulty, faultChecker)
   }.ensuring(res => !faultAssumption() ==> !res.faultAssumption())
@@ -78,12 +73,7 @@ case class Blockchain(
     require(height < chain.height)
     val headerCommit = getHeader(height + 1).lastCommit
     val blockHeader = getHeader(height)
-    LightBlock(
-      blockHeader.header,
-      headerCommit,
-      blockHeader.validatorSet,
-      blockHeader.nextValidatorSet,
-      Blockchain.peer())
+    LightBlock(blockHeader.header, headerCommit, blockHeader.validatorSet, blockHeader.nextValidatorSet, Blockchain.peer())
   }
 
   private def getHeaderInternal(height: Height, chain: Chain): BlockHeader = {
@@ -97,6 +87,7 @@ case class Blockchain(
           getHeaderInternal(height, tail)
     }
   }.ensuring(res => res.header.height == height)
+
 }
 
 object Blockchain {
@@ -125,13 +116,13 @@ object Blockchain {
     @induct chain: Chain,
     faulty: Set[Address],
     newFaulty: Set[Address]): Unit = {
-    require(faulty subsetOf newFaulty)
+    require(faulty.subsetOf(newFaulty))
   }.ensuring { _ =>
     FaultChecker.moreFaultyDoesNotHelp(faultChecker, faulty, newFaulty)
-    !chain.forAll(
-      header => now > header.header.time.addTime(duration) || faultChecker.isCorrect(header.nextValidatorSet, faulty)) ==>
-      !chain.forAll(
-        header => now > header.header.time.addTime(duration) || faultChecker.isCorrect(header.nextValidatorSet, newFaulty))
+    !chain.forAll(header =>
+      now > header.header.time.addTime(duration) || faultChecker.isCorrect(header.nextValidatorSet, faulty)) ==>
+      !chain.forAll(header =>
+        now > header.header.time.addTime(duration) || faultChecker.isCorrect(header.nextValidatorSet, newFaulty))
   }
 
   @opaque
@@ -144,9 +135,10 @@ object Blockchain {
     faulty: Set[Address]): Unit = {
     require(now <= newNow)
   }.ensuring { _ =>
-    chain.forAll(
-      header => now > header.header.time.addTime(duration) || faultChecker.isCorrect(header.nextValidatorSet, faulty)) ==>
-      chain.forAll(
-        header => newNow > header.header.time.addTime(duration) || faultChecker.isCorrect(header.nextValidatorSet, faulty))
+    chain.forAll(header =>
+      now > header.header.time.addTime(duration) || faultChecker.isCorrect(header.nextValidatorSet, faulty)) ==>
+      chain.forAll(header =>
+        newNow > header.header.time.addTime(duration) || faultChecker.isCorrect(header.nextValidatorSet, faulty))
   }
+
 }
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
@@ -17,9 +17,9 @@ object BlockchainStates {
     maxVotingPower: VotingPower,
     blockchain: Blockchain): Boolean = {
     blockchain.faultAssumption() &&
-      maxVotingPower.isPositive &&
-      !blockchain.finished &&
-      globalStateInvariant(allNodes, faulty, blockchain)
+    maxVotingPower.isPositive &&
+    !blockchain.finished &&
+    globalStateInvariant(allNodes, faulty, blockchain)
   }
 
   @inline
@@ -29,31 +29,32 @@ object BlockchainStates {
     maxVotingPower: VotingPower,
     blockchain: Blockchain): Boolean = {
     !blockchain.faultAssumption() &&
-      maxVotingPower.isPositive &&
-      !blockchain.finished &&
-      globalStateInvariant(allNodes, faulty, blockchain)
+    maxVotingPower.isPositive &&
+    !blockchain.finished &&
+    globalStateInvariant(allNodes, faulty, blockchain)
   }
 
   @inline
   private def finishedStateInvariant(allNodes: Set[Address], faulty: Set[Address], blockchain: Blockchain): Boolean = {
     blockchain.faultAssumption() &&
-      blockchain.finished &&
-      globalStateInvariant(allNodes, faulty, blockchain)
+    blockchain.finished &&
+    globalStateInvariant(allNodes, faulty, blockchain)
   }
 
   // state invariant forced in TLA
   @inline
   private def globalStateInvariant(allNodes: Set[Address], faulty: Set[Address], blockchain: Blockchain): Boolean = {
     allNodes.nonEmpty && // makes no sense to have no nodes
-      (faulty subsetOf allNodes) && // faulty nodes need to be from the set of existing nodes
-      faulty == blockchain.faulty &&
-      blockchain.chain.forAll(_.nextValidatorSet.keys.subsetOf(allNodes)) &&
-      blockchain.chain.forAll(_.lastCommit.forBlock.subsetOf(allNodes)) &&
-      blockchain.chain.forAll(_.validatorSet.keys.subsetOf(allNodes))
+    faulty.subsetOf(allNodes) && // faulty nodes need to be from the set of existing nodes
+    faulty == blockchain.faulty &&
+    blockchain.chain.forAll(_.nextValidatorSet.keys.subsetOf(allNodes)) &&
+    blockchain.chain.forAll(_.lastCommit.forBlock.subsetOf(allNodes)) &&
+    blockchain.chain.forAll(_.validatorSet.keys.subsetOf(allNodes))
   }
 
   @inlineInvariant
   sealed abstract class BlockchainState {
+
     @pure
     @inline
     def step(systemStep: SystemStep): BlockchainState
@@ -81,14 +82,12 @@ object BlockchainStates {
       require(height < currentHeight())
       blockchain.getLightBlock(height)
     }.ensuring(res => res.header.height == height)
+
   }
 
   @inlineInvariant
-  case class Running(
-    allNodes: Set[Address],
-    faulty: Set[Address],
-    maxVotingPower: VotingPower,
-    blockchain: Blockchain) extends BlockchainState {
+  case class Running(allNodes: Set[Address], faulty: Set[Address], maxVotingPower: VotingPower, blockchain: Blockchain)
+      extends BlockchainState {
     require(runningStateInvariant(allNodes, faulty, maxVotingPower, blockchain))
 
     @pure
@@ -97,7 +96,7 @@ object BlockchainStates {
       systemStep match {
         // faultyNode is from expected nodes and at least one correct node exists
         case Fault(faultyNode)
-          if allNodes.contains(faultyNode) && (allNodes != (faulty + faultyNode)) && !faulty.contains(faultyNode) =>
+            if allNodes.contains(faultyNode) && (allNodes != (faulty + faultyNode)) && !faulty.contains(faultyNode) =>
           val newFaulty = faulty + faultyNode
           SetInvariants.setAdd(faulty, faultyNode, allNodes)
           val newChain = blockchain.setFaulty(newFaulty)
@@ -113,16 +112,16 @@ object BlockchainStates {
 
         // ignores append messages which do not preserve guarantees of the system
         case AppendBlock(lastCommit, nextValidatorSet: ValidatorSet)
-          if lastCommit.forBlock.subsetOf(blockchain.chain.head.validatorSet.keys) &&
-            nextValidatorSet.values.forall(_.votingPower <= maxVotingPower) &&
-            nextValidatorSet.keys.subsetOf(allNodes) &&
-            lastCommit.forBlock.subsetOf(allNodes) &&
-            lastCommit.forBlock.nonEmpty /* obvious from AppendBlock adt invariant times-out */ =>
-
+            if lastCommit.forBlock.subsetOf(blockchain.chain.head.validatorSet.keys) &&
+              nextValidatorSet.values.forall(_.votingPower <= maxVotingPower) &&
+              nextValidatorSet.keys.subsetOf(allNodes) &&
+              lastCommit.forBlock.subsetOf(allNodes) &&
+              lastCommit.forBlock.nonEmpty /* obvious from AppendBlock adt invariant times-out */ =>
           val lastBlock = blockchain.chain.head
           if (
             VotingPowerVerifiers.defaultTrustVerifier.consensusObtained(lastBlock.validatorSet, lastCommit) &&
-              blockchain.faultChecker.isCorrect(nextValidatorSet, faulty)) {
+            blockchain.faultChecker.isCorrect(nextValidatorSet, faulty)
+          ) {
             val newBlockchain = blockchain.appendBlock(lastCommit, nextValidatorSet)
             assert(newBlockchain.chain.head.validatorSet.keys.subsetOf(allNodes))
             assert(globalStateInvariant(allNodes, faulty, newBlockchain))
@@ -145,14 +144,12 @@ object BlockchainStates {
 
     @pure
     override def currentHeight(): Height = blockchain.chain.height
+
   }
 
   @inlineInvariant
-  case class Faulty(
-    allNodes: Set[Address],
-    faulty: Set[Address],
-    maxVotingPower: VotingPower,
-    blockchain: Blockchain) extends BlockchainState {
+  case class Faulty(allNodes: Set[Address], faulty: Set[Address], maxVotingPower: VotingPower, blockchain: Blockchain)
+      extends BlockchainState {
     require(faultyStateInvariant(allNodes, faulty, maxVotingPower, blockchain))
 
     @pure
@@ -169,14 +166,15 @@ object BlockchainStates {
             Faulty(allNodes, faulty, maxVotingPower, updated)
 
         case Fault(faultyNode)
-          if allNodes.contains(faultyNode) && (allNodes != (faulty + faultyNode)) && !faulty.contains(faultyNode) =>
+            if allNodes.contains(faultyNode) && (allNodes != (faulty + faultyNode)) && !faulty.contains(faultyNode) =>
           val newFaulty = SetInvariants.setAdd(faulty, faultyNode, allNodes)
           Faulty(allNodes, newFaulty, maxVotingPower, blockchain.setFaulty(newFaulty))
 
         case _ => this
       }
-    }.ensuring(res => (res.blockchain.faultAssumption() && res.isInstanceOf[Running]) ||
-      (!res.blockchain.faultAssumption() && res.isInstanceOf[Faulty]))
+    }.ensuring(res =>
+      (res.blockchain.faultAssumption() && res.isInstanceOf[Running]) ||
+        (!res.blockchain.faultAssumption() && res.isInstanceOf[Faulty]))
 
     override def maxHeight: Height = blockchain.maxHeight
 
@@ -186,6 +184,7 @@ object BlockchainStates {
 
     @pure
     override def currentHeight(): Height = blockchain.chain.height
+
   }
 
   @inlineInvariant
@@ -203,6 +202,7 @@ object BlockchainStates {
 
     @pure
     override def currentHeight(): Height = blockchain.chain.height
+
   }
 
 }
diff --git a/...ain/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/blockchain/BlockchainSystem.scala b/...ain/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/blockchain/BlockchainSystem.scala
@@ -7,7 +7,6 @@ import ch.epfl.ognjanovic.stevan.tendermint.verified.types._
 import stainless.annotation._
 import stainless.lang._
 
-
 object BlockchainSystem {
 
   @ghost
@@ -22,16 +21,18 @@ object BlockchainSystem {
     require(
       validatorSet.values.forall(_.votingPower.value == 1) &&
         maxPower.isPositive &&
-        (nextValidatorSet.keys subsetOf validatorSet.keys) &&
+        nextValidatorSet.keys.subsetOf(validatorSet.keys) &&
         faultChecker.isCorrect(nextValidatorSet, Set.empty) && initialCommit.forBlock.isEmpty)
 
     val noFaulty = Set.empty[Address]
 
-    val genesisBlock = BlockHeader(Blockchain.constructHeader(Height(1), Timestamp(0, 0)), initialCommit, validatorSet, nextValidatorSet)
+    val genesisBlock =
+      BlockHeader(Blockchain.constructHeader(Height(1), Timestamp(0, 0)), initialCommit, validatorSet, nextValidatorSet)
     val initialChain = Genesis(genesisBlock)
     val minTrustedTime = Timestamp(1, 0)
 
-    val startingBlockchain: Blockchain = Blockchain(maxHeight, minTrustedTime, Duration(100, 0), initialChain, Set.empty, faultChecker)
+    val startingBlockchain: Blockchain =
+      Blockchain(maxHeight, minTrustedTime, Duration(100, 0), initialChain, Set.empty, faultChecker)
 
     if (maxHeight.value == BigInt(1))
       Finished(validatorSet.keys, noFaulty, startingBlockchain)
@@ -54,8 +55,8 @@ object BlockchainSystem {
   @inlineOnce
   def neverStuckFalse2(blockchainState: BlockchainState): Boolean = {
     blockchainState.isInstanceOf[Faulty] ||
-      (blockchainState.isInstanceOf[Running] ||
-        blockchainState.isInstanceOf[Finished])
+    (blockchainState.isInstanceOf[Running] ||
+    blockchainState.isInstanceOf[Finished])
   }
 
   /**
@@ -82,4 +83,5 @@ object BlockchainSystem {
   def neverStuckFalse1(blockchainState: BlockchainState): Boolean = {
     blockchainState.isInstanceOf[Running]
   }
+
 }