		Search-engine friendly clone of the ACL2 documentation.

Fault-tolerance

All-system-committees-fault-tolerant-p

Check if all the system states in an execution from a system state via a sequence of events are fault-tolerant.

Signature
(all-system-committees-fault-tolerant-p systate events) → yes/no
Arguments: systate — Guard (system-statep systate).; events — Guard (event-listp events).
Returns: yes/no — Type (booleanp yes/no).

When talking about properties of executions, i.e. sequences of states from a starting state through a serie of states that result from a sequence of events, we need to make the hypothesis that all the committees along the way are fault-tolerant. This predicate expresses that: systate is the starting state, and events are the events that take the system through a sequence of states from the starting state.

For this predicate to hold, first the starting state must be fault-tolerant. If there are no events, there is no other requirement. Otherwise, we execute the event and we recursively call this predicate with the resulting state: this covers all the states in the execution.

We show that this predicate holds if the final state is fault-tolerant and the initial state satisfies two invariants about blockchain rounds.

Definitions and Theorems

Function: all-system-committees-fault-tolerant-p

(defun all-system-committees-fault-tolerant-p (systate events)
  (declare (xargs :guard (and (system-statep systate)
                              (event-listp events))))
  (declare (xargs :guard (events-possiblep events systate)))
  (let ((__function__ 'all-system-committees-fault-tolerant-p))
    (declare (ignorable __function__))
    (b* (((unless (system-committees-fault-tolerant-p systate))
          nil)
         ((when (endp events)) t))
      (all-system-committees-fault-tolerant-p
           (event-next (car events) systate)
           (cdr events)))))

Theorem: booleanp-of-all-system-committees-fault-tolerant-p

(defthm booleanp-of-all-system-committees-fault-tolerant-p
 (b*
  ((yes/no (all-system-committees-fault-tolerant-p systate events)))
  (booleanp yes/no))
 :rule-classes :rewrite)

Theorem: all-system-committees-fault-tolerant-p-when-final

(defthm all-system-committees-fault-tolerant-p-when-final
 (implies
  (and (last-blockchain-round-p systate)
       (ordered-blockchain-p systate)
       (events-possiblep events systate))
  (b* ((new-systate (events-next events systate)))
    (implies
         (system-committees-fault-tolerant-p new-systate)
         (all-system-committees-fault-tolerant-p systate events)))))

Theorem: all-system-committees-fault-tolerant-p-of-system-state-fix-systate

(defthm
 all-system-committees-fault-tolerant-p-of-system-state-fix-systate
 (equal
  (all-system-committees-fault-tolerant-p (system-state-fix systate)
                                          events)
  (all-system-committees-fault-tolerant-p systate events)))

Theorem: all-system-committees-fault-tolerant-p-system-state-equiv-congruence-on-systate

(defthm
 all-system-committees-fault-tolerant-p-system-state-equiv-congruence-on-systate
 (implies
  (system-state-equiv systate systate-equiv)
  (equal
     (all-system-committees-fault-tolerant-p systate events)
     (all-system-committees-fault-tolerant-p systate-equiv events)))
 :rule-classes :congruence)

Theorem: all-system-committees-fault-tolerant-p-of-event-list-fix-events

(defthm
    all-system-committees-fault-tolerant-p-of-event-list-fix-events
  (equal (all-system-committees-fault-tolerant-p
              systate (event-list-fix events))
         (all-system-committees-fault-tolerant-p systate events)))

Theorem: all-system-committees-fault-tolerant-p-event-list-equiv-congruence-on-events

(defthm
 all-system-committees-fault-tolerant-p-event-list-equiv-congruence-on-events
 (implies
  (event-list-equiv events events-equiv)
  (equal
     (all-system-committees-fault-tolerant-p systate events)
     (all-system-committees-fault-tolerant-p systate events-equiv)))
 :rule-classes :congruence)