		Search-engine friendly clone of the ACL2 documentation.

Transitions-augment

Augment-possiblep

Check if an augment event is possible in a system state.

Signature
(augment-possiblep prop endor systate) → yes/no
Arguments: prop — Guard (proposalp prop).; endor — Guard (addressp endor).; systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

The prop and endor parameters of this function are the corresponding components of the augment event.

The validator affected by this event is the author of the proposal, which must be correct in order for this event to happen, as explained in transitions-augment.

This event occurs when the network contains an endorsement message consisting of the proposal and the endorser (which is thus isomorphic to the event).

The validator must have that proposal pending, in its finite map from proposals to endorsing addresses.

Definitions and Theorems

Function: augment-possiblep

(defun augment-possiblep (prop endor systate)
  (declare (xargs :guard (and (proposalp prop)
                              (addressp endor)
                              (system-statep systate))))
  (let ((__function__ 'augment-possiblep))
    (declare (ignorable __function__))
    (b* (((proposal prop) prop)
         ((unless (in prop.author
                      (correct-addresses systate)))
          nil)
         (msg (make-message-endorsement :proposal prop
                                        :endorser endor))
         ((unless (in msg (get-network-state systate)))
          nil)
         ((validator-state vstate)
          (get-validator-state prop.author systate))
         (prop+endors (omap::assoc (proposal-fix prop)
                                   vstate.proposed))
         ((unless prop+endors) nil))
      t)))

Theorem: booleanp-of-augment-possiblep

(defthm booleanp-of-augment-possiblep
  (b* ((yes/no (augment-possiblep prop endor systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: augment-possiblep-of-proposal-fix-prop

(defthm augment-possiblep-of-proposal-fix-prop
  (equal (augment-possiblep (proposal-fix prop)
                            endor systate)
         (augment-possiblep prop endor systate)))

Theorem: augment-possiblep-proposal-equiv-congruence-on-prop

(defthm augment-possiblep-proposal-equiv-congruence-on-prop
  (implies (proposal-equiv prop prop-equiv)
           (equal (augment-possiblep prop endor systate)
                  (augment-possiblep prop-equiv endor systate)))
  :rule-classes :congruence)

Theorem: augment-possiblep-of-address-fix-endor

(defthm augment-possiblep-of-address-fix-endor
  (equal (augment-possiblep prop (address-fix endor)
                            systate)
         (augment-possiblep prop endor systate)))

Theorem: augment-possiblep-address-equiv-congruence-on-endor

(defthm augment-possiblep-address-equiv-congruence-on-endor
  (implies (address-equiv endor endor-equiv)
           (equal (augment-possiblep prop endor systate)
                  (augment-possiblep prop endor-equiv systate)))
  :rule-classes :congruence)

Theorem: augment-possiblep-of-system-state-fix-systate

(defthm augment-possiblep-of-system-state-fix-systate
  (equal (augment-possiblep prop endor (system-state-fix systate))
         (augment-possiblep prop endor systate)))

Theorem: augment-possiblep-system-state-equiv-congruence-on-systate

(defthm augment-possiblep-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (augment-possiblep prop endor systate)
                  (augment-possiblep prop endor systate-equiv)))
  :rule-classes :congruence)