		Search-engine friendly clone of the ACL2 documentation.

Transitions-commit

Commit-next

New state resulting from a commit event.

Signature
(commit-next val systate) → new-systate
Arguments: val — Guard (addressp val).; systate — Guard (system-statep systate).
Returns: new-systate — Type (system-statep new-systate).

The val input of this function is the address in the commit event; see event.

Because of commit-possiblep, the validator is in an odd round greater than one, and the even round immediately before it has an anchor for the leader at that round. We retrieve that anchor, and we use collect-anchors to collect that anchor and all the preceding anchors that must be committed and have not already been committed. Then we use extend-blockchain to extend the blockchain, and the set of all committed certificates. We also update the last committed round to the one for the latest anchor we committed.

Definitions and Theorems

Function: commit-next

(defun commit-next (val systate)
 (declare (xargs :guard (and (addressp val)
                             (system-statep systate))))
 (declare (xargs :guard (commit-possiblep val systate)))
 (let ((__function__ 'commit-next))
  (declare (ignorable __function__))
  (b*
   (((validator-state vstate)
     (get-validator-state val systate))
    (commit-round (1- vstate.round))
    (commtt
         (active-committee-at-round commit-round vstate.blockchain))
    (leader (leader-at-round commit-round commtt))
    (anchor (cert-with-author+round leader commit-round vstate.dag))
    (anchors (collect-anchors anchor (- commit-round 2)
                              vstate.last
                              vstate.dag vstate.blockchain))
    ((mv new-blockchain new-committed)
     (extend-blockchain anchors vstate.dag
                        vstate.blockchain vstate.committed))
    (new-vstate (change-validator-state vstate
                                        :last commit-round
                                        :blockchain new-blockchain
                                        :committed new-committed))
    (systate (update-validator-state val new-vstate systate)))
   systate)))

Theorem: system-statep-of-commit-next

(defthm system-statep-of-commit-next
  (b* ((new-systate (commit-next val systate)))
    (system-statep new-systate))
  :rule-classes :rewrite)

Theorem: correct-addresses-of-commit-next

(defthm correct-addresses-of-commit-next
  (implies (commit-possiblep val systate)
           (b* ((?new-systate (commit-next val systate)))
             (equal (correct-addresses new-systate)
                    (correct-addresses systate)))))

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

(defthm validator-state->round-of-commit-next
 (implies
  (commit-possiblep val systate)
  (b* ((?new-systate (commit-next val systate)))
   (equal
     (validator-state->round (get-validator-state val1 new-systate))
     (validator-state->round (get-validator-state val1 systate))))))

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

(defthm validator-state->dag-of-commit-next
 (implies
  (commit-possiblep val systate)
  (b* ((?new-systate (commit-next val systate)))
   (equal
       (validator-state->dag (get-validator-state val1 new-systate))
       (validator-state->dag (get-validator-state val1 systate))))))

Theorem: validator-state->buffer-of-commit-next

(defthm validator-state->buffer-of-commit-next
 (implies
  (commit-possiblep val systate)
  (b* ((?new-systate (commit-next val systate)))
   (equal
    (validator-state->buffer (get-validator-state val1 new-systate))
    (validator-state->buffer (get-validator-state val1 systate))))))

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

(defthm validator-state->endorsed-of-commit-next
  (implies (commit-possiblep val systate)
           (b* ((?new-systate (commit-next val systate)))
             (equal (validator-state->endorsed
                         (get-validator-state val1 new-systate))
                    (validator-state->endorsed
                         (get-validator-state val1 systate))))))

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

(defthm validator-state->last-of-commit-next
 (implies
  (commit-possiblep val systate)
  (b* ((?new-systate (commit-next val systate)))
   (equal
    (validator-state->last (get-validator-state val1 new-systate))
    (if
     (equal (address-fix val1)
            (address-fix val))
     (1- (validator-state->round (get-validator-state val systate)))
     (validator-state->last (get-validator-state val1 systate)))))))

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

(defthm validator-state->blockchain-of-commit-next
 (implies
  (and (in val1 (correct-addresses systate))
       (commit-possiblep val systate))
  (b* ((?new-systate (commit-next val systate)))
   (equal
    (validator-state->blockchain
         (get-validator-state val1 new-systate))
    (if
     (equal val1 (address-fix val))
     (b*
      (((validator-state vstate)
        (get-validator-state val1 systate))
       (commit-round (1- vstate.round))
       (commtt
         (active-committee-at-round commit-round vstate.blockchain))
       (leader (leader-at-round commit-round commtt))
       (anchor
            (cert-with-author+round leader commit-round vstate.dag))
       (anchors (collect-anchors anchor (- commit-round 2)
                                 vstate.last
                                 vstate.dag vstate.blockchain)))
      (mv-nth
           0
           (extend-blockchain anchors vstate.dag
                              vstate.blockchain vstate.committed)))
     (validator-state->blockchain
          (get-validator-state val1 systate)))))))

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

(defthm validator-state->committed-of-commit-next
 (implies
  (and (in val1 (correct-addresses systate))
       (commit-possiblep val systate))
  (b* ((?new-systate (commit-next val systate)))
   (equal
    (validator-state->committed
         (get-validator-state val1 new-systate))
    (if
     (equal val1 (address-fix val))
     (b*
      (((validator-state vstate)
        (get-validator-state val systate))
       (commit-round (1- vstate.round))
       (commtt
         (active-committee-at-round commit-round vstate.blockchain))
       (leader (leader-at-round commit-round commtt))
       (anchor
            (cert-with-author+round leader commit-round vstate.dag))
       (anchors (collect-anchors anchor (- commit-round 2)
                                 vstate.last
                                 vstate.dag vstate.blockchain)))
      (mv-nth
           1
           (extend-blockchain anchors vstate.dag
                              vstate.blockchain vstate.committed)))
     (validator-state->committed
          (get-validator-state val1 systate)))))))

Theorem: validator-state->timer-of-commit-next

(defthm validator-state->timer-of-commit-next
 (implies
  (commit-possiblep val systate)
  (b* ((?new-systate (commit-next val systate)))
   (equal
     (validator-state->timer (get-validator-state val1 new-systate))
     (validator-state->timer (get-validator-state val1 systate))))))

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

(defthm get-network-state-of-commit-next
  (b* ((?new-systate (commit-next val systate)))
    (equal (get-network-state new-systate)
           (get-network-state systate))))

Theorem: commit-next-of-address-fix-val

(defthm commit-next-of-address-fix-val
  (equal (commit-next (address-fix val) systate)
         (commit-next val systate)))

Theorem: commit-next-address-equiv-congruence-on-val

(defthm commit-next-address-equiv-congruence-on-val
  (implies (address-equiv val val-equiv)
           (equal (commit-next val systate)
                  (commit-next val-equiv systate)))
  :rule-classes :congruence)

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

(defthm commit-next-of-system-state-fix-systate
  (equal (commit-next val (system-state-fix systate))
         (commit-next val systate)))

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

(defthm commit-next-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (commit-next val systate)
                  (commit-next val systate-equiv)))
  :rule-classes :congruence)