		Search-engine friendly clone of the ACL2 documentation.

Transitions-propose

Propose-next

New system state resulting from a propose event.

Signature
(propose-next prop dests systate) → new-systate
Arguments: prop — Guard (proposalp prop).; dests — Guard (address-setp dests).; systate — Guard (system-statep systate).
Returns: new-systate — Type (system-statep new-systate).

The props and dests parameters of this function are the corresponding components of the propose event.

If the author of the proposal is faulty, the only change is to the network: a message with the proposal is added for each destination. If the author of the proposal is correct, the same happens to the network, and in addition the validator adds the proposal to the map of pending proposals, with associated the empty set, because the proposal has no endorsements yet.

Definitions and Theorems

Function: propose-next

(defun propose-next (prop dests systate)
 (declare (xargs :guard (and (proposalp prop)
                             (address-setp dests)
                             (system-statep systate))))
 (declare (xargs :guard (propose-possiblep prop dests systate)))
 (let ((__function__ 'propose-next))
   (declare (ignorable __function__))
   (b*
     (((proposal prop) prop)
      (network (get-network-state systate))
      (msgs (make-proposal-messages prop dests))
      (new-network (union network msgs))
      (systate (update-network-state new-network systate))
      ((unless (in prop.author
                   (correct-addresses systate)))
       systate)
      ((validator-state vstate)
       (get-validator-state prop.author systate))
      (new-proposed (omap::update (proposal-fix prop)
                                  nil 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-propose-next

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

Theorem: correct-addresses-of-propose-next

(defthm correct-addresses-of-propose-next
  (b* ((?new-systate (propose-next prop dests systate)))
    (equal (correct-addresses new-systate)
           (correct-addresses systate))))

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

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

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

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

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

(defthm validator-state->proposed-of-propose-next
 (b* ((?new-systate (propose-next prop dests 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)
      nil
      (validator-state->proposed (get-validator-state val systate)))
    (validator-state->proposed
         (get-validator-state val systate))))))

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

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

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

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

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

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

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

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

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

(defthm get-network-state-of-propose-next
  (b* ((?new-systate (propose-next prop dests systate)))
    (equal (get-network-state new-systate)
           (union (get-network-state systate)
                  (make-proposal-messages prop dests)))))

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

(defthm propose-next-of-proposal-fix-prop
  (equal (propose-next (proposal-fix prop)
                       dests systate)
         (propose-next prop dests systate)))

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

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

Theorem: propose-next-of-address-set-fix-dests

(defthm propose-next-of-address-set-fix-dests
  (equal (propose-next prop (address-set-fix dests)
                       systate)
         (propose-next prop dests systate)))

Theorem: propose-next-address-set-equiv-congruence-on-dests

(defthm propose-next-address-set-equiv-congruence-on-dests
  (implies (address-set-equiv dests dests-equiv)
           (equal (propose-next prop dests systate)
                  (propose-next prop dests-equiv systate)))
  :rule-classes :congruence)

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

(defthm propose-next-of-system-state-fix-systate
  (equal (propose-next prop dests (system-state-fix systate))
         (propose-next prop dests systate)))

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

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