		Search-engine friendly clone of the ACL2 documentation.

Operations-faults-and-quora

Max-faulty

Maximum number of faulty validators tolerated by the system.

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

This is F: see the discussion in max-faulty-for-total.

Definitions and Theorems

Function: max-faulty

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

Theorem: natp-of-max-faulty

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

Theorem: number-validators-lower-bound-wrt-max-faulty

(defthm number-validators-lower-bound-wrt-max-faulty
  (implies (> (number-validators systate) 0)
           (>= (number-validators systate)
               (1+ (* 3 (max-faulty systate)))))
  :rule-classes :linear)

Theorem: max-faulty-of-system-state-fix-systate

(defthm max-faulty-of-system-state-fix-systate
  (equal (max-faulty (system-state-fix systate))
         (max-faulty systate)))

Theorem: max-faulty-system-state-equiv-congruence-on-systate

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