		Search-engine friendly clone of the ACL2 documentation.

Transitions-advance-round

Advance-round-possiblep

Check if a round advancement event is possible.

Signature
(advance-round-possiblep val systate) → yes/no
Arguments: val — Guard (addressp val).; systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

The val input of this function is the address in the advance-round event; see event.

The validator must be a correct one. We only model round advancement in correct validators. Faulty validators have no internal state in our model.

The committee at the current round must be known. Otherwise, we cannot check the appropriate conditions.

There are three cases to consider: round 1, even round, and odd round different from 1. The reason why even and odd rounds differ is that odd rounds vote for the leader at the preceding even round. The reason why round 1 is different from other odd rounds is that there is no round before round 1 and thus no leader to vote.

The following conditions for round advancement are based on our previous model of AleoBFT with static committee, which was in turn based on a probably now outdated snarkOS implementation. We will probably need to revise these conditions, but there is no urgency, because they do not affect the properties that we have proved so far: for those properties, we could simply define that round advancement is always possible.

In round 1, we always allow the round to advance. Note that this may lead to a quick deadlock, if all the validators in the genesis committee advance their round before generating a certificate for round 1, because when they are in round 2 they will never have enough certificates in round 1 to create a certificate for round 2. But again, this does not matter for now. Obviosuly, our model does not require that validators go into deadlock, it merely allows that.

In an even round, we advance if (1) we have the leader certificate (i.e. anchor) at this even round, or (2) the timer is expired and we have a quorum of certificates in this even round. The leader and quorum are calculated over the active committee at the current, even round.

In an odd round different from 1, there are four possible conditions for advancing: (1) there is no leader certificate (i.e. anchor) at the even round that immediately precedes this odd round; (2) there are at least f + 1 certificates at this odd round that vote for the leader certificate at the preceding even round; (3) there are at least n - f certificates at this odd round that do not vote for the leader certificate at the preceding even round; (4) the timer is expired. Recall that f is introduced in max-faulty-for-total. Note that the leader is calculated over the active committee at the previous, even round (which must be known because we have already checked that the active committee at the current, odd round is known), while the votes are calculated over the active committee at the current, odd round.

Note that we instantiate the all-vals parameter of active-committee-at-round with the set of all the addresses of all validators in the system; that is indeed the rols of all-vals, as explained in update-committee-with-transaction.

Definitions and Theorems

Function: advance-round-possiblep

(defun advance-round-possiblep (val systate)
 (declare (xargs :guard (and (addressp val)
                             (system-statep systate))))
 (let ((__function__ 'advance-round-possiblep))
  (declare (ignorable __function__))
  (b*
    (((unless (in (address-fix val)
                  (correct-addresses systate)))
      nil)
     ((validator-state vstate)
      (get-validator-state val systate))
     (commtt
          (active-committee-at-round vstate.round vstate.blockchain
                                     (all-addresses systate)))
     ((unless commtt) nil)
     ((when (= vstate.round 1)) t))
   (if
    (evenp vstate.round)
    (b* ((leader (leader-at-round vstate.round commtt))
         (anchor? (certificate-with-author+round
                       leader vstate.round vstate.dag)))
     (or
      (and anchor? t)
      (and
         (timer-case vstate.timer :expired)
         (>= (cardinality
                  (certificates-with-round vstate.round vstate.dag))
             (committee-quorum commtt)))))
    (b*
      ((prev-commtt
            (active-committee-at-round (1- vstate.round)
                                       vstate.blockchain
                                       (all-addresses systate)))
       (leader (leader-at-round (1- vstate.round)
                                prev-commtt))
       (anchor?
            (certificate-with-author+round leader (1- vstate.round)
                                           vstate.dag))
       (voters (certificates-with-round vstate.round vstate.dag))
       ((mv yes-votes no-votes)
        (tally-leader-votes leader voters)))
      (or (not anchor?)
          (>= yes-votes
              (1+ (committee-max-faulty commtt)))
          (>= no-votes (committee-quorum commtt))
          (timer-case vstate.timer :expired)))))))

Theorem: booleanp-of-advance-round-possiblep

(defthm booleanp-of-advance-round-possiblep
  (b* ((yes/no (advance-round-possiblep val systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: advance-round-possiblep-of-address-fix-val

(defthm advance-round-possiblep-of-address-fix-val
  (equal (advance-round-possiblep (address-fix val)
                                  systate)
         (advance-round-possiblep val systate)))

Theorem: advance-round-possiblep-address-equiv-congruence-on-val

(defthm advance-round-possiblep-address-equiv-congruence-on-val
  (implies (address-equiv val val-equiv)
           (equal (advance-round-possiblep val systate)
                  (advance-round-possiblep val-equiv systate)))
  :rule-classes :congruence)

Theorem: advance-round-possiblep-of-system-state-fix-systate

(defthm advance-round-possiblep-of-system-state-fix-systate
  (equal (advance-round-possiblep val (system-state-fix systate))
         (advance-round-possiblep val systate)))

Theorem: advance-round-possiblep-system-state-equiv-congruence-on-systate

(defthm
   advance-round-possiblep-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (advance-round-possiblep val systate)
                  (advance-round-possiblep val systate-equiv)))
  :rule-classes :congruence)