		Search-engine friendly clone of the ACL2 documentation.

Signer-records

Signer-records-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 event adds a new certificate to the set of certificates signed by each signer of the certificate. We prove a theorem saying that the author and round of the new certificate satisfy the invariant, which follows from the definition of the creation of the certificate, which adds the certificate to the author's DAG and the author-round pair to the endorsers' endorser sets. We prove another theorem saying that the old recorded certificates are still recorded in the new states, because there is no other change for those w.r.t. their records. Then we prove a theorem showing the preservation of the system invariant on all certificates after create, via the two aforementioned theorems for new and old certificates.

For all other kinds of events, we prove two theorems: one is for each generic validator, and one is for the whole system.

An accept event may remove an endorsed pair, but it also adds the certificate, whose author and round are the ones of the removed pair, to the buffer. So the invariant is preserved for that certificate. For the other certificates, the invariant is also preserved because nothing changes for them in terms of their records.

For the other kinds of events, nothing changes for any certificate in terms of its records.

Definitions and Theorems

Theorem: signer-record-p-of-create-next-new

(defthm signer-record-p-of-create-next-new
 (implies
     (and (in signer (certificate->signers cert))
          (in signer (correct-addresses systate)))
     (signer-record-p
          (certificate->author cert)
          (certificate->round cert)
          (get-validator-state signer (create-next cert systate)))))

Theorem: signer-record-p-of-create-next-old

(defthm signer-record-p-of-create-next-old
 (implies
     (and (in signer (correct-addresses systate))
          (signer-record-p (certificate->author cert1)
                           (certificate->round cert1)
                           (get-validator-state signer systate)))
     (signer-record-p
          (certificate->author cert1)
          (certificate->round cert1)
          (get-validator-state signer (create-next cert systate)))))

Theorem: signer-records-p-of-create-next

(defthm signer-records-p-of-create-next
  (implies (signer-records-p systate)
           (signer-records-p (create-next cert systate))))

Theorem: signer-record-p-of-accept-next

(defthm signer-record-p-of-accept-next
 (implies
      (and (in signer (correct-addresses systate))
           (signer-record-p (certificate->author cert)
                            (certificate->round cert)
                            (get-validator-state signer systate))
           (accept-possiblep msg systate))
      (signer-record-p
           (certificate->author cert)
           (certificate->round cert)
           (get-validator-state signer (accept-next msg systate)))))

Theorem: signer-records-p-of-accept-next

(defthm signer-records-p-of-accept-next
  (implies (and (signer-records-p systate)
                (accept-possiblep msg systate))
           (signer-records-p (accept-next msg systate))))

Theorem: signer-record-p-of-advance-next

(defthm signer-record-p-of-advance-next
 (implies
     (and (in signer (correct-addresses systate))
          (signer-record-p (certificate->author cert)
                           (certificate->round cert)
                           (get-validator-state signer systate))
          (advance-possiblep val systate))
     (signer-record-p
          (certificate->author cert)
          (certificate->round cert)
          (get-validator-state signer (advance-next val systate)))))

Theorem: signer-records-p-of-advance-next

(defthm signer-records-p-of-advance-next
  (implies (and (signer-records-p systate)
                (advance-possiblep val systate))
           (signer-records-p (advance-next val systate))))

Theorem: signer-record-p-of-commit-next

(defthm signer-record-p-of-commit-next
 (implies
      (and (in signer (correct-addresses systate))
           (signer-record-p (certificate->author cert)
                            (certificate->round cert)
                            (get-validator-state signer systate))
           (commit-possiblep val systate))
      (signer-record-p
           (certificate->author cert)
           (certificate->round cert)
           (get-validator-state signer (commit-next val systate)))))

Theorem: signer-records-p-of-commit-next

(defthm signer-records-p-of-commit-next
  (implies (and (signer-records-p systate)
                (commit-possiblep val systate))
           (signer-records-p (commit-next val systate))))

Theorem: signer-records-p-of-event-next

(defthm signer-records-p-of-event-next
  (implies (and (signer-records-p systate)
                (event-possiblep event systate))
           (signer-records-p (event-next event systate))))