		Search-engine friendly clone of the ACL2 documentation.

Unequivocal-signed-certificates

Not-signer-record-p-when-create-possiblep

If create-possiblep holds, then signer-record-p is false for its correct signers.

This is a key fact needed to prove our invariant. It says that, in order for a new certificate to be created, its correct signers must have no record of its author and round. This is then used to show that equivocation is not possible for the set of certificates signed by a validator.

This fact follows from the definition of create-possiblep, as well as from another previously proved system invariant.

Consider the author first. For the author, create-possiblep requires that no certificates in the DAG have the author and round of the new certificates. It says nothing endorsed pairs, but an invariant come to the rescue here: no-self-endorsed tells us that the certificate's author's endorsed pairs include no pair whose first component is this validator, and so in particular the pair consisting of this validator plus the certificate's round. All together, these facts tell us that signer-record-p does not hold.

Consider an endorser next. Here create-possiblep directly requires the negation of all the disjunctions of signer-record-p, which therefore is false.

We prove theorems for the predicates that make up create-possiblep, culminating with the one for create-possiblep. In the theorem about create-author-possiblep, we add hypotheses corresponding to part of the body of no-self-endorsed-p, which, in the theorem about create-possiblep, get discharged via the -necc rule of the invariant.

Definitions and Theorems

Theorem: not-signer-record-p-when-create-author-possiblep

(defthm not-signer-record-p-when-create-author-possiblep
  (implies (and (create-author-possiblep cert vstate)
                (equal (address+pos-pairs-with-address
                            (certificate->author cert)
                            (validator-state->endorsed vstate))
                       nil))
           (not (signer-record-p (certificate->author cert)
                                 (certificate->round cert)
                                 vstate))))

Theorem: not-signer-record-p-when-create-endorser-possiblep

(defthm not-signer-record-p-when-create-endorser-possiblep
  (implies (create-endorser-possiblep cert vstate)
           (not (signer-record-p (certificate->author cert)
                                 (certificate->round cert)
                                 vstate))))

Theorem: not-signer-record-p-when-create-endorsers-possiblep-loop

(defthm not-signer-record-p-when-create-endorsers-possiblep-loop
 (implies
    (and (create-endorsers-possiblep-loop cert endorsers systate)
         (in endorser endorsers)
         (in endorser (correct-addresses systate)))
    (not (signer-record-p (certificate->author cert)
                          (certificate->round cert)
                          (get-validator-state endorser systate)))))

Theorem: not-signer-record-p-when-create-endorsers-possiblep

(defthm not-signer-record-p-when-create-endorsers-possiblep
 (implies
    (and (create-endorsers-possiblep cert systate)
         (in endorser (certificate->endorsers cert))
         (in endorser (correct-addresses systate)))
    (not (signer-record-p (certificate->author cert)
                          (certificate->round cert)
                          (get-validator-state endorser systate)))))

Theorem: not-signer-record-p-when-create-possiblep

(defthm not-signer-record-p-when-create-possiblep
 (implies
      (and (create-possiblep cert systate)
           (in signer (certificate->signers cert))
           (in signer (correct-addresses systate))
           (no-self-endorsed-p systate))
      (not (signer-record-p (certificate->author cert)
                            (certificate->round cert)
                            (get-validator-state signer systate)))))