		Search-engine friendly clone of the ACL2 documentation.

Transitions-endorse

Endorse-possiblep

Check if an endorse event is possible in a system state.

Signature
(endorse-possiblep prop endor systate) → yes/no
Arguments: prop — Guard (proposalp prop).; endor — Guard (addressp endor).; systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

The prop and endor parameters of this function are the corresponding components of the endorse event.

For the event to occur, the network must contain a proposal message that consists of the proposal and the endorser as destination: that is, the proposal must be addressed to the endorser. The message is isomorphic to the event, in fact.

If the endorser is faulty, there is no further condition. If the faulty validators decided not to endorse the proposal instead, that would be a non-event, i.e. it would not be represented by this event: an endorse event captures the case in which the validator actually endorses the proposal. We could also add an event to model the situation in which a faulty validator consumes the proposal message, but does not send back an endorsement; however, the only difference is that, in our current model, the proposal message may sit in the network forever, which can be just ignored.

If the endorser is correct, the following conditions must hold:

The proposal author and the endorser must be both in the active committee at the proposal round, which the endorser must be thus able to calculate.
The endorser must have no certificate, in the DAG, with the same author and round as the proposal.
The endorser must not have already endorsed a proposal with the same author and round as the proposal to endorse. This is looked up in the component of the validator state that keeps track of the proposals endorsed so far, whose corresponding certificates are not in the validator's DAG yet.
If the proposal's round number is 1, the proposal must have no references to previous certificates. Otherwise, all the referenced certificates must be in the DAG, and their authors must form a non-empty quorum.

Some of these conditions are the same as in propose-possiblep. This is unsurprising, because (correct) authors and endorsers must perform similar checks.

Note that, as in propose-possiblep, the endorser does not check that the authors of the previous certificates are members of the active committee at the previous round. The reason is that this is an invariant, so it can be safely skipped. Indeed, we use committee-validators-stake to check the quorum the condition.

The same observation about (non-)empty committees applies here, which is made in the documentation of propose-possiblep.

Definitions and Theorems

Function: endorse-possiblep

(defun endorse-possiblep (prop endor systate)
 (declare (xargs :guard (and (proposalp prop)
                             (addressp endor)
                             (system-statep systate))))
 (let ((__function__ 'endorse-possiblep))
  (declare (ignorable __function__))
  (b*
   ((msg (make-message-proposal :proposal prop
                                :destination endor))
    ((unless (in msg (get-network-state systate)))
     nil)
    ((unless (in (address-fix endor)
                 (correct-addresses systate)))
     t)
    ((proposal prop) prop)
    ((validator-state vstate)
     (get-validator-state endor systate))
    (commtt
         (active-committee-at-round prop.round vstate.blockchain))
    ((unless commtt) nil)
    ((unless (in prop.author (committee-members commtt)))
     nil)
    ((unless (in (address-fix endor)
                 (committee-members commtt)))
     nil)
    ((unless
      (emptyp
       (certs-with-author+round prop.author prop.round vstate.dag)))
     nil)
    ((unless
      (emptyp (props-with-author+round prop.author
                                       prop.round vstate.endorsed)))
     nil)
    ((when (= prop.round 1))
     (emptyp prop.previous))
    ((when (emptyp prop.previous)) nil)
    ((unless
        (subset
             prop.previous
             (cert-set->author-set (certs-with-round (1- prop.round)
                                                     vstate.dag))))
     nil)
    (prev-commtt (active-committee-at-round (1- prop.round)
                                            vstate.blockchain))
    ((unless
          (>= (committee-validators-stake prop.previous prev-commtt)
              (committee-quorum-stake prev-commtt)))
     nil))
   t)))

Theorem: booleanp-of-endorse-possiblep

(defthm booleanp-of-endorse-possiblep
  (b* ((yes/no (endorse-possiblep prop endor systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: endorse-possiblep-of-proposal-fix-prop

(defthm endorse-possiblep-of-proposal-fix-prop
  (equal (endorse-possiblep (proposal-fix prop)
                            endor systate)
         (endorse-possiblep prop endor systate)))

Theorem: endorse-possiblep-proposal-equiv-congruence-on-prop

(defthm endorse-possiblep-proposal-equiv-congruence-on-prop
  (implies (proposal-equiv prop prop-equiv)
           (equal (endorse-possiblep prop endor systate)
                  (endorse-possiblep prop-equiv endor systate)))
  :rule-classes :congruence)

Theorem: endorse-possiblep-of-address-fix-endor

(defthm endorse-possiblep-of-address-fix-endor
  (equal (endorse-possiblep prop (address-fix endor)
                            systate)
         (endorse-possiblep prop endor systate)))

Theorem: endorse-possiblep-address-equiv-congruence-on-endor

(defthm endorse-possiblep-address-equiv-congruence-on-endor
  (implies (address-equiv endor endor-equiv)
           (equal (endorse-possiblep prop endor systate)
                  (endorse-possiblep prop endor-equiv systate)))
  :rule-classes :congruence)

Theorem: endorse-possiblep-of-system-state-fix-systate

(defthm endorse-possiblep-of-system-state-fix-systate
  (equal (endorse-possiblep prop endor (system-state-fix systate))
         (endorse-possiblep prop endor systate)))

Theorem: endorse-possiblep-system-state-equiv-congruence-on-systate

(defthm endorse-possiblep-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (endorse-possiblep prop endor systate)
                  (endorse-possiblep prop endor systate-equiv)))
  :rule-classes :congruence)