		Search-engine friendly clone of the ACL2 documentation.

Transitions-advance

Advance-possiblep

Check if a round advancement event is possible.

Signature
(advance-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 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 models of AleoBFT with static and dynamic committees without stake, 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 of interest in the short term: 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 at least a quorum of certificates in this even round. The leader and quorum are calculated over the active committee at the current, even round. The check that the authors of the certificates in this even round are all members of the active committee at that round is an invariant, proved elsewhere; but that invariant is not available here, so we add an explicit check, which turns out to be superfluous under that invariant.

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 is more than f stake of the authors of the 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. The check that the voters, i.e. the authors of the certificates in this odd round, are all members of the active committee at that round is an invariant, proved elsewhere; but that invariant is not available here, so we add an explicit check, which turns out to be superfluous under that invariant.

Above we say `more than f', which is equivalent to `at least f+1. The latter is more common when talking about numbers of validators, because it often is exactly f+1, but with stake it seems cleaner to talk about f, since generally stake does not align exactly that way.

To satisfy the guard of leader-at-round, we check that the committee at the even round is not empty. If it is empty, there is no leader, and no leader certificate; it is similar to the case in which there is a leader but no leader certificate.

Definitions and Theorems

Function: advance-possiblep

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

Theorem: booleanp-of-advance-possiblep

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

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

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

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

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

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

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

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

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