		Search-engine friendly clone of the ACL2 documentation.

Certificates-of-validators

Signed-certificates

Certificates signed by a validator.

Signature
(signed-certificates 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-owned-certificates, validators own (in the precise sense of owned-certificates) the same set of certificates; so any such set of owned certificates is the set of all 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-certificates

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

Theorem: certificate-setp-of-signed-certificates

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

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

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

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

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

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

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

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

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