		Search-engine friendly clone of the ACL2 documentation.

Transitions-advance-round

Advance-round-possiblep

Check if an advance-round 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 conditions for advancing to the next round are different for even and odd rounds.

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.

In an odd round that is not 1 (which is treated specially, see below), 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, i.e. that have edges to that certificate; (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, i.e. that have no edged to that certificate; (4) the timer is expired. Recall that F is introduced in max-faulty-for-total.

For round 1, note that there is no preceding even round, so there is no notion of leader certificate for the preceding round. In this case, there is no leader certificate, and so we always advance.

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 val (correct-addresses systate)))
        nil)
       (vstate (get-validator-state val systate))
       (round (validator-state->round vstate))
       (dag (validator-state->dag vstate))
       (timeout (timer-case (validator-state->timer vstate)
                            :expired))
       (vals (all-addresses systate)))
   (if
    (evenp round)
    (b* ((leader (leader-at-round round vals))
         (anchor? (certificate-with-author+round leader round dag)))
      (or (and anchor? t)
          (and timeout
               (>= (cardinality (certificates-with-round round dag))
                   (quorum systate)))))
    (or
      (equal round 1)
      (b* ((leader (leader-at-round (1- round) vals))
           (anchor? (certificate-with-author+round leader (1- round)
                                                   dag))
           (voters (certificates-with-round round dag))
           ((mv yes-votes no-votes)
            (tally-leader-votes leader voters)))
        (or (not anchor?)
            (>= yes-votes (1+ (max-faulty systate)))
            (>= no-votes (quorum systate))
            timeout)))))))

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-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)