		Search-engine friendly clone of the ACL2 documentation.

Transitions-commit-anchors

Commit-anchors-possiblep

Check if a commit-anchors event is possible.

Signature
(commit-anchors-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 commit-anchors 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 validator must be at an odd round that is not 1. Thus, there is a preceding even round, which is the round with possibly the anchor to be committed (possibly along with other previous anchors).

The commit (i.e. even) round must be ahead of the last committed round, otherwise it means that we have already committed the anchor. Note that the last committed round may be 0, in case no anchor has been committed yet.

The anchor must be present in the commit round, i.e. there must be a certificate authored by the leader. To calculate the leader, we need the active committee at the even round.

The current odd round must have sufficient voters with edges to the anchor. Note that we need to use the committee for the current odd round to calculate f + 1 (where f is introduced in max-faulty-for-total.

The committees at both the odd and even round must be known; they may differ or not. Since the odd round is ahead, if the committee is known there, it is also known for the even round, which is smaller. In order for the committee (at odd, and therefore also even, round) to be known, the validator's round must not have advanced further than the lookback amount from the latest block, otherwise the validator is effectively in a deadlocked state, ever unable to extend the blockchain. The latter aspect of AleoBFT may need some further study and analysis, in particular to establish a quantifiably adequate lookback amount.

If all of the above conditions are met, the anchor can be committed, along with possibly some prceding ones, down to, but not including, the one at the last committed round, or all of them is the last committed round is 0.

Note that we instantiate the all-vals parameter of create-certificate-endorser-possiblep 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: commit-anchors-possiblep

(defun commit-anchors-possiblep (val systate)
 (declare (xargs :guard (and (addressp val)
                             (system-statep systate))))
 (let ((__function__ 'commit-anchors-possiblep))
  (declare (ignorable __function__))
  (b*
   (((unless (in (address-fix val)
                 (correct-addresses systate)))
     nil)
    ((validator-state vstate)
     (get-validator-state val systate))
    ((when (evenp vstate.round)) nil)
    ((when (equal vstate.round 1)) nil)
    (vstate.round-commtt
         (active-committee-at-round vstate.round vstate.blockchain
                                    (all-addresses systate)))
    ((unless vstate.round-commtt) nil)
    (commit-round (1- vstate.round))
    ((unless (> commit-round vstate.last))
     nil)
    (commit-round-commtt
         (active-committee-at-round commit-round vstate.blockchain
                                    (all-addresses systate)))
    (leader (leader-at-round commit-round commit-round-commtt))
    (anchor?
     (certificate-with-author+round leader commit-round vstate.dag))
    ((unless anchor?) nil)
    (voters (certificates-with-round vstate.round vstate.dag))
    ((mv yes-votes &)
     (tally-leader-votes leader voters))
    ((unless (>= yes-votes
                 (1+ (committee-max-faulty vstate.round-commtt))))
     nil))
   t)))

Theorem: booleanp-of-commit-anchors-possiblep

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

Theorem: commit-anchors-possiblep-of-address-fix-val

(defthm commit-anchors-possiblep-of-address-fix-val
  (equal (commit-anchors-possiblep (address-fix val)
                                   systate)
         (commit-anchors-possiblep val systate)))

Theorem: commit-anchors-possiblep-address-equiv-congruence-on-val

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

Theorem: commit-anchors-possiblep-of-system-state-fix-systate

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

Theorem: commit-anchors-possiblep-system-state-equiv-congruence-on-systate

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