		Search-engine friendly clone of the ACL2 documentation.

Certificate

Make-certificate

Basic constructor macro for certificate structures.

Syntax

(make-certificate [:author <author>] 
                  [:round <round>] 
                  [:transactions <transactions>] 
                  [:previous <previous>] 
                  [:endorsers <endorsers>])

This is the usual way to construct certificate structures. It simply conses together a structure with the specified fields.

This macro generates a new certificate structure from scratch. See also change-certificate, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-certificate

(defmacro make-certificate (&rest args)
  (std::make-aggregate 'certificate
                       args
                       '((:author)
                         (:round)
                         (:transactions)
                         (:previous)
                         (:endorsers))
                       'make-certificate
                       nil))

Function: certificate

(defun certificate (author round transactions previous endorsers)
 (declare (xargs :guard (and (addressp author)
                             (posp round)
                             (transaction-listp transactions)
                             (address-setp previous)
                             (address-setp endorsers))))
 (declare (xargs :guard t))
 (let ((__function__ 'certificate))
  (declare (ignorable __function__))
  (b* ((author (mbe :logic (address-fix author)
                    :exec author))
       (round (mbe :logic (pos-fix round)
                   :exec round))
       (transactions (mbe :logic (transaction-list-fix transactions)
                          :exec transactions))
       (previous (mbe :logic (address-set-fix previous)
                      :exec previous))
       (endorsers (mbe :logic (address-set-fix endorsers)
                       :exec endorsers)))
    (list (cons 'author author)
          (cons 'round round)
          (cons 'transactions transactions)
          (cons 'previous previous)
          (cons 'endorsers endorsers)))))