		Search-engine friendly clone of the ACL2 documentation.

Backward-closure

Backward-closed-p-of-next

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

The only two kinds of events that extend DAGs are create and accept. For these two kinds of events, first we prove theorems saying that the added certificate has all the predecessors in the DAG, which is ensured by create-possiblep and accept-possiblep. Then we prove the main theorems, using rule dag-closedp-of-insert to handle the addition of the certificate.

For the other four kinds of events, the proof is easy.

Definitions and Theorems

Theorem: certificate-previous-in-dag-p-when-create-possiblep

(defthm certificate-previous-in-dag-p-when-create-possiblep
  (implies (and (create-possiblep cert systate)
                (in (certificate->author cert)
                    (correct-addresses systate)))
           (certificate-previous-in-dag-p
                cert
                (validator-state->dag
                     (get-validator-state (certificate->author cert)
                                          systate)))))

Theorem: backward-closed-p-of-create-next

(defthm backward-closed-p-of-create-next
  (implies (and (backward-closed-p systate)
                (create-possiblep cert systate)
                (certificatep cert))
           (backward-closed-p (create-next cert systate))))

Theorem: certificate-previous-in-dag-p-when-accept-possiblep

(defthm certificate-previous-in-dag-p-when-accept-possiblep
  (implies (accept-possiblep msg systate)
           (certificate-previous-in-dag-p
                (message->certificate msg)
                (validator-state->dag
                     (get-validator-state (message->destination msg)
                                          systate)))))

Theorem: backward-closed-p-of-accept-next

(defthm backward-closed-p-of-accept-next
  (implies (and (backward-closed-p systate)
                (accept-possiblep msg systate))
           (backward-closed-p (accept-next msg systate))))

Theorem: backward-closed-p-of-advance-next

(defthm backward-closed-p-of-advance-next
  (implies (and (backward-closed-p systate)
                (advance-possiblep val systate))
           (backward-closed-p (advance-next val systate))))

Theorem: backward-closed-p-of-commit-next

(defthm backward-closed-p-of-commit-next
  (implies (and (backward-closed-p systate)
                (commit-possiblep val systate))
           (backward-closed-p (commit-next val systate))))

Theorem: backward-closed-p-of-event-next

(defthm backward-closed-p-of-event-next
  (implies (and (backward-closed-p systate)
                (event-possiblep event systate))
           (backward-closed-p (event-next event systate))))