spec: Add multiplexing of events on step change (#104)

* Added handling around StepChange function

* started with stepchange

* firest version of step propose without test

* re-did structure of StepChange

* finished first complete version of StepChange (TODO: tests)

* typo

* paramTest fixed

* fixed tests and DSL

* start refactor asyncmodelstest

* refactored tests from asyncModelsTest except disagreement

* refactored old asyncModelTests

* seems to fix changes to sum types

* fixed line28test

* commented big test. added todo

Specs/Quint/TendermintDSL.qnt

@@ -9,12 +9,17 @@ val validatorList = validators.fold(List(), (s, x) => s.append(x))
 val correctList = Correct.fold(List(), (s, x) => s.append(x))
 val faultyList = Faulty.fold(List(), (s, x) => s.append(x))
 
+def SetFromList(L) = {
+    L.foldl(Set(), (s, x) => s.union(Set(x)))
+}
+
+
 run ListTakeAStep (active) = {
     active.length().reps(i => valStep(active[i]))
 }
 
-run ListDeliverProposal (active, proposalMsg) = {
-    active.length().reps(i => deliverProposal(active[i], proposalMsg))
+run ListDeliverProposal (active, propMsg) = {
+    active.length().reps(i => deliverProposal(active[i], propMsg))
 }
 
 run ListDeliverSomeProposal (active) = {
@@ -29,23 +34,72 @@ run ListDeliverAllVotes (cstep, fromList, toList, valset, h, r, value) = {
     toList.length().reps(i => ProcessDeliverAllVotes (cstep, toList[i], fromList, valset, h, r, value))
 }
 
+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")),
+        ListTakeAStep(active)
+    })
+    .then(deliverSomeProposal(p))
+    .then(ListTakeAStep(active))
+    .then(all{ 
+        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == "Prevote")),
+        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 }
+    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")),
+        ListTakeAStep(active)
+    })
+    .then(all {
+        assert(true),
+        ListDeliverProposal(active, propMsg)
+    })
+    .then(ListTakeAStep(active))
+    .then(all{ 
+        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == "Prevote")),
+        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 }
     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")),
+        ListTakeAStep(active)
+    })
     .then(all {
         assert(true),
-        ListDeliverSomeProposal(active)
+        ListDeliverProposal(active, propMsg)
     })
-    .then(ListTakeAStep(active))    
+    .then(ListTakeAStep(active))
+    .then(all{ 
+        assert(SetFromList(active).forall(proc => system.get(proc).es.pendingStepChange == "Prevote")),
+        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)
+   })            
 }
 
 

Specs/Quint/disagreementRun.qnt

@@ -0,0 +1,42 @@
+// -*- mode: Bluespec; -*-
+
+module disagreementRun {
+
+import TendermintDSL.* from "./TendermintDSL"
+export TendermintDSL.*
+
+const groupA : Set[Address_t]
+val groupB = Correct.exclude(groupA)
+val aList = groupA.fold(List(), (s, x) => s.append(x)) 
+val bList = groupB.fold(List(), (s, x) => s.append(x)) 
+
+// A run for too many faulty nodes
+
+// TODO: assertions about proposer being faulty
+run DisagreementRun = {
+    val thisProposer = Proposer (validatorSet, 0, 0)
+    init
+    .then(2.reps(_ => ListTakeAStep(correctList)))
+    .then(ListDeliverProposal(aList, { height: 0, proposal: "a", round: 0, src: thisProposer, validRound: -1 }))
+    .then(ListDeliverProposal(bList, { height: 0, proposal: "b", round: 0, src: thisProposer, validRound: -1 }))
+    .then(ListTakeAStep(correctList))
+    // they voted differently
+    .then(ListTakeAStep(correctList)) // consume step change
+    .then(ListDeliverAllVotes("Prevote", aList.concat(faultyList), aList, validatorSet, 0, 0, "a"))
+    .then(ListDeliverAllVotes("Prevote", bList.concat(faultyList), bList, validatorSet, 0, 0, "b"))  
+    .then(aList.concat(faultyList).length().reps(_ => ListTakeAStep(aList)))
+    .then(bList.concat(faultyList).length().reps(_ => ListTakeAStep(bList)))
+    .then(ListTakeAStep(correctList)) // timeout prevote started -> extra step to consume pending
+    // they precommited differently
+    .then(ListTakeAStep(correctList)) // consume step change
+    .then(ListDeliverAllVotes("Precommit", aList.concat(faultyList), aList, validatorSet, 0, 0, "a"))
+    .then(ListDeliverAllVotes("Precommit", bList.concat(faultyList), bList, validatorSet, 0, 0, "b"))  
+    .then(aList.concat(faultyList).length().reps(_ => ListTakeAStep(aList)))
+    .then(bList.concat(faultyList).length().reps(_ => ListTakeAStep(bList)))
+    .then(all{
+        assert(not(AgreementInv)),
+        unchangedAll
+    })   
+}
+
+}