		Search-engine friendly clone of the ACL2 documentation.

Transitions-commit

Commit-next

New system 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 parameter of this function is the corresponding component of the commit 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: 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)