		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 validator must be at an odd round that is not 1. Thus, there is a preceding non-zero even round, which is the round with possibly the anchor to be committed (possibly along with previous anchors). The commit round must be ahead of the last committed round, otherwise it means that we have already committed the anchor. The anchor must be present in the commit round, i.e. there must be a certificate authored by the leader. Furthermore, the current odd round must have sufficient voters with edges to the anchor. If all of these 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; the committing is specified in commit-anchors-next.

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 val (correct-addresses systate)))
        nil)
       (vstate (get-validator-state val systate))
       (current-round (validator-state->round vstate))
       ((when (evenp current-round)) nil)
       ((when (equal current-round 1)) nil)
       (commit-round (1- current-round))
       (last-committed-round (validator-state->last vstate))
       ((unless (> commit-round last-committed-round))
        nil)
       (vals (all-addresses systate))
       (leader (leader-at-round commit-round vals))
       (dag (validator-state->dag vstate))
       (anchor?
            (certificate-with-author+round leader commit-round dag))
       ((unless anchor?) nil)
       (voters (certificates-with-round current-round dag))
       ((mv yes-votes &)
        (tally-leader-votes leader voters))
       ((unless (>= yes-votes (1+ (max-faulty systate))))
        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-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)