		Search-engine friendly clone of the ACL2 documentation.

Dag-certificate-next

Cert-with-author+round-of-next

Transition invariant for cert-with-author+round.

The only kinds of events that change the DAG are create and accept. They do so by extending the DAG, adding a certificate to it. We have already proved the preservation of the DAG non-equivocation invariant, and here we need to use, directly, the fact that DAG non-equivocation is preserved by the transitions: this tells us that the new DAG (the one with the added certificate) is unequivocal, which lets us use cert-with-author+round-of-unequivocal-superset to show that we retrieve the same certificate.

We need to assume a number of previously proved invariants, which are hypotheses for the preservation of DAG non-equivocation.

The other four kinds of events do not change the DAG, and thus the proof is easy.

Definitions and Theorems

Theorem: cert-with-author+round-of-create-next

(defthm cert-with-author+round-of-create-next
 (implies
  (and
     (system-committees-fault-tolerant-p systate)
     (no-self-endorsed-p systate)
     (signer-records-p systate)
     (signer-quorum-p systate)
     (unequivocal-dags-p systate)
     (same-committees-p systate)
     (in val (correct-addresses systate))
     (create-possiblep cert systate)
     (cert-with-author+round
          author round
          (validator-state->dag (get-validator-state val systate))))
  (equal
   (cert-with-author+round
        author round
        (validator-state->dag
             (get-validator-state val (create-next cert systate))))
   (cert-with-author+round
        author round
        (validator-state->dag (get-validator-state val systate))))))

Theorem: cert-with-author+round-of-accept-next

(defthm cert-with-author+round-of-accept-next
 (implies
  (and
     (system-committees-fault-tolerant-p systate)
     (signer-quorum-p systate)
     (unequivocal-signed-certs-p systate)
     (unequivocal-dags-p systate)
     (same-committees-p systate)
     (in val (correct-addresses systate))
     (accept-possiblep msg systate)
     (messagep msg)
     (cert-with-author+round
          author round
          (validator-state->dag (get-validator-state val systate))))
  (equal
   (cert-with-author+round
        author round
        (validator-state->dag
             (get-validator-state val (accept-next msg systate))))
   (cert-with-author+round
        author round
        (validator-state->dag (get-validator-state val systate))))))

Theorem: cert-with-author+round-of-advance-next

(defthm cert-with-author+round-of-advance-next
 (implies
  (advance-possiblep val1 systate)
  (equal
   (cert-with-author+round
        author round
        (validator-state->dag
             (get-validator-state val (advance-next val1 systate))))
   (cert-with-author+round
        author round
        (validator-state->dag (get-validator-state val systate))))))

Theorem: cert-with-author+round-of-commit-next

(defthm cert-with-author+round-of-commit-next
 (implies
  (commit-possiblep val1 systate)
  (equal
   (cert-with-author+round
        author round
        (validator-state->dag
             (get-validator-state val (commit-next val1 systate))))
   (cert-with-author+round
        author round
        (validator-state->dag (get-validator-state val systate))))))

Theorem: cert-with-author+round-of-event-next

(defthm cert-with-author+round-of-event-next
 (implies
  (and
     (system-committees-fault-tolerant-p systate)
     (no-self-endorsed-p systate)
     (signer-records-p systate)
     (unequivocal-signed-certs-p systate)
     (signer-quorum-p systate)
     (unequivocal-dags-p systate)
     (same-committees-p systate)
     (in val (correct-addresses systate))
     (event-possiblep event systate)
     (cert-with-author+round
          author round
          (validator-state->dag (get-validator-state val systate))))
  (equal
   (cert-with-author+round
        author round
        (validator-state->dag
             (get-validator-state val (event-next event systate))))
   (cert-with-author+round
        author round
        (validator-state->dag (get-validator-state val systate))))))