		Search-engine friendly clone of the ACL2 documentation.

Signed-certificates

Signed-certs

Certificates signed by a validator.

Signature
(signed-certs val systate) → certs
Arguments: val — Guard (addressp val).; systate — Guard (system-statep systate).
Returns: certs — Type (certificate-setp certs).

These are all the certificates in the system signed by the validator. We define this notion only for correct validators (signers). We could also define it for faulty validators, since they can be signers, but we only need this notion for correct validators.

Definitions and Theorems

Function: signed-certs

(defun signed-certs (val systate)
  (declare (xargs :guard (and (addressp val)
                              (system-statep systate))))
  (declare (xargs :guard (in val (correct-addresses systate))))
  (let ((__function__ 'signed-certs))
    (declare (ignorable __function__))
    (certs-with-signer val (system-certs systate))))

Theorem: certificate-setp-of-signed-certs

(defthm certificate-setp-of-signed-certs
  (b* ((certs (signed-certs val systate)))
    (certificate-setp certs))
  :rule-classes :rewrite)

Theorem: in-signed-certs-when-in-system-and-signer

(defthm in-signed-certs-when-in-system-and-signer
  (implies (and (in cert (system-certs systate))
                (in signer (certificate->signers cert))
                (in signer (correct-addresses systate)))
           (in cert (signed-certs signer systate))))

Theorem: signed-certs-of-address-fix-val

(defthm signed-certs-of-address-fix-val
  (equal (signed-certs (address-fix val) systate)
         (signed-certs val systate)))

Theorem: signed-certs-address-equiv-congruence-on-val

(defthm signed-certs-address-equiv-congruence-on-val
  (implies (address-equiv val val-equiv)
           (equal (signed-certs val systate)
                  (signed-certs val-equiv systate)))
  :rule-classes :congruence)

Theorem: signed-certs-of-system-state-fix-systate

(defthm signed-certs-of-system-state-fix-systate
  (equal (signed-certs val (system-state-fix systate))
         (signed-certs val systate)))

Theorem: signed-certs-system-state-equiv-congruence-on-systate

(defthm signed-certs-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (signed-certs val systate)
                  (signed-certs val systate-equiv)))
  :rule-classes :congruence)