		Search-engine friendly clone of the ACL2 documentation.

System-certificates

Validators-certs

Certificates from the DAGs of a set of (correct) validators.

Signature
(validators-certs vals systate) → certs
Arguments: vals — Guard (address-setp vals).; systate — Guard (system-statep systate).
Returns: certs — Type (certificate-setp certs).

We union the DAGs of the given validators.

Definitions and Theorems

Function: validators-certs

(defun validators-certs (vals systate)
  (declare (xargs :guard (and (address-setp vals)
                              (system-statep systate))))
  (declare (xargs :guard (subset vals (correct-addresses systate))))
  (let ((__function__ 'validators-certs))
    (declare (ignorable __function__))
    (b* (((when (or (not (mbt (address-setp vals)))
                    (emptyp vals)))
          nil)
         (vstate (get-validator-state (head vals)
                                      systate)))
      (union (validator-state->dag vstate)
             (validators-certs (tail vals)
                               systate)))))

Theorem: certificate-setp-of-validators-certs

(defthm certificate-setp-of-validators-certs
  (b* ((certs (validators-certs vals systate)))
    (certificate-setp certs))
  :rule-classes :rewrite)

Theorem: in-of-validators-certs-when-in-some-dag

(defthm in-of-validators-certs-when-in-some-dag
 (implies
  (and
      (address-setp vals)
      (subset vals (correct-addresses systate))
      (in val vals)
      (in cert
          (validator-state->dag (get-validator-state val systate))))
  (in cert (validators-certs vals systate))))

Theorem: validators-certs-of-address-set-fix-vals

(defthm validators-certs-of-address-set-fix-vals
  (equal (validators-certs (address-set-fix vals)
                           systate)
         (validators-certs vals systate)))

Theorem: validators-certs-address-set-equiv-congruence-on-vals

(defthm validators-certs-address-set-equiv-congruence-on-vals
  (implies (address-set-equiv vals vals-equiv)
           (equal (validators-certs vals systate)
                  (validators-certs vals-equiv systate)))
  :rule-classes :congruence)

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

(defthm validators-certs-of-system-state-fix-systate
  (equal (validators-certs vals (system-state-fix systate))
         (validators-certs vals systate)))

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

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