		Search-engine friendly clone of the ACL2 documentation.

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

Dag-previous-quorum-p

Definition of the invariant: for each certificate in the DAG of each validator, either the certificate's round is 1 and the certificate has no references to previous certificates, or the certificate's round is not 1 and the references to previous certificates form a non-zero quorum in the committee of the preceding round of the certificate.

This invariant, along with backward closure and non-equivocation, guarantees that dag-predecessor-quorum-p holds, as we prove here. The key lemma is predecessor-quorum-when-validator-dag-previous-quorum-p proved in validator-dag-previous-quorum-p. Here we just need to enable some rules to establish the hypotheses of that lemma.

Definitions and Theorems

Theorem: dag-previous-quorum-p-necc

(defthm dag-previous-quorum-p-necc
 (implies
  (dag-previous-quorum-p systate)
  (implies
   (and
      (in val (correct-addresses systate))
      (in cert
          (validator-state->dag (get-validator-state val systate))))
   (validator-dag-previous-quorum-p
        cert
        (get-validator-state val systate)))))

Theorem: booleanp-of-dag-previous-quorum-p

(defthm booleanp-of-dag-previous-quorum-p
  (b* ((yes/no (dag-previous-quorum-p systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: dag-previous-quorum-p-of-system-state-fix-systate

(defthm dag-previous-quorum-p-of-system-state-fix-systate
  (equal (dag-previous-quorum-p (system-state-fix systate))
         (dag-previous-quorum-p systate)))

Theorem: dag-previous-quorum-p-system-state-equiv-congruence-on-systate

(defthm
     dag-previous-quorum-p-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (dag-previous-quorum-p systate)
                  (dag-previous-quorum-p systate-equiv)))
  :rule-classes :congruence)

Theorem: dag-predecessor-quorum-p-when-dag-previous-quorum-p

(defthm dag-predecessor-quorum-p-when-dag-previous-quorum-p
  (implies
       (and (dag-previous-quorum-p systate)
            (backward-closed-p systate)
            (in val (correct-addresses systate)))
       (dag-predecessor-quorum-p
            (validator-state->dag (get-validator-state val systate))
            (validator-state->blockchain
                 (get-validator-state val systate)))))