		Search-engine friendly clone of the ACL2 documentation.

Signer-quorum

Validator-signer-quorum-p

Check if the signers of a certificate are a subset of the committee for a certificate's round and form a quorum in that committee, where the committee is calculated by a validator (represented by its state).

Signature
(validator-signer-quorum-p cert vstate) → yes/no
Arguments: cert — Guard (certificatep cert).; vstate — Guard (validator-statep vstate).
Returns: yes/no — Type (booleanp yes/no).

This is used by signer-quorum-p to define our invariant. The guard ensures that the validator can calculate the committee.

Definitions and Theorems

Function: validator-signer-quorum-p

(defun validator-signer-quorum-p (cert vstate)
 (declare (xargs :guard (and (certificatep cert)
                             (validator-statep vstate))))
 (declare (xargs :guard (active-committee-at-round
                             (certificate->round cert)
                             (validator-state->blockchain vstate))))
 (let ((__function__ 'validator-signer-quorum-p))
   (declare (ignorable __function__))
   (b*
    (((validator-state vstate) vstate)
     ((certificate cert) cert)
     (commtt
          (active-committee-at-round cert.round vstate.blockchain)))
    (and (subset (certificate->signers cert)
                 (committee-members commtt))
         (>= (committee-members-stake (certificate->signers cert)
                                      commtt)
             (committee-quorum-stake commtt))))))

Theorem: booleanp-of-validator-signer-quorum-p

(defthm booleanp-of-validator-signer-quorum-p
  (b* ((yes/no (validator-signer-quorum-p cert vstate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: validator-signer-quorum-p-of-certificate-fix-cert

(defthm validator-signer-quorum-p-of-certificate-fix-cert
  (equal (validator-signer-quorum-p (certificate-fix cert)
                                    vstate)
         (validator-signer-quorum-p cert vstate)))

Theorem: validator-signer-quorum-p-certificate-equiv-congruence-on-cert

(defthm
     validator-signer-quorum-p-certificate-equiv-congruence-on-cert
  (implies (certificate-equiv cert cert-equiv)
           (equal (validator-signer-quorum-p cert vstate)
                  (validator-signer-quorum-p cert-equiv vstate)))
  :rule-classes :congruence)

Theorem: validator-signer-quorum-p-of-validator-state-fix-vstate

(defthm validator-signer-quorum-p-of-validator-state-fix-vstate
  (equal
       (validator-signer-quorum-p cert (validator-state-fix vstate))
       (validator-signer-quorum-p cert vstate)))

Theorem: validator-signer-quorum-p-validator-state-equiv-congruence-on-vstate

(defthm
 validator-signer-quorum-p-validator-state-equiv-congruence-on-vstate
 (implies (validator-state-equiv vstate vstate-equiv)
          (equal (validator-signer-quorum-p cert vstate)
                 (validator-signer-quorum-p cert vstate-equiv)))
 :rule-classes :congruence)