		Search-engine friendly clone of the ACL2 documentation.

Operations-faults-and-quora

Quorum

Quorum number for the protocol.

Signature
(quorum systate) → quorum
Arguments: systate — Guard (system-statep systate).
Returns: quorum — Type (natp quorum).

The execution of the protocol (i.e. the transitions in our system) involves checking conditions that certain numbers reach quorum, which is defined as n - F. This is equivalent to 2F + 1 only when n = 3F + 1, as we also prove here; it is not when n = 3F + 2 or n = 3F + 3.

Some BFT literature is not always clear about the distinction between n - F and 2F + 1: for instance, both the Narwhal and the Bullshark papers use 2F + 1 in their description of the protocol, even though the description should be for all values of n. Sometimes the BFT literature makes the n = 3F + 1 assumption, but such assumption does not seem to appear (clearly or at all) in the aforementioned papers, and it seems indeed strange to use 2F + 1 in the description of what should be a general protocol, when using n - F would be much clearer and correct.

Definitions and Theorems

Function: quorum

(defun quorum (systate)
  (declare (xargs :guard (system-statep systate)))
  (let ((__function__ 'quorum))
    (declare (ignorable __function__))
    (- (number-validators systate)
       (max-faulty systate))))

Theorem: natp-of-quorum

(defthm natp-of-quorum
  (b* ((quorum (quorum systate)))
    (natp quorum))
  :rule-classes :rewrite)

Theorem: posp-of-quorum-when-there-are-validators

(defthm posp-of-quorum-when-there-are-validators
  (implies (not (emptyp (all-addresses systate)))
           (posp (quorum systate)))
  :rule-classes (:rewrite :type-prescription))

Theorem: quorum-when-3f+1

(defthm quorum-when-3f+1
  (implies (equal (number-validators systate)
                  (1+ (* 3 (max-faulty systate))))
           (equal (quorum systate)
                  (1+ (* 2 (max-faulty systate))))))

Theorem: quorum-of-system-state-fix-systate

(defthm quorum-of-system-state-fix-systate
  (equal (quorum (system-state-fix systate))
         (quorum systate)))

Theorem: quorum-system-state-equiv-congruence-on-systate

(defthm quorum-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (quorum systate)
                  (quorum systate-equiv)))
  :rule-classes :congruence)