diff --git a/.github/workflows/quint.yml b/.github/workflows/quint.yml index 03ebab6db..186268d6f 100644 --- a/.github/workflows/quint.yml +++ b/.github/workflows/quint.yml @@ -15,15 +15,22 @@ jobs: quint-typecheck: name: Typecheck runs-on: ubuntu-latest - defaults: - run: - working-directory: ./Specs/Quint steps: - uses: actions/checkout@v4 - uses: actions/setup-node@v3 with: node-version: "18" - run: npm install -g @informalsystems/quint - - run: npx @informalsystems/quint typecheck consensus.qnt - - run: npx @informalsystems/quint typecheck voteBookkeeper.qnt + - run: bash Scripts/quint-forall.sh typecheck Specs/Quint/*.qnt + + quint-test: + name: Test + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-node@v3 + with: + node-version: "18" + - run: npm install -g @informalsystems/quint + - run: bash Scripts/quint-forall.sh test Specs/Quint/*Test.qnt diff --git a/Scripts/quint-forall.sh b/Scripts/quint-forall.sh new file mode 100644 index 000000000..dc0fb1bd7 --- /dev/null +++ b/Scripts/quint-forall.sh @@ -0,0 +1,48 @@ +#!/bin/env bash + +BLUE=$(tput setaf 4) +RED=$(tput setaf 1) +RESET=$(tput sgr0) +UNDERLINE=$(tput smul) + +# [INFO] message in blue +info() +{ + echo "${BLUE}[INFO] $*${RESET}" +} + +# [ERROR] message in red +error() +{ + echo "${RED}[ERROR] $*${RESET} " +} + +# Run `quint $command` on all given files. + +cmd="$1" +files=("${@:2}") + +if [[ "${#files[@]}" -eq 0 ]]; then + echo "${UNDERLINE}Usage:${RESET} $0 [ ...]" + exit 1 +fi + +failed=0 +failed_files=() + +for file in "${files[@]}"; do + info "Running: quint $cmd ${UNDERLINE}$file" + if ! npx @informalsystems/quint "$cmd" "$file"; then + failed_files+=("$file") + failed=$((failed + 1)) + fi + echo "" +done + +if [[ "$failed" -gt 0 ]]; then + error "Failed on $failed files:" + for file in "${failed_files[@]}"; do + error " - ${UNDERLINE}$file" + done + exit 1 +fi diff --git a/Specs/Quint/asyncModelsTest.qnt b/Specs/Quint/asyncModelsTest.qnt new file mode 100644 index 000000000..5b22b976f --- /dev/null +++ b/Specs/Quint/asyncModelsTest.qnt @@ -0,0 +1,158 @@ +// -*- mode: Bluespec; -*- + +module asyncModelsTest { + +import statemachineAsync( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), + Faulty = Set(), + Values = Set("a", "b"), + Rounds = Set(0, 1, 2, 3), + Heights = Set(0) // , 1, 2, 3) +) as N4F0 from "./statemachineAsync" + +run NewRoundTest = { + N4F0::init + .then(N4F0::setNextValueToPropose("v2", "block")) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + .then(N4F0::valStep("v4")) + .then(N4F0::valStep("v1")) + .then(N4F0::deliverProposal("v2", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 })) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v1", step: "Prevote" })) + .then(N4F0::deliverVote("v1", { height: 0, id: "block", round: 0, src: "v2", step: "Prevote" })) + .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v3", step: "Prevote" })) + .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v1", step: "Prevote" })) + .then(N4F0::deliverVote("v2", { height: 0, id: "block", round: 0, src: "v2", step: "Prevote" })) + .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v3", step: "Prevote" })) + .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v1", step: "Prevote" })) + .then(N4F0::deliverVote("v3", { height: 0, id: "block", round: 0, src: "v2", step: "Prevote" })) + .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v3", step: "Prevote" })) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + // timeoutPrevote started + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v1", step: "Precommit" })) + .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v2", step: "Precommit" })) + .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v3", step: "Precommit" })) + .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v1", step: "Precommit" })) + .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v2", step: "Precommit" })) + .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v3", step: "Precommit" })) + .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v1", step: "Precommit" })) + .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v2", step: "Precommit" })) + .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v3", step: "Precommit" })) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + // .then(N4F0::deliverProposal("v1", { height: 0, proposal: "block", round: 1, src: "v2", validRound: -1 })) +/* .then(N4F0::deliverProposal("v1", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 })) + .then(N4F0::deliverProposal("v2", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 })) + .then(N4F0::deliverProposal("v3", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 })) + .then(N4F0::valStep("v1")) + .then(N4F0::valStep("v2")) + .then(N4F0::valStep("v3")) + + */ +} + +import statemachineAsync( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), + Faulty = Set("v1"), + Values = Set("a", "b"), + Rounds = Set(0, 1, 2, 3), + Heights = Set(0) // , 1, 2, 3) +) as N4F1 from "./statemachineAsync" + +// quint run --init=N4F1::init --step=N4F1::step --invariant=N4F1::AgreementInv AsyncModels.qnt +// quint run --init=N4F1::init --step=N4F1::step --invariant=N4F1::ConsensusOutputInv AsyncModels.qnt + +import statemachineAsync( + validators = Set("v1", "v2", "v3", "v4"), + validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1), + Faulty = Set("v1", "v2"), + Values = Set("a", "b"), + Rounds = Set(0), // , 1, 2, 3) + Heights = Set(0) // , 1, 2, 3) +) as N4F2 from "./statemachineAsync" + +// v3 and v4 are correct. v2 is a N4N4F22aulty proposal and proposes diN4N4F22N4N4F22erently to v3 and v4 +// this run leads to disagreement +run DisagreementTest = { + N4F2::init + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v4")) + .then(N4F2::deliverProposal("v3", { height: 0, proposal: "b", round: 0, src: "v2", validRound: -1 })) + .then(N4F2::deliverProposal("v4", { height: 0, proposal: "a", round: 0, src: "v2", validRound: -1 })) + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v4")) + .then(all{ + // they voted diN4F2N4F2erently + assert(N4F2::voteBuffer == Map( + "v3" -> Set({ height: 0, id: "a", round: 0, src: "v4", step: "Prevote" }, + { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }), + "v4" -> Set({ height: 0, id: "a", round: 0, src: "v4", step: "Prevote" }, + { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }))), + N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v1", step: "Prevote" }) + }) + .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v2", step: "Prevote" })) + .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v1", step: "Prevote" })) + .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v2", step: "Prevote" })) + .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" })) + .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v4", step: "Prevote" })) + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v4")) + .then(N4F2::valStep("v4")) + .then(N4F2::valStep("v4")) + .then(all{ + // they precommited diN4F2N4F2erently + assert( N4F2::voteBuffer.get("v3").contains({ height: 0, id: "a", round: 0, src: "v4", step: "Precommit" }) and + N4F2::voteBuffer.get("v4").contains({ height: 0, id: "b", round: 0, src: "v3", step: "Precommit" })), + N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v1", step: "Precommit" }) }) + .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v2", step: "Precommit" })) + .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v1", step: "Precommit" })) + .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v2", step: "Precommit" })) + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v4")) + .then(N4F2::valStep("v4")) + .then(all{ + assert(N4F2::AgreementInv), + N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v4", step: "Precommit" }) }) + .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v3", step: "Precommit" })) + .then(N4F2::valStep("v3")) + .then(N4F2::valStep("v4")) + .then(all{ + assert(not(N4F2::AgreementInv)), + N4F2::unchangedAll}) +} + + + +} \ No newline at end of file diff --git a/Specs/Quint/consensus.qnt b/Specs/Quint/consensus.qnt index cf2d43b4c..3991b091b 100644 --- a/Specs/Quint/consensus.qnt +++ b/Specs/Quint/consensus.qnt @@ -1,7 +1,23 @@ // -*- mode: Bluespec; -*- -module consensus { +/* +TODO: check +- whether we have "step" checks in place everywhere +- "the first time": checks here or in executor +- check against arXiv +- tests +- types (e.g., heights in the messages) +- discuss "decision tree" in executor +- Should we think again about the components and the boundaries (especially between + voteBookkeeper and executor) +- Do we need tests for executor and bookkeeping +- test id(v): most likely we need to change the type of Value_t as Quint doesn't have + string operators. Perhaps we make Value_t = int and then id(v) = -v +*/ + +module consensus { + // a process address is just a string type Address_t = str // a value is also a string @@ -15,36 +31,47 @@ module consensus { // timeours are identified by strings type Timeout_t = str - // the type of propose messages - type ProposeMsg_t = { +// the type of propose messages +type ProposeMsg_t = { src: Address_t, height: Height_t, round: Round_t, - proposal: Value_t, + proposal: Value_t, // an actual value. All other values are id(proposal) validRound: Round_t - } +} - // the type of Prevote and Precommit messages - type VoteMsg_t = { +// the type of Prevote and Precommit messages +type VoteMsg_t = { src: Address_t, height: Height_t, round: Round_t, - step: Step_t, // "prevote" or "precommit" + step: Step_t, // "Prevote" or "Precommit" id: Value_t, - } +} type ConsensusState = { p: Address_t, height : Height_t, round: Round_t, - step: Step_t, // "newRound", propose, prevote, precommit, decided + step: Step_t, // "newRound", propose, Prevote, Precommit, decided lockedRound: Round_t, - lockedValue: Value_t, + lockedValue: Value_t, // id("of a value") validRound: Round_t, - validValue: Value_t, + validValue: Value_t, // id("of a value") //continue } +pure def initConsensusState (v: Address_t) : ConsensusState = { + p: v, + round: -1, + step: "newRound", + height : 0, + lockedRound: -1, + lockedValue: "nil", + validRound: -1, + validValue: "nil" +} + type Event = { name : str, height : Height_t, @@ -54,7 +81,7 @@ type Event = { } // what is a good way to encode optionals? I do with default values -type Result = { +type ConsensusOutput = { name : str, proposal: ProposeMsg_t, voteMessage: VoteMsg_t, @@ -63,10 +90,26 @@ type Result = { skipRound: Round_t } -val consensusEvents = Set( +val consensusOutputs = Set ( + "proposal", + "votemessage", + "timeout", + "decided", + "skipRound" +) + +type ConsResult = { + cs: ConsensusState, + out: ConsensusOutput, +// pending: Set[ConsensusOutput], // TODO: not sure we need this +} + +type ConsensusEvent = str + +val ConsensusEvents = Set( "NewHeight", // Setups the state-machine for a single-height execution "NewRound", // Start a new round, not as proposer. - "NewRoundProposer(Value)", // Start a new round as proposer with the proposed Value. + "NewRoundProposer", // Start a new round as proposer with the proposed Value. "Proposal", // Receive a proposal without associated valid round. "ProposalAndPolkaPreviousAndValid", // Receive a valid proposal with an associated valid round, attested by a a Polka(vr). "ProposalInvalid", // Receive an invalid proposal: L26 and L32 when valid(v) == false @@ -78,22 +121,22 @@ val consensusEvents = Set( "RoundSkip", // Receive +1/3 messages from different validators for a higher round. "TimeoutPropose", // Timeout waiting for proposal. "TimeoutPrevote", // Timeout waiting for prevotes for a value. - "TimeoutPrecommit" // Timeout waiting for precommits for a value. + "TimeoutPrecommit", // Timeout waiting for precommits for a value. +// found after Montebello + "ProposalAndPolkaAndInValid" // TODO: Discuss what to do about it ) /* - - "PolkaValue(ValueId)", // Receive +2/3 prevotes for Value. - "PrecommitValue(ValueId)", // Receive +2/3 precommits for Value. - -) */ + "PolkaValue(ValueId)", // Receive +2/3 Prevotes for Value. + "PrecommitValue(ValueId)", // Receive +2/3 Precommits for Value. +*/ val noProp : ProposeMsg_t = {src: "", height: -1, round: -1, proposal: "", validRound: -1} val noVote : VoteMsg_t = {src: "", height: -1, round: -1, step: "", id: ""} val noTimeout : Timeout_t = "" val noDecided = "" val noSkipRound : Round_t = -1 -val defaultResult : Result = { +val defaultResult : ConsensusOutput = { name: "", proposal: noProp, voteMessage: noVote, @@ -102,224 +145,249 @@ val defaultResult : Result = { skipRound: noSkipRound} -// Implies StartRound(0) -pure def NewHeight (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - val newstate = { ...state, - round: 0, + +pure def NewHeight (state: ConsensusState, ev: Event) : ConsResult = { + if (ev.height > state.height) + val newstate = { p: state.p, + round: -1, + // must be -1, as nothing should be done before a NewRound + // function is called step: "newRound", height : ev.height, lockedRound: -1, lockedValue: "nil", validRound: -1, validValue: "nil" - } - (newstate, defaultResult) + } + {cs: newstate, out: defaultResult } + else + {cs: state, out: defaultResult } } // line 11.14 -pure def NewRoundProposer (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - // TODO: ev.round must match state.round - val newstate = { ...state, round: ev.round, step: "propose"} - val proposal = if (state.validValue != "nil") state.validValue - else ev.value - val result = { ...defaultResult, name: "proposal", - proposal: { src: state.p, - height: state.height, - round: ev.round, - proposal: proposal, - validRound: state.validRound}} - (newstate, result) +pure def NewRoundProposer (state: ConsensusState, ev: Event) : ConsResult = { + if (ev.round > state.round) + val newstate = { ...state, round: ev.round, step: "propose"} + val proposal = if (state.validValue != "nil") state.validValue + else ev.value + val result = { ...defaultResult, name: "proposal", + proposal: { src: state.p, + height: state.height, + round: ev.round, + proposal: proposal, + validRound: state.validRound}} + {cs: newstate, out: result } + else + {cs: state, out: defaultResult } } // line 11.20 -pure def NewRound (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - // TODO: ev.round must match state.round - val newstate = { ...state, round: ev.round, step: "propose" } - val result = { ...defaultResult, name: "timeout", timeout: "timeoutPropose"} // do we need the roundnumber here? YES - (newstate, result) +pure def NewRound (state: ConsensusState, ev: Event) : ConsResult = { + // TODO: discuss comment "ev.round must match state.round" + if (ev.round > state.round) + val newstate = { ...state, round: ev.round, step: "propose" } + val result = { ...defaultResult, name: "timeout", timeout: "TimeoutPropose"} + // 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 + {cs: newstate, out: result} + else + {cs: state, out: defaultResult } } // line 22 -pure def Proposal (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (state.step == "propose") { - val newstate = state.with("step", "prevote") +// Here it is assumed that +// - the value has been checked to be valid +// - it is for the current round +// The executor checks this upon receiving a propose message "ProposalMsg" +pure def Proposal (state: ConsensusState, ev: Event) : ConsResult = { + if (state.step == "propose") + val newstate = { ...state, step: "Prevote" } if (state.lockedRound == -1 or state.lockedValue == ev.value) val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, - step: "prevote", + step: "Prevote", id: ev.value}} - (newstate, result) + {cs: newstate, out: result} else val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, - step: "prevote", + step: "Prevote", id: "nil"}} - (newstate, result) - } + {cs: newstate, out: result} + else + {cs: state, out: defaultResult} + // This should be dead code as the executor checks the step +} + +// line 26 +pure def ProposalInvalid (state: ConsensusState, ev: Event) : ConsResult = { + if (state.step == "propose") + val newstate = state.with("step", "Prevote") + val result = { ...defaultResult, name: "votemessage", + voteMessage: { src: state.p, + height: state.height, + round: state.round, + step: "Prevote", + id: "nil"}} + {cs: newstate, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } // line 28 -pure def ProposalAndPolkaPreviousAndValid (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (state.step == "propose" and ev.vr >= 0 and ev.vr < state.round) { - val newstate = state.with("step", "prevote") +pure def ProposalAndPolkaPreviousAndValid (state: ConsensusState, ev: Event) : ConsResult = { + if (state.step == "propose" and ev.vr >= 0 and ev.vr < state.round) + val newstate = state.with("step", "Prevote") if (state.lockedRound <= ev.vr or state.lockedValue == ev.value) val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, - step: "prevote", + step: "Prevote", id: ev.value}} - (newstate, result) + {cs: newstate, out: result} else val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, - step: "prevote", + step: "Prevote", id: "nil"}} - (newstate, result) - } + {cs: newstate, out: result} else - (state, defaultResult) -} - -// Lines 22 or 28 with valid(v) == false -pure def ProposalInvalid (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (state.step == "propose") { - val newstate = state.with("step", "prevote") - val result = { ...defaultResult, name: "votemessage", - voteMessage: { src: state.p, - height: state.height, - round: state.round, - step: "prevote", - id: "nil"}} - (newstate, result) - } - else { - (state, defaultResult ) - } + {cs: state, out: defaultResult} + // TODO: should we add the event to pending in this case. We would need to + // do this in the executor } // line 34 -pure def PolkaAny (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (state.step == "prevote") { - val result = { ...defaultResult, name: "timeout", timeout: "timeoutPrevote" } // do we need the roundnumber here? YES - (state, result) - } +pure def PolkaAny (state: ConsensusState, ev: Event) : ConsResult = { + if (state.step == "Prevote") + val result = { ...defaultResult, name: "timeout", timeout: "TimeoutPrevote" } + // 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 + {cs: state, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } // line 36 -pure def ProposalAndPolkaAndValid (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { +pure def ProposalAndPolkaAndValid (state: ConsensusState, ev: Event) : ConsResult = { val auxState = { ...state, validValue: ev.value, validRound: state.round } - if (state.step == "prevote") { + if (state.step == "Prevote") val newstate = { ...auxState, lockedValue: ev.value, lockedRound: state.round, - step: "precommit" } + step: "Precommit" } val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, - step: "precommit", + step: "Precommit", id: ev.value}} - (newstate, result) - } - else { - // TODO: if state > prevote, we should update the valid round! - (state, defaultResult) - } + {cs: newstate, out: result} + else if (state.step == "Precommit") + // TODO: check whether Daniel's comment + // "if state > prevote, we should update the valid round!" + // was properly addressed + {cs: auxState, out: defaultResult} + else + {cs: state, out: defaultResult} + // TODO: should we add the event to pending in this case. We would need to + // do this in the executor } // line 44 -pure def PolkaNil (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (state.step == "prevote") - val newstate = { ...state, step: "precommit"} +pure def PolkaNil (state: ConsensusState, ev: Event) : ConsResult = { + if (state.step == "Prevote") + val newstate = { ...state, step: "Precommit"} val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, height: state.height, round: state.round, - step: "precommit", + step: "Precommit", id: "nil"}} - (newstate, result) + {cs: newstate, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } // line 47 -pure def PrecommitAny (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (state.step == "precommit") { - val result = { ...defaultResult, name: "timeout", timeout: "timeoutPrecommit" } // do we need the roundnumber here? YES - (state, result) - } - else - (state, defaultResult) +pure def PrecommitAny (state: ConsensusState, ev: Event) : ConsResult = { + val result = { ...defaultResult, name: "timeout", timeout: "TimeoutPrecommit" } + {cs: state, out: result} } // line 49 -pure def ProposalAndCommitAndValid (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { +pure def ProposalAndCommitAndValid (state: ConsensusState, ev: Event) : ConsResult = { if (state.step != "decided") { val newstate = { ...state, step: "decided"} val result = { ...defaultResult, name: "decided", decided: ev.value} - (newstate, result) + {cs: newstate, out: result} } else - (state, defaultResult) -} + {cs: state, out: defaultResult} +} // line 55 -pure def RoundSkip (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { +pure def RoundSkip (state: ConsensusState, ev: Event) : ConsResult = { if (ev.round > state.round) val result = { ...defaultResult, name: "skipRound", skipRound: ev.round } - (state, result) + {cs: state, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } -pure def TimeoutPropose (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { +pure def TimeoutPropose (state: ConsensusState, ev: Event) : ConsResult = { if (ev.height == state.height and ev.round == state.round and state.step == "propose") - val newstate = { ...state, step: "prevote"} + val newstate = { ...state, step: "Prevote"} val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, - height: state.height, - round: state.round, - step: "prevote", - id: "nil"}} - (newstate, result) + height: state.height, + round: state.round, + step: "Prevote", + id: "nil"}} + {cs: newstate, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } -pure def TimeoutPrevote (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { - if (ev.height == state.height and ev.round == state.round and state.step == "prevote") - val newstate = { ...state, step: "precommit"} +pure def TimeoutPrevote (state: ConsensusState, ev: Event) : ConsResult = { + if (ev.height == state.height and ev.round == state.round and state.step == "Prevote") + val newstate = { ...state, step: "Precommit"} + // TODO: should we send precommit nil again ? val result = { ...defaultResult, name: "votemessage", voteMessage: { src: state.p, - height: state.height, - round: state.round, - step: "precommit", - id: "nil"}} - (newstate, result) + height: state.height, + round: state.round, + step: "Precommit", + id: "nil"}} + {cs: newstate, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } -pure def TimeoutPrecommit (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { +pure def TimeoutPrecommit (state: ConsensusState, ev: Event) : ConsResult = { if (ev.height == state.height and ev.round == state.round) + // TODO: here we should call newRound. For this we would need to know whether + // we are proposer for next round. val result = {...defaultResult, name: "skipRound", skipRound: state.round + 1} - (state, result) + {cs: state, out: result} else - (state, defaultResult) + {cs: state, out: defaultResult} } -pure def consensus (state: ConsensusState, ev: Event) : (ConsensusState, Result) = { +/* ********************************************************* + * Main entry point + * ********************************************************/ + +pure def consensus (state: ConsensusState, ev: Event) : ConsResult = { if (ev.name == "NewHeight") NewHeight (state, ev) else if (ev.name == "NewRoundProposer") @@ -349,167 +417,8 @@ pure def consensus (state: ConsensusState, ev: Event) : (ConsensusState, Result) else if (ev.name == "TimeoutPrecommit") TimeoutPrecommit (state, ev) else - (state, defaultResult) -} - -/* **************************************************************************** - * Global state - * ************************************************************************* */ - -var system : Address_t -> ConsensusState - -// Auxiliary fields for better debugging -var _Result : Result -var _Event : Event - - -pure def initialProcess (name: Address_t) : ConsensusState = { - { p: name, height : 1, round: 0, step: "newRound", lockedRound: -1, lockedValue: "nil", validRound: -1, validValue: "nil"} -} - -action init = all { - system' = Map ("Josef" -> initialProcess("Josef")), - _Result' = defaultResult, - _Event' = {name : "Initial", - height : -1, - round: -1, - value: "", - vr: -1} -} - - - -// just to write a test. -action FireEvent(eventName: str, proc: Address_t, h: Height_t, r: Round_t, value: Value_t, vr: Round_t) : bool = all { - val event = {name : eventName, - height : h, - round: r, - value: value, - vr: vr} - val res = consensus(system.get(proc), event ) - all { - system' = system.put(proc, res._1), - _Result' = res._2, - _Event' = event - } -} - -action step = any { - nondet name = oneOf(consensusEvents) - nondet height = 1//oneOf(1.to(4)) - nondet round = 0//oneOf(1.to(4)) - nondet value = oneOf(Set("block 1", "block 2", "block 3")) - nondet vr = oneOf(Set(-1, 1, 2, 3, 4)) - FireEvent(name, "Josef", height, round, value, vr) -} - -action unchangedAll = all { - system' = system, - _Result' = _Result, - _Event' = _Event, + {cs: state, out: defaultResult} } - -// This test should call each event at least once -run DecideNonProposerTest = { - init - .then(FireEvent("NewRound", "Josef", 1, 0, "", -1)) - .then(all{ - assert(_Result.timeout == "timeoutPropose"), - unchangedAll - }) - .then(FireEvent("Proposal", "Josef", 1, 0, "block", -1)) - .then(all{ - assert(_Result.voteMessage.step == "prevote" and _Result.voteMessage.id == "block"), - unchangedAll - }) - .then(FireEvent("ProposalAndPolkaAndValid", "Josef", 1, 0, "block", -1)) - .then(all{ - assert(_Result.voteMessage.step == "precommit" and _Result.voteMessage.id == "block"), - unchangedAll - }) - .then(FireEvent("ProposalAndCommitAndValid", "Josef", 1, 0, "block", -1)) - .then(all{ - assert(_Result.decided == "block"), - unchangedAll - }) - .then(FireEvent("NewHeight", "Josef", system.get("Josef").height + 1, 0, "", -1)) - .then(all{ - assert(system.get("Josef").height == 2), - unchangedAll - }) - .then(FireEvent("NewRoundProposer", "Josef", 2, 0, "nextBlock", -1)) - .then(all{ - // TODO: should we prevent timeout in this case? See issue #21 - assert(_Result.timeout != "timeoutPropose" and _Result.proposal.proposal == "nextBlock"), - unchangedAll - }) - .then(FireEvent("Proposal", "Josef", 2, 0, "nextBlock", -1)) // it is assumed that the proposer receives its own message - .then(all{ - assert(_Result.voteMessage.step == "prevote" and system.get("Josef").step == "prevote"), - unchangedAll - }) - .then(FireEvent("PolkaAny", "Josef", 2, 0, "nextBlock", -1)) - .then(all{ - assert(_Result.timeout == "timeoutPrevote"), - unchangedAll - }) - .then(FireEvent("TimeoutPrevote", "Josef", 2, 0, "nextBlock", -1)) // FIXME: why a value for the timeout? - .then(all{ - assert(_Result.voteMessage.step == "precommit" and _Result.voteMessage.id == "nil" and - system.get("Josef").step == "precommit"), - unchangedAll - }) - .then(FireEvent("PrecommitAny", "Josef", 2, 0, "nextBlock", -1)) - .then(all{ - assert(_Result.timeout == "timeoutPrecommit"), - unchangedAll - }) - .then(FireEvent("TimeoutPrecommit", "Josef", 2, 0, "nextBlock", -1)) - .then(all{ - assert(_Result.skipRound == 1), - unchangedAll - }) - .then(FireEvent("NewRound", "Josef", 2, 1, "", -1)) - .then(all{ - assert(_Result.timeout == "timeoutPropose"), - unchangedAll - }) - .then(FireEvent("TimeoutPropose", "Josef", 2, 1, "nextBlock", -1)) - .then(all{ - assert(_Result.voteMessage.step == "prevote" and _Result.voteMessage.id == "nil" and - system.get("Josef").step == "prevote"), - unchangedAll - }) - .then(FireEvent("PolkaNil", "Josef", 2, 1, "nextBlock", -1)) - .then(all{ - assert(_Result.voteMessage.step == "precommit" and _Result.voteMessage.id == "nil" and - system.get("Josef").step == "precommit"), - unchangedAll - }) - .then(FireEvent("PrecommitAny", "Josef", 2, 1, "nextBlock", -1)) - .then(all{ - assert(_Result.timeout == "timeoutPrecommit"), - unchangedAll - }) - .then(FireEvent("TimeoutPrecommit", "Josef", 2, 1, "nextBlock", -1)) - .then(all{ - assert(_Result.skipRound == 2), - unchangedAll - }) - .then(FireEvent("NewRound", "Josef", 2, 2, "", -1)) - .then(all{ - assert(_Result.timeout == "timeoutPropose"), - unchangedAll - }) - .then(FireEvent("ProposalInvalid", "Josef", 2, 2, "", -1)) - .then(all{ - assert(_Result.voteMessage.step == "prevote" and _Result.voteMessage.id == "nil" and - system.get("Josef").step == "prevote"), - unchangedAll - }) -} - - } diff --git a/Specs/Quint/consensusTest.qnt b/Specs/Quint/consensusTest.qnt new file mode 100644 index 000000000..fb7a2df24 --- /dev/null +++ b/Specs/Quint/consensusTest.qnt @@ -0,0 +1,129 @@ +// -*- mode: Bluespec; -*- + +module consensusTest { + +import consensus.* from "./consensus" + +/* **************************************************************************** + * Global state + * ************************************************************************* */ + +var system : Address_t -> ConsensusState +var _Result : ConsensusOutput +var _Event : Event + + +pure def initialProcess (name: Address_t) : ConsensusState = { + { p: name, height : 1, round: -1, step: "newRound", lockedRound: -1, lockedValue: "nil", validRound: -1, validValue: "nil"} +} + +action init = all { + system' = Map ("Josef" -> initialProcess("Josef")), + _Result' = defaultResult, + _Event' = { name : "Initial", + height : 0, + round: -1, + value: "", + vr: -1} +} + + + +// just to write a test. +action FireEvent(eventName: str, proc: Address_t, h: Height_t, r: Round_t, value: Value_t, vr: Round_t) : bool = all { + val event = { name : eventName, + height : h, + round: r, + value: value, + vr: vr} + val res = consensus(system.get(proc), event ) + all { + system' = system.put(proc, res.cs), + _Result' = res.out, + _Event' = event + } +} + +action step = any { + nondet name = oneOf(ConsensusEvents) + nondet height = 1//oneOf(1.to(4)) + nondet round = 0//oneOf(1.to(4)) + nondet value = oneOf(Set("block 1", "block 2", "block 3")) + nondet vr = oneOf(Set(-1, 1, 2, 3, 4)) + FireEvent(name, "Josef", height, round, value, vr) +} + +action unchangedAll = all { + system' = system, + _Result' = _Result, + _Event' = _Event, +} + +// This test should call each event at least once +run DecideNonProposerTest = { + init + .then(FireEvent("NewRound", "Josef", 1, 0, "", -1)) + .then(all{ + assert(_Result.timeout == "TimeoutPropose"), + FireEvent("Proposal", "Josef", 1, 0, "block", -1)}) + .then(all{ + assert(_Result.voteMessage.step == "Prevote" and _Result.voteMessage.id == "block"), + FireEvent("ProposalAndPolkaAndValid", "Josef", 1, 0, "block", -1)}) + .then(all{ + assert(_Result.voteMessage.step == "Precommit" and _Result.voteMessage.id == "block"), + FireEvent("ProposalAndCommitAndValid", "Josef", 1, 0, "block", -1)}) + .then(all{ + assert(_Result.decided == "block"), + FireEvent("NewHeight", "Josef", system.get("Josef").height + 1, 0, "", -1)}) + .then(all{ + assert(system.get("Josef").height == 2), + FireEvent("NewRoundProposer", "Josef", 2, 0, "nextBlock", -1)}) + .then(all{ + assert(_Result.timeout != "TimeoutPropose" and _Result.proposal.proposal == "nextBlock"), + FireEvent("Proposal", "Josef", 2, 0, "nextBlock", -1)}) // it is assumed that the proposer receives its own message + .then(all{ + assert(_Result.voteMessage.step == "Prevote" and system.get("Josef").step == "Prevote"), + FireEvent("PolkaAny", "Josef", 2, 0, "nextBlock", -1)}) + .then(all{ + assert(_Result.timeout == "TimeoutPrevote"), + FireEvent("TimeoutPrevote", "Josef", 2, 0, "nextBlock", -1)}) + .then(all{ + assert(_Result.voteMessage.step == "Precommit" and _Result.voteMessage.id == "nil" and + system.get("Josef").step == "Precommit"), + FireEvent("PrecommitAny", "Josef", 2, 0, "nextBlock", -1)}) + .then(all{ + assert(_Result.timeout == "TimeoutPrecommit"), + FireEvent("TimeoutPrecommit", "Josef", 2, 0, "nextBlock", -1)}) + .then(all{ + assert(_Result.skipRound == 1), + FireEvent("NewRound", "Josef", 2, 1, "", -1)}) + .then(all{ + assert(_Result.timeout == "TimeoutPropose"), + FireEvent("TimeoutPropose", "Josef", 2, 1, "nextBlock", -1)}) + .then(all{ + assert(_Result.voteMessage.step == "Prevote" and _Result.voteMessage.id == "nil" and + system.get("Josef").step == "Prevote"), + FireEvent("PolkaNil", "Josef", 2, 1, "nextBlock", -1)}) + .then(all{ + assert(_Result.voteMessage.step == "Precommit" and _Result.voteMessage.id == "nil" and + system.get("Josef").step == "Precommit"), + FireEvent("PrecommitAny", "Josef", 2, 1, "nextBlock", -1)}) + .then(all{ + assert(_Result.timeout == "TimeoutPrecommit"), + FireEvent("TimeoutPrecommit", "Josef", 2, 1, "nextBlock", -1)}) + .then(all{ + assert(_Result.skipRound == 2), + FireEvent("NewRound", "Josef", 2, 2, "", -1)}) + .then(all{ + assert(_Result.timeout == "TimeoutPropose"), + FireEvent("ProposalInvalid", "Josef", 2, 2, "", -1)}) + .then(all{ + assert(_Result.voteMessage.step == "Prevote" and _Result.voteMessage.id == "nil" and + system.get("Josef").step == "Prevote"), + unchangedAll + }) +} + + +} + diff --git a/Specs/Quint/executor.qnt b/Specs/Quint/executor.qnt new file mode 100644 index 000000000..718dc522c --- /dev/null +++ b/Specs/Quint/executor.qnt @@ -0,0 +1,590 @@ +// -*- mode: Bluespec; -*- + +/* + TODO: round switch upon f+1 messages from the future is not done yet. We need to catch + the event from the bookkeeper +*/ + +module executor { + +import consensus.* from "./consensus" +import voteBookkeeper.* from "./voteBookkeeper" + +pure def initBookKeeper (totalVotingPower: int): Bookkeeper = + { height: 0, totalWeight: totalVotingPower, rounds: Map() } + + +type ExecutorState = { + bk : Bookkeeper, + cs : ConsensusState, + proposals: Set[ProposeMsg_t], + valset: Address_t -> int, + executedEvents: List[(Event, Height_t, Round_t)], // We record that to have the information in the trace + pendingEvents: Set[(Event, Height_t, Round_t)], + started: bool, + applyvotesResult: ExecutorEvent, //debug TODO + chain : List[Value_t], + nextValueToPropose: Value_t, +} + +pure def initExecutor (v: Address_t, vs: Address_t -> int) : ExecutorState = { + val tvp = vs.keys().fold(0, (sum, key) => sum + vs.get(key)) + { + bk: initBookKeeper(tvp), + cs: initConsensusState(v), + proposals: Set(), + valset: vs, + executedEvents: List(), + pendingEvents: Set(), + started: false, + applyvotesResult: toEvent(0, "", {name: "", value: ""}), // debug + chain : List(), + nextValueToPropose: "", + } +} + +type NodeState = { + es: ExecutorState, + timeout: Set[(Timeout_t, Height_t, Round_t)], + incomingVotes: Set[VoteMsg_t], + incomingProposals: Set[ProposeMsg_t], +} + +pure def initNode (v: Address_t, vs: Address_t -> int) : NodeState = { + es: initExecutor(v,vs), + timeout: Set(), + incomingVotes: Set(), + incomingProposals: Set(), +} + +type ExecutorInput = { + name: str, // TODO: make a set of values. + proposal: ProposeMsg_t, + vote: VoteMsg_t, + timeout: str, + event: Event, + nextValueToPropose: Value_t +} + +val defaultInput: ExecutorInput = { + name: "", + proposal: { src: "", height: 0, round: 0, proposal: "", validRound: 0 }, + vote: { src: "", height: 0, round: 0, step: "", id: "", }, + timeout: "", + event: defaultEvent, + nextValueToPropose: "" +} + +// this is to match the type from the bookkeeper. When we add heights there we should +// unify +pure def toVote (v: VoteMsg_t) : Vote = + { typ: v.step, round: v.round, value: v.id, address: v.src } + +val defaultEvent : Event = { name : "", height : 0, round: 0, value: "", vr: 0 } + +/* +encode the following decision tree + +proposal + invalid -> consensus event + valid: BK list of events + generate all Consensus events C + feed all events to Consensus + +Precommit + BK applyVote + (see whether we can make (A) 2f+1 Any for current or + (B) 2f+1 plus proposal for current) + -> feed all events to Consensus + +Prevote + BK applyVote + For current round PolkaVal -> PolkaAny and PolkaNil -> PolkaAny: list of Events + check proposal: list of Consensus evens (considering line 28) + -> feed all events to Consensus +*/ + +val emptyProposal : ProposeMsg_t= + { src: "none", height: 0, round: 0, proposal: "none", validRound: 0 } + +val emptyVote = + { src: "none", height: 0, round: 0, step: "None", id: "None" } + +// +// Interface to app and/or mempool (Proposer, getValue, valid) +// + +// In the implementation this could be a callback to the application. But it needs to be +// a function, that is, any two validators need to agree on this +pure def Proposer(valset: Address_t -> int, height: Height_t, round: Round_t) : Address_t = { + // Here: rotating coordinator. We can do something more clever actually using the valset + val prop = (round + 1) % 4 + if (prop == 0) "v1" + else if (prop == 1) "v2" + else if (prop == 2) "v3" + else "v4" +} + +pure def getValue(es: ExecutorState) : Value_t = es.nextValueToPropose + +pure def valid(p: ProposeMsg_t) :bool = { + // for simulation, if the value is "invalid", so is the proposal + // if this is to become "non-deterministic", we must push it + // and its use into the state machine + p.proposal != "invalid" +} + +// efficient hashing function +pure def id(v) = v + + +type ConsensusCall = { + es: ExecutorState, + event: Event, + out: ConsensusOutput +} + +pure def ListContains(list, value) = + list.foldl(false, (s,x) => s or x == value) + +// check whether the event has been already sent to consensus. If not, do so. +pure def callConsensus (es: ExecutorState, bk: Bookkeeper, ev: Event) : (ExecutorState, ConsensusOutput) = { + // check whether we already executed the event already + if (es.executedEvents.ListContains((ev, es.cs.height, es.cs.round))) + ( { ...es, bk:bk, cs: es.cs}, + defaultResult ) + else + val res = consensus(es.cs, ev) + ( { ...es, bk: bk, cs: res.cs, executedEvents: es.executedEvents.append((ev, res.cs.height, res.cs.round))}, + res.out ) +} + + +// We do this if the executor receives a Precommit +pure def Precommit (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) : (ExecutorState, ConsensusOutput) = { + if (eev.name == "PrecommitValue") + if (es.proposals.exists(x => eev.round == x.round and eev.value == id(x.proposal))) { + callConsensus(es, es.bk, { name : "ProposalAndCommitAndValid", + height : input.vote.height, + round: input.vote.round, + value: input.vote.id, + vr: -1}) + } + else { + if (eev.round == es.cs.round) { + callConsensus(es, es.bk, { name: "PrecommitAny", + height: input.vote.height, + round: input.vote.round, + value: input.vote.id, + vr: -1}) + } + else if (eev.round > es.cs.round) { + // if it is for a future round I can trigger skipround + // TODO: should we really do this. It is dead code as the f+1 event already happened + callConsensus(es, es.bk, { name: "RoundSkip", + height: input.vote.height, + round: input.vote.round, + value: input.vote.id, + vr: -1}) + } + else { + // messages from past round -> ignore + (es, defaultResult) + } + } + else if (eev.name == "PrecommitAny" and eev.round == es.cs.round) { + callConsensus(es, es.bk, { name: "PrecommitAny", + height: input.vote.height, + round: input.vote.round, + value: input.vote.id, + vr: -1}) + } + else + // none of the supported Precommit events. Do nothing + // TODO: catch skip round event + (es, defaultResult) +} + + +// We do this if the executor receives a Prevote +pure def Prevote (es: ExecutorState, input: ExecutorInput, eev: ExecutorEvent) : (ExecutorState, ConsensusOutput) = { + // TODO: events do not have heights now. + // TODO: Polka implications missing. + if (eev.name == "PolkaValue") + if (eev.round < es.cs.round and + es.proposals.exists(p => p.round == es.cs.round and + eev.round == p.validRound and id(p.proposal) == eev.value)) + callConsensus(es, es.bk, { name: "ProposalAndPolkaPreviousAndValid", + height: es.cs.height, + round: es.cs.round, + value: eev.value, + vr: eev.round}) + // TODO: the value should come from the proposal + else if (eev.round == es.cs.round and + es.proposals.exists(p => p.round == es.cs.round and + id(p.proposal) == eev.value)) + callConsensus(es, es.bk, { name: "ProposalAndPolkaAndValid", + height: es.cs.height, + round: es.cs.round, + value: eev.value, + vr: eev.round}) + else + // we don't have a matching proposal so we do nothing + // TODO: we might check whether it is for a future round and jump + (es, defaultResult) + else if (eev.name == "PolkaAny") + if (eev.round == es.cs.round) + // call consensus and remember that we did it + callConsensus(es, es.bk, { name: "PolkaAny", + height: es.cs.height, + round: es.cs.round, + value: eev.value, + vr: eev.round}) + else + // TODO: we might check whether it is for a future round and jump + (es, defaultResult) + else if (eev.name == "PolkaNil" and eev.round == es.cs.round) + callConsensus(es, es.bk, { name: "PolkaNil", + height: es.cs.height, + round: es.cs.round, + value: eev.value, + vr: eev.round}) + else + // TODO: catch skip round event + (es, defaultResult) +} + + +// We do this if a timeout expires at the executor +pure def Timeout (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = { + // TODO: We assume that the timeout event is always for the current round. If this is not + // the case, we need to encode it in the input to which round the timeout belongs + val event: Event = {name: input.timeout, + height: es.cs.height, + round: es.cs.round, + value: "", + vr: 0} + callConsensus(es, es.bk, event) +} + + +// We do this if the executor receives a proposal +pure def ProposalMsg (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = { + val newES = { ...es, proposals: es.proposals.union(Set(input.proposal))} + if (input.proposal.src != Proposer(es.valset, input.proposal.height, input.proposal.round)) + // proposer does not match the height/round of the proposal + // keep ES (don't use newES here), that is, drop proposal + (es, defaultResult) + else if (valid(input.proposal)) + val receivedCommit = checkThreshold( newES.bk, + input.proposal.round, + "Precommit", + {name: "PrecommitValue", + value: id(input.proposal.proposal)}) + if (receivedCommit) + // we have a commit that matches the proposal. We don't need to compare against + // es.cs.round + // TODO: check heights in bookkeeper + callConsensus( newES, + newES.bk, + { name: "ProposalAndCommitAndValid", + height: input.proposal.height, + round: input.proposal.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}) + else if (input.proposal.round != es.cs.round or input.proposal.height != es.cs.round) + // the proposal is from the right proposer and valid, but not for this round + // keep the proposal, do nothing else + (newES, defaultResult) + else + // for current round and q, valid, and from right proposer + val receivedPolkaValidRoundVal = checkThreshold(newES.bk, + input.proposal.validRound, + "Prevote", + {name: "PolkaValue", + value: id(input.proposal.proposal)}) + val receivedPolkaCurrentVal = checkThreshold( newES.bk, + newES.cs.round, + "Prevote", + {name: "PolkaValue", + value: id(input.proposal.proposal)}) + val receivedCommitCurrentVal = checkThreshold( newES.bk, + newES.cs.round, + "Precommit", + {name: "PrecommitValue", + value: id(input.proposal.proposal)}) + if (newES.cs.step == "propose") + if (input.proposal.validRound == -1) + if (receivedPolkaCurrentVal) + callConsensus( newES, + newES.bk, + { name: "ProposalAndPolkaAndValid", + height: input.proposal.height, + round: input.proposal.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}) + else + callConsensus( newES, + newES.bk, + { name: "Proposal", + height: input.proposal.height, + round: input.proposal.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}) + else if (receivedPolkaValidRoundVal) + callConsensus( newES, + newES.bk, + { name: "ProposalAndPolkaPreviousAndValid", + height: input.proposal.height, + round: input.proposal.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}) + else + (newES, defaultResult) + else if (newES.cs.step == "Prevote" or newES.cs.step == "Precommit") + if (receivedCommitCurrentVal) + // here we need to call both, Commit and Polka. + // We do commit and append pola to pending + val pend = ( { name: "ProposalAndPolkaAndValid", + height: newES.cs.height, + round: newES.cs.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}, + newES.cs.height, + newES.cs.round) + callConsensus( { ...newES, pendingEvents: newES.pendingEvents.union(Set(pend))}, + newES.bk, + { name: "ProposalAndCommitAndValid", + height: newES.cs.height, + round: newES.cs.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}) + else if (receivedPolkaCurrentVal) + callConsensus( newES , + newES.bk, + { name: "ProposalAndPolkaAndValid", + height: newES.cs.height, + round: newES.cs.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound}) + else + (newES, defaultResult) + else + (newES, defaultResult) + else + // (not(valid(input.proposal))) + // keep ES (don't use newES here), that is, drop proposal + if (es.cs.step == "propose" and es.cs.round == input.proposal.round and es.cs.height == input.proposal.height) + if (checkThreshold(es.bk, es.cs.round, "Prevote", {name: "PolkaValue", value: id(input.proposal.proposal)})) + val event: Event = {name: "ProposalAndPolkaAndInValid", + height: es.cs.height, + round: es.cs.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound} + callConsensus(es, es.bk, event) + else + val event: Event = {name: "ProposalInvalid", + height: es.cs.height, + round: es.cs.round, + value: id(input.proposal.proposal), + vr: input.proposal.validRound} + callConsensus(es, es.bk, event) + else + (es, defaultResult) +} + + +// We do this when we need to jump to a new round +pure def skip (es: ExecutorState, r: int) : (ExecutorState, ConsensusOutput) = { + // line 15 + val prop = if (es.cs.validValue != "nil") es.cs.validValue + else getValue(es) + if (Proposer(es.valset, es.cs.height, es.cs.round + 1) == es.cs.p) + callConsensus(es, es.bk, { name: "NewRoundProposer", + height: es.cs.height, + round: r, + // what value? + value: prop, + vr: es.cs.validRound}) + else + callConsensus(es, es.bk, { name: "NewRound", + height: es.cs.height, + round: r, + value: "", + vr: es.cs.validRound}) + // what do we do now in the new round? Shouldn't we look whether we can build an event. + // TODO: compute pending events. +} + + +// We do this when we have decided +pure def decided (es: ExecutorState, res: ConsensusOutput) : (ExecutorState, ConsensusOutput) = { + // here we call consensus to set a new height, that is, to initialize the state machine + // and then we call skip to start round 0 + +/* // The following can be used to get to the next height. For now this + // function does nothing + // If we choose to move getValue out of the executor logic into the environment (gossip) + // then, we would not do this here, but expect the environment to create a (to be defined) + // ExecutorInput + val s1 = callConsensus(es, es.bk, {name : "NewHeight", + height : es.cs.height + 1, + round: -1, + value: "", + vr: es.cs.validRound}) + skip (s1._1, 0) +*/ + ({ ...es, chain: es.chain.append(res.decided) } , res) +} + + +// take input out of pending events and then call consensus with that event +// We do this when the executor is asked to work on pending events +pure def PendingEvent (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = { + val newState = { ...es, pendingEvents: es.pendingEvents.exclude(Set((input.event, es.cs.height, es.cs.round)))} + callConsensus(newState, es.bk, input.event) +} + + +pure def setValue(es: ExecutorState, value: Value_t) : (ExecutorState, ConsensusOutput) = + ({ ...es, nextValueToPropose: value }, defaultResult) + + + + +/* ********************************************************* + * Main entry point + * ********************************************************/ + +// TODO: return ConsensusEvent so that we know from outside what event was fired. +pure def executor (es: ExecutorState, input: ExecutorInput) : (ExecutorState, ConsensusOutput) = { + // TODO: shall we check whether the sender actually is in the validator set + if (input.name == "proposal") { + val cons_res = ProposalMsg(es, input) + if (cons_res._2.name == "decided") + decided (cons_res._1, cons_res._2) + else + cons_res + } + else if (input.name == "votemessage" and input.vote.step == "Precommit") { + val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src)) + val newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event} + // only a commit event can come here. + val cons_res = Precommit(newES, input, res.event) + if (cons_res._2.name == "decided") + decided (cons_res._1, cons_res._2) + else + cons_res + } + else if (input.name == "votemessage" and input.vote.step == "Prevote") { + val res = applyVote(es.bk, toVote(input.vote), es.valset.get(input.vote.src)) + val newES = { ...es, bk: res.bookkeeper, applyvotesResult: res.event} + // only a commit event can come here. + Prevote(newES, input, res.event) + } + else if (input.name == "timeout") { + val res = Timeout(es, input) + // result should be vote or skip + if (res._2.name == "skipRound") + skip (res._1, res._2.skipRound) + // skip starts a new round. This may involve getValue. If we choose to move the getValue + // logic out of the executor, we wouldn't call skip here but add a (to be defined) + // ExecutorInput + else + res + } + else if (input.name == "start") { + // + val new = { ...es, started: true} + skip (new, 0) + } + else if (input.name == "pending") { + PendingEvent(es, input) + } + else if (input.name == "SetNextProposedValue") + setValue(es, input.nextValueToPropose) + else + (es, defaultResult) +} + + +// This is a simple function that figures out in what external events (messages, +// timeouts, etc.) the node should act. +// currently this is linked in via the state machine. But we can move it into +// the functional layer/ +pure def nextAction (state: NodeState) : (NodeState, ExecutorInput) = { + if (not(state.es.started)) + (state, { ...defaultInput, name: "start" }) + + else if (state.incomingProposals != Set()) + // pick proposal, remove it from incoming + // val prop = state.incomingProposals.chooseSome() + val prop = state.incomingProposals.fold (emptyProposal, (sum, y) => y) + val newstate = { ...state, incomingProposals: state.incomingProposals.exclude(Set(prop))} + (newstate, { ...defaultInput, name: "proposal", proposal: prop}) + + else if (state.incomingVotes != Set()) + // pick vote, remove it from incoming + // val vote = state.incomingVotes.chooseSome() + val vote = state.incomingVotes.fold(emptyVote, (sum, y) => y) + val newstate = { ...state, incomingVotes: state.incomingVotes.exclude(Set(vote))} + (newstate, { ...defaultInput, name: "votemessage", vote: vote}) + + else if (state.timeout.exists(x => x._2 == state.es.cs.height and + x._3 == state.es.cs.round)) + // pick timeout, remove it from incoming + val timeouts = state.timeout.filter(x => x._2 == state.es.cs.height and + x._3 == state.es.cs.round) + // val timeout = timeouts.chooseSome() + val timeout = timeouts.fold(("", 0, 0), (sum, y) => y) + val newstate = { ...state, timeout: state.timeout.exclude(Set(timeout))} + (newstate, { ...defaultInput, name: "timeout", timeout: timeout._1}) + + else if (state.es.pendingEvents != Set()) + // this might be cheating as we look into the "es" + (state, { ...defaultInput, name: "pending" }) + // TODO: In the "starkBFT Spec" Google doc, it is written that pending events + // should be executed before new messages, which would requir to push this + // branch up. + else + (state, defaultInput) +} + +// This function can be used to control test runs better. +pure def nextActionCommand (state: NodeState, command: str) : (NodeState, ExecutorInput) = { + if (command == "start" and not(state.es.started)) + (state, { ...defaultInput, name: "start" }) + + else if (command == "proposal" and state.incomingProposals != Set()) + // pick proposal, remove it from incoming + // val prop = state.incomingProposals.chooseSome() + val prop = state.incomingProposals.fold (emptyProposal, (sum, y) => y) + val newstate = { ...state, incomingProposals: state.incomingProposals.exclude(Set(prop))} + (newstate, { ...defaultInput, name: "proposal", proposal: prop}) + + else if (command == "vote" and state.incomingVotes != Set()) + // pick vote, remove it from incoming + // val vote = state.incomingVotes.chooseSome() + val vote = state.incomingVotes.fold(emptyVote, (sum, y) => y) + val newstate = { ...state, incomingVotes: state.incomingVotes.exclude(Set(vote))} + (newstate, { ...defaultInput, name: "votemessage", vote: vote}) + + else if (command == "timeout" and state.timeout.exists(x => x._2 == state.es.cs.height and + x._3 == state.es.cs.round)) + // pick timeout, remove it from incoming + val timeouts = state.timeout.filter(x => x._2 == state.es.cs.height and + x._3 == state.es.cs.round) + // val timeout = timeouts.chooseSome() + val timeout = timeouts.fold(("", 0, 0), (sum, y) => y) + val newstate = { ...state, timeout: state.timeout.exclude(Set(timeout))} + (newstate, { ...defaultInput, name: "timeout", timeout: timeout._1}) + + else if (command == "pending" and state.es.pendingEvents != Set()) + // this might be cheating as we look into the "es" + (state, { ...defaultInput, name: "pending" }) + + else + (state, defaultInput) +} + +} \ No newline at end of file diff --git a/Specs/Quint/extraSpells.qnt b/Specs/Quint/extraSpells.qnt index b0444ed17..a0fb9b7cc 100644 --- a/Specs/Quint/extraSpells.qnt +++ b/Specs/Quint/extraSpells.qnt @@ -115,6 +115,22 @@ module extraSpells { assert(Set(3) == Set(3).setAdd(3)), } + /// Add a set element only if a condition is true. + /// + /// - @param __set a set to add an element to + /// - @param __elem an element to add + /// - @param __cond a condition that must be true to add the element to the set + /// - @returns a new set that contains all elements of __set and __elem, if __cond is true + pure def setAddIf(__set: Set[a], __elem: a, __cond: bool): Set[a] = + if (__cond) __set.setAdd(__elem) else __set + + run setAddIfTest = all { + assert(Set(2, 3, 4, 5) == Set(2, 3, 4).setAddIf(5, true)), + assert(Set(2, 3, 4) == Set(2, 3, 4).setAddIf(5, false)), + assert(Set(3) == Set(3).setAddIf(3, true)), + assert(Set(3) == Set(3).setAddIf(3, false)), + } + /// Safely set a map entry. /// /// - @param __map a map to set an entry to @@ -160,11 +176,24 @@ module extraSpells { /// plus the ones in __entries pure def mapAddSet(__map: a -> int, __entries: a -> int): a -> int = { __map.keys().union(__entries.keys()).mapBy(__k => if (__map.has(__k) and __entries.has(__k)) __map.get(__k) + __entries.get(__k) - else if (__map.has(__k)) __map.get(__k) else __entries.get(__k)) + else if (__map.has(__k)) __map.get(__k) else __entries.get(__k)) } run mapAddSetTest = all { assert(Map(2 -> 3, 4 -> 5, 7 -> 8).mapAddSet(Map(3 -> 6, 8 -> 9)) == Map(2 -> 3, 4 -> 5, 3 -> 6, 7 -> 8, 8 -> 9)), assert(Map(2 -> 3, 4 -> 5, 7 -> 8).mapAddSet(Map(3 -> 6, 7 -> 9)) == Map(2 -> 3, 4 -> 5, 3 -> 6, 7 -> 17)), } + + /// Compute the sum of all values in the map. + /// + /// - @param __map a map with values of type int + /// - @returns the sum of the values of all entries in __map + pure def mapSumValues(__map: a -> int): int = + __map.keys().fold(0, (__acc, __val) => __acc + __map.get(__val)) + + run mapSumValuesTest = all { + assert(0 == Map().mapSumValues()), + assert(6 == Map("a" -> 0, "b" -> 1, "c" -> 2, "d" -> 3).mapSumValues()), + } + } \ No newline at end of file diff --git a/Specs/Quint/statemachineAsync.qnt b/Specs/Quint/statemachineAsync.qnt new file mode 100644 index 000000000..2d532e2ff --- /dev/null +++ b/Specs/Quint/statemachineAsync.qnt @@ -0,0 +1,187 @@ +// -*- mode: Bluespec; -*- + +/* + This contains asynchronous message transfer semantics, that is, + - upon sending, messages are put into a buffer (for each receiver). + The buffer is part of the network and not in any validator state + - there is a deliver event that takes a message out of the buffer + and puts it into the incoming set of the validator (alternatively + a message by a faulty process may be put into the incoming set) + - this allows re-ordering of message in the network, that is, a + process may receive message m1 before m2 while another process + may receive m2 before m1 + Example models using this specification can be found in AsyncModels.qnt +*/ + + +module statemachineAsync { + +import executor.* from "./executor" +import consensus.* from "./consensus" +import voteBookkeeper.* from "./voteBookkeeper" + +const validators : Set[Address_t] +const validatorSet : Address_t -> int +const Faulty : Set[Address_t] +val Correct = validators.exclude(Faulty) + +// These are used to define what messages can be sent by faulty validators +const Values : Set[Value_t] +const Rounds : Set[Round_t] +const Heights : Set[Height_t] + +// putting all messages that could be ever sent by faulty validators into +// AllFaultyVotes and AllFaultyProposals + +val RoundsOrNil = Rounds.union(Set(-1)) +val Steps = Set("Prevote", "Precommit") + +val AllFaultyVotes : Set[VoteMsg_t] = + tuples(Faulty, Heights, Rounds, Values, Steps) + .map(t => { src: t._1, height: t._2, round: t._3, id: t._4, step: t._5 }) + +// val AllFaultyVotes : Set[VoteMsg_t] = +// tuples(Faulty, Heights, Rounds, Values, Steps) +// .map(((p, h, r, v, s)) => { src: p, height: h, round: r, id: v, step: s }) + +val AllFaultyProposals : Set[ProposeMsg_t] = + tuples(Faulty, Heights, Rounds, Values, RoundsOrNil) + .map(t => { src: t._1, height: t._2, round: t._3, proposal: t._4, validRound: t._5 }) + + +// Global State +var system : Address_t -> NodeState +var propBuffer : Address_t -> Set[ProposeMsg_t] +var voteBuffer : Address_t -> Set[VoteMsg_t] +var _hist: { validator: Address_t, input: ExecutorInput, output: ConsensusOutput } + +val ConsensusOutputInv = consensusOutputs.union(Set(defaultResult.name)).contains(_hist.output.name) + + +action unchangedAll = all { + system' = system, + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + _hist' = _hist +} + +val AgreementInv = tuples(Correct, Correct).forall(p => + (system.get(p._1).es.chain != List() and system.get(p._2).es.chain != List()) + implies + system.get(p._1).es.chain[0] == system.get(p._2).es.chain[0]) + +// Actions +action init = all { + system' = Correct.mapBy(v => initNode(v, validatorSet)), + propBuffer' = Correct.mapBy(v => Set()), + voteBuffer' = Correct.mapBy(v => Set()), + _hist' = { validator: "INIT", input: defaultInput, output: defaultResult } +} + +// Put the proposal into the buffers of all validators +pure def sendProposal (buffer: Address_t -> Set[ProposeMsg_t], prop: ProposeMsg_t) : Address_t -> Set[ProposeMsg_t] = { + buffer.keys().mapBy(x => + { buffer.get(x).union(Set(prop)) }) +} + +// Put the vote into the inbuffers of all validators +pure def sendVote (sys: Address_t -> Set[VoteMsg_t], vote: VoteMsg_t) : Address_t -> Set[VoteMsg_t] = { + sys.keys().mapBy(x => + { ...sys.get(x).union(Set(vote)) }) +} + +// Record that a timeout has started at node v +pure def startTimeout (sys: Address_t -> NodeState, v: Address_t, toName: str) : Address_t -> NodeState = { + sys.put(v, { ...sys.get(v), timeout: sys.get(v).timeout.union(Set( + {(toName, sys.get(v).es.cs.height, sys.get(v).es.cs.round)} + ))}) +} + +action valStep(v: Address_t) : bool = { + // pick action + val input = system.get(v).nextAction() // TODO: nextAction could go within executor boundary + // remove action from v + val sys1 = system.put(v, input._1) + // call executor + val res = executor(sys1.get(v).es, input._2) + all { + // update v's state after the step + val sys = sys1.put(v, { ...sys1.get(v), es: res._1}) + // do networking + if (res._2.name == "proposal") all { + propBuffer' = sendProposal(propBuffer, res._2.proposal), // TODO: this is immediate + voteBuffer' = voteBuffer, + system' = sys, + } + else if (res._2.name == "votemessage") all { + propBuffer' = propBuffer, + voteBuffer' = sendVote(voteBuffer, res._2.voteMessage), // TODO: this is immediate + system' = sys, + } + else if (res._2.name == "timeout") all { + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + system' = startTimeout(sys, v, res._2.timeout), + } + else if (res._2.name == "skipRound") all { + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + //skipRound should never leave the executor + system' = sys, + } + else all { + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, + system' = sys, + }, + _hist' = { validator: v, input: input._2, output: res._2 } +// _histSimple' = (v, input._2.name, res._2.name) + } +} + +action setNextValueToPropose(v: Address_t, value: Value_t) : bool = all { + val res = executor(system.get(v).es, { ...defaultInput, name: "SetNextProposedValue", nextValueToPropose: value}) + val newNS = { ...system.get(v), es: res._1} + system' = system.put(v, newNS), + _hist' = _hist, + propBuffer' = propBuffer, + voteBuffer' = voteBuffer, +} + +action deliverProposal(v: Address_t, p: ProposeMsg_t) : bool = all { + propBuffer.get(v).union(AllFaultyProposals).contains(p), // the proposal must be sent or from a faulty node + propBuffer' = propBuffer.put(v, propBuffer.get(v).exclude(Set(p))), + system' = system.put(v, { ...system.get(v), incomingProposals: system.get(v).incomingProposals.union(Set(p)) }), + _hist' = _hist, + voteBuffer' = voteBuffer, +} + +action deliverVote(v: Address_t, vote: VoteMsg_t) : bool = all { + voteBuffer.get(v).union(AllFaultyVotes).contains(vote), // the vote must be sent or from a faulty node + voteBuffer' = voteBuffer.put(v, voteBuffer.get(v).exclude(Set(vote))), + system' = system.put(v, { ...system.get(v), incomingVotes: system.get(v).incomingVotes.union(Set(vote)) }), + _hist' = _hist, + propBuffer' = propBuffer, +} + +// deliver a message. Take it from the network buffer of from the faulty set +// and put it into the incoming sets +action deliver(v: Address_t) : bool = any { + nondet prop = oneOf(propBuffer.get(v).union(AllFaultyProposals)) + deliverProposal(v, prop), + nondet vote = oneOf(voteBuffer.get(v).union(AllFaultyVotes)) + deliverVote(v, vote) +} + +action step = { + nondet v = oneOf(Correct) + nondet value = oneOf(Values) + any { + valStep(v), + deliver(v), + setNextValueToPropose(v, value), + } +} + + +} \ No newline at end of file diff --git a/Specs/Quint/statemachineTest.qnt b/Specs/Quint/statemachineTest.qnt new file mode 100644 index 000000000..1e2115ae8 --- /dev/null +++ b/Specs/Quint/statemachineTest.qnt @@ -0,0 +1,223 @@ +// -*- mode: Bluespec; -*- + +/* + This contains some (non-standard) synchronous message transfer + semantics, that is, + - upon sending, messages are put into the incoming set of the + validator + - no faulty messages are modeled here + The model is quite simple but might be useful to generates + traces. +*/ + +module statemachineTest { + +import executor.* from "./executor" +import consensus.* from "./consensus" +import voteBookkeeper.* from "./voteBookkeeper" + +val validators = Set("v1", "v2", "v3", "v4") +val validatorSet = validators.mapBy(x => 1) + +var system : Address_t -> NodeState +var _hist: (str, ExecutorInput, ConsensusOutput) +//var _histSimple: (str, str, str) + +action init = all { + system' = validators.mapBy(v => initNode(v, validatorSet)), + _hist' = ("INIT", defaultInput, defaultResult) +// _histSimple' = ("INIT", "", "") +} + +// Put the proposal into the inbuffers of all validators +pure def deliverProposal (sys: Address_t -> NodeState, prop: ProposeMsg_t) : Address_t -> NodeState = { + sys.keys().mapBy(x => + { ...sys.get(x), incomingProposals: sys.get(x).incomingProposals.union(Set(prop)) }) +} + +// Put the vote into the inbuffers of all validators +pure def deliverVote (sys: Address_t -> NodeState, vote: VoteMsg_t) : Address_t -> NodeState = { + sys.keys().mapBy(x => + { ...sys.get(x), incomingVotes: sys.get(x).incomingVotes.union(Set(vote)) }) +} + +// Record that a timeout has started at node v +pure def startTimeout (sys: Address_t -> NodeState, v: Address_t, toName: str) : Address_t -> NodeState = { + sys.put(v, { ...sys.get(v), timeout: sys.get(v).timeout.union(Set( + {(toName, sys.get(v).es.cs.height, sys.get(v).es.cs.round)} + ))}) +} + +// this is a simple semantics that puts messages that are sent immediately in the +// inbuffer of the receivers. By the way nextAction() is implemented timeouts +// hardly ever are fired +action valStep(v: Address_t) : bool = { + // pick action + val input = system.get(v).nextAction() // TODO: nextAction could go within executor boundary + // remove action from v + val sys1 = system.put(v, input._1) + // call executor + val res = executor(sys1.get(v).es, input._2) + all { + // update v's state after the step + val sys = sys1.put(v, { ...sys1.get(v), es: res._1}) + // do networking + if (res._2.name == "proposal") + system' = deliverProposal(sys, res._2.proposal) // TODO: this is immediate + else if (res._2.name == "votemessage") + system' = deliverVote(sys, res._2.voteMessage) // TODO: this is immediate + else if (res._2.name == "timeout") + system' = startTimeout(sys, v, res._2.timeout) + else if (res._2.name == "skipRound") + //skipRound should never leave the executor + system' = sys + else + system' = sys, + _hist' = (v, input._2, res._2) +// _histSimple' = (v, input._2.name, res._2.name) + } +} + +action setNextValueToPropose(v: Address_t, value: Value_t) : bool = all { + val res = executor(system.get(v).es, { ...defaultInput, name: "SetNextProposedValue", nextValueToPropose: value}) + val newNS = { ...system.get(v), es: res._1} + system' = system.put(v, newNS), + _hist' = _hist +} + +action step = { + nondet v = oneOf(validators) + nondet value = oneOf(Set("a", "b", "c")) + any { + valStep(v), + setNextValueToPropose(v, value), + } +} + + + +action valStepCommand(v: Address_t, command: str) : bool = { + // pick action + val input = system.get(v).nextActionCommand(command) + // remove action from v + val sys1 = system.put(v, input._1) + // call executor + val res = executor(sys1.get(v).es, input._2) + all { + // update v's state after the step + val sys = sys1.put(v, { ...sys1.get(v), es: res._1}) + // do networking + if (res._2.name == "proposal") + system' = deliverProposal(sys, res._2.proposal) // TODO: this is immediate + else if (res._2.name == "votemessage") + system' = deliverVote(sys, res._2.voteMessage) // TODO: this is immediate + else if (res._2.name == "timeout") + system' = startTimeout(sys, v, res._2.timeout) + else if (res._2.name == "skipRound") + //skipRound should never leave the executor + system' = sys + else + system' = sys, + _hist' = (v, input._2, res._2) +// _histSimple' = (v, input._2.name, res._2.name) + } +} + +run DecidingRunTest = { + init + .then(setNextValueToPropose("v2", "a block")) + .then(valStepCommand("v1", "start")) + .then(valStepCommand("v2", "start")) + .then(valStepCommand("v3", "start")) + .then(valStepCommand("v4", "start")) + .then(valStepCommand("v1", "proposal")) + .then(valStepCommand("v2", "proposal")) + .then(valStepCommand("v3", "proposal")) + .then(valStepCommand("v4", "proposal")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(all{ + assert(system.get("v1").incomingVotes.contains( + { src: "v1", height: 0, round: 0, step: "Precommit", id: "a block" } + )), + valStepCommand("v2", "vote") + }) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(all{ + assert(system.get("v2").incomingVotes.contains( + { src: "v2", height: 0, round: 0, step: "Precommit", id: "a block" } + )), + valStepCommand("v3", "vote") + }) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(all{ + assert(system.get("v3").incomingVotes.contains( + { src: "v3", height: 0, round: 0, step: "Precommit", id: "a block" } + )), + assert(system.get("v3").es.chain == List()), + valStepCommand("v3", "vote") + }) + .then(all{ + // validator 3 decided on "a block" + assert(system.get("v3").es.chain.head() == "a block"), + system' = system, + _hist' = _hist + }) +} + + +run TimeoutRunTest = { + init + .then(setNextValueToPropose("v2", "a block")) + .then(valStepCommand("v1", "start")) + .then(valStepCommand("v2", "start")) + .then(valStepCommand("v3", "start")) + .then(valStepCommand("v4", "start")) + .then(valStepCommand("v1", "timeout")) + .then(valStepCommand("v2", "proposal")) + .then(valStepCommand("v3", "timeout")) + .then(valStepCommand("v4", "timeout")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v3", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v2", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v1", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "vote")) + .then(valStepCommand("v4", "timeout")) + .then(all { + // validator 4 timed out and went to round 1 + assert(system.get("v4").es.cs.round == 1), + system' = system, + _hist' = _hist, + }) +} + +} + diff --git a/Specs/Quint/voteBookkeeper.qnt b/Specs/Quint/voteBookkeeper.qnt index 1d089ce0a..051abf9a0 100644 --- a/Specs/Quint/voteBookkeeper.qnt +++ b/Specs/Quint/voteBookkeeper.qnt @@ -21,12 +21,13 @@ module voteBookkeeper { // A value is a string type Value = str - // Weigth is an integer + // Weight is an integer type Weight = int - // The vote type + type VoteType = str + type Vote = { - typ: str, + typ: VoteType, round: Round, value: Value, address: Address @@ -72,59 +73,83 @@ module voteBookkeeper { // Internal functions // creates a new voteCount - pure def newVoteCount(total: Weight): VoteCount = { - {totalWeight: total, valuesWeights: Map(), votesAddresses: Set()} - } + pure def newVoteCount(total: Weight): VoteCount = + { totalWeight: total, valuesWeights: Map(), votesAddresses: Set() } // Returns true if weight > 2/3 * total (quorum: at least f+1 correct) - pure def isQuorum(weight: int, total: int): bool = { + pure def isQuorum(weight: Weight, total: Weight): bool = 3 * weight > 2 * total - } + + // True iff the vote count has a quorum on a specific value. + pure def hasQuorumOnValue(voteCount: VoteCount, value: Value): bool = + isQuorum(voteCount.valuesWeights.getOrElse(value, 0), voteCount.totalWeight) + + // True iff the vote count has a quorum on any value. + pure def hasQuorumOnAny(voteCount: VoteCount): bool = + isQuorum(voteCount.valuesWeights.mapSumValues(), voteCount.totalWeight) // Returns true if weight > 1/3 * total (small quorum: at least one correct) - pure def isSkip(weight: int, total: int): bool = { + pure def isSkip(weight: Weight, total: Weight): bool = 3 * weight > total - } + // Adds a vote of weight weigth to a voteCount if there is not vote registered for the voter. - pure def addVote(voteCount: VoteCount, vote: Vote, weight: Weight): VoteCount = { - if (vote.address.in(voteCount.votesAddresses)) voteCount - else val newWeight = voteCount.valuesWeights.getOrElse(vote.value, 0) + weight - voteCount.with("valuesWeights", voteCount.valuesWeights.mapSafeSet(vote.value, newWeight)) - .with("votesAddresses", voteCount.votesAddresses.setAdd(vote.address)) - } + pure def addVote(voteCount: VoteCount, vote: Vote, weight: Weight): VoteCount = + if (vote.address.in(voteCount.votesAddresses)) + // Do not count vote if address has already voted. + voteCount + else + val newWeight = voteCount.valuesWeights.getOrElse(vote.value, 0) + weight + voteCount + .with("valuesWeights", voteCount.valuesWeights.mapSafeSet(vote.value, newWeight)) + .with("votesAddresses", voteCount.votesAddresses.setAdd(vote.address)) // Given a voteCount and a value, the function returns: // - A threshold Value if there is a quorum for the given value; // - A threshold Nil if there is a quorum for the nil and no quorum for the value; // - A threshold Any if there is no quorum for the value or nil and there is a quroum for any (including nil); // - A threshold Unreached otherwise indicating that no quorum has been yet reached. - pure def computeThreshold(voteCount: VoteCount, value: Value): Threshold = { - val weight = voteCount.valuesWeights.getOrElse(value, 0) - val totalWeight = voteCount.totalWeight - val sumWeight = voteCount.valuesWeights.keys().fold(0, (sum, v) => sum + voteCount.valuesWeights.get(v)) - if (value != "nil" and isQuorum(weight, totalWeight)) {name: "Value", value: value} - else if (value == "nil" and isQuorum(weight, totalWeight)) {name: "Nil", value: "null"} - else if (isQuorum(sumWeight, totalWeight)) {name: "Any", value: "null"} - else {name: "Unreached", value: "null"} - } - - // Given a round, voteType and threshold it resturns the corresponding ExecutorEvent - pure def toEvent(round: Round, voteType: str, threshold: Threshold): ExecutorEvent = { - if (threshold.name == "Unreached") {round: round, name: "None", value: "null"} - else if (voteType == "Prevote" and threshold.name == "Value") {round: round, name: "PolkaValue", value: threshold.value} - else if (voteType == "Prevote" and threshold.name == "Nil") {round: round, name: "PolkaNil", value: "null"} - else if (voteType == "Prevote" and threshold.name == "Any") {round: round, name: "PolkaAny", value: "null"} - else if (voteType == "Precommit" and threshold.name == "Value") {round: round, name: "PrecommitValue", value: threshold.value} - else if (voteType == "Precommit" and threshold.name == "Any") {round: round, name: "PrecommitAny", value: "null"} - else if (threshold.name == "Skip") {round: round, name: "Skip", value: "null"} - else {round: round, name: "None", value: "null"} - } - - + pure def computeThreshold(voteCount: VoteCount, value: Value): Threshold = + if (voteCount.hasQuorumOnValue(value)) { + if (value == "nil") + { name: "Nil", value: "null" } + else + { name: "Value", value: value } + } else if (voteCount.hasQuorumOnAny()) { + { name: "Any", value: "null" } + } else + { name: "Unreached", value: "null" } + + // Given a round, voteType and threshold, return the corresponding ExecutorEvent + pure def toEvent(round: Round, voteType: VoteType, threshold: Threshold): ExecutorEvent = + if (threshold.name == "Unreached") + { round: round, name: "None", value: "null" } + + // prevote + else if (voteType == "Prevote" and threshold.name == "Value") + { round: round, name: "PolkaValue", value: threshold.value } + else if (voteType == "Prevote" and threshold.name == "Nil") + { round: round, name: "PolkaNil", value: "null" } + else if (voteType == "Prevote" and threshold.name == "Any") + { round: round, name: "PolkaAny", value: "null" } + + // precommit + else if (voteType == "Precommit" and threshold.name == "Value") + { round: round, name: "PrecommitValue", value: threshold.value } + else if (voteType == "Precommit" and threshold.name == "Any") + { round: round, name: "PrecommitAny", value: "null" } + else if (voteType == "Precommit" and threshold.name == "Nil") + { round: round, name: "PrecommitAny", value: "null" } + + else if (threshold.name == "Skip") + { round: round, name: "Skip", value: "null" } + + else + { round: round, name: "None", value: "null" } // Executor interface + type BKResult = { bookkeeper: Bookkeeper, event: ExecutorEvent } - // Called by the executor when it receives a vote. The functiojn takes the following steps: + // Called by the executor when it receives a vote. The function takes the following steps: // - It first adds the vote and then computes a threshold. // - If there exist a threshold and has not emitted before, the function returns the corresponsing ExecutorEvent. // - Othewise, the function returns a no-threshold event. @@ -132,52 +157,102 @@ module voteBookkeeper { // TO DISCUSS: // - There might be a problem if we generalize from single-shot to multi-shot: the keeper only keeps the totalWeight // of the current height; I wonder if we need to keep the totalWeight for every Height that we may receive a vote for. - pure def applyVote(keeper: Bookkeeper, vote: Vote, weight: int): {bookkeeper: Bookkeeper, event: ExecutorEvent} = { + pure def applyVote(keeper: Bookkeeper, vote: Vote, weight: Weight): { bookkeeper: Bookkeeper, event: ExecutorEvent } = val height = keeper.height val total = keeper.totalWeight - val roundVotes = keeper.rounds.getOrElse(vote.round, {height: height, - round: vote.round, - prevotes: newVoteCount(total), - precommits: newVoteCount(total), - emittedEvents: Set(), - votesAddressesWeights: Map()}) - val updatedVoteCount = if (vote.typ == "Prevote") roundVotes.prevotes.addVote(vote, weight) - else roundVotes.precommits.addVote(vote, weight) + + val defaultRoundVotes = { + height: height, + round: vote.round, + prevotes: newVoteCount(total), + precommits: newVoteCount(total), + emittedEvents: Set(), + votesAddressesWeights: Map() + } + val roundVotes = keeper.rounds.getOrElse(vote.round, defaultRoundVotes) + + val updatedVoteCount = + if (vote.typ == "Prevote") + roundVotes.prevotes.addVote(vote, weight) + else + roundVotes.precommits.addVote(vote, weight) + + val updatedVotesAddressesWeights = + if (roundVotes.votesAddressesWeights.has(vote.address)) + roundVotes.votesAddressesWeights + else + roundVotes.votesAddressesWeights.mapSafeSet(vote.address, weight) + val threshold = computeThreshold(updatedVoteCount, vote.value) val event = toEvent(vote.round, vote.typ, threshold) - val updatedVotesAddressesWeights = if (roundVotes.votesAddressesWeights.has(vote.address)) roundVotes.votesAddressesWeights - else roundVotes.votesAddressesWeights.mapSafeSet(vote.address, weight) - val sumSkip = updatedVotesAddressesWeights.keys().fold(0, (sum, v) => sum + updatedVotesAddressesWeights.get(v)) - val finalEvent = if (not(event.in(roundVotes.emittedEvents))) event - else if (roundVotes.emittedEvents == Set() and isSkip(sumSkip, total)) {round: vote.round, name: "Skip", value: "null"} - else {round: vote.round, name: "None", value: "null"} - val updatedRoundVotes = if (vote.typ == "Prevote") roundVotes.with("prevotes", updatedVoteCount) - else roundVotes.with("precommits", updatedVoteCount) - val updatedEmmittedEvents = if (finalEvent.name != "None") roundVotes.emittedEvents.setAdd(finalEvent) - else roundVotes.emittedEvents - val updatedBookkeeper = keeper.with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes.with("votesAddressesWeights", updatedVotesAddressesWeights) - .with("emittedEvents", updatedEmmittedEvents))) - {bookkeeper: updatedBookkeeper, event: finalEvent} - } + val finalEvent = + if (not(event.in(roundVotes.emittedEvents))) + event + else if (roundVotes.emittedEvents == Set() and isSkip(updatedVotesAddressesWeights.mapSumValues(), total)) + { round: vote.round, name: "Skip", value: "null" } + else + { round: vote.round, name: "None", value: "null" } + + val updatedEmmittedEvents = roundVotes.emittedEvents.setAddIf(finalEvent, finalEvent.name != "None") + + val updatedRoundVotes = + if (vote.typ == "Prevote") + roundVotes.with("prevotes", updatedVoteCount) + else + roundVotes.with("precommits", updatedVoteCount) + val updatedRoundVotes2 = updatedRoundVotes + .with("votesAddressesWeights", updatedVotesAddressesWeights) + .with("emittedEvents", updatedEmmittedEvents) + + { + bookkeeper: keeper.with("rounds", keeper.rounds.mapSafeSet(vote.round, updatedRoundVotes2)), + event: finalEvent + } // Called by the executor to check if there is a specific threshold for a given round and voteType. // TO DISCUSS: // - The function does not consider Skip threshold. This because if the executor receives a Skip event // and do not act on it, this means that it will never do it in the future. We should discuss that this // is the case. - pure def checkThreshold(keeper: Bookkeeper, round: Round, voteType: str, threshold: Threshold): bool = { + pure def checkThreshold(keeper: Bookkeeper, round: Round, voteType: VoteType, threshold: Threshold): bool = if (keeper.rounds.has(round)) { val roundVotes = keeper.rounds.get(round) - val voteCount = if (voteType == "Prevote") roundVotes.prevotes - else roundVotes.precommits - val total = voteCount.totalWeight - val sumWeight = voteCount.valuesWeights.keys().fold(0, (sum, v) => sum + voteCount.valuesWeights.get(v)) - if (threshold.name == "Value") isQuorum(voteCount.valuesWeights.getOrElse(threshold.value, 0), total) - else if (threshold.name == "Nil") isQuorum(voteCount.valuesWeights.getOrElse("nil", 0), total) - else if (threshold.name == "Any") isQuorum(sumWeight, total) - else false + val voteCount = if (voteType == "Prevote") roundVotes.prevotes else roundVotes.precommits + if (threshold.name == "Value") { + voteCount.hasQuorumOnValue(threshold.value) + } else if (threshold.name == "Nil") { + voteCount.hasQuorumOnValue("nil") + } else if (threshold.name == "Any") { + voteCount.hasQuorumOnAny() + } else false } else false - } + +// run PrecommitTest = all { +// val bin : Bookkeeper = { +// height: 0, +// rounds: +// Map( +// 0 -> +// { +// height: 0, +// precommits: { total: 4, valuesAddresses: Map(), valuesWeights: Map() }, +// prevotes: { total: 4, valuesAddresses: Map(), valuesWeights: Map("a block" -> 1, "nil" -> 3) }, +// round: 0 +// } +// ), +// totalWeight: 4 +// } +// val o1 = applyVote(bin, {value: "nil", round: 0, address: "v0", typ: "Precommit" }, 1) +// val o2 = applyVote(o1.bookkeeper, {value: "nil", round: 0, address: "v1", typ: "Precommit" }, 1) +// val o3 = applyVote(o2.bookkeeper, {value: "nil", round: 0, address: "v2", typ: "Precommit" }, 1) +// val o4 = applyVote(o3.bookkeeper, {value: "nil", round: 0, address: "v3", typ: "Precommit" }, 1) +// all{ +// assert(o1.event.name == "None"), +// assert(o2.event.name == "None"), +// assert(o3.event.name == "PrecommitAny"), +// assert(o4.event.name == "PrecommitAny") +// } +// } // **************************************************************************** // Unit tests @@ -196,7 +271,7 @@ module voteBookkeeper { assert(isSkip(3,6) == true) } - run addVoteTest = { + run addVoteTest = val voteCount = {totalWeight: 100, valuesWeights: Map("val1" -> 30, "val2" -> 20), votesAddresses: Set("alice", "bob")} val vote = {typ: "precommit", round: 10, value: "val3", address: "john"} all { @@ -207,14 +282,12 @@ module voteBookkeeper { // existing voter assert(addVote(voteCount, vote.with("address", "alice"), 10) == voteCount), } - } - run computeThresholdTest = { + run computeThresholdTest = val voteCount = {totalWeight: 100, valuesWeights: Map(), votesAddresses: Set("alice", "bob")} val mapValueReached = Map("val1" -> 67, "val2" -> 20) val mapNilReached = Map("nil" -> 70, "val2" -> 20) val mapNoneReached = Map("nil" -> 20, "val2" -> 20) - all { assert(computeThreshold(voteCount, "val3") == {name: "Unreached", value: "null"}), assert(computeThreshold(voteCount.with("valuesWeights", mapValueReached), "val1") == {name: "Value", value: "val1"}), @@ -224,9 +297,8 @@ module voteBookkeeper { assert(computeThreshold(voteCount.with("valuesWeights", mapNoneReached), "val1") == {name: "Unreached", value: "null"}), assert(computeThreshold(voteCount.with("valuesWeights", mapNoneReached), "nil") == {name: "Unreached", value: "null"}), } - } - run toEventTest = { + run toEventTest = val thresholdUnreached = {name: "Unreached", value: "null"} val thresholdAny = {name: "Any", value: "null"} val thresholdNil = {name: "Nil", value: "null"} @@ -240,101 +312,13 @@ module voteBookkeeper { assert(toEvent(round, "Prevote", thresholdNil) == {round: round, name: "PolkaNil", value: "null"}), assert(toEvent(round, "Prevote", thresholdValue) == {round: round, name: "PolkaValue", value: "val1"}), assert(toEvent(round, "Precommit", thresholdAny) == {round: round, name: "PrecommitAny", value: "null"}), - assert(toEvent(round, "Precommit", thresholdNil) == {round: round, name: "None", value: "null"}), + assert(toEvent(round, "Precommit", thresholdNil) == {round: round, name: "PrecommitAny", value: "null"}), assert(toEvent(round, "Precommit", thresholdValue) == {round: round, name: "PrecommitValue", value: "val1"}), assert(toEvent(round, "Prevote", thresholdSkip) == {round: round, name: "Skip", value: "null"}), assert(toEvent(round, "Precommit", thresholdSkip) == {round: round, name: "Skip", value: "null"}), assert(toEvent(round, "Precommit", {name: "Error", value: "null"}) == {round: round, name: "None", value: "null"}), assert(toEvent(round, "Error", thresholdAny) == {round: round, name: "None", value: "null"}), } - } - - // **************************************************************************** - // State machine state - // **************************************************************************** - - // Bookkeeper state - var bookkeeper: Bookkeeper - // Last emitted event - var lastEmitted: ExecutorEvent - - // **************************************************************************** - // Execution - // **************************************************************************** - - action allUnchanged: bool = all { - bookkeeper' = bookkeeper, - lastEmitted' = lastEmitted - } - - action initial(totalWeight: Weight): bool = all { - bookkeeper' = {height: 10, totalWeight: totalWeight, rounds: Map()}, - lastEmitted' = {round: -1, name: "", value: "null"} - } - - action applyVoteAction(vote: Vote, weight: Weight): bool = all { - val result = applyVote(bookkeeper, vote, weight) - all { - bookkeeper' = result.bookkeeper, - lastEmitted' = result.event - } - } - action init = all { - initial(100) - } - - action step = all { - nondet validator = oneOf(Set( - { address: "alice", weight: 60 }, - { address: "bob", weight: 30 }, - { address: "john", weight: 10 } - )) - nondet typ = oneOf(Set("Prevote", "Precommit")) - nondet value = oneOf(Set("null", "proposal")) - - val vote = {typ: typ, round: 1, value: value, address: validator.address} - applyVoteAction(vote, validator.weight) - } - - // **************************************************************************** - // Test traces - // **************************************************************************** - - // Consensus full execution with all honest validators (including the leader) and a synchronous network: - // all messages are received in order. We assume three validators in the validator set wtih 60%, 30% and 10% - // each of the total voting power - run synchronousConsensusTest = { - initial(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "john"}, 10)) - .then(all{ assert(lastEmitted == {round: 1, name: "PolkaValue", value: "proposal"}), allUnchanged }) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "bob"}, 30)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) - .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "bob"}, 30)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) - .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "john"}, 10)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) - .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "alive"}, 60)) - .then(all{ assert(lastEmitted == {round: 1, name: "PrecommitValue", value: "proposal"}), allUnchanged }) - } - - // Reaching PolkaAny - run polkaAnyTest = { - initial(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10)) - .then(all{ assert(lastEmitted == {round: 1, name: "PolkaAny", value: "null"}), allUnchanged }) - } - - // Reaching PolkaNil - run polkaNilTest = { - initial(100) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60)) - .then(all{ assert(lastEmitted == {round: 1, name: "None", value: "null"}), allUnchanged }) - .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10)) - .then(all{ assert(lastEmitted == {round: 1, name: "PolkaNil", value: "null"}), allUnchanged }) - } } + diff --git a/Specs/Quint/voteBookkeeperTest.qnt b/Specs/Quint/voteBookkeeperTest.qnt new file mode 100644 index 000000000..3ffa98f44 --- /dev/null +++ b/Specs/Quint/voteBookkeeperTest.qnt @@ -0,0 +1,77 @@ +module voteBookkeeperTest { + + import voteBookkeeper.* from "./voteBookkeeper" + + // **************************************************************************** + // State machine state + // **************************************************************************** + + // Bookkeeper state + var bookkeeper: Bookkeeper + // Last emitted event + var lastEmitted: ExecutorEvent + + // **************************************************************************** + // Execution + // **************************************************************************** + + action allUnchanged: bool = all { + bookkeeper' = bookkeeper, + lastEmitted' = lastEmitted, + } + + action init(totalWeight: Weight): bool = all { + bookkeeper' = { height: 10, totalWeight: totalWeight, rounds: Map() }, + lastEmitted' = { round: -1, name: "", value: "null" }, + } + + action applyVoteAction(vote: Vote, weight: Weight): bool = + val result = applyVote(bookkeeper, vote, weight) + all { + bookkeeper' = result.bookkeeper, + lastEmitted' = result.event, + } + + // **************************************************************************** + // Test traces + // **************************************************************************** + + // auxiliary action for tests + action _assert(predicate: bool): bool = + all { predicate, allUnchanged } + + // Consensus full execution with all honest validators (including the leader) and a synchronous network: + // all messages are received in order. We assume three validators in the validator set wtih 60%, 30% and 10% + // each of the total voting power + run synchronousConsensusTest = + init(100) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "alice"}, 60)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "PolkaValue", value: "proposal"})) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "proposal", address: "bob"}, 30)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "bob"}, 30)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Precommit", round: 1, value: "proposal", address: "alice"}, 60)) + .then(_assert(lastEmitted == {round: 1, name: "PrecommitValue", value: "proposal"})) + + // Reaching PolkaAny + run polkaAnyTest = + init(100) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "val1", address: "alice"}, 60)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "PolkaAny", value: "null"})) + + // Reaching PolkaNil + run polkaNilTest = + init(100) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "alice"}, 60)) + .then(_assert(lastEmitted == {round: 1, name: "None", value: "null"})) + .then(applyVoteAction({typ: "Prevote", round: 1, value: "nil", address: "john"}, 10)) + .then(_assert(lastEmitted == {round: 1, name: "PolkaNil", value: "null"})) + +}