Add initial specification in Quint (#135)

This PR adds an initial formal specification of the ChonkyBFT protocol
in Quint.
It also contains tests and experiments results we have performed.

---------

Signed-off-by: Denis Kolegov <[email protected]>
Co-authored-by: Igor Konnov <[email protected]>
Co-authored-by: Bruno França <[email protected]>

.github/workflows/spec.yaml

@@ -0,0 +1,27 @@
+name: Specification testing
+
+on: 
+  pull_request
+    paths: 
+      - 'spec/**'
+
+jobs:
+
+  test:
+    runs-on: ubuntu-latest
+
+    steps:
+      - name: Checkout the repository
+        uses: actions/checkout@v4
+
+      - name: Install node
+        uses: actions/setup-node@v4
+        with:
+          node-version: ">= 18"
+          check-latest: true
+
+      - name: Install quint
+        run: npm i @informalsystems/quint -g
+
+      - name: Run test
+        run: cd spec && make test

.gitignore

@@ -12,3 +12,6 @@ logs/
 
 # Binaries generated in Docker
 node/tools/docker_binaries
+
+# Apalache files
+**/_apalache-out

spec/Makefile

@@ -0,0 +1,24 @@
+.PHONY: test unit check repl integration smoke-tests
+
+repl:
+	cd protocol-spec && echo "init\n step\n step\n step" | quint -r main.qnt::main 
+
+check:
+	cd protocol-spec && quint typecheck main.qnt
+
+integration:
+	cd protocol-spec/tests && quint test ./tests_n6f1b0.qnt
+	cd protocol-spec/tests && quint test ./tests_n6f1b1.qnt
+	cd protocol-spec/tests && quint test ./tests_n6f1b2.qnt
+
+unit:
+	cd protocol-spec/tests && quint test ./unit_tests.qnt	
+
+test: check repl unit integration smoke-tests
+
+smoke-tests:
+	cd protocol-spec/experiments && quint verify --max-steps=1 --invariant=all_invariants n7f1b0.qnt
+	cd protocol-spec/experiments && quint verify --max-steps=1 --invariant=all_invariants n6f1b3.qnt
+	cd protocol-spec/experiments && quint verify --max-steps=1 --invariant=all_invariants n6f1b2.qnt
+	cd protocol-spec/experiments && quint verify --max-steps=1 --invariant=all_invariants n6f1b1.qnt
+	cd protocol-spec/experiments && quint verify --max-steps=1 --invariant=all_invariants n6f1b0.qnt

spec/README.md

@@ -0,0 +1,3 @@
+# ChonkyBFT's Specification
+
+This is a formal specification of ChonkyBFT consensus protocol in Quint.

spec/informal-spec/README.md

@@ -0,0 +1,11 @@
+# ChonkyBFT Specification
+
+This is a ChonkyBFT specification in pseudocode.
+
+There's a couple of considerations that are not described in the pseudo-code:
+
+- **Network model**. Messages might be delivered out of order, but we don’t guarantee eventual delivery for *all* messages. Actually, our network only guarantees eventual delivery of the most recent message for each type. That’s because each replica only stores the last outgoing message of each type in memory, and always tries to deliver those messages whenever it reconnects with another replica.
+- **Garbage collection**. We can’t store all messages, the goal here is to bound the number of messages that each replica stores, in order to avoid DoS attacks. We handle messages like this:
+    - `NewView` messages are never stored, so no garbage collection is necessary.
+    - We keep all `Proposal` messages until the proposal (or a proposal with the same block number) is finalized (which means any honest replica having both the `Proposal` and the corresponding `CommitQC`, we assume that any honest replica in that situation will immediately broadcast the block on the gossip network).
+    - We only store the newest `CommitVote` **and** `TimeoutVote` for each replica. Honest replicas only change views on QCs, so if they send a newer message, they must also have sent a `NewView` on the transition, which means we can just get the QC from that replica. Even if the other replicas don’t receive the QC, it will just trigger a reproposal.

spec/informal-spec/fetcher.rs

@@ -0,0 +1,15 @@
+// Asynchronous block fetcher.
+// Fetches all the committed blocks that it doesn't have locally from the peers.
+
+fn on_start(replica_state: &ReplicaState) {
+    loop {
+        let next_block_number = replica_state.committed_blocks.len();
+        let Some(commit_qc_ = replica_state.high_commit_qc else { continue };
+        if commit_qc.vote.block_number < next_block_number { continue }
+        // this function queries other replicas whether they have a CommittedBlock
+        // with the given number, and fetches it from them. The fetched block and
+        // its commit_qc are verified locally.
+        let block : CommittedBlock = self.fetch_block_from_peers(next_block_number);
+        self.committed_blocks.push(block);
+    }
+}

spec/informal-spec/proposer.rs

@@ -0,0 +1,44 @@
+// Proposer
+
+// This is called when the proposer starts. At the beginning of the consensus.
+fn on_start(replica_state: &ReplicaState) {
+    // The proposer has visibility into the replica state. But CANNOT write to it.
+    let mut cur_view = replica_state.view;
+
+    loop {
+        // Check if we are in a new view and we are the leader.
+        // Note that by definition, it's impossible to be the leader for view 0.
+        // We always let view 0 timeout.
+        if cur_view < replica_state.view && replica_state.pk == leader(replica_state.view) {
+            cur_view = replica_state.view;
+
+            // Get the justification for this view. If we have both a commit QC
+            // and a timeout QC for this view (highly unlikely), we should prefer
+            // to use the commit QC.
+            let justification = replica_state.get_justification(cur_view);
+
+            // Get the block number and check if this must be a reproposal.
+            let (block_number, opt_block_hash) = justification.get_implied_block();
+
+            // Propose only if you have collected all committed blocks so far.
+            assert!(block_number == self.committed_blocks.last().map_or(0,|b|b.commit_qc.vote.block_number+1)); 
+
+            // Now we create the block.
+            let block = if opt_block_hash.is_some() {
+                // There was some proposal last view that at least SUBQUORUM_WEIGHT replicas
+                // voted for and could have been finalized. We need to repropose it.
+                None
+            } else {
+                // The previous proposal was finalized, so we can propose a new block.
+                // If we don't have the previous block, this call will fail. This is
+                // fine as we can just not propose anything and let our turn end.
+                Some(self.create_proposal(block_number))
+            };
+
+            // Create the proposal message and send it to all replicas
+            let proposal = Proposal::new(block, justification);
+
+            self.send(proposal);
+        }
+    }
+}

spec/informal-spec/replica.rs

@@ -0,0 +1,256 @@
+// Replica
+
+/// A block with a matching valid certificate.
+/// invariants: hash(block) == commit_qc.vote.block_hash
+struct CommittedBlock {
+    block: Block,
+    commit_qc: CommitQC,
+}
+
+struct ReplicaState {
+    // The view this replica is currently in.
+    view: ViewNumber,
+    // The phase of the replica. Determines if we already voted for a proposal
+    // this view.
+    phase: Phase,
+    // The commit vote with the highest view that this replica has signed, if any.
+    high_vote: Option<CommitVote>,
+    // The commit quorum certificate with the highest view that this replica
+    // has observed, if any.
+    high_commit_qc: Option<CommitQC>,
+    // The timeout quorum certificate with the highest view that this replica
+    // has observed, if any.
+    high_timeout_qc: Option<TimeoutQC>,
+    // A list of every replica (including us) and their respective weights.
+    committee: Map<ValidatorPubKey, Weight>,
+    // Our public key. It also acts as our identifier.
+    pk: ValidatorPubKey,
+    // A cache of not-yet-committed proposals.
+    // Collects all received proposals sent by the proposers.
+    // In real implementation this cache would be actively pruned.
+    cached_proposals: Map<(BlockNumber,BlockHash),Block>,
+    // A history of committed blocks.
+    // invariant: committed_blocks[i].commit_qc.vote.block_number == i
+    committed_blocks: Vec<CommittedBlock>,
+}
+
+enum Phase {
+    Prepare,
+    Commit,
+    Timeout
+}
+
+// This is called when the replica starts. At the beginning of the consensus.
+// It is a loop that takes incoming messages and calls the corresponding
+// method for each message.
+fn on_start(self) {
+    // Imagine there's a timer util that just has two states (finished or not) and
+    // counts down from some given duration. For example, it counts down from 1s.
+    // If that time elapses, the timer will change state to finished.
+    // If it is reset before that, it starts counting down again from 1s.
+    let timer = Timer::new(duration);
+
+    // Get the current view.
+    let mut cur_view = self.view;
+
+    loop {
+        // If the view has increased before the timeout, we reset the timer.
+        if cur_view < self.view {
+            cur_view = self.view;
+            timer.reset();
+        }
+
+        // If the timer has finished, we send a timeout vote.
+        // If this is the first view, we immediately timeout. This will force the replicas
+        // to synchronize right at the beginning and will provide a justification for the
+        // proposer at view 1.
+        // If we have already timed out, we don't need to send another timeout vote.
+        if (timer.is_finished() || cur_view == 0) && self.phase != Phase::Timeout {
+            let vote = TimeoutVote::new(self.view,
+                                        self.high_vote,
+                                        self.high_commit_qc);
+
+            // Update our state so that we can no longer vote commit in this view.
+            self.phase = Phase::Timeout;
+
+            // Send the vote to all replicas (including ourselves).
+            self.send(vote);
+        }
+
+        // Try to get a message from the message queue and process it. We don't
+        // detail the message queue structure since it's boilerplate.
+        if let Some(message) = message_queue.pop() {
+            match message {
+                Proposal(msg) => {
+                    self.on_proposal(msg);
+                }
+                Commit(msg) => {
+                    self.on_commit(msg);
+                }
+                Timeout(msg) => {
+                    self.on_timeout(msg);
+                }
+                NewView(msg) => {
+                    self.on_new_view(msg);
+                }
+            }
+        }
+    }
+}
+
+fn on_proposal(self, proposal: Proposal) {
+    // We only allow proposals for the current view if we have not voted in
+    // it yet.
+    assert!((proposal.view() == self.view && self.phase == Prepare) || proposal.view() > self.view);
+
+    // We ignore proposals from the wrong leader.
+    assert!(proposal.leader() == leader(proposal.view()));
+
+    // Check that the proposal is valid.
+    assert!(proposal.verify());
+
+    // Get the implied block number and hash (if any).
+    let (block_number, opt_block_hash) = proposal.justification.get_implied_block();
+
+    // Vote only if you have collected all committed blocks so far.
+    assert!(block_number == self.committed_blocks.last().map_or(0,|b|b.commit_qc.vote.block_number+1));
+
+    // Check if this is a reproposal or not, and do the necessary checks.
+    // As a side result, get the correct block hash.
+    let block_hash = match opt_block_hash {
+        Some(hash) => {
+            // This is a reproposal. We let the leader repropose blocks without sending
+            // them in the proposal (it sends only the number + hash). That allows a
+            // leader to repropose a block without having it stored.
+            // It is an optimization that allows us to not wait for a leader that has
+            // the previous proposal stored (which can take 4f views), and to somewhat
+            // speed up reproposals by skipping block broadcast.
+            // This only saves time because we have a gossip network running in parallel,
+            // and any time a replica is able to create a finalized block (by possessing
+            // both the block and the commit QC) it broadcasts the finalized block (this
+            // was meant to propagate the block to full nodes, but of course validators
+            // will end up receiving it as well).
+            // However, this can be difficult to model and we might want to just
+            // ignore the gossip network in the formal model. We will still have liveness
+            // but in the model we'll end up waiting 4f views to get a leader that has the
+            // previous block before proposing a new one. This is not that bad, since
+            // then we can be sure that the consensus will continue even if the gossip
+            // network is failing for some reason.
+
+            // For sanity reasons, we'll check that there's no block in the proposal.
+            // But this check is completely unnecessary (in theory at least).
+            assert!(proposal.block.is_none());
+
+            hash
+        }
+        None => {
+            // This is a new proposal, so we need to verify it (i.e. execute it).
+            assert!(proposal.block.is_some());
+            let block = proposal.block.unwrap();
+            // To verify the block, replica just tries to apply it to the current
+            // state. Current state is the result of applying all the committed blocks until now.
+            assert!(self.verify_block(block_number, block));
+            // We cache the new proposals, waiting for them to be committed.
+            self.cached_proposals.insert((block_number,proposal.block.hash()),block);
+            block.hash()
+        }
+    };
+
+    // Update the state.
+    let vote = CommitVote::new(proposal.view(), block_number, block_hash);
+
+    self.view = proposal.view();
+    self.phase = Phase::Commit;
+    self.high_vote = Some(vote);
+    match proposal.justification {
+        Commit(qc) => self.process_commit_qc(Some(qc)),
+        Timeout(qc) => {
+            self.process_commit_qc(qc.high_qc());
+            self.high_timeout_qc = max(Some(qc), self.high_timeout_qc);
+        }
+    };
+
+    // Send the commit vote to all replicas (including ourselves).
+    self.send(vote);
+}
+
+// Processed an (already verified) commit_qc received from the network
+// as part of some message. It bumps the local high_commit_qc and if
+// we have the proposal corresponding to this qc, we append it to the committed_blocks.
+fn process_commit_qc(self, qc_opt: Option[CommitQC]) {
+    if let Some(qc) = qc_opt {
+        self.high_commit_qc = max(Some(qc), self.high_commit_qc);
+        let Some(block) = self.cached_proposals.get((qc.vote.block_number,qc.vote.block_hash)) else { return };
+        if self.committed_blocks.len()==qc.vote.block_number {
+            self.committed_blocks.push(CommittedBlock{block,commit_qc:qc});
+        }
+    }
+}
+
+fn on_commit(self, sig_vote: SignedCommitVote) {
+    // If the vote isn't current, just ignore it.
+    assert!(sig_vote.view() >= self.view)
+
+    // Check that the signed vote is valid.
+    assert!(sig_vote.verify());
+
+    // Store the vote. We will never store duplicate (same view and sender) votes.
+    // If we already have this vote, we exit early.
+    assert!(self.store(sig_vote).is_ok());
+
+    // Check if we now have a commit QC for this view.
+    if let Some(qc) = self.get_commit_qc(sig_vote.view()) {
+        self.process_commit_qc(Some(qc));
+        self.start_new_view(sig_vote.view() + 1);
+    }
+}
+
+fn on_timeout(self, sig_vote: SignedTimeoutVote) {
+    // If the vote isn't current, just ignore it.
+    assert!(sig_vote.view() >= self.view)
+
+    // Check that the signed vote is valid.
+    assert!(sig_vote.verify());
+
+    // Store the vote. We will never store duplicate (same view and sender) votes.
+    // If we already have this vote, we exit early.
+    assert!(self.store(sig_vote).is_ok());
+
+    // Check if we now have a timeout QC for this view.
+    if let Some(qc) = self.get_timeout_qc(sig_vote.view()) {
+        self.process_commit_qc(qc.high_qc());
+        self.high_timeout_qc = max(Some(qc), self.high_timeout_qc);
+        self.start_new_view(sig_vote.view() + 1);
+    }
+}
+
+fn on_new_view(self, new_view: NewView) {
+    // If the message isn't current, just ignore it.
+    assert!(new_view.view() >= self.view)
+
+    // Check that the new view is valid.
+    assert!(new_view.verify());
+
+    // Update our state.
+    match new_view.justification {
+        Commit(qc) => self.process_commit_qc(Some(qc)),
+        Timeout(qc) => {
+            self.process_commit_qc(qc.high_qc());
+            self.high_timeout_qc = max(Some(qc), self.high_timeout_qc);
+        }
+    };
+
+    if new_view.view() > self.view {
+        self.start_new_view(new_view.view());
+    }
+}
+
+fn start_new_view(self, view: ViewNumber) {
+    self.view = view;
+    self.phase = Phase::Prepare;
+
+    // Send a new view message to the other replicas, for synchronization.
+    let new_view = NewView::new(self.get_justification(view));
+
+    self.send(new_view);
+}