		Search-engine friendly clone of the ACL2 documentation.

Transitions-propose

Propose-possiblep

Check if a propose event is possible in a system state.

Signature
(propose-possiblep prop dests systate) → yes/no
Arguments: prop — Guard (proposalp prop).; dests — Guard (address-setp dests).; systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

The prop and dests parameters of this function are the corresponding components of the propose event.

The author of the proposal identifies the validator that creates the proposal. Since signatures of correct validators cannot be forged, a faulty validator cannot impersonate a correct one, and thus the fact that the proposal's author is a correct validator means that the proposal is indeed created by that validator. If the author of the proposal is faulty, it does not matter whether the proposal actually originates from that validator, or instead it originates from some other (faulty) validator impersonating the author; the correctness of the protocol does not not depend on that. If the author of the proposal is a faulty validator, there are almost no other requirements: nothing prevents a faulty validator from generating a proposal with arbitrary round, transactions, and previous certificate addresses.

The `almost' above refers to the fact that we constrain faulty validators to send a proposal to at least one validator. This is merely a modeling convenience, not a real restriction: if a faulty validator creates a proposal and sends it to nobody, the event would cause no actual change to our modeled system state, because faulty validators have no external state. If there is at least one destination for the proposal, then there is a state change, consisting of at least one message being added to the network.

If the proposal's author is correct, the following conditions apply; that is, the event can happen only if these conditions are satisfied:

The round of the proposal must match the round of the validator. A correct validator always generates proposals for the current round.
The author must be in the active committee for that round. This means that the author must be able to calculate that committee.
The validator must not have already created another proposal with the same round, because that would cause equivocation. Not only the DAG must include no certificate with that author and round, but also the pending proposals must not include a proposal with that round (as proved elsewhere, it is an invariant that all the pending proposals are authored by the validator, so there is no need to check the author).
The certificates referenced in the previous component must be present in the DAG, and their authors must form a non-empty quorum in the active committee for the round just before the current one (which, as noted above, is the same as the proposal); note that the validator can always calculate this committee, if it can calculate the one for the current round, as mentioned above. This condition only applies if the round is not 1; if the round is 1, the previous component must be empty.

For the case of a round that is not 1, we use committee-validators-stake for the quorum test; we do not check that the previous certificate authors are in fact members of the committee at the previous round. As proved elsewhere, it is an invariant that those authors are indeed members of the committee; so the check can be safely skipped.

Note that above we say `non-empty quorum', not just `quorum'. The two are equivalent only if the committee (at the previous round) is not empty. Our model allows committees to become empty, but this non-emptiness check of the previous quorum enforces, in the protocol, that committees do not actually become empty. If they do, the protocol effectively stops; correct validators cannot create new certificates.

A correct validator broadcasts the proposal to all the other validators in the active committee, which it calculates as already mentioned above. These may include both correct and faulty validators: the proposal author cannot distinguish them. Additionally, we allow additional messages to other faulty validators, for the modeling reason described in transitions-propose.

A faulty validator may send the proposal to any set of validators, correct or faulty, whether part of (any) committees or not.

Note that we do not model any form of reliable broadcast here. For the purpose of properties like blockchain nonforking, it does not matter there there is any form of reliable broadcast; however, it matters for other kinds of properties, so we plan to refine our model when studying those other properties.

Definitions and Theorems

Function: propose-possiblep

(defun propose-possiblep (prop dests systate)
 (declare (xargs :guard (and (proposalp prop)
                             (address-setp dests)
                             (system-statep systate))))
 (let ((__function__ 'propose-possiblep))
  (declare (ignorable __function__))
  (b*
   (((proposal prop) prop)
    ((when (not (in prop.author
                    (correct-addresses systate))))
     (not (emptyp (address-set-fix dests))))
    ((validator-state vstate)
     (get-validator-state prop.author systate))
    ((unless (= prop.round vstate.round))
     nil)
    (commtt
         (active-committee-at-round prop.round vstate.blockchain))
    ((unless commtt) nil)
    ((unless (in prop.author (committee-members commtt)))
     nil)
    ((unless (subset (delete prop.author (committee-members commtt))
                     (address-set-fix dests)))
     nil)
    ((when (in prop.author (address-set-fix dests)))
     nil)
    ((unless (subset (intersect (address-set-fix dests)
                                (correct-addresses systate))
                     (committee-members commtt)))
     nil)
    ((unless
      (emptyp
       (certs-with-author+round prop.author prop.round vstate.dag)))
     nil)
    ((unless
          (emptyp (props-with-round prop.round
                                    (omap::keys vstate.proposed))))
     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-propose-possiblep

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

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

(defthm propose-possiblep-of-proposal-fix-prop
  (equal (propose-possiblep (proposal-fix prop)
                            dests systate)
         (propose-possiblep prop dests systate)))

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

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

Theorem: propose-possiblep-of-address-set-fix-dests

(defthm propose-possiblep-of-address-set-fix-dests
  (equal (propose-possiblep prop (address-set-fix dests)
                            systate)
         (propose-possiblep prop dests systate)))

Theorem: propose-possiblep-address-set-equiv-congruence-on-dests

(defthm propose-possiblep-address-set-equiv-congruence-on-dests
  (implies (address-set-equiv dests dests-equiv)
           (equal (propose-possiblep prop dests systate)
                  (propose-possiblep prop dests-equiv systate)))
  :rule-classes :congruence)

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

(defthm propose-possiblep-of-system-state-fix-systate
  (equal (propose-possiblep prop dests (system-state-fix systate))
         (propose-possiblep prop dests systate)))

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

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