		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. As proved in same-associated-certificates, validators have the same associated certificates, so any such set of associated certificates is the set of all the certificates in the system. We pick the set of the signer, and we select the ones whose signers include the signer.

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 (associated-certs val 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: 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)