		Search-engine friendly clone of the ACL2 documentation.

Dag-previous-quorum-def-and-init-and-next

Dag-previous-quorum-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 may change the DAG are create and accept.

For create, there are two cases to consider. For an existing (i.e. old) certificate in the DAG, we just need to show that the previous quorum property is preserved: this is easy, and relies on the fact that the blockchain, from which the committee is calculated, does not change for create. For a newly created certificate in create, the only change to the DAG is for the author: the other validators are sent the certificate in messages, but the messages are in the network, not in their DAGs. The certificate's author adds the certificate directly to the DAG. But create-possiblep explicitly checks the previous quorum condition.

For accept, we have a similar split, considering a certificate already in the DAG (i.e. old), and the newly stored certificate, moved from the network. The case of an old certificate is similar to create; again, we use the fact that the blockchain does not change under an accept event. The case of the newly stored certificate is more complicated. The conditions in accept-possiblep include the fact that the certificate is signed by a quorum, which, assuming fault tolerance (which we do), must contain at least one correct validator: see pick-correct-validator-when-fault-tolerant-and-geq-quorum in pick-correct-validator. We appeal to the previously proved invariant signed-previous-quorum-p to obtain that the previous quorum condition is satisfied with respect to the signing validator (which may differ from the target validator of accept). Then we use the invariant same-committees-p to show that, if signer and storer differ, they agree on that committee, and thus on the previous quorum requirement. Fault tolerance and the other invariants used in the proof propagate to the theorem about event-next.

DAGs do not change for the other kinds of events, so the proofs for them always rely on the preservaton of the properties. For each kind of event, we prove a lemma about validator-dag-previous-quorum-p and then a theorem about dag-previous-quorum-p. For advance, there is no change to the blockchain, so the proof is fairly easy. For commit, the blockchain changes, but we use the fact that extending the blockchain does not affect the committees calculated prior to the extension. This property depends on the previously proved invariants that blockchain rounds are even and ordered, that the last committed round in the validator state matches the latest block's round (or they are both 0 if there are no blocks), and that a validator can calculate the active committees at all the rounds in which it has certificates; so we need to add these invariants as hypothesis, which therefore propagate to the theorem about event-next.

Definitions and Theorems

Theorem: validator-dag-previous-quorum-p-of-create-next-old

(defthm validator-dag-previous-quorum-p-of-create-next-old
  (implies
       (validator-dag-previous-quorum-p
            cert1 (get-validator-state val systate))
       (validator-dag-previous-quorum-p
            cert1
            (get-validator-state val (create-next cert systate)))))

Theorem: validator-dag-previous-quorum-p-of-create-next-new

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

Theorem: dag-previous-quorum-p-of-create-next

(defthm dag-previous-quorum-p-of-create-next
  (implies (and (dag-previous-quorum-p systate)
                (create-possiblep cert systate))
           (dag-previous-quorum-p (create-next cert systate))))

Theorem: validator-dag-previous-quorum-p-of-accept-next-old

(defthm validator-dag-previous-quorum-p-of-accept-next-old
  (implies
       (and (validator-dag-previous-quorum-p
                 cert (get-validator-state val systate))
            (accept-possiblep msg systate))
       (validator-dag-previous-quorum-p
            cert
            (get-validator-state val (accept-next msg systate)))))

Theorem: validator-dag-previous-quorum-p-of-accept-next-new

(defthm validator-dag-previous-quorum-p-of-accept-next-new
  (implies (and (system-committees-fault-tolerant-p systate)
                (signed-previous-quorum-p systate)
                (same-committees-p systate)
                (accept-possiblep msg systate)
                (messagep msg))
           (validator-dag-previous-quorum-p
                (message->certificate msg)
                (get-validator-state (message->destination msg)
                                     (accept-next msg systate)))))

Theorem: dag-previous-quorum-p-of-accept-next

(defthm dag-previous-quorum-p-of-accept-next
  (implies (and (dag-previous-quorum-p systate)
                (system-committees-fault-tolerant-p systate)
                (signed-previous-quorum-p systate)
                (same-committees-p systate)
                (accept-possiblep msg systate)
                (messagep msg))
           (dag-previous-quorum-p (accept-next msg systate))))

Theorem: validator-dag-previous-quorum-p-of-advance-next

(defthm validator-dag-previous-quorum-p-of-advance-next
  (implies
       (and (validator-dag-previous-quorum-p
                 cert (get-validator-state val1 systate))
            (advance-possiblep val systate))
       (validator-dag-previous-quorum-p
            cert
            (get-validator-state val1 (advance-next val systate)))))

Theorem: dag-previous-quorum-p-of-advance-next

(defthm dag-previous-quorum-p-of-advance-next
  (implies (and (dag-previous-quorum-p systate)
                (advance-possiblep val systate))
           (dag-previous-quorum-p (advance-next val systate))))

Theorem: validator-dag-previous-quorum-p-of-commit-next

(defthm validator-dag-previous-quorum-p-of-commit-next
 (implies
  (and
      (last-blockchain-round-p systate)
      (ordered-blockchain-p systate)
      (signer-quorum-p systate)
      (in val1 (correct-addresses systate))
      (in cert
          (validator-state->dag (get-validator-state val1 systate)))
      (validator-dag-previous-quorum-p
           cert (get-validator-state val1 systate))
      (commit-possiblep val systate)
      (addressp val))
  (validator-dag-previous-quorum-p
       cert
       (get-validator-state val1 (commit-next val systate)))))

Theorem: dag-previous-quorum-p-of-commit-next

(defthm dag-previous-quorum-p-of-commit-next
  (implies (and (dag-previous-quorum-p systate)
                (last-blockchain-round-p systate)
                (ordered-blockchain-p systate)
                (signer-quorum-p systate)
                (commit-possiblep val systate)
                (addressp val))
           (dag-previous-quorum-p (commit-next val systate))))

Theorem: dag-previous-quorum-p-of-event-next

(defthm dag-previous-quorum-p-of-event-next
  (implies (and (dag-previous-quorum-p systate)
                (system-committees-fault-tolerant-p systate)
                (last-blockchain-round-p systate)
                (ordered-blockchain-p systate)
                (signed-previous-quorum-p systate)
                (signer-quorum-p systate)
                (same-committees-p systate)
                (event-possiblep event systate))
           (dag-previous-quorum-p (event-next event systate))))