		Search-engine friendly clone of the ACL2 documentation.

Signer-records

Signer-record-p

Check if (the state of) a signer has a record of a certificate author and round.

Signature
(signer-record-p author round vstate) → yes/no
Arguments: author — Guard (addressp author).; round — Guard (posp round).; vstate — Guard (validator-statep vstate).
Returns: yes/no — Type (booleanp yes/no).

This is the case if the DAG has some certificate with the given author and round, or the given author and round are in the set of endorsed pairs. We express the first condition by saying that cert-with-author+round does not return nil. The signer is represented by its state vstate here.

Definitions and Theorems

Function: signer-record-p

(defun signer-record-p (author round vstate)
  (declare (xargs :guard (and (addressp author)
                              (posp round)
                              (validator-statep vstate))))
  (let ((__function__ 'signer-record-p))
    (declare (ignorable __function__))
    (b* (((validator-state vstate) vstate)
         (author (address-fix author))
         (round (pos-fix round)))
      (or (and (cert-with-author+round author round vstate.dag)
               t)
          (in (make-address+pos :address author
                                :pos round)
              vstate.endorsed)))))

Theorem: booleanp-of-signer-record-p

(defthm booleanp-of-signer-record-p
  (b* ((yes/no (signer-record-p author round vstate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: signer-record-p-of-address-fix-author

(defthm signer-record-p-of-address-fix-author
  (equal (signer-record-p (address-fix author)
                          round vstate)
         (signer-record-p author round vstate)))

Theorem: signer-record-p-address-equiv-congruence-on-author

(defthm signer-record-p-address-equiv-congruence-on-author
  (implies (address-equiv author author-equiv)
           (equal (signer-record-p author round vstate)
                  (signer-record-p author-equiv round vstate)))
  :rule-classes :congruence)

Theorem: signer-record-p-of-pos-fix-round

(defthm signer-record-p-of-pos-fix-round
  (equal (signer-record-p author (pos-fix round)
                          vstate)
         (signer-record-p author round vstate)))

Theorem: signer-record-p-pos-equiv-congruence-on-round

(defthm signer-record-p-pos-equiv-congruence-on-round
  (implies (acl2::pos-equiv round round-equiv)
           (equal (signer-record-p author round vstate)
                  (signer-record-p author round-equiv vstate)))
  :rule-classes :congruence)

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

(defthm signer-record-p-of-validator-state-fix-vstate
  (equal (signer-record-p author
                          round (validator-state-fix vstate))
         (signer-record-p author round vstate)))

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

(defthm signer-record-p-validator-state-equiv-congruence-on-vstate
  (implies (validator-state-equiv vstate vstate-equiv)
           (equal (signer-record-p author round vstate)
                  (signer-record-p author round vstate-equiv)))
  :rule-classes :congruence)