		Search-engine friendly clone of the ACL2 documentation.

Committees

Committee-total

Total number of validators in a committee.

Signature
(committee-total commtt) → total
Arguments: commtt — Guard (committeep commtt).
Returns: total — Type (posp total).

This is just the number of addresses.

This is n, using the notation in max-faulty-for-total. But note that, unlike typical BFT literature, where there is a fixed set of validators, in AleoBFT we have dynamic committees, and so n is a function of the committee.

Definitions and Theorems

Function: committee-total

(defun committee-total (commtt)
  (declare (xargs :guard (committeep commtt)))
  (let ((__function__ 'committee-total))
    (declare (ignorable __function__))
    (cardinality (committee-members commtt))))

Theorem: posp-of-committee-total

(defthm posp-of-committee-total
  (b* ((total (committee-total commtt)))
    (posp total))
  :rule-classes (:rewrite :type-prescription))

Theorem: committee-total-of-committee-fix-commtt

(defthm committee-total-of-committee-fix-commtt
  (equal (committee-total (committee-fix commtt))
         (committee-total commtt)))

Theorem: committee-total-committee-equiv-congruence-on-commtt

(defthm committee-total-committee-equiv-congruence-on-commtt
  (implies (committee-equiv commtt commtt-equiv)
           (equal (committee-total commtt)
                  (committee-total commtt-equiv)))
  :rule-classes :congruence)