		Search-engine friendly clone of the ACL2 documentation.

Validator-state

Make-validator-state

Basic constructor macro for validator-state structures.

Syntax

(make-validator-state [:round <round>] 
                      [:dag <dag>] 
                      [:buffer <buffer>] 
                      [:endorsed <endorsed>] 
                      [:last <last>] 
                      [:blockchain <blockchain>] 
                      [:committed <committed>] 
                      [:timer <timer>])

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

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

Definition

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

Macro: make-validator-state

(defmacro make-validator-state (&rest args)
  (std::make-aggregate 'validator-state
                       args
                       '((:round)
                         (:dag)
                         (:buffer)
                         (:endorsed)
                         (:last)
                         (:blockchain)
                         (:committed)
                         (:timer))
                       'make-validator-state
                       nil))

Function: validator-state

(defun validator-state (round dag buffer endorsed
                              last blockchain committed timer)
  (declare (xargs :guard (and (posp round)
                              (certificate-setp dag)
                              (certificate-setp buffer)
                              (address+pos-setp endorsed)
                              (natp last)
                              (block-listp blockchain)
                              (certificate-setp committed)
                              (timerp timer))))
  (declare (xargs :guard t))
  (let ((__function__ 'validator-state))
    (declare (ignorable __function__))
    (b* ((round (mbe :logic (pos-fix round)
                     :exec round))
         (dag (mbe :logic (certificate-set-fix dag)
                   :exec dag))
         (buffer (mbe :logic (certificate-set-fix buffer)
                      :exec buffer))
         (endorsed (mbe :logic (address+pos-set-fix endorsed)
                        :exec endorsed))
         (last (mbe :logic (nfix last) :exec last))
         (blockchain (mbe :logic (block-list-fix blockchain)
                          :exec blockchain))
         (committed (mbe :logic (certificate-set-fix committed)
                         :exec committed))
         (timer (mbe :logic (timer-fix timer)
                     :exec timer)))
      (list (cons 'round round)
            (cons 'dag dag)
            (cons 'buffer buffer)
            (cons 'endorsed endorsed)
            (cons 'last last)
            (cons 'blockchain blockchain)
            (cons 'committed committed)
            (cons 'timer timer)))))