|
|
|---|
|
|
|
|---|
Some theorems about causal histories in unequivocal, backward-closed DAGs.
The first theorem says that the causal history of a certificate in a backward-closed subset of an unequivocal DAG is the same in the superset. That is, causal histories are ``stable'' as DAGs of validators grow. New certificates, with their own causal histories, may be added as the DAG grows, but without affecting histories of certificates already there.
The second theorem says that the causal histories of a common certificate of two backward-closed, individually and mutually unequivocal DAGs, are the same in the two DAGs. This is an important property for consistency of blockchains across different validators: if two validators had different causal histories for the same certificate, they could commit different transactions to their blockchains; yhis theorem rules out that situation.
Theorem:
(defthm certificate-causal-history-of-unequivocal-superdag (implies (and (certificate-setp dag0) (certificate-setp dag) (subset dag0 dag) (certificate-set-unequivocalp dag) (dag-closedp dag0) (in cert dag0)) (equal (certificate-causal-history cert dag) (certificate-causal-history cert dag0))))
Theorem:
(defthm certificate-causal-history-of-unequivocal-dags (implies (and (certificate-setp dag1) (certificate-setp dag2) (certificate-sets-unequivocalp dag1 dag2) (certificate-set-unequivocalp dag1) (certificate-set-unequivocalp dag2) (dag-closedp dag1) (dag-closedp dag2) (in cert dag1) (in cert dag2)) (equal (certificate-causal-history cert dag1) (certificate-causal-history cert dag2))))