		Search-engine friendly clone of the ACL2 documentation.

Committed-redundant-def-and-init-and-next

Committed-redundant-p-of-next

Preservation of the invariant: if the invariant holds in a system state, it also holds in the next system state.

A create or accept event does not change the set of committed certificates or the last anchor, but it extends the DAGs with a certificate. However, since the last anchor is already present, its causal history does not change, because the newly added certificate cannot be in its causal history; the key theorem used in this proof is certificate-causal-history-of-unequivocal-superdag. To discharge its hypothesis that the extended DAG is unequivocal, we use the already proved preservation theorem unequivocal-dags-certificates-p-of-create-next, along with a :use hint to force the application of non-equivocation on the new state rather than the old one.

A commit event changes, for the target validator, the last anchor and the set of committed certificates, but not the DAG. According to the theorem new-committed-certs-of-extend-blockchain proved in extend-blockchain, the new set of committed certificates is the union of the old ones with the causal history of the new anchor. But the invariant in the old state tells us that the old set of committed anchors is the causal history of the old last anchor: so the new set of committed certificates is the union of the causal history of the new last anchor and the causal history of the old last anchor. But, as previously proved, there is a path in the DAG from the new last anchor and the old last anchor, and therefore by certificate-causal-history-subset-when-path the causal history of the old last anchor is a subset of the causal history of the new last anchor: thus the union reduces to the latter, and the invariant is re-established in the new state.

An advance event does not change the set of committed certificates or the last anchor or the DAG, and thus the proof is easy.

Definitions and Theorems

Theorem: validator-committed-redundant-p-of-create-next

(defthm validator-committed-redundant-p-of-create-next
  (implies
       (and (system-committees-fault-tolerant-p systate)
            (backward-closed-p systate)
            (signer-records-p systate)
            (no-self-endorsed-p systate)
            (signer-quorum-p systate)
            (unequivocal-dags-p systate)
            (same-committees-p systate)
            (last-anchor-present-p systate)
            (in val (correct-addresses systate))
            (validator-committed-redundant-p
                 (get-validator-state val systate))
            (create-possiblep cert systate))
       (validator-committed-redundant-p
            (get-validator-state val (create-next cert systate)))))

Theorem: committed-redundant-p-of-create-next

(defthm committed-redundant-p-of-create-next
  (implies (and (committed-redundant-p systate)
                (system-committees-fault-tolerant-p systate)
                (backward-closed-p systate)
                (signer-records-p systate)
                (no-self-endorsed-p systate)
                (signer-quorum-p systate)
                (unequivocal-dags-p systate)
                (same-committees-p systate)
                (last-anchor-present-p systate)
                (create-possiblep cert systate))
           (committed-redundant-p (create-next cert systate))))

Theorem: validator-committed-redundant-p-of-accept-next

(defthm validator-committed-redundant-p-of-accept-next
  (implies
       (and (system-committees-fault-tolerant-p systate)
            (backward-closed-p systate)
            (signer-quorum-p systate)
            (unequivocal-signed-certs-p systate)
            (unequivocal-dags-p systate)
            (same-committees-p systate)
            (last-anchor-present-p systate)
            (in val (correct-addresses systate))
            (validator-committed-redundant-p
                 (get-validator-state val systate))
            (accept-possiblep msg systate)
            (messagep msg))
       (validator-committed-redundant-p
            (get-validator-state val (accept-next msg systate)))))

Theorem: committed-redundant-p-of-accept-next

(defthm committed-redundant-p-of-accept-next
  (implies (and (committed-redundant-p systate)
                (system-committees-fault-tolerant-p systate)
                (backward-closed-p systate)
                (signer-quorum-p systate)
                (unequivocal-signed-certs-p systate)
                (unequivocal-dags-p systate)
                (same-committees-p systate)
                (last-anchor-present-p systate)
                (accept-possiblep msg systate)
                (messagep msg))
           (committed-redundant-p (accept-next msg systate))))

Theorem: validator-committed-redundant-p-of-advance-next

(defthm validator-committed-redundant-p-of-advance-next
  (implies
       (and (in val (correct-addresses systate))
            (advance-possiblep val1 systate)
            (validator-committed-redundant-p
                 (get-validator-state val systate)))
       (validator-committed-redundant-p
            (get-validator-state val (advance-next val1 systate)))))

Theorem: committed-redundant-p-of-advance-next

(defthm committed-redundant-p-of-advance-next
  (implies (and (committed-redundant-p systate)
                (advance-possiblep val systate))
           (committed-redundant-p (advance-next val systate))))

Theorem: validator-committed-redundant-p-of-commit-next-same

(defthm validator-committed-redundant-p-of-commit-next-same
  (implies
       (and (last-blockchain-round-p systate)
            (ordered-blockchain-p systate)
            (signer-quorum-p systate)
            (unequivocal-dags-p systate)
            (last-anchor-present-p systate)
            (omni-paths-p systate)
            (in val (correct-addresses systate))
            (commit-possiblep val systate)
            (addressp val)
            (validator-committed-redundant-p
                 (get-validator-state val systate)))
       (validator-committed-redundant-p
            (get-validator-state val (commit-next val systate)))))

Theorem: validator-committed-redundant-p-of-commit-next-diff

(defthm validator-committed-redundant-p-of-commit-next-diff
  (implies
       (and (last-blockchain-round-p systate)
            (ordered-blockchain-p systate)
            (signer-quorum-p systate)
            (in val (correct-addresses systate))
            (commit-possiblep val1 systate)
            (addressp val1)
            (validator-committed-redundant-p
                 (get-validator-state val systate))
            (not (equal val val1)))
       (validator-committed-redundant-p
            (get-validator-state val (commit-next val1 systate)))))

Theorem: validator-committed-redundant-p-of-commit-next

(defthm validator-committed-redundant-p-of-commit-next
  (implies
       (and (last-blockchain-round-p systate)
            (ordered-blockchain-p systate)
            (signer-quorum-p systate)
            (unequivocal-dags-p systate)
            (last-anchor-present-p systate)
            (omni-paths-p systate)
            (in val (correct-addresses systate))
            (commit-possiblep val1 systate)
            (addressp val1)
            (validator-committed-redundant-p
                 (get-validator-state val systate)))
       (validator-committed-redundant-p
            (get-validator-state val (commit-next val1 systate)))))

Theorem: committed-redundant-p-of-commit-next

(defthm committed-redundant-p-of-commit-next
  (implies (and (committed-redundant-p systate)
                (last-blockchain-round-p systate)
                (ordered-blockchain-p systate)
                (signer-quorum-p systate)
                (unequivocal-dags-p systate)
                (last-anchor-present-p systate)
                (omni-paths-p systate)
                (commit-possiblep val systate)
                (addressp val))
           (committed-redundant-p (commit-next val systate))))

Theorem: committed-redundant-p-of-event-next

(defthm committed-redundant-p-of-event-next
  (implies (and (committed-redundant-p systate)
                (system-committees-fault-tolerant-p systate)
                (backward-closed-p systate)
                (last-blockchain-round-p systate)
                (ordered-blockchain-p systate)
                (signer-records-p systate)
                (no-self-endorsed-p systate)
                (signer-quorum-p systate)
                (unequivocal-signed-certs-p systate)
                (unequivocal-dags-p systate)
                (same-committees-p systate)
                (last-anchor-present-p systate)
                (omni-paths-p systate)
                (event-possiblep event systate))
           (committed-redundant-p (event-next event systate))))