		Search-engine friendly clone of the ACL2 documentation.

System-states

Number-validators

Number of validators in the system.

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

This is the total number of validators in the system, often denoted n in the BFT literature.

Definitions and Theorems

Function: number-validators

(defun number-validators (systate)
  (declare (xargs :guard (system-statep systate)))
  (let ((__function__ 'number-validators))
    (declare (ignorable __function__))
    (cardinality (all-addresses systate))))

Theorem: natp-of-number-validators

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

Theorem: number-validators-alt-def

(defthm number-validators-alt-def
  (equal (number-validators systate)
         (omap::size (system-state->validators systate))))

Theorem: number-validator-gt-0-when-nonempty-all-addresses

(defthm number-validator-gt-0-when-nonempty-all-addresses
  (implies (not (emptyp (all-addresses systate)))
           (> (number-validators systate) 0))
  :rule-classes :linear)

Theorem: number-validators-of-system-state-fix-systate

(defthm number-validators-of-system-state-fix-systate
  (equal (number-validators (system-state-fix systate))
         (number-validators systate)))

Theorem: number-validators-system-state-equiv-congruence-on-systate

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