Skip to content

Commit

Permalink
Renaming + comments
Browse files Browse the repository at this point in the history
  • Loading branch information
@hvanz
hvanz committed Dec 11, 2023
1 parent cf01a02 commit b13ae58
Show file tree
Hide file tree
Showing 4 changed files with 156 additions and 146 deletions.
88 changes: 44 additions & 44 deletions Specs/Quint/consensus.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ module consensus {

type ConsensusState = {
p: Address,
height : Height,
height: Height,
round: Round,
step: Step, // NewRound, Propose, Prevote, Precommit, decided
lockedRound: Round,
Expand Down Expand Up @@ -56,38 +56,38 @@ module consensus {
// For the initial state
| NoConsensusInput
// Setup the state-machine for a single-height execution
| NewHeightConInput(Height)
| NewHeightCInput(Height)
// Start a new round, not as proposer.
| NewRoundConInput(Round)
| NewRoundCInput(Round)
// Start a new round as proposer with the proposed Value.
| NewRoundProposerConInput((Round, NonNilValue))
| NewRoundProposerCInput((Round, NonNilValue))
// Receive a proposal without associated valid round.
| ProposalConInput((Round, Value))
| ProposalCInput((Round, Value))
// Receive a valid proposal with an associated valid round, attested by a a Polka(vr).
| ProposalAndPolkaPreviousAndValidConInput((Value, Round))
| ProposalAndPolkaPreviousAndValidCInput((Value, Round))
// Receive an invalid proposal: L26 and L32 when isValid(v) == false
| ProposalInvalidConInput
| ProposalInvalidCInput
// Receive +2/3 prevotes for nil.
| PolkaNilConInput
| PolkaNilCInput
// Receive +2/3 prevotes from different validators, not for the same value or nil.
| PolkaAnyConInput
| PolkaAnyCInput
// Proposal and 2/3+ prevotes for the proposal: L36 when valid and step >= prevote
| ProposalAndPolkaAndValidConInput(Value)
| ProposalAndPolkaAndValidCInput(Value)
// Receive +2/3 precommits from different validators, not for the same value or nil.
| PrecommitAnyConInput
| PrecommitAnyCInput
// Proposal and 2/3+ commits for the proposal => decision
| ProposalAndCommitAndValidConInput(Value)
| ProposalAndCommitAndValidCInput(Value)
// Receive +1/3 messages from different validators for a higher round.
| RoundSkipConInput(Round)
| RoundSkipCInput(Round)
// Timeout waiting for proposal.
| TimeoutProposeConInput((Height, Round))
| TimeoutProposeCInput((Height, Round))
// Timeout waiting for prevotes for a value.
| TimeoutPrevoteConInput((Height, Round))
| TimeoutPrevoteCInput((Height, Round))
// Timeout waiting for precommits for a value.
| TimeoutPrecommitConInput((Height, Round))
| TimeoutPrecommitCInput((Height, Round))
// found after Montebello
// TODO: Discuss what to do about it
| ProposalAndPolkaAndInvalidConInput((Height, Round, Value))
| ProposalAndPolkaAndInvalidCInput((Height, Round, Value))

// *************************************************************************
// Consensus output
Expand Down Expand Up @@ -145,13 +145,13 @@ module consensus {
| NoConsensusInput =>
state.toErrorOutput("NoConsensusInput is not a valid consensus input")

| NewHeightConInput(h) =>
| NewHeightCInput(h) =>
if (h > state.height)
initConsensusState(state.p, h).toNoConsensusOutput()
else state.toNoConsensusOutput()

// line 11.14
| NewRoundProposerConInput(round_value) =>
| NewRoundProposerCInput(round_value) =>
val r = round_value._1
val v = round_value._2
if (r > state.round)
Expand All @@ -164,7 +164,7 @@ module consensus {

// line 11.20
// TODO: discuss comment "ev.round must match state.round"
| NewRoundConInput(r) =>
| NewRoundCInput(r) =>
if (r > state.round)
// We just report that a timeout should be started. The executor must take care
// of figuring out whether it needs to record the round number and height per
Expand All @@ -180,7 +180,7 @@ module consensus {
// - the value has been checked to be valid
// - it is for the current round
// The executor checks this upon receiving a propose message "ProposalMsg"
| ProposalConInput(round_value) =>
| ProposalCInput(round_value) =>
val r = round_value._1
val v = round_value._2
if (state.step == ProposeStep)
Expand All @@ -192,18 +192,18 @@ module consensus {
state
.with("step", PrevoteStep)
.toPrevoteOutput(state.p, state.height, state.round, Nil) // line 26
else state.toErrorOutput("ProposalConInput when not in ProposeStep")
else state.toErrorOutput("ProposalCInput when not in ProposeStep")

// line 26
| ProposalInvalidConInput =>
| ProposalInvalidCInput =>
if (state.step == ProposeStep)
state
.with("step", PrevoteStep)
.toPrevoteOutput(state.p, state.height, state.round, Nil)
else state.toErrorOutput("ProposalConInput when not in ProposeStep")
else state.toErrorOutput("ProposalCInput when not in ProposeStep")

// line 28
| ProposalAndPolkaPreviousAndValidConInput(value_vr) =>
| ProposalAndPolkaPreviousAndValidCInput(value_vr) =>
val v = value_vr._1
val vr = value_vr._2
if (state.step == ProposeStep and vr >= 0 and vr < state.round) // line 28
Expand All @@ -215,21 +215,21 @@ module consensus {
state
.with("step", PrevoteStep) // line 33
.toPrevoteOutput(state.p, state.height, state.round, Nil) // line 32
else state.toErrorOutput("ProposalAndPolkaPreviousAndValidConInput")
else state.toErrorOutput("ProposalAndPolkaPreviousAndValidCInput")
// TODO: should we add the event to pending in this case. We would need to
// do this in the executor

// line 34
| PolkaAnyConInput =>
| PolkaAnyCInput =>
if (state.step == PrevoteStep)
// We just report that a timeout should be started. The executor must take care
// of figuring out whether it needs to record the round number and height per
// timeout
state.toTimeoutOutput(PrevoteTimeout)
else state.toErrorOutput("PolkaAnyConInput when not in PrevoteStep")
else state.toErrorOutput("PolkaAnyCInput when not in PrevoteStep")

// line 36
| ProposalAndPolkaAndValidConInput(v) =>
| ProposalAndPolkaAndValidCInput(v) =>
match state.step {
| PrevoteStep =>
state
Expand All @@ -247,69 +247,69 @@ module consensus {
.with("validValue", v) // line 42
.with("validRound", state.round) // line 43
.toNoConsensusOutput()
| _ => state.toErrorOutput("ProposalAndPolkaAndValidConInput when not in PrevoteStep or PrecommitStep")
| _ => state.toErrorOutput("ProposalAndPolkaAndValidCInput when not in PrevoteStep or PrecommitStep")
}

// line 44
| PolkaNilConInput =>
| PolkaNilCInput =>
if (state.step == PrevoteStep)
state
.with("step", PrecommitStep)
.toPrecommitOutput(state.p, state.height, state.round, Nil)
else state.toErrorOutput("PolkaNilConInput when not in PrevoteStep")
else state.toErrorOutput("PolkaNilCInput when not in PrevoteStep")

// line 47
| PrecommitAnyConInput =>
| PrecommitAnyCInput =>
state.toTimeoutOutput(PrecommitTimeout)

// line 49
| ProposalAndCommitAndValidConInput(v) =>
| ProposalAndCommitAndValidCInput(v) =>
if (state.step != DecidedStep)
state
.with("step", DecidedStep)
.toDecidedOutput(v)
else state.toErrorOutput("ProposalAndCommitAndValidConInput when in DecidedStep")
else state.toErrorOutput("ProposalAndCommitAndValidCInput when in DecidedStep")

| ProposalAndPolkaAndInvalidConInput =>
| ProposalAndPolkaAndInvalidCInput =>
// TODO
state.toNoConsensusOutput()

// line 55
| RoundSkipConInput(r) =>
| RoundSkipCInput(r) =>
if (r > state.round)
state.toSkipRoundOutput(r)
else state.toErrorOutput("RoundSkipConInput for round not bigger than current round")
else state.toErrorOutput("RoundSkipCInput for round not bigger than current round")

// line 57
| TimeoutProposeConInput(height_round) =>
| TimeoutProposeCInput(height_round) =>
val h = height_round._1
val r = height_round._2
if (h == state.height and r == state.round and state.step == ProposeStep)
state
.with("step", PrevoteStep)
.toPrevoteOutput(state.p, state.height, state.round, Nil)
else state.toErrorOutput("TimeoutProposeConInput")
else state.toErrorOutput("TimeoutProposeCInput")

// line 61
| TimeoutPrevoteConInput(height_round) =>
| TimeoutPrevoteCInput(height_round) =>
val h = height_round._1
val r = height_round._2
if (h == state.height and r == state.round and state.step == PrevoteStep)
// TODO: should we send precommit nil again ?
state
.with("step", PrecommitStep)
.toPrecommitOutput(state.p, state.height, state.round, Nil)
else state.toErrorOutput("TimeoutPrevoteConInput")
else state.toErrorOutput("TimeoutPrevoteCInput")

// line 65
| TimeoutPrecommitConInput(height_round) =>
| TimeoutPrecommitCInput(height_round) =>
val h = height_round._1
val r = height_round._2
if (h == state.height and r == state.round)
// TODO: here we should call newRound. For this we would need to know whether
// we are proposer for next round.
state.toSkipRoundOutput(state.round + 1)
else state.toErrorOutput("TimeoutPrecommitConInput")
else state.toErrorOutput("TimeoutPrecommitCInput")

}

Expand Down
68 changes: 34 additions & 34 deletions Specs/Quint/consensusTest.qnt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,22 +36,22 @@ module consensusTest {
nondet v = oneOf(Set("A", "B", "C"))
nondet vr = oneOf(Set(-1, 1, 2, 3, 4))
any {
fireInput("Josef", NewHeightConInput(h)),
fireInput("Josef", NewRoundConInput(r)),
fireInput("Josef", NewRoundProposerConInput((r, v))),
fireInput("Josef", ProposalConInput((r, Val(v)))),
fireInput("Josef", ProposalAndPolkaPreviousAndValidConInput((Val(v), r))),
fireInput("Josef", ProposalInvalidConInput),
fireInput("Josef", PolkaNilConInput),
fireInput("Josef", PolkaAnyConInput),
fireInput("Josef", ProposalAndPolkaAndValidConInput(Val(v))),
fireInput("Josef", PrecommitAnyConInput),
fireInput("Josef", ProposalAndCommitAndValidConInput(Val(v))),
fireInput("Josef", RoundSkipConInput(r)),
fireInput("Josef", TimeoutProposeConInput((h, r))),
fireInput("Josef", TimeoutPrevoteConInput((h, r))),
fireInput("Josef", TimeoutPrecommitConInput((h, r))),
fireInput("Josef", ProposalAndPolkaAndInvalidConInput((h, r, Val(v)))),
fireInput("Josef", NewHeightCInput(h)),
fireInput("Josef", NewRoundCInput(r)),
fireInput("Josef", NewRoundProposerCInput((r, v))),
fireInput("Josef", ProposalCInput((r, Val(v)))),
fireInput("Josef", ProposalAndPolkaPreviousAndValidCInput((Val(v), r))),
fireInput("Josef", ProposalInvalidCInput),
fireInput("Josef", PolkaNilCInput),
fireInput("Josef", PolkaAnyCInput),
fireInput("Josef", ProposalAndPolkaAndValidCInput(Val(v))),
fireInput("Josef", PrecommitAnyCInput),
fireInput("Josef", ProposalAndCommitAndValidCInput(Val(v))),
fireInput("Josef", RoundSkipCInput(r)),
fireInput("Josef", TimeoutProposeCInput((h, r))),
fireInput("Josef", TimeoutPrevoteCInput((h, r))),
fireInput("Josef", TimeoutPrecommitCInput((h, r))),
fireInput("Josef", ProposalAndPolkaAndInvalidCInput((h, r, Val(v)))),
}

action unchangedAll = all {
Expand All @@ -71,58 +71,58 @@ module consensusTest {
// This test should call each input type at least once
run DecideNonProposerTest =
initFor(Set("Josef"))
.then(fireInput("Josef", NewRoundConInput(0)))
.then(fireInput("Josef", NewRoundCInput(0)))
.then(_assert(_output == TimeoutOutput(ProposeTimeout)))

.then(fireInput("Josef", ProposalConInput((0, Val("block")))))
.then(fireInput("Josef", ProposalCInput((0, Val("block")))))
.then(_assert(_output.isVoteMsgWith(Prevote, Val("block"))))

.then(fireInput("Josef", ProposalAndPolkaAndValidConInput(Val("block"))))
.then(fireInput("Josef", ProposalAndPolkaAndValidCInput(Val("block"))))
.then(_assert(_output.isVoteMsgWith(Precommit, Val("block"))))

.then(fireInput("Josef", ProposalAndCommitAndValidConInput(Val("block"))))
.then(fireInput("Josef", ProposalAndCommitAndValidCInput(Val("block"))))
.then(_assert(_output == DecidedOutput(Val("block"))))

.then(fireInput("Josef", NewHeightConInput(system.get("Josef").height + 1)))
.then(fireInput("Josef", NewHeightCInput(system.get("Josef").height + 1)))
.then(_assert(system.get("Josef").height == 2))

.then(fireInput("Josef", NewRoundProposerConInput((0, "nextBlock"))))
.then(fireInput("Josef", NewRoundProposerCInput((0, "nextBlock"))))
.then(_assert(_output == ProposalOutput(mkProposal("Josef", 2, 0, "nextBlock", -1))))

.then(fireInput("Josef", ProposalConInput((0, Val("nextBlock"))))) // it is assumed that the proposer receives its own message
.then(fireInput("Josef", ProposalCInput((0, Val("nextBlock"))))) // it is assumed that the proposer receives its own message
.then(_assert(_output.isVoteMsgWith(Prevote, Val("nextBlock")) and system.get("Josef").step == PrevoteStep))

.then(fireInput("Josef", PolkaAnyConInput))
.then(fireInput("Josef", PolkaAnyCInput))
.then(_assert(_output == TimeoutOutput(PrevoteTimeout)))

.then(fireInput("Josef", TimeoutPrevoteConInput((2, 0))))
.then(fireInput("Josef", TimeoutPrevoteCInput((2, 0))))
.then(_assert(_output.isVoteMsgWith(Precommit, Nil) and system.get("Josef").step == PrecommitStep))

.then(fireInput("Josef", PrecommitAnyConInput))
.then(fireInput("Josef", PrecommitAnyCInput))
.then(_assert(_output == TimeoutOutput(PrecommitTimeout)))

.then(fireInput("Josef", TimeoutPrecommitConInput((2, 0))))
.then(fireInput("Josef", TimeoutPrecommitCInput((2, 0))))
.then(_assert(_output == SkipRoundOutput(1)))

.then(fireInput("Josef", NewRoundConInput(1)))
.then(fireInput("Josef", NewRoundCInput(1)))
.then(_assert(_output == TimeoutOutput(ProposeTimeout)))

.then(fireInput("Josef", TimeoutProposeConInput((2, 1))))
.then(fireInput("Josef", TimeoutProposeCInput((2, 1))))
.then(_assert(_output.isVoteMsgWith(Prevote, Nil) and system.get("Josef").step == PrevoteStep))

.then(fireInput("Josef", PolkaNilConInput))
.then(fireInput("Josef", PolkaNilCInput))
.then(_assert(_output.isVoteMsgWith(Precommit, Nil) and system.get("Josef").step == PrecommitStep))

.then(fireInput("Josef", PrecommitAnyConInput))
.then(fireInput("Josef", PrecommitAnyCInput))
.then(_assert(_output == TimeoutOutput(PrecommitTimeout)))

.then(fireInput("Josef", TimeoutPrecommitConInput((2, 1))))
.then(fireInput("Josef", TimeoutPrecommitCInput((2, 1))))
.then(_assert(_output == SkipRoundOutput(2)))

.then(fireInput("Josef", NewRoundConInput(2)))
.then(fireInput("Josef", NewRoundCInput(2)))
.then(_assert(_output == TimeoutOutput(ProposeTimeout)))

.then(fireInput("Josef", ProposalInvalidConInput))
.then(fireInput("Josef", ProposalInvalidCInput))
.then(_assert(_output.isVoteMsgWith(Prevote, Nil) and system.get("Josef").step == PrevoteStep))

}
Loading

0 comments on commit b13ae58

Please sign in to comment.