		Search-engine friendly clone of the ACL2 documentation.

Initialization

System-initp

Check if a system state is an initial one.

Signature
(system-initp systate) → yes/no
Arguments: systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

Every correct validator must be in the initial state, and the genesis committee must be a subset of all the validators. Note that a committee may include correct and faulty validators.

Furthermore, the network is initially empty.

Definitions and Theorems

Function: system-initp

(defun system-initp (systate)
  (declare (xargs :guard (system-statep systate)))
  (let ((__function__ 'system-initp))
    (declare (ignorable __function__))
    (and (system-validators-initp systate)
         (subset (committee-members (genesis-committee))
                 (all-addresses systate))
         (emptyp (get-network-state systate)))))

Theorem: booleanp-of-system-initp

(defthm booleanp-of-system-initp
  (b* ((yes/no (system-initp systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: system-initp-of-system-state-fix-systate

(defthm system-initp-of-system-state-fix-systate
  (equal (system-initp (system-state-fix systate))
         (system-initp systate)))

Theorem: system-initp-system-state-equiv-congruence-on-systate

(defthm system-initp-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (system-initp systate)
                  (system-initp systate-equiv)))
  :rule-classes :congruence)