		Search-engine friendly clone of the ACL2 documentation.

Certificate

Make-certificate

Basic constructor macro for certificate structures.

Syntax

(make-certificate [:proposal <proposal>] 
                  [: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 '((:proposal) (:endorsers))
                       'make-certificate
                       nil))

Function: certificate

(defun certificate (proposal endorsers)
  (declare (xargs :guard (and (proposalp proposal)
                              (address-setp endorsers))))
  (declare (xargs :guard t))
  (let ((__function__ 'certificate))
    (declare (ignorable __function__))
    (b* ((proposal (mbe :logic (proposal-fix proposal)
                        :exec proposal))
         (endorsers (mbe :logic (address-set-fix endorsers)
                         :exec endorsers)))
      (list (cons 'proposal proposal)
            (cons 'endorsers endorsers)))))