|
1 | 1 | // -*- mode: Bluespec; -*- |
2 | | -module TendermintAcc { |
| 2 | +module Tendermint { |
3 | 3 | /* |
4 | 4 | A Quint specification of a simplified Tendermint consensus, tuned for |
5 | 5 | fork accountability. The simplifications are as follows: |
@@ -320,9 +320,9 @@ module TendermintAcc { |
320 | 320 | } |
321 | 321 |
|
322 | 322 | // lines 34-35 + lines 61-64 (onTimeoutPrevote) |
323 | | - action UponQuorumOfPrevotesAny(p, Evidence) = |
| 323 | + action UponQuorumOfPrevotesAny(p: str, Evidence: Set[{ id: Value_t, round: Round_t, src: Proc_t }]): bool = |
324 | 324 | // find the unique voters in the evidence |
325 | | - val Voters = Evidence.map(m => m.src) |
| 325 | + val Voters: Set[str] = Evidence.map(m => m.src) |
326 | 326 | // compare the number of the unique voters against the threshold |
327 | 327 | all { |
328 | 328 | step.get(p) == "prevote", // line 34 and 61 |
@@ -380,9 +380,9 @@ module TendermintAcc { |
380 | 380 | } |
381 | 381 |
|
382 | 382 | // lines 47-48 + 65-67 (onTimeoutPrecommit) |
383 | | - action UponQuorumOfPrecommitsAny(p, Evidence) = |
| 383 | + action UponQuorumOfPrecommitsAny(p: str, Evidence: Set[{ id: Value_t, round: Round_t, src: Proc_t }]): bool = |
384 | 384 | // find the unique committers in the evidence |
385 | | - val Committers = Evidence.map( m => m.src ) |
| 385 | + val Committers: Set[str] = Evidence.map( m => m.src ) |
386 | 386 | // compare the number of the unique committers against the threshold |
387 | 387 | all { |
388 | 388 | size(Committers) >= THRESHOLD2, // line 47 |
@@ -531,23 +531,22 @@ module TendermintAcc { |
531 | 531 | } |
532 | 532 |
|
533 | 533 | //**************************** FORK SCENARIOS *************************** |
| 534 | + def EquivocationIn(p, S) = |
| 535 | + tuples(S, S).exists((m1, m2) => |
| 536 | + and { |
| 537 | + m1 != m2, |
| 538 | + m1.src == p, |
| 539 | + m2.src == p, |
| 540 | + m1.round == m2.round, |
| 541 | + } |
| 542 | + ) |
534 | 543 |
|
535 | 544 | // equivocation by a process p |
536 | | - def EquivocationBy(p) = |
537 | | - def EquivocationIn(S) = |
538 | | - tuples(S, S).exists((m1, m2) => |
539 | | - and { |
540 | | - m1 != m2, |
541 | | - m1.src == p, |
542 | | - m2.src == p, |
543 | | - m1.round == m2.round, |
544 | | - } |
545 | | - ) |
546 | | - |
| 545 | + def EquivocationBy(p: str): bool = |
547 | 546 | or { |
548 | | - EquivocationIn(evidencePropose), |
549 | | - EquivocationIn(evidencePrevote), |
550 | | - EquivocationIn(evidencePrecommit), |
| 547 | + EquivocationIn(p, evidencePropose), |
| 548 | + EquivocationIn(p, evidencePrevote), |
| 549 | + EquivocationIn(p, evidencePrecommit), |
551 | 550 | } |
552 | 551 |
|
553 | 552 | // amnesic behavior by a process p |
@@ -661,122 +660,3 @@ module TendermintAcc { |
661 | 660 | AllInMax implies AllDecided |
662 | 661 | ) |
663 | 662 | } |
664 | | - |
665 | | -// Tests that demonstrate typical behavior. |
666 | | -module TendermintTest { |
667 | | - import TendermintAcc.* |
668 | | - export TendermintAcc.* |
669 | | - |
670 | | - // Quint will automatically compute the unchanged block in the future |
671 | | - action unchangedAll = all { |
672 | | - step' = step, |
673 | | - fired_action' = fired_action, |
674 | | - round' = round, |
675 | | - validValue' = validValue, |
676 | | - validRound' = validRound, |
677 | | - msgsPrevote' = msgsPrevote, |
678 | | - msgsPropose' = msgsPropose, |
679 | | - msgsPrecommit' = msgsPrecommit, |
680 | | - decision' = decision, |
681 | | - lockedValue' = lockedValue, |
682 | | - lockedRound' = lockedRound, |
683 | | - evidencePropose' = evidencePropose, |
684 | | - evidencePrevote' = evidencePrevote, |
685 | | - evidencePrecommit' = evidencePrecommit, |
686 | | - } |
687 | | - |
688 | | - // three correct processes behave and decide on the same value |
689 | | - run decisionTest = { |
690 | | - nondet v = oneOf(ValidValues) |
691 | | - val p1 = Proposer.get(0) |
692 | | - nondet p2 = Corr.exclude(Set(p1)).oneOf() |
693 | | - nondet p3 = Corr.exclude(Set(p1, p2)).oneOf() |
694 | | - Init.then(InsertProposal(p1, v)) |
695 | | - .then(UponProposalInPropose(p1, v)) |
696 | | - .then(UponProposalInPropose(p2, v)) |
697 | | - .then(UponProposalInPropose(p3, v)) |
698 | | - .then(UponProposalInPrevoteOrCommitAndPrevote(p1, v, NilRound)) |
699 | | - .then(UponProposalInPrevoteOrCommitAndPrevote(p2, v, NilRound)) |
700 | | - .then(UponProposalInPrevoteOrCommitAndPrevote(p3, v, NilRound)) |
701 | | - .then(UponProposalInPrecommitNoDecision(p1, v, 0, NilRound)) |
702 | | - .then(UponProposalInPrecommitNoDecision(p2, v, 0, NilRound)) |
703 | | - .then(UponProposalInPrecommitNoDecision(p3, v, 0, NilRound)) |
704 | | - .then(all { |
705 | | - assert(decision.get(p1) == v), |
706 | | - assert(decision.get(p2) == v), |
707 | | - assert(decision.get(p3) == v), |
708 | | - unchangedAll, |
709 | | - }) |
710 | | - } |
711 | | - |
712 | | - // a correct proposer cannot propose twice in the same round |
713 | | - run noProposeTwiceTest = { |
714 | | - val p1 = Proposer.get(0) |
715 | | - Init.then(InsertProposal(p1, "v0")) |
716 | | - .then(InsertProposal(p1, "v1")) |
717 | | - .fail() |
718 | | - } |
719 | | - |
720 | | - // a correct proposer proposes but other processes timeout |
721 | | - run timeoutProposeTest = { |
722 | | - val p1 = Proposer.get(0) |
723 | | - nondet p2 = Corr.exclude(Set(p1)).oneOf() |
724 | | - nondet p3 = Corr.exclude(Set(p1, p2)).oneOf() |
725 | | - Init.then(InsertProposal(p1, "v0")) |
726 | | - .then(UponProposalInPropose(p1, "v0")) |
727 | | - .then(OnTimeoutPropose(p2)) |
728 | | - .then(OnTimeoutPropose(p3)) |
729 | | - .then( |
730 | | - val E = msgsPrevote.get(0).filter(m => m.src.in(Corr)) |
731 | | - UponQuorumOfPrevotesAny(p1, E) |
732 | | - .then(UponQuorumOfPrevotesAny(p2, E)) |
733 | | - .then(UponQuorumOfPrevotesAny(p3, E)) |
734 | | - ) |
735 | | - .then( |
736 | | - val E = msgsPrecommit.get(0).filter(m => m.src.in(Corr)) |
737 | | - UponQuorumOfPrecommitsAny(p1, E) |
738 | | - .then(UponQuorumOfPrecommitsAny(p2, E)) |
739 | | - .then(UponQuorumOfPrecommitsAny(p3, E)) |
740 | | - ) |
741 | | - .then(all { |
742 | | - // all correct processes switch to the next round |
743 | | - assert(Corr.forall(p => round.get(p) == 1)), |
744 | | - unchangedAll, |
745 | | - }) |
746 | | - } |
747 | | -} |
748 | | - |
749 | | -module InstanceTests { |
750 | | - import TendermintTest( |
751 | | - Corr = Set("p1", "p2", "p3"), |
752 | | - Faulty = Set("p4"), |
753 | | - N = 4, |
754 | | - T = 1, |
755 | | - ValidValues = Set("v0", "v1"), |
756 | | - InvalidValues = Set("v2"), |
757 | | - MaxRound = 4, |
758 | | - Proposer = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4", 4 -> "p1") |
759 | | - ) as Tendermint_n4_f1 |
760 | | - |
761 | | - import TendermintTest( |
762 | | - Corr = Set("p1", "p2", "p3"), |
763 | | - Faulty = Set("p3", "p4"), |
764 | | - N = 4, |
765 | | - T = 1, |
766 | | - ValidValues = Set("v0", "v1"), |
767 | | - InvalidValues = Set("v2"), |
768 | | - MaxRound = 4, |
769 | | - Proposer = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4", 4 -> "p1") |
770 | | - ) as Tendermint_n4_f2 |
771 | | - |
772 | | - import TendermintTest( |
773 | | - Corr = Set("p1", "p2", "p3"), |
774 | | - Faulty = Set("p4", "p5"), |
775 | | - N = 5, |
776 | | - T = 1, |
777 | | - ValidValues = Set("v0", "v1"), |
778 | | - InvalidValues = Set("v2"), |
779 | | - MaxRound = 4, |
780 | | - Proposer = Map(0 -> "p1", 1 -> "p2", 2 -> "p3", 3 -> "p4", 4 -> "p1") |
781 | | - ) as Tendermint_n5_f2 |
782 | | -} |
0 commit comments