spec: Refactor consensus and driver modules using sum types (#116)

* Use sum type for VoteType * Use sum type for Threshold * Use sum type for ExecutorEvent * Use sum type for Value * Update executor using votekeeper's new types * Move unit tests near definition * Fix SM and tests after merge * Add types module * Comment out id in types * spec: remove initialRound * fix spec * Update itf tests * cargo fmt * Rename conflicting definitions * Use `itf` native support for sum types (#111) * spec driver: Bring some changes from main + some nits * spec driver: another missing fix * Rename voteBookkeepesSM to Models * Move votekeeper types to common types * WIP * Add timeout state functions * Fixes to value types * fix driver typecheck * fix more types * Fix value type * Renaming + comments * Fix another value expression + type annotations * renaming, commentrs, type Command * rename missing * replace match for if * Replace NewRoundStep with NoStep * Fix driver.qnt Co-authored-by: Josef Widder <[email protected]> * nits * comments * Driver indentation * Driver comments and order of declarations * Rename timeout to timeouts * Rename es parameter --------- Co-authored-by: Romain Ruetschi <[email protected]> Co-authored-by: Josef Widder <[email protected]>
informalsystems · Dec 14, 2023 · 32498ca · 32498ca
1 parent 2faed8e
commit 32498ca
Show file tree

Hide file tree

Showing 14 changed files with 1,203 additions and 1,547 deletions.
diff --git a/Specs/Quint/TendermintDSL.qnt b/Specs/Quint/TendermintDSL.qnt
@@ -2,6 +2,8 @@
 
 module TendermintDSL {
 
+import types.* from "./types"
+export types.*
 import statemachineAsync.* from "./statemachineAsync"
 export statemachineAsync.*
 
@@ -13,7 +15,6 @@ def SetFromList(L) = {
     L.foldl(Set(), (s, x) => s.union(Set(x)))
 }
 
-
 run ListTakeAStep (active) = {
     active.length().reps(i => valStep(active[i]))
 }
@@ -26,38 +27,36 @@ run ListDeliverSomeProposal (active) = {
     active.length().reps(i => deliverSomeProposal(active[i]))
 }
 
-run ProcessDeliverAllVotes  (cstep, recepient, fromList, valset, h, r, value) = {
-    fromList.length().reps(i => deliverVote(recepient, { src: fromList[i], height: h, round: r, step: cstep, id: value }))
-}
+run ProcessDeliverAllVotes(voteType, recepient, fromList, valset, h, r, value) =
+    fromList.length().reps(i => deliverVote(recepient, mkVote(voteType, fromList[i], h, r, value)))
 
-run ListDeliverAllVotes (cstep, fromList, toList, valset, h, r, value) = {
-    toList.length().reps(i => ProcessDeliverAllVotes (cstep, toList[i], fromList, valset, h, r, value))
-}
+run ListDeliverAllVotes(voteType, fromList, toList, valset, h, r, value) =
+    toList.length().reps(i => ProcessDeliverAllVotes(voteType, toList[i], fromList, valset, h, r, value))
 
-run onlyProposerReceivesProposal (active, valList, valset, h, r, value) = {
-    val p = Proposer (valset, h, r)
+run onlyProposerReceivesProposal(active, valList, valset, h, r, value) = {
+    val p = proposer(valset, h, r)
     setNextValueToPropose(p, value)
     .then(ListTakeAStep(active))
     .then(all{ // after new round an empty step to clean step "propose"
-        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == "propose")),
+        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == ProposeStep)),
         ListTakeAStep(active)
     })
     .then(deliverSomeProposal(p))
     .then(ListTakeAStep(active))
     .then(all{ 
-        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == "Prevote")),
+        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == PrevoteStep)),
         ListTakeAStep(active)
     })            
 }
 
 // TODO: add valid round more cleanly on one run for all cases
 run everyoneReceivesProposalVR (active, valList, valset, h, r, value, vr) = {
-    val p = Proposer (valset, h, r)
-    val propMsg = { height: h, proposal: value, round: r, src: p, validRound: vr }
+    val p = proposer(valset, h, r)
+    val propMsg = mkProposal(p, h, r, value, vr)
     setNextValueToPropose(p, value)
     .then(ListTakeAStep(active))
     .then(all{ // after new round an empty step to clean step "propose"
-        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == "propose")),
+        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == ProposeStep)),
         ListTakeAStep(active)
     })
     .then(all {
@@ -66,18 +65,18 @@ run everyoneReceivesProposalVR (active, valList, valset, h, r, value, vr) = {
     })
     .then(ListTakeAStep(active))
     .then(all{ 
-        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == "Prevote")),
+        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == PrevoteStep)),
         ListTakeAStep(active)
     })        
 }
 
 run everyoneReceivesProposal (active, valList, valset, h, r, value) = {
-    val p = Proposer (valset, h, r)
-    val propMsg = { height: h, proposal: value, round: r, src: p, validRound: -1 }
+    val p = proposer(valset, h, r)
+    val propMsg = mkProposal(p, h, r, value, -1)
     setNextValueToPropose(p, value)
     .then(ListTakeAStep(active))
     .then(all{ // after new round an empty step to clean step "propose"
-        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == "propose")),
+        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == ProposeStep)),
         ListTakeAStep(active)
     })
     .then(all {
@@ -86,21 +85,19 @@ run everyoneReceivesProposal (active, valList, valset, h, r, value) = {
     })
     .then(ListTakeAStep(active))
     .then(all{ 
-        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == "Prevote")),
+        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == PrevoteStep)),
         ListTakeAStep(active)
     })        
 }
 
-run fromPrevoteToPrecommit (prevoteSenders, prevoteReceivers, valList, valset, h, r, value) = {
-    ListDeliverAllVotes("Prevote", prevoteSenders, prevoteReceivers, valset, h, r, value)
-    .then(prevoteSenders.length().reps(_ => ListTakeAStep(prevoteReceivers)))
-    // extra step due to timeoutprevote double step
-    .then(ListTakeAStep(prevoteReceivers))
-   .then(all{ 
-       assert(SetFromList(prevoteReceivers).forall(proc => system.get(proc).es.pendingStepChange == "Precommit")),
-       ListTakeAStep(prevoteReceivers)
-   })            
-}
-
+run fromPrevoteToPrecommit(prevoteSenders, prevoteReceivers, valList, valset, h, r, value) =
+    ListDeliverAllVotes(Prevote, prevoteSenders, prevoteReceivers, valset, h, r, value)
+        .then(prevoteSenders.length().reps(_ => ListTakeAStep(prevoteReceivers)))
+        // extra step due to timeoutprevote double step
+        .then(ListTakeAStep(prevoteReceivers))
+    .then(all{ 
+        assert(SetFromList(prevoteReceivers).forall(proc => system.get(proc).es.pendingStepChange == PrecommitStep)),
+        ListTakeAStep(prevoteReceivers)
+    })
 
-}
+}