		Search-engine friendly clone of the ACL2 documentation.

Operations-anchors

Anchorp

Check if a certificate is an anchor in a DAG.

Signature
(anchorp anchor dag vals) → yes/no
Arguments: anchor — Guard (certificatep anchor).; dag — Guard (certificate-setp dag).; vals — Guard (address-setp vals).
Returns: yes/no — Type (booleanp yes/no).

Besides the certificate and the DAG, we also pass the set of validator addresses to this predicate. That set is needed to calculate the leader at the round of the certificate, to check whether the address of the certificate is the leader of that round. We also check that the certificate is in the DAG.

This predicate does not require, either in the guard or as a check in the body, that the round is even, although anchors are only at even rounds. So this predicate is perhaps slightly looser than it should be, but it is not wrong, as it can be used for even rounds only as needed.

Definitions and Theorems

Function: anchorp

(defun anchorp (anchor dag vals)
  (declare (xargs :guard (and (certificatep anchor)
                              (certificate-setp dag)
                              (address-setp vals))))
  (declare (xargs :guard (not (emptyp vals))))
  (let ((__function__ 'anchorp))
    (declare (ignorable __function__))
    (and (in anchor dag)
         (evenp (certificate->round anchor))
         (equal (certificate->author anchor)
                (leader-at-round (certificate->round anchor)
                                 vals)))))

Theorem: booleanp-of-anchorp

(defthm booleanp-of-anchorp
  (b* ((yes/no (anchorp anchor dag vals)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: not-anchorp-of-nil

(defthm not-anchorp-of-nil
  (not (anchorp nil dag vals)))

Theorem: anchorp-of-last-anchor

(defthm anchorp-of-last-anchor
  (implies (and (last-anchor vstate vals)
                (evenp (validator-state->last vstate)))
           (anchorp (last-anchor vstate vals)
                    (validator-state->dag vstate)
                    vals)))