|
|
|---|
|
|
|
|---|
Causal history of a certificate in a DAG.
(certificate-causal-history cert dag) → hist
This is the set of all the certificates in the DAG that the certificate has a path to. This includes the certificate itself, which has an empty path to itself. We calculate the causal history by going backwards through rounds.
We start with the certificate. If its round number is 1, we stop and return the singleton set with the certificate. Since certificates have positive round numbers, the DAG cannot have any certificate at round 0. It is in fact an invariant that a certificate at round 1 has no edges to previous certificates, although the invariant is not available here.
If the certificate's round number is not 1, we retrieve its immediate predecessor certificates, which all have the round number that precedes the certificate's. We use a mutually recursive companion of this function to go through the set of preceding certificates, obtaining the causal history for all of them (i.e. the union of their causal histories). Then we add the current certificate to those combined causal histories, and return the result.
This function is executable, but not necessarily efficient: it tries out all possible paths in the DAG. It is adequate for specification, because it has a simple definition that is easier to assess and to prove properties about, compared to a more efficient definition. A more efficient definition could be provided as well, and proved equivalent to this one.
The termination measure and proof is similar to the one for path-to-author+round; see that function for details.
Theorem:
(defthm return-type-of-certificate-causal-history.hist (b* ((acl2::?hist (certificate-causal-history cert dag))) (certificate-setp hist)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-certificate-set-causal-history.hist (b* ((acl2::?hist (certificate-set-causal-history certs dag))) (certificate-setp hist)) :rule-classes :rewrite)
Theorem:
(defthm certificate-causal-history-subset (implies (and (certificate-setp dag) (in cert dag)) (b* ((acl2::?hist (certificate-causal-history cert dag))) (subset hist dag))))
Theorem:
(defthm certificate-set-causal-history-subset (implies (and (certificate-setp dag) (subset certs dag)) (b* ((acl2::?hist (certificate-set-causal-history certs dag))) (subset hist dag))))