		Search-engine friendly clone of the ACL2 documentation.

Transitions-augment

Augment-next

New system state resulting from an augment event.

Signature
(augment-next prop endor systate) → new-systate
Arguments: prop — Guard (proposalp prop).; endor — Guard (addressp endor).; systate — Guard (system-statep systate).
Returns: new-systate — Type (system-statep new-systate).

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

The message is removed from the network; it is consumed.

The address of the endorser is added to the set of endorser addresses associated to the proposal in the finite map in the validator state. Recall that, in our model, these addresses represent signatures.

Definitions and Theorems

Function: augment-next

(defun augment-next (prop endor systate)
 (declare (xargs :guard (and (proposalp prop)
                             (addressp endor)
                             (system-statep systate))))
 (declare (xargs :guard (augment-possiblep prop endor systate)))
 (let ((__function__ 'augment-next))
   (declare (ignorable __function__))
   (b*
     (((proposal prop) prop)
      ((validator-state vstate)
       (get-validator-state prop.author systate))
      (msg (make-message-endorsement :proposal prop
                                     :endorser endor))
      (network (get-network-state systate))
      (new-network (delete msg network))
      (systate (update-network-state new-network systate))
      (endors (omap::lookup (proposal-fix prop)
                            vstate.proposed))
      (new-endors (insert (address-fix endor) endors))
      (new-proposed (omap::update (proposal-fix prop)
                                  new-endors vstate.proposed))
      (new-vstate (change-validator-state vstate
                                          :proposed new-proposed))
      (systate
           (update-validator-state prop.author new-vstate systate)))
     systate)))

Theorem: system-statep-of-augment-next

(defthm system-statep-of-augment-next
  (b* ((new-systate (augment-next prop endor systate)))
    (system-statep new-systate))
  :rule-classes :rewrite)

Theorem: correct-addresses-of-augment-next

(defthm correct-addresses-of-augment-next
  (implies (augment-possiblep prop endor systate)
           (b* ((?new-systate (augment-next prop endor systate)))
             (equal (correct-addresses new-systate)
                    (correct-addresses systate)))))

Theorem: validator-state->round-of-augment-next

(defthm validator-state->round-of-augment-next
 (b* ((?new-systate (augment-next prop endor systate)))
  (equal
      (validator-state->round (get-validator-state val new-systate))
      (validator-state->round (get-validator-state val systate)))))

Theorem: validator-state->dag-of-augment-next

(defthm validator-state->dag-of-augment-next
 (b* ((?new-systate (augment-next prop endor systate)))
   (equal
        (validator-state->dag (get-validator-state val new-systate))
        (validator-state->dag (get-validator-state val systate)))))

Theorem: validator-state->proposed-of-augment-next

(defthm validator-state->proposed-of-augment-next
 (implies
  (augment-possiblep prop endor systate)
  (b* ((?new-systate (augment-next prop endor systate)))
   (equal
    (validator-state->proposed
         (get-validator-state val new-systate))
    (if
     (and (equal (address-fix val)
                 (proposal->author prop))
          (in (address-fix val)
              (correct-addresses systate)))
     (omap::update
      (proposal-fix prop)
      (insert
           (address-fix endor)
           (omap::lookup (proposal-fix prop)
                         (validator-state->proposed
                              (get-validator-state val systate))))
      (validator-state->proposed (get-validator-state val systate)))
     (validator-state->proposed
          (get-validator-state val systate)))))))

Theorem: validator-state->endorsed-of-augment-next

(defthm validator-state->endorsed-of-augment-next
 (b* ((?new-systate (augment-next prop endor systate)))
  (equal
   (validator-state->endorsed (get-validator-state val new-systate))
   (validator-state->endorsed (get-validator-state val systate)))))

Theorem: validator-state->last-of-augment-next

(defthm validator-state->last-of-augment-next
 (b* ((?new-systate (augment-next prop endor systate)))
  (equal
       (validator-state->last (get-validator-state val new-systate))
       (validator-state->last (get-validator-state val systate)))))

Theorem: validator-state->blockchain-of-augment-next

(defthm validator-state->blockchain-of-augment-next
  (b* ((?new-systate (augment-next prop endor systate)))
    (equal (validator-state->blockchain
                (get-validator-state val new-systate))
           (validator-state->blockchain
                (get-validator-state val systate)))))

Theorem: validator-state->committed-of-augment-next

(defthm validator-state->committed-of-augment-next
 (b* ((?new-systate (augment-next prop endor systate)))
  (equal
   (validator-state->committed
        (get-validator-state val new-systate))
   (validator-state->committed (get-validator-state val systate)))))

Theorem: get-network-state-of-augment-next

(defthm get-network-state-of-augment-next
  (b* ((?new-systate (augment-next prop endor systate)))
    (equal (get-network-state new-systate)
           (delete (message-endorsement prop endor)
                   (get-network-state systate)))))

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

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

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

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

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

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

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

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

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

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

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

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