		Search-engine friendly clone of the ACL2 documentation.

Signed-previous-quorum

Signed-previous-quorum-p

Definition of the invariant: for each certificate signed by each correct validator, either the certificate's round is 1 and the certificate has no references to previous certificates, or the certificate's round is not 1 and the references to previous certificates form a non-zero quorum in the committee of the preceding round of the certificate.

Definitions and Theorems

Theorem: signed-previous-quorum-p-necc

(defthm signed-previous-quorum-p-necc
  (implies (signed-previous-quorum-p systate)
           (implies (and (in val (correct-addresses systate))
                         (in cert (signed-certs val systate)))
                    (validator-signed-previous-quorum-p
                         cert
                         (get-validator-state val systate)))))

Theorem: booleanp-of-signed-previous-quorum-p

(defthm booleanp-of-signed-previous-quorum-p
  (b* ((yes/no (signed-previous-quorum-p systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: signed-previous-quorum-p-of-system-state-fix-systate

(defthm signed-previous-quorum-p-of-system-state-fix-systate
  (equal (signed-previous-quorum-p (system-state-fix systate))
         (signed-previous-quorum-p systate)))

Theorem: signed-previous-quorum-p-system-state-equiv-congruence-on-systate

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