		Search-engine friendly clone of the ACL2 documentation.

Initialization

Validator-init

Initial (correct) validator state.

Signature
(validator-init) → vstate
Returns: vstate — Type (validator-statep vstate).

Initially, each correct validator is in round 1, has empty DAG and buffer, has no record of endorsed certificates, has 0 as last committed round (meaning that no anchors have been committed yet, since 0 is not a valid round number), has an empty blockchain, has no committed certificates, and the timer is expired (i.e. not running).

Definitions and Theorems

Function: validator-init

(defun validator-init nil
  (declare (xargs :guard t))
  (let ((__function__ 'validator-init))
    (declare (ignorable __function__))
    (make-validator-state :round 1
                          :dag nil
                          :buffer nil
                          :endorsed nil
                          :last 0
                          :blockchain nil
                          :committed nil
                          :timer (timer-expired))))

Theorem: validator-statep-of-validator-init

(defthm validator-statep-of-validator-init
  (b* ((vstate (validator-init)))
    (validator-statep vstate))
  :rule-classes :rewrite)