|
|
|---|
|
|
|
|---|
Check if all the previous certificates referenced by a given certificate are in a given DAG.
(certificate-previous-in-dag-p cert dag) → yes/no
The check succeeds immediately if the certificate's round number is 1. In that case, it is an invariant (proved elsewhere) that certificates in round 1 reference no previous certificates; therefore, the requirement is trivially satisfied.
For the more common case in which the certificate's round number is not 1, we retrieve all the certificates from the DAG at the previous round, we obtain their set of authors, and we check that those are a superset of the set of previous certificate authors referenced by the certificate.
For a given certificate,
this predicate is preserved by extending the DAG,
because extending the DAG cannot remove
any referenced predecessor certificates.
We prove this in
Function:
(defun certificate-previous-in-dag-p (cert dag) (declare (xargs :guard (and (certificatep cert) (certificate-setp dag)))) (let ((__function__ 'certificate-previous-in-dag-p)) (declare (ignorable __function__)) (b* (((certificate cert) cert)) (or (= (certificate->round cert) 1) (subset (certificate->previous cert) (cert-set->author-set (certs-with-round (1- (certificate->round cert)) dag)))))))
Theorem:
(defthm booleanp-of-certificate-previous-in-dag-p (b* ((yes/no (certificate-previous-in-dag-p cert dag))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm certificate-previous-in-dag-p-when-subset (implies (and (certificate-setp dag) (certificate-setp dag1) (subset dag dag1) (certificate-previous-in-dag-p cert dag)) (certificate-previous-in-dag-p cert dag1)))