		Search-engine friendly clone of the ACL2 documentation.

Dags

Path-to-author+round

Retrieve the certificate with the given author and round reachable from a given certificate through the DAG edges.

Signature
(path-to-author+round cert author round dag) → previous-cert?
Arguments: cert — Guard (certificatep cert).; author — Guard (addressp author).; round — Guard (posp round).; dag — Guard (certificate-setp dag).
Returns: previous-cert? — Type (certificate-optionp previous-cert?).

If the certificate is found, it is returned. Otherwise, nil is returned.

The guard requires the target round to be no later than the round of the current certificate. Otherwise, there could be no path, since paths never go forward (i.e. from smaller to larger rounds).

If the target round is the same as the one of the current cerfificate, we are looking for an empty path in the DAG; this is the base case of the recursion. In order for an empty path to exist, the target certificate must be the current certificate: that is, the author of the certificate must be the target one. If that is the case, we return the current certificate. If the author differs, we return nil: there is no (empty) path.

Otherwise, we must look for a non-empty path. We take all the certificates from the previous round to which the current certificate has a path of length 1, i.e. the previous certificates that the current certificate references. Every path from the current certificate must go through at least one of these previous certificates. We try and find a path from each of these certificates to the target round and author, recursively. We use a mutually recursive companion function to loop through the elements of the set of previous certificates.

The mutually recursive function terminates when the set is empty: no path has been found in this case. If the set is not empty, it first tries to find a path from the minimal (head) element of the set, using the mutually recursive companion (the main function). If that fails, it recursively tries the rest of the set.

The termination proof for these two mutually recursive functions takes a little bit of guidance from the user. We use lexicographic measures, as follows. When the main function calls the one on the set, the round number of the certificates in the set is less than the one in the initial certificate; the round numbers are all the same in fact, but we use a function that returns their maximum, which is more flexible (requiring fewer constraints to be considered) and suffices to prove termination. When the function on the set calls the main function, the round number does not change, but we just say, in the measures, that the main function is ``smaller'' than the one on the set, by using the numbers 1 and 0 as the second components of the measures. Finally, for the call of the function on the set to itself, the set gets smaller, and so we use the cardinality of the set as the third component of the measure; this does not apply to the main function, but we need the measure lists to have the same length (otherwise the shorter list would be always less than the longer list), and so we just use 0 there.

This function is executable, although it is not particularly efficient. But its main purpose is to be a clear specification, for which things can be proved conveniently.

Theorem: return-type-of-path-to-author+round.previous-cert?

(defthm return-type-of-path-to-author+round.previous-cert?
  (b*
    ((?previous-cert? (path-to-author+round cert author round dag)))
    (certificate-optionp previous-cert?))
  :rule-classes :rewrite)

Theorem: return-type-of-path-to-author+round-set.previous-cert?

(defthm return-type-of-path-to-author+round-set.previous-cert?
  (b* ((?previous-cert?
            (path-to-author+round-set certs author round dag)))
    (certificate-optionp previous-cert?))
  :rule-classes :rewrite)

Theorem: certificate->author-of-path-to-author+round

(defthm certificate->author-of-path-to-author+round
  (b*
    ((?previous-cert? (path-to-author+round cert author round dag)))
    (implies previous-cert?
             (equal (certificate->author previous-cert?)
                    (address-fix author)))))

Theorem: certificate->author-of-path-to-author+round-set

(defthm certificate->author-of-path-to-author+round-set
  (b* ((?previous-cert?
            (path-to-author+round-set certs author round dag)))
    (implies previous-cert?
             (equal (certificate->author previous-cert?)
                    (address-fix author)))))

Theorem: certificate->round-of-path-to-author+round

(defthm certificate->round-of-path-to-author+round
  (b*
    ((?previous-cert? (path-to-author+round cert author round dag)))
    (implies previous-cert?
             (equal (certificate->round previous-cert?)
                    (pos-fix round)))))

Theorem: certificate->round-of-path-to-author+round-set

(defthm certificate->round-of-path-to-author+round-set
  (b* ((?previous-cert?
            (path-to-author+round-set certs author round dag)))
    (implies previous-cert?
             (equal (certificate->round previous-cert?)
                    (pos-fix round)))))

Theorem: path-to-author+round-in-dag

(defthm path-to-author+round-in-dag
 (implies
   (and (certificate-setp dag)
        (in cert dag))
   (b*
    ((?previous-cert? (path-to-author+round cert author round dag)))
    (implies previous-cert?
             (in previous-cert? dag)))))

Theorem: path-to-author+round-set-in-dag

(defthm path-to-author+round-set-in-dag
  (implies
       (and (certificate-setp dag)
            (subset certs dag))
       (b* ((?previous-cert?
                 (path-to-author+round-set certs author round dag)))
         (implies previous-cert?
                  (in previous-cert? dag)))))

Theorem: round-leq-when-path-to-author+round

(defthm round-leq-when-path-to-author+round
  (b*
    ((?previous-cert? (path-to-author+round cert author round dag)))
    (implies previous-cert?
             (<= round (certificate->round cert))))
  :rule-classes :linear)

Theorem: round-leq-when-path-to-author+round-set

(defthm round-leq-when-path-to-author+round-set
  (b* ((?previous-cert?
            (path-to-author+round-set certs author round dag)))
    (implies previous-cert?
             (<= round
                 (pos-set-max (certificate-set->round-set certs)))))
  :rule-classes :linear)

Theorem: path-to-author+round-of-self

(defthm path-to-author+round-of-self
  (implies
       (and (certificate-setp dag)
            (in cert dag))
       (equal (path-to-author+round cert (certificate->author cert)
                                    (certificate->round cert)
                                    dag)
              cert)))

Theorem: path-to-author+round-set-when-path-to-author+round-of-element

(defthm
      path-to-author+round-set-when-path-to-author+round-of-element
  (implies (and (in cert certs)
                (path-to-author+round cert author round dag))
           (path-to-author+round-set certs author round dag)))

Subtopics

Path-to-author+round-set